c launch: /data/cnf/sc2014/app/hwmcc10-timeframe-expansion-k50-pdtvisns3p00-tseitin.cnf.bz2
c host: atom14
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/hwmcc10-timeframe-expansion-k50-pdtvisns3p00-tseitin.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/hwmcc10-timeframe-expansion-k50-pdtvisns3p00-tseitin.cnf.bz2
c no embedded options
c found 'p cnf 183325 546914' header
c read 183325 variables, 546914 clauses, 1276130 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=5
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 183323 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] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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  183323   546912         0       0      0     0    0     0   34   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 992 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 992 out of 992 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 2 at-most-one constraints, 2 used 100%
c [card-1] exported 2 binary clauses, 1.0 per/constraint
c [decomp-1] removed 2 variables
c [simpleprobe-1] all 183323 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 12265 variables
c [simpleprobe-1] 5431 variables remain 3% (165627 retained 97%)
c [simpleprobe-1] removed 12265 variables, found 15391 hbrs, 1 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 12 units, 181 failed, 754 tauts, 0 hbrs, 326 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 170970 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 19557 not tried 11% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 148238 = 87% variables out of 170970 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 162732 negative 92.9% of 175240 except 12508 7.1%
c [phase-count-1] 153535 positive 87.6% of 175240 except 21705 12.4%
c [phase-1] phase bias: 5935 positive 26%, 16797 negative 74%
c [sort-queue-1] sorted 22732 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 22732 (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 160591 variables 87.6% (22732 remain 12%)
c [simplification-1] removed 371672 irredundant clauses 68.0% (175240 remain 32%)
c [simplification-1] maximum reduction of 88% = max (88%, 68%)
c [simplification-1] large reduction 88% >= 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    4.5   22731   175239       142      89     33   652    0     4   25   3%      0    4    1    0 19817%
c i    4.6   22722   175234       883     583    162   694    1    11   25   6%      3   11    3    0 8005%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 18 variables
c [simpleprobe-2] 467 schedulable variables 2%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 9 variables
c [simpleprobe-2] 599 variables remain 3% (22106 retained 97%)
c [simpleprobe-2] removed 9 variables, found 70 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 23292 literals 51%
c [treelook-1] scheduling used 300040 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 307438 steps
c [treelook-1] 23132 literals remain 51%
c [treelook-1] 18283 variables remain to probed next time 81%
c [decomp-5] removed 1 variables
c [treelook-1] removed 2 variables, found 529 hbrs
c [basicprobe-1] limit 1399856 based on 174982 irredundant clauses
c [basicprobe-1-0] 9925 probes remain 44% after last round
c [basicprobe-1-0] 23 units = 23 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 96 variables, found 3579 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 2 units, 16 failed, 165 tauts, 0 hbrs, 29862 literals
c [elim-2] 19432 variables 86% will be scheduled this time
c [elim-2] scheduled 19432 variables 86%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 954 not tried 4% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 4260 = 22% variables out of 19432 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 143068 negative 92.8% of 154087 except 11019 7.2%
c [phase-count-2] 139974 positive 90.8% of 154087 except 14113 9.2%
c [phase-2] phase bias: 291 positive 88%, 38 negative 12%
c [sort-queue-2] sorted 15231 enqueued variables after 1000 conflicts
c [score-dist-2] active 3087 (17%), one 0 (0%), zero 15231 (83%)
c [score-dist-2] max exp 749, different 238 (32%)
c [score-dist-2] median active exp 661, avg 646.3
c [simplification-2] removed 4404 variables 19.4% (18318 remain 10%)
c [simplification-2] removed 21146 irredundant clauses 12.1% (154087 remain 28%)
c [simplification-2] maximum reduction of 19% = max (19%, 12%)
c [simplification-2] large reduction 19% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
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   18317   154084      1398     829    245  3019    1    14   24   7%      4   13    3    0 5188%
c i    6.1   18316   154084      1413     837    249  3021    1    14   24   7%      4   13    3    0 5053%
c i    6.2   18315   154083      1802    1122    308  3039    1    16   24   7%      4   16    3    0 3830%
c i    6.2   18314   154083      1913    1206    324  3043    1    17   24   7%      3   16    4    0 3858%
c i    6.3   18313   154082      2660    1725    462  3084    1    21   24   7%      5   21    3    0 2435%
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 342 at-most-one constraints of average size 3.0
c [card-2] found 12 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 354 out of 354 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 88 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 19404 literals 53%
c [treelook-2] scheduling used 300006 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 301858 steps
c [treelook-2] 19247 literals remain 53%
c [treelook-2] 12159 variables remain to probed next time 67%
c [decomp-7] removed 2 variables
c [treelook-2] removed 2 variables, found 191 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 11 failed, 7703 tauts, 0 hbrs, 16464 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 18222 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 590 not tried 3% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1258 = 7% variables out of 18222 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 131880 negative 92.9% of 141940 except 10060 7.1%
c [phase-count-3] 128619 positive 90.6% of 141940 except 13321 9.4%
c [phase-3] phase bias: 36 positive 37%, 61 negative 63%
c [sort-queue-3] sorted 11872 enqueued variables after 3000 conflicts
c [score-dist-3] active 5092 (30%), one 4 (0%), zero 11868 (70%)
c [score-dist-3] max exp 754, different 611 (81%)
c [score-dist-3] median active exp 595, avg 511.0
c [simplification-3] removed 1349 variables 7.4% (16964 remain 9%)
c [simplification-3] removed 12142 irredundant clauses 7.9% (141940 remain 26%)
c [simplification-3] maximum reduction of 8% = max (7%, 8%)
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 15000 (soft 5000 + delta 10000)
c [simplification-3] new conflict limit 5000 (hard 15000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    7.5   16963   141938      3791    2425    643  2819    2    27   23   7%      8   26    3    0 1853%
c i    7.5   16962   141938      3917    2532    653  2823    2    27   23   7%      8   27    3    0 1905%
c i    7.5   16961   141938      4120    2680    679  2827    2    28   23   7%      6   27    3    0 1744%
c i    7.6   16960   141936      4548    3009    727  2854    2    29   23   8%      5   28    3    0 1584%
c i    7.6   16959   141936      4824    3220    759  2862    2    30   23   8%      5   29    4    0 1574%
c 
c [simplification-4] limit 5000 conflicts (hard 15000) hit after 5001 conflicts
c [decomp-8] removed 24 variables
c [basicprobe-2] limit 1136806 penalty 0 = 0 + 0
c [basicprobe-2-0] 3505 probes remain 21% after last round
c [basicprobe-2-0] 23 units = 21 failed (91%) + 2 lifted (9%)
c [basicprobe-2-0] removed 22 variables, found 2857 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 3 units, 45 failed, 216 tauts, 0 hbrs, 13620 literals
c [elim-4] 577 variables 3% will be scheduled this time
c [elim-4] scheduled 577 variables 3%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 45135924 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 577 scheduled
c [phase-count-4] 120536 negative 92.1% of 130810 except 10274 7.9%
c [phase-count-4] 117097 positive 89.5% of 130810 except 13713 10.5%
c [phase-4] phase bias: 21 positive 46%, 25 negative 54%
c [sort-queue-4] sorted 11726 enqueued variables after 5001 conflicts
c [score-dist-4] active 5180 (31%), one 963 (6%), zero 10763 (64%)
c [score-dist-4] max exp 757, different 591 (78%)
c [score-dist-4] median active exp 610, avg 526.8
c [simplification-4] removed 53 variables 0.3% (16906 remain 9%)
c [simplification-4] removed 11123 irredundant clauses 7.8% (130810 remain 24%)
c [simplification-4] maximum reduction of 8% = max (0%, 8%)
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 17001 (soft 7001 + delta 10000)
c [simplification-4] new conflict limit 7001 (hard 17001)
c 
c [simplification-5] limit 7001 conflicts (hard 17001) hit after 7001 conflicts
c [quatres-1] found 30363 quaternary clauses 47% in total
c [quatres-1-1] removed 8 duplicate quaternary clauses
c [quatres-1-1] added 2 double-self-subsuming ternary resolvents
c [quatres-1-2] added 571 single-self-subsuming ternary resolvents
c [quatres-1-2] added 2529 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 16906 free variables schedulable
c [ternres-1] 52597 ternary resolvents (1227 bin, 51370 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 634 xors of average arity 2.9
c [gauss-1] connected 1840 occurrences of 408 variables (average 4.5)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 46 variables
c [simpleprobe-3] 254 schedulable variables 2%
c [simpleprobe-3] limit 2000000 penalty 0 = 0 + 0
c [decomp-10] removed 9 variables
c [simpleprobe-3] 431 variables remain 3% (16420 retained 97%)
c [simpleprobe-3] removed 9 variables, found 182 hbrs, 0 units
c [unhide-5] limit 100000 with penalty 0 = 0 + 0
c [unhide-5-5] 14 units, 27 failed, 1895 tauts, 0 hbrs, 5670 literals
c [transred-1] limit 325438 with penalty 0 = 0 + 0
c [transred-1] removed 1023 transitive binary clauses
c [transred-1] found 6 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 16814 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 529 blocked clauses
c [block-1] 529 < 1/100 * 129137 = 1291 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 22 (5%) of length 11
c [cce-1-1] eliminated 3 clauses out of 34 (9%) of length 10
c [cce-1-1] eliminated 17 clauses out of 334 (5%) of length 9
c [cce-1-1] eliminated 64 clauses out of 1058 (6%) of length 8
c [cce-1-1] eliminated 469 clauses out of 3008 (16%) of length 7
c [cce-1-1] eliminated 1523 clauses out of 7255 (21%) of length 6
c [cce-1-1] eliminated 371 clauses out of 18764 (2%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 2448 large clauses in 30000044 steps
c [cce-1-1] allowing another 15000022 steps for small clauses
c [cce-1-1] scheduling 49524 clauses = 15869 binary + 33655 ternary
c [cce-1-1] tried to eliminate 19773 small clauses 40%
c [cce-1-1] eliminated 397 binary clauses 3%
c [cce-1-1] eliminated 4350 ternary clauses 13%
c [cce-1-1] eliminated 4747 small clauses 10%
c [cce-1-1] eliminated 4747 small clauses in 30000003 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 7195 covered clauses in round 1
c [cce-1] eliminated 7195 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 242668 added (scaled 2)
c [bca-1] 23885 out of 33630 literals actually usable 71%
c [bca-1] added 170 blocked clauses in 83416 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 7334 pos 43.6% + 9480 neg 56.4% = 16814 sched 100.0% ret 0
c [sweep-1-1] 1003647 steps 135 queries 2382.96 avg class size
c [sweep-1-1] 2453 decisions 133 SAT calls 38.51 avg env size
c [sweep-1-1] 14903 variables remain 89% (1911 retained 11%)
c [decomp-11] removed 53 variables
c [sweep-1-1] removed 53 vars (0 failed, 4 eqs, 14 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 53 vars in TOTAL (1 rounds, 134 queries)
c [phase-count-5] 111712 negative 92.4% of 120929 except 9217 7.6%
c [phase-count-5] 107920 positive 89.2% of 120929 except 13009 10.8%
c [phase-5] phase bias: 23 positive 35%, 42 negative 65%
c [sort-queue-5] sorted 11180 enqueued variables after 7001 conflicts
c [score-dist-5] active 5581 (33%), one 1475 (9%), zero 9705 (58%)
c [score-dist-5] max exp 794, different 595 (75%)
c [score-dist-5] median active exp 675, avg 583.3
c [simplification-5] removed 145 variables 0.9% (16761 remain 9%)
c [simplification-5] removed 9879 irredundant clauses 7.6% (120929 remain 22%)
c [simplification-5] maximum reduction of 8% = max (1%, 8%)
c [simplification-5] large reduction 8% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 19001 (soft 9001 + delta 10000)
c [simplification-5] new conflict limit 9001 (hard 19001)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   10.8   16760   120929      7271    7343  53255  8802    3    38   26   8%     23   36    4    0 1133%
c i   11.1   16759   120928      8826    8649  53400  8842    3    42   26   7%     16   39    4    0  887%
c 
c [simplification-6] limit 9001 conflicts (hard 19001) hit after 9002 conflicts
c [quatres-2] found 32764 quaternary clauses 51% in total
c [quatres-2-1] removed 5 duplicate quaternary clauses
c [quatres-2-1] added 11 double-self-subsuming ternary resolvents
c [quatres-2-2] added 503 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1274 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 16759 free variables schedulable
c [ternres-2] 1317 ternary resolvents (40 bin, 1277 trn)
c [ternres-2] 6490 variables remain 39% (10269 retained 61%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 259 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 259 out of 259 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 8 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 15487 literals 46%
c [treelook-3] scheduling used 300002 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 305587 steps
c [treelook-3] 15317 literals remain 46%
c [treelook-3] 9526 variables remain to probed next time 57%
c [decomp-13] removed 5 variables
c [treelook-3] removed 5 variables, found 608 hbrs
c [unhide-6] limit 100000 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 28 failed, 11673 tauts, 0 hbrs, 8819 literals
c [transred-2] limit 483685 with penalty 0 = 0 + 0
c [transred-2] removed 1026 transitive binary clauses
c [transred-2] found 2 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 2214 (0%) of length 7
c [cce-2-1] eliminated 2 clauses out of 5593 (0%) of length 6
c [cce-2-1] eliminated 458 clauses out of 16616 (3%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 461 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2-1] scheduling 35349 clauses = 15563 binary + 19786 ternary
c [cce-2-1] tried to eliminate 18441 small clauses 52%
c [cce-2-1] eliminated 349 binary clauses 2%
c [cce-2-1] eliminated 2469 ternary clauses 12%
c [cce-2-1] eliminated 2818 small clauses 8%
c [cce-2-1] eliminated 2960 small clauses in 30000004 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 3421 covered clauses in round 1
c [cce-2] eliminated 3421 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 16730 variables 100%
c [elim-5] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 1018 not tried 6% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1400 = 8% variables out of 16730 scheduled
c [bca-2] limit of 10000000 steps and 227313 added (scaled 2)
c [bca-2] 20726 out of 30662 literals actually usable 68%
c [bca-2] added 32 blocked clauses in 73284 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 5818 pos 42.8% + 7760 neg 57.2% = 13578 sched 88.6% ret 1752
c [sweep-2-1] 1005255 steps 144 queries 1794.64 avg class size
c [sweep-2-1] 2702 decisions 143 SAT calls 35.88 avg env size
c [sweep-2-1] 11764 variables remain 77% (3566 retained 23%)
c [decomp-14] removed 14 variables
c [sweep-2-1] removed 14 vars (0 failed, 4 eqs, 10 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 14 vars in TOTAL (1 rounds, 143 queries)
c [phase-count-6] 105476 negative 93.1% of 113330 except 7854 6.9%
c [phase-count-6] 101499 positive 89.6% of 113330 except 11831 10.4%
c [phase-6] phase bias: 9 positive 53%, 8 negative 47%
c [sort-queue-6] sorted 9425 enqueued variables after 9002 conflicts
c [score-dist-6] active 5891 (38%), one 1438 (9%), zero 7987 (52%)
c [score-dist-6] max exp 843, different 665 (79%)
c [score-dist-6] median active exp 636, avg 563.7
c [simplification-6] removed 1443 variables 8.6% (15316 remain 8%)
c [simplification-6] removed 7598 irredundant clauses 6.3% (113330 remain 21%)
c [simplification-6] maximum reduction of 9% = max (9%, 6%)
c [simplification-6] large reduction 9% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 21002 (soft 11002 + delta 10000)
c [simplification-6] new conflict limit 11002 (hard 21002)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   13.2   15315   113330      9815    9121  37294  7503    3    42   24   8%     11   39    4    0  916%
c 
c [simplification-7] limit 11002 conflicts (hard 21002) hit after 11002 conflicts
c [quatres-3] found 33349 quaternary clauses 52% in total
c [quatres-3-1] removed 8 duplicate quaternary clauses
c [quatres-3-1] added 32 double-self-subsuming ternary resolvents
c [quatres-3-2] added 703 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1161 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 5878 schedulable variables 38%
c [ternres-3] 3834 ternary resolvents (113 bin, 3721 trn)
c [ternres-3] 161 variables remain 1% (15154 retained 99%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 374 xors of average arity 2.9
c [gauss-2] connected 1102 occurrences of 321 variables (average 3.4)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 23 variables
c [basicprobe-3] limit 3128862 penalty 0 = 0 + 0
c [basicprobe-3-0] 4142 sched 27%, 43 failed, 0 lifted, 4043 hbrs
c [decomp-16] removed 70 variables
c [basicprobe-3-1] 4853 probes remain 32% after last round
c [basicprobe-3-1] 76 units = 76 failed (100%) + 0 lifted (0%)
c [basicprobe-3-1] removed 103 variables, found 5289 hbrs
c [bate-1] eliminated 352 asymmetric tautologies during probing
c [unhide-7] limit 125154 with penalty 0 = 0 + 0
c [unhide-7-7] 3 units, 11 failed, 2298 tauts, 0 hbrs, 3620 literals
c [transred-3] limit 625772 with penalty 0 = 0 + 0
c [transred-3] removed 1182 transitive binary clauses
c [transred-3] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 15180 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 68 blocked clauses
c [block-2] 68 < 1/100 * 111383 = 1113 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 6 clauses out of 8 (75%) of length 13
c [cce-3-1] eliminated 2 clauses out of 14 (14%) of length 12
c [cce-3-1] eliminated 5 clauses out of 41 (12%) of length 10
c [cce-3-1] eliminated 13 clauses out of 313 (4%) of length 9
c [cce-3-1] eliminated 39 clauses out of 855 (5%) of length 8
c [cce-3-1] eliminated 213 clauses out of 2392 (9%) of length 7
c [cce-3-1] eliminated 1012 clauses out of 6247 (16%) of length 6
c [cce-3-1] eliminated 892 clauses out of 15639 (6%) of length 5
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2182 large clauses in 30000035 steps
c [cce-3-1] allowing another 15000017 steps for small clauses
c [cce-3-1] scheduling 41720 clauses = 13388 binary + 28332 ternary
c [cce-3-1] tried to eliminate 15276 small clauses 37%
c [cce-3-1] eliminated 512 binary clauses 4%
c [cce-3-1] eliminated 3207 ternary clauses 11%
c [cce-3-1] eliminated 3719 small clauses 9%
c [cce-3-1] eliminated 3719 small clauses in 30000131 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 5901 covered clauses in round 1
c [cce-3] eliminated 5901 covered clauses in TOTAL during 1 rounds
c [elim-6] 1013 variables 7% will be scheduled this time
c [elim-6] scheduled 1013 variables 7%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 28 not tried 0% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 1013 scheduled
c [bca-3] limit of 10000000 steps and 210391 added (scaled 2)
c [bca-3] 18820 out of 30360 literals actually usable 62%
c [bca-3] added 30 blocked clauses in 67691 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 5159 pos 44.3% + 6483 neg 55.7% = 11642 sched 76.7% ret 3537
c [sweep-3-1] 1003456 steps 134 queries 1976.53 avg class size
c [sweep-3-1] 2355 decisions 132 SAT calls 34.02 avg env size
c [sweep-3-1] 10380 variables remain 68% (4798 retained 32%)
c [decomp-17] removed 34 variables
c [sweep-3-1] removed 34 vars (0 failed, 3 eqs, 6 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 34 vars in TOTAL (1 rounds, 133 queries)
c [phase-count-7] 97954 negative 93.5% of 104798 except 6844 6.5%
c [phase-count-7] 93727 positive 89.4% of 104798 except 11071 10.6%
c [phase-7] phase bias: 2 positive 40%, 3 negative 60%
c [sort-queue-7] sorted 8771 enqueued variables after 11002 conflicts
c [score-dist-7] active 6374 (42%), one 1861 (12%), zero 6910 (46%)
c [score-dist-7] max exp 873, different 687 (79%)
c [score-dist-7] median active exp 705, avg 636.7
c [simplification-7] removed 170 variables 1.1% (15145 remain 8%)
c [simplification-7] removed 8531 irredundant clauses 7.5% (104798 remain 19%)
c [simplification-7] maximum reduction of 8% = max (1%, 8%)
c [simplification-7] large reduction 8% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 23002 (soft 13002 + delta 10000)
c [simplification-7] new conflict limit 13002 (hard 23002)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   15.8   15144   104798     12141   11945  41295 11243    4    49   25   7%     22   44    4    1  621%
c 
c [simplification-8] limit 13002 conflicts (hard 23002) hit after 13002 conflicts
c [quatres-4] found 33970 quaternary clauses 56% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 5 double-self-subsuming ternary resolvents
c [quatres-4-2] added 363 single-self-subsuming ternary resolvents
c [quatres-4-2] added 623 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 157 schedulable variables 1%
c [ternres-4] 4587 ternary resolvents (127 bin, 4460 trn)
c [ternres-4] 3 variables remain 0% (15141 retained 100%)
c [decomp-18] removed 25 variables
c [simpleprobe-4] 399 schedulable variables 3%
c [simpleprobe-4] limit 3188974 penalty 0 = 0 + 0
c [decomp-19] removed 9 variables
c [simpleprobe-4] 594 variables remain 4% (14517 retained 96%)
c [simpleprobe-4] removed 9 variables, found 419 hbrs, 0 units
c [unhide-8] limit 159448 with penalty 0 = 0 + 0
c [unhide-8-8] 0 units, 58 failed, 4795 tauts, 0 hbrs, 6269 literals
c [transred-4] limit 797243 with penalty 0 = 0 + 0
c [transred-4] removed 806 transitive binary clauses
c [transred-4] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 286 (0%) of length 9
c [cce-4-1] eliminated 4 clauses out of 4958 (0%) of length 6
c [cce-4-1] eliminated 2759 clauses out of 13011 (21%) of length 5
c [cce-4-1] eliminated 4079 clauses out of 28036 (15%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 6843 large clauses in 74731759 steps
c [cce-4-1] allowing another 37365879 steps for small clauses
c [cce-4-1] scheduling 29604 clauses = 13041 binary + 16563 ternary
c [cce-4-1] tried to eliminate 29604 small clauses 100%
c [cce-4-1] eliminated 280 binary clauses 2%
c [cce-4-1] eliminated 2756 ternary clauses 17%
c [cce-4-1] eliminated 3036 small clauses 10%
c [cce-4-1] eliminated 3110 small clauses in 58688292 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 9953 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 32152203 steps for small clauses
c [cce-4-2] scheduling 26570 clauses = 12761 binary + 13809 ternary
c [cce-4-2] tried to eliminate 26570 small clauses 100%
c [cce-4-2] eliminated 2 ternary clauses 0%
c [cce-4-2] eliminated 2 small clauses 0%
c [cce-4-2] eliminated 2 small clauses in 52057877 steps
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 2 covered clauses in round 2
c [cce-4-3] completed large round (ATE)
c [cce-4-3] allowing another 32160591 steps for small clauses
c [cce-4-3] scheduling 26568 clauses = 12761 binary + 13807 ternary
c [cce-4-3] tried to eliminate 26568 small clauses 100%
c [cce-4-3] completed small round (ATE)
c [cce-4-3] eliminated 0 covered clauses in round 3
c [cce-4] eliminated 9955 covered clauses in TOTAL during 3 rounds
c [bca-4] limit of 10000000 steps and 189804 added (scaled 2)
c [bca-4] 17709 out of 30198 literals actually usable 59%
c [bca-4] added 8 blocked clauses in 65003 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 4958 pos 48.1% + 5351 neg 51.9% = 10309 sched 68.3% ret 4789
c [sweep-4-1] 1003996 steps 166 queries 1246.70 avg class size
c [sweep-4-1] 2583 decisions 162 SAT calls 35.23 avg env size
c [sweep-4-1] 8718 variables remain 58% (6380 retained 42%)
c [decomp-20] removed 7 variables
c [sweep-4-1] removed 7 vars (0 failed, 4 eqs, 8 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 7 vars in TOTAL (1 rounds, 165 queries)
c [phase-count-8] 88823 negative 93.9% of 94578 except 5755 6.1%
c [phase-count-8] 83981 positive 88.8% of 94578 except 10597 11.2%
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-8] sorted 7353 enqueued variables after 13002 conflicts
c [score-dist-8] active 7738 (51%), one 1799 (12%), zero 5554 (37%)
c [score-dist-8] max exp 910, different 777 (85%)
c [score-dist-8] median active exp 733, avg 653.0
c [simplification-8] removed 53 variables 0.3% (15091 remain 8%)
c [simplification-8] removed 10220 irredundant clauses 9.8% (94578 remain 17%)
c [simplification-8] maximum reduction of 10% = max (0%, 10%)
c [simplification-8] large reduction 10% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 25002 (soft 15002 + delta 10000)
c [simplification-8] new conflict limit 15002 (hard 25002)
c 
c [simplification-9] limit 15002 conflicts (hard 25002) hit after 15002 conflicts
c [quatres-5] found 30633 quaternary clauses 57% in total
c [quatres-5-1] removed 13 duplicate quaternary clauses
c [quatres-5-1] added 5 double-self-subsuming ternary resolvents
c [quatres-5-2] added 241 single-self-subsuming ternary resolvents
c [quatres-5-2] added 545 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] 3 schedulable variables 0%
c [ternres-5] 1990 ternary resolvents (47 bin, 1943 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-21] removed 4 variables
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 14874 literals 49%
c [treelook-4] scheduling used 300014 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 301350 steps
c [treelook-4] 14685 literals remain 49%
c [treelook-4] 7972 variables remain to probed next time 53%
c [treelook-4] removed 0 variables, found 264 hbrs
c [unhide-9] limit 192015 with penalty 0 = 0 + 0
c [unhide-9-9] 3 units, 2 failed, 965 tauts, 0 hbrs, 1624 literals
c [transred-5] limit 960078 with penalty 0 = 0 + 0
c [transred-5] removed 558 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 23 (4%) of length 11
c [cce-5-1] eliminated 3 clauses out of 32 (9%) of length 10
c [cce-5-1] eliminated 2 clauses out of 614 (0%) of length 8
c [cce-5-1] eliminated 5 clauses out of 2022 (0%) of length 7
c [cce-5-1] eliminated 4 clauses out of 4919 (0%) of length 6
c [cce-5-1] eliminated 1145 clauses out of 10098 (11%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1160 large clauses in 30000005 steps
c [cce-5-1] allowing another 15000002 steps for small clauses
c [cce-5-1] scheduling 38614 clauses = 12778 binary + 25836 ternary
c [cce-5-1] tried to eliminate 17400 small clauses 45%
c [cce-5-1] eliminated 410 binary clauses 3%
c [cce-5-1] eliminated 2412 ternary clauses 9%
c [cce-5-1] eliminated 2822 small clauses 7%
c [cce-5-1] eliminated 2838 small clauses in 30000003 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 3998 covered clauses in round 1
c [cce-5] eliminated 3998 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 15083 variables 100%
c [elim-7] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 609 not tried 4% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 2180 = 14% variables out of 15083 scheduled
c [bca-5] limit of 10000000 steps and 172486 added (scaled 2)
c [bca-5] 14962 out of 25808 literals actually usable 58%
c [bca-5] added 79 blocked clauses in 58163 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 4016 pos 54.8% + 3309 neg 45.2% = 7325 sched 56.8% ret 5578
c [sweep-5-1] 5585151 steps 1441 queries 144.46 avg class size
c [sweep-5-1] 21669 decisions 1407 SAT calls 28.62 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-23] removed 65 variables
c [sweep-5-1] removed 65 vars (0 failed, 66 eqs, 138 impls)
c [sweep-5-2] 6328 pos 49.3% + 6510 neg 50.7% = 12838 sched 100.0% ret 0
c [sweep-5-2] 4416242 steps 766 queries 370.24 avg class size
c [sweep-5-2] 13706 decisions 764 SAT calls 34.88 avg env size
c [sweep-5-2] 2286 variables remain 18% (10552 retained 82%)
c [decomp-24] removed 2 variables
c [sweep-5-2] removed 2 vars (0 failed, 4 eqs, 20 impls)
c [sweep-5] removed 67 vars in TOTAL (2 rounds, 2205 queries)
c [sort-queue-9] sorted 6781 enqueued variables after 15002 conflicts
c [score-dist-9] active 6055 (47%), one 2889 (23%), zero 3892 (30%)
c [score-dist-9] max exp 691, different 611 (88%)
c [score-dist-9] median active exp 528, avg 474.6
c [simplification-9] removed 2255 variables 14.9% (12836 remain 7%)
c [simplification-9] removed 8782 irredundant clauses 9.3% (85796 remain 16%)
c [simplification-9] maximum reduction of 15% = max (15%, 9%)
c [simplification-9] large reduction 15% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 27002 (soft 17002 + delta 10000)
c [simplification-9] new conflict limit 17002 (hard 27002)
c 
c [simplification-10] limit 17002 conflicts (hard 27002) hit after 17003 conflicts
c [quatres-6] found 28839 quaternary clauses 53% in total
c [quatres-6-1] removed 10 duplicate quaternary clauses
c [quatres-6-1] added 24 double-self-subsuming ternary resolvents
c [quatres-6-2] added 869 single-self-subsuming ternary resolvents
c [quatres-6-2] added 909 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 12836 free variables schedulable
c [ternres-6] 4256 ternary resolvents (63 bin, 4193 trn)
c [ternres-6] 580 variables remain 5% (12256 retained 95%)
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 74 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 250000 for elimination
c [card-4] 74 out of 74 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 260 xors of average arity 3.0
c [gauss-3] connected 780 occurrences of 241 variables (average 3.2)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 4 variables
c [basicprobe-4] limit 5407169 penalty 0 = 0 + 0
c [basicprobe-4-0] 3966 sched 31%, 12 failed, 0 lifted, 1106 hbrs
c [decomp-26] removed 14 variables
c [basicprobe-4-1] 6531 sched 51%, 4 failed, 0 lifted, 549 hbrs
c [decomp-27] removed 4 variables
c [basicprobe-4-2] 3805 probes remain 30% after last round
c [basicprobe-4-2] 16 units = 16 failed (100%) + 0 lifted (0%)
c [basicprobe-4-2] removed 18 variables, found 1740 hbrs
c [bate-2] eliminated 290 asymmetric tautologies during probing
c [unhide-10] limit 216286 with penalty 0 = 0 + 0
c [unhide-10-10] 0 units, 0 failed, 3372 tauts, 0 hbrs, 5833 literals
c [transred-6] limit 1081433 with penalty 0 = 0 + 0
c [transred-6] removed 539 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 12814 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 21 blocked clauses
c [block-3] 21 < 1/100 * 85333 = 853 considered unsuccessful
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 13
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 12
c [cce-6-1] eliminated 1 clauses out of 59 (2%) of length 10
c [cce-6-1] eliminated 11 clauses out of 357 (3%) of length 9
c [cce-6-1] eliminated 62 clauses out of 698 (9%) of length 8
c [cce-6-1] eliminated 206 clauses out of 2377 (9%) of length 7
c [cce-6-1] eliminated 391 clauses out of 5366 (7%) of length 6
c [cce-6-1] eliminated 834 clauses out of 9897 (8%) of length 5
c [cce-6-1] eliminated 5 clauses out of 22204 (0%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 1514 large clauses in 30000059 steps
c [cce-6-1] allowing another 15000029 steps for small clauses
c [cce-6-1] scheduling 23110 clauses = 10754 binary + 12356 ternary
c [cce-6-1] tried to eliminate 21020 small clauses 91%
c [cce-6-1] eliminated 71 binary clauses 1%
c [cce-6-1] eliminated 727 ternary clauses 6%
c [cce-6-1] eliminated 798 small clauses 3%
c [cce-6-1] eliminated 798 small clauses in 30000002 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 2312 covered clauses in round 1
c [cce-6] eliminated 2312 covered clauses in TOTAL during 1 rounds
c [elim-8] 28 variables 0% will be scheduled this time
c [elim-8] scheduled 28 variables 0%
c [elim-8] boosting limit by 20
c [elim-8] limit of 432573520 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 1142457 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 28 scheduled
c [bca-6] limit of 10000000 steps and 166625 added (scaled 2)
c [bca-6] 13664 out of 25630 literals actually usable 53%
c [bca-6] added 11 blocked clauses in 56612 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 1208 pos 53.0% + 1073 neg 47.0% = 2281 sched 17.8% ret 10533
c [sweep-6-1] 1000560 steps 232 queries 289.88 avg class size
c [sweep-6-1] 3767 decisions 226 SAT calls 32.73 avg env size
c [sweep-6-1] 1609 variables remain 13% (11205 retained 87%)
c [decomp-28] removed 9 variables
c [sweep-6-1] removed 9 vars (0 failed, 7 eqs, 17 impls)
c [sweep-6] 9 < 1/1000 * 12814 = 12 considered unsuccessful
c [sweep-6] removed 9 vars in TOTAL (1 rounds, 231 queries)
c [sort-queue-10] sorted 6518 enqueued variables after 17003 conflicts
c [score-dist-10] active 6287 (49%), one 2943 (23%), zero 3575 (28%)
c [score-dist-10] max exp 736, different 669 (91%)
c [score-dist-10] median active exp 589, avg 500.5
c [simplification-10] removed 31 variables 0.2% (12805 remain 7%)
c [simplification-10] removed 2824 irredundant clauses 3.3% (82972 remain 15%)
c [simplification-10] maximum reduction of 3% = max (0%, 3%)
c [simplification-10] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-10] new conflict interval 5000
c [simplification-10] penalized conflict interval 5000 = 1 * 5000
c [simplification-10] hard conflict limit 32003 (soft 22003 + delta 10000)
c [simplification-10] new conflict limit 22003 (hard 32003)
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   25.8   12804    82972     19824   17276  31928  8310    4    52   23   8%     97   42    5    1  475%
c i   26.1   12803    82972     21264   18512  32064  8329    4    52   23   8%     28   41    4    1  398%
c 
c [simplification-11] limit 22003 conflicts (hard 32003) hit after 22003 conflicts
c [quatres-7] found 29815 quaternary clauses 55% in total
c [quatres-7-1] removed 2 duplicate quaternary clauses
c [quatres-7-1] added 7 double-self-subsuming ternary resolvents
c [quatres-7-2] added 477 single-self-subsuming ternary resolvents
c [quatres-7-2] added 339 quaternary resolvents
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] 577 schedulable variables 5%
c [ternres-7] 5656 ternary resolvents (78 bin, 5578 trn)
c [ternres-7] 31 variables remain 0% (12768 retained 100%)
c [decomp-29] removed 14 variables
c [simpleprobe-5] 537 schedulable variables 4%
c [simpleprobe-5] limit 5957794 penalty 0 = 0 + 0
c [decomp-30] removed 7 variables
c [simpleprobe-5] 386 variables remain 3% (12398 retained 97%)
c [simpleprobe-5] removed 7 variables, found 1215 hbrs, 5 units
c [transred-7] limit 1489448 with penalty 0 = 0 + 0
c [transred-7] removed 795 transitive binary clauses
c [transred-7] found 1 units
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 12
c [cce-7-1] eliminated 1 clauses out of 25 (4%) of length 11
c [cce-7-1] eliminated 4 clauses out of 51 (8%) of length 10
c [cce-7-1] eliminated 6 clauses out of 344 (2%) of length 9
c [cce-7-1] eliminated 7 clauses out of 624 (1%) of length 8
c [cce-7-1] eliminated 35 clauses out of 2162 (2%) of length 7
c [cce-7-1] eliminated 276 clauses out of 4912 (6%) of length 6
c [cce-7-1] eliminated 635 clauses out of 9037 (7%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 965 large clauses in 30000027 steps
c [cce-7-1] allowing another 15000013 steps for small clauses
c [cce-7-1] scheduling 31897 clauses = 10668 binary + 21229 ternary
c [cce-7-1] tried to eliminate 18180 small clauses 57%
c [cce-7-1] eliminated 203 binary clauses 2%
c [cce-7-1] eliminated 2059 ternary clauses 10%
c [cce-7-1] eliminated 2262 small clauses 7%
c [cce-7-1] eliminated 2274 small clauses in 30000007 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 3239 covered clauses in round 1
c [cce-7] eliminated 3239 covered clauses in TOTAL during 1 rounds
c [bca-7] limit of 10000000 steps and 159895 added (scaled 2)
c [bca-7] 12575 out of 25566 literals actually usable 49%
c [bca-7] added 8 blocked clauses in 57202 steps
c [sort-queue-11] sorted 7069 enqueued variables after 22003 conflicts
c [score-dist-11] active 5713 (45%), one 4041 (32%), zero 3028 (24%)
c [score-dist-11] max exp 538, different 461 (86%)
c [score-dist-11] median active exp 424, avg 387.8
c [simplification-11] removed 17 variables 0.1% (12782 remain 7%)
c [simplification-11] removed 3357 irredundant clauses 4.0% (79615 remain 15%)
c [simplification-11] maximum reduction of 4% = max (0%, 4%)
c [simplification-11] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-11] new conflict interval 9000
c [simplification-11] penalized conflict interval 9000 = 1 * 9000
c [simplification-11] hard conflict limit 41003 (soft 31003 + delta 10000)
c [simplification-11] new conflict limit 31003 (hard 41003)
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   27.6   12781    79614     22646   19877  39764  8806    4    53   24   8%     11   41    4    1  347%
c 
c [simplification-12] limit 31003 conflicts (hard 41003) hit after 31005 conflicts
c [quatres-8] found 30834 quaternary clauses 53% in total
c [quatres-8-1] removed 2 duplicate quaternary clauses
c [quatres-8-1] added 3 double-self-subsuming ternary resolvents
c [quatres-8-2] added 107 single-self-subsuming ternary resolvents
c [quatres-8-2] added 170 quaternary resolvents
c [ternres-8] limit 4000000 with penalty 0 = 0 + 0
c [ternres-8] 31 schedulable variables 0%
c [ternres-8] 2277 ternary resolvents (73 bin, 2204 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-31] removed 3 variables
c [unhide-11] limit 229106 with penalty 1 = 1 + 0
c [unhide-11-11] 0 units, 0 failed, 702 tauts, 0 hbrs, 4101 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 590 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 12
c [cce-8-1] eliminated 1 clauses out of 338 (0%) of length 9
c [cce-8-1] eliminated 3 clauses out of 621 (0%) of length 8
c [cce-8-1] eliminated 6 clauses out of 4566 (0%) of length 6
c [cce-8-1] eliminated 21 clauses out of 8332 (0%) of length 5
c [cce-8-1] eliminated 677 clauses out of 21813 (3%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 710 large clauses in 51366676 steps
c [cce-8-1] allowing another 25683338 steps for small clauses
c [cce-8-1] scheduling 22485 clauses = 10497 binary + 11988 ternary
c [cce-8-1] tried to eliminate 22485 small clauses 100%
c [cce-8-1] eliminated 10 binary clauses 0%
c [cce-8-1] eliminated 225 ternary clauses 2%
c [cce-8-1] eliminated 235 small clauses 1%
c [cce-8-1] eliminated 235 small clauses in 40863812 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 945 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 25209448 steps for small clauses
c [cce-8-2] scheduling 22250 clauses = 10487 binary + 11763 ternary
c [cce-8-2] tried to eliminate 22250 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 945 covered clauses in TOTAL during 2 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 12779 variables 100%
c [elim-9] limit of 22910695 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 831 variables 7% in round 1 in 20160517 steps
c [elim-9-1] backward subsumption/strengthening limit 2750178
c [elim-9-1-1] backward checking 4039 touched variables 32%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 17 and strengthened 59 clauses in 1360001 steps
c [elim-9-1] rescheduled 234 variables 2% by backward subsumption
c [elim-9-2] eliminated 3 variables 0% in round 2 in 803013 steps
c [elim-9-2] backward subsumption/strengthening limit 587164
c [elim-9-2-1] backward checking 31 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 1 and strengthened 4 clauses in 103356 steps
c [elim-9-2] rescheduled 12 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 49947 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 834 = 7% variables out of 12779 scheduled
c [bca-8] limit of 10000000 steps and 154339 added (scaled 2)
c [bca-8] 10776 out of 23892 literals actually usable 45%
c [bca-8] added 46 blocked clauses in 58658 steps
c [sweep-7] limit 500000 penalty 1 = 1 + 0
c [sweep-7-1] 709 pos 47.5% + 783 neg 52.5% = 1492 sched 12.5% ret 10453
c [sweep-7-1] 502973 steps 62 queries 376.95 avg class size
c [sweep-7-1] 1149 decisions 61 SAT calls 36.26 avg env size
c [sweep-7-1] 1349 variables remain 11% (10596 retained 89%)
c [decomp-32] removed 2 variables
c [sweep-7-1] removed 2 vars (0 failed, 0 eqs, 1 impls)
c [sweep-7] 2 < 1/1000 * 11945 = 11 considered unsuccessful
c [sweep-7] removed 2 vars in TOTAL (1 rounds, 61 queries)
c [sort-queue-12] sorted 5653 enqueued variables after 31005 conflicts
c [score-dist-12] active 6290 (53%), one 3259 (27%), zero 2394 (20%)
c [score-dist-12] max exp 887, different 687 (77%)
c [score-dist-12] median active exp 777, avg 665.8
c [simplification-12] removed 838 variables 6.6% (11943 remain 7%)
c [simplification-12] removed 2781 irredundant clauses 3.5% (76833 remain 14%)
c [simplification-12] maximum reduction of 7% = max (7%, 3%)
c [simplification-12] large reduction 7% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 43005 (soft 33005 + delta 10000)
c [simplification-12] new conflict limit 33005 (hard 43005)
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.5   11942    76833     31274   25595  34017  7056    5    51   24   9%    104   34    5    2  340%
c i   32.8   11941    76833     32759   26839  34180  7081    5    49   24   9%     23   31    5    2  301%
c 
c [simplification-13] limit 33005 conflicts (hard 43005) hit after 33006 conflicts
c [quatres-9] found 29544 quaternary clauses 52% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-2] added 202 single-self-subsuming ternary resolvents
c [quatres-9-2] added 539 quaternary resolvents
c [ternres-9] limit 4000000 with penalty 0 = 0 + 0
c [ternres-9] all 11935 free variables schedulable
c [ternres-9] 1720 ternary resolvents (26 bin, 1694 trn)
c [ternres-9] 835 variables remain 7% (11100 retained 93%)
c [decomp-33] removed 9 variables
c [treelook-5] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 6907 literals 29%
c [treelook-5] scheduling used 150003 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 151613 steps
c [treelook-5] 6870 literals remain 29%
c [treelook-5] 4825 variables remain to probed next time 40%
c [treelook-5] removed 0 variables, found 110 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 285 transitive binary clauses
c [transred-9] found 1 units
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 13
c [cce-9-1] eliminated 2 clauses out of 18 (11%) of length 11
c [cce-9-1] eliminated 2 clauses out of 74 (3%) of length 10
c [cce-9-1] eliminated 9 clauses out of 420 (2%) of length 9
c [cce-9-1] eliminated 37 clauses out of 957 (4%) of length 8
c [cce-9-1] eliminated 58 clauses out of 2106 (3%) of length 7
c [cce-9-1] eliminated 287 clauses out of 4710 (6%) of length 6
c [cce-9-1] eliminated 546 clauses out of 8244 (7%) of length 5
c [cce-9-1] eliminated 124 clauses out of 20691 (1%) of length 4
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 1066 large clauses in 30000106 steps
c [cce-9-1] allowing another 15000053 steps for small clauses
c [cce-9-1] scheduling 28379 clauses = 9755 binary + 18624 ternary
c [cce-9-1] tried to eliminate 18619 small clauses 66%
c [cce-9-1] eliminated 121 binary clauses 1%
c [cce-9-1] eliminated 1081 ternary clauses 6%
c [cce-9-1] eliminated 1202 small clauses 4%
c [cce-9-1] eliminated 1208 small clauses in 30000001 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 2274 covered clauses in round 1
c [cce-9] eliminated 2274 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 11933 variables 100%
c [elim-10] limit of 49123270 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 232 variables 2% in round 1 in 18351695 steps
c [elim-10-1] backward subsumption/strengthening limit 18351600
c [elim-10-1-1] backward checking 1552 touched variables 13%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 12 clauses in 669767 steps
c [elim-10-1] rescheduled 38 variables 0% by backward subsumption
c [elim-10-2] eliminated 2 variables 0% in round 2 in 161721 steps
c [elim-10-2] backward subsumption/strengthening limit 161700
c [elim-10-2-1] backward checking 16 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 1 clauses in 54244 steps
c [elim-10-2] rescheduled 5 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 10655 steps
c [elim-10-3] backward subsumption/strengthening limit 10600
c [elim-10-3-1] backward checking 12 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 0 and strengthened 0 clauses in 10601 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 235 = 2% variables out of 11933 scheduled
c [bca-9] limit of 10000000 steps and 148522 added (scaled 2)
c [bca-9] 10186 out of 23398 literals actually usable 44%
c [bca-9] added 24 blocked clauses in 58612 steps
c [sort-queue-13] sorted 5507 enqueued variables after 33006 conflicts
c [score-dist-13] active 6191 (53%), one 3231 (28%), zero 2276 (19%)
c [score-dist-13] max exp 907, different 683 (75%)
c [score-dist-13] median active exp 763, avg 667.9
c [simplification-13] removed 237 variables 2.0% (11698 remain 6%)
c [simplification-13] removed 2918 irredundant clauses 3.8% (73915 remain 14%)
c [simplification-13] maximum reduction of 4% = max (2%, 4%)
c [simplification-13] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-13] new conflict interval 13000
c [simplification-13] penalized conflict interval 13000 = 1 * 13000
c [simplification-13] hard conflict limit 56006 (soft 46006 + delta 10000)
c [simplification-13] new conflict limit 46006 (hard 56006)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   34.5   11697    73915     33364   27412  34904  6823    5    49   24  10%      8   31    5    2  332%
c i   35.5   11694    73915     37173   30712  35249  6861    5    49   24  10%     28   30    5    2  284%
c i   35.9   11692    73915     38602   31967  35379  6868    5    52   24  10%      5   31    6    2  297%
c i   36.4   11691    73915     40464   33623  35519  6880    5    51   24  10%      3   30    6    2  290%
c i   37.2   11690    73915     43897   36633  35814  6910    5    49   25  10%     22   27    5    2  235%
c 
c [simplification-14] limit of 4910 ternary hit after 4910 ternaries
c [quatres-10] found 30492 quaternary clauses 50% in total
c [quatres-10-1] removed 2 duplicate quaternary clauses
c [quatres-10-2] added 147 single-self-subsuming ternary resolvents
c [quatres-10-2] added 254 quaternary resolvents
c [ternres-10] limit 4000000 with penalty 0 = 0 + 0
c [ternres-10] 814 schedulable variables 7%
c [ternres-10] 2558 ternary resolvents (39 bin, 2519 trn)
c [ternres-10] 23 variables remain 0% (11667 retained 100%)
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] extracted 124 xors of average arity 3.0
c [gauss-4] connected 370 occurrences of 165 variables (average 2.2)
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-35] removed 4 variables
c [basicprobe-5] limit 17597802 penalty 0 = 0 + 0
c [basicprobe-5-0] 3533 sched 30%, 18 failed, 1 lifted, 1279 hbrs
c [decomp-36] removed 22 variables
c [basicprobe-5-1] 5684 sched 49%, 8 failed, 0 lifted, 1126 hbrs
c [decomp-37] removed 9 variables
c [basicprobe-5-2] 5646 sched 48%, 4 failed, 0 lifted, 372 hbrs
c [decomp-38] removed 4 variables
c [basicprobe-5-3] 5638 sched 48%, 3 failed, 0 lifted, 62 hbrs
c [decomp-39] removed 3 variables
c [basicprobe-5-4] 5640 sched 48%, 0 failed, 0 lifted, 37 hbrs
c [basicprobe-5-5] 5640 sched 48%, 0 failed, 0 lifted, 26 hbrs
c [basicprobe-5-6] 2281 probes remain 20% after last round
c [basicprobe-5-6] 34 units = 33 failed (97%) + 1 lifted (3%)
c [basicprobe-5-6] removed 38 variables, found 2906 hbrs
c [bate-3] eliminated 37 asymmetric tautologies during probing
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 491 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 11648 variables 100%
c [block-4] limit of 6250000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 5 blocked clauses
c [block-4] 5 < 1/100 * 73634 = 736 considered unsuccessful
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 15
c [cce-10-1] eliminated 1 clauses out of 12 (8%) of length 11
c [cce-10-1] eliminated 3 clauses out of 406 (1%) of length 9
c [cce-10-1] eliminated 12 clauses out of 1019 (1%) of length 8
c [cce-10-1] eliminated 32 clauses out of 2066 (2%) of length 7
c [cce-10-1] eliminated 53 clauses out of 4407 (1%) of length 6
c [cce-10-1] eliminated 66 clauses out of 7654 (1%) of length 5
c [cce-10-1] eliminated 6 clauses out of 20283 (0%) of length 4
c [cce-10-1] incomplete large round (ATE)
c [cce-10-1] eliminated 174 large clauses in 30000004 steps
c [cce-10-1] allowing another 15000002 steps for small clauses
c [cce-10-1] scheduling 20464 clauses = 9511 binary + 10953 ternary
c [cce-10-1] tried to eliminate 20464 small clauses 100%
c [cce-10-1] eliminated 8 binary clauses 0%
c [cce-10-1] eliminated 294 ternary clauses 3%
c [cce-10-1] eliminated 302 small clauses 1%
c [cce-10-1] eliminated 302 small clauses in 28886860 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 476 covered clauses in round 1
c [cce-10-2] incomplete large round (ATE)
c [cce-10-2] allowing another 556582 steps for small clauses
c [cce-10-2] scheduling 20162 clauses = 9503 binary + 10659 ternary
c [cce-10-2] tried to eliminate 820 small clauses 4%
c [cce-10-2] incomplete small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 476 covered clauses in TOTAL during 2 rounds
c [cce-10] 476 < 1/100 * 73629 = 736 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 11648 variables 100%
c [elim-11] limit of 70391208 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 58 variables 0% in round 1 in 17808244 steps
c [elim-11-1] backward subsumption/strengthening limit 17808200
c [elim-11-1-1] backward checking 568 touched variables 5%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 288148 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 58 = 0% variables out of 11648 scheduled
c [elim-11] 58 < 1/100 * 11648 = 116 considered unsuccessful
c [bca-10] limit of 10000000 steps and 146742 added (scaled 2)
c [bca-10] 9037 out of 23182 literals actually usable 39%
c [bca-10] added 22 blocked clauses in 64658 steps
c [sort-queue-14] sorted 4936 enqueued variables after 44393 conflicts
c [score-dist-14] active 6654 (57%), one 3127 (27%), zero 1809 (16%)
c [score-dist-14] max exp 870, different 672 (77%)
c [score-dist-14] median active exp 759, avg 658.3
c [simplification-14] removed 100 variables 0.9% (11590 remain 6%)
c [simplification-14] removed 896 irredundant clauses 1.2% (73019 remain 13%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] forced so keeping old conflict interval 13000
c [simplification-14] conflict limit remains at 46006 (hard 56006)
c [simplification-14] new ternary interval 10000
c 
c [simplification-15] limit 46006 conflicts (hard 56006) hit after 46006 conflicts
c [quatres-11] found 30511 quaternary clauses 50% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 82 single-self-subsuming ternary resolvents
c [quatres-11-2] added 79 quaternary resolvents
c [ternres-11] limit 4000000 with penalty 0 = 0 + 0
c [ternres-11] 23 schedulable variables 0%
c [ternres-11] 404 ternary resolvents (8 bin, 396 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 125000 penalty 4 = 4 + 0
c [card-5] found 47 at-most-one constraints of average size 3.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 125000 for elimination
c [card-5] 47 out of 47 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [simpleprobe-6] 356 schedulable variables 3%
c [simpleprobe-6] limit 14703075 penalty 0 = 0 + 0
c [decomp-43] removed 3 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 3 variables, found 1652 hbrs, 0 units
c [unhide-12] limit 183788 with penalty 2 = 2 + 0
c [unhide-12-12] 0 units, 0 failed, 4420 tauts, 0 hbrs, 14861 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 600 transitive binary clauses
c [bca-11] limit of 10000000 steps and 146743 added (scaled 2)
c [bca-11] 8913 out of 23176 literals actually usable 38%
c [bca-11] added 5 blocked clauses in 64819 steps
c [sweep-8] limit 275682 penalty 2 = 2 + 0
c [sweep-8-1] 844 pos 64.1% + 473 neg 35.9% = 1317 sched 11.4% ret 10270
c [sweep-8-1] 454434 steps 29 queries 382.31 avg class size
c [sweep-8-1] 587 decisions 27 SAT calls 31.74 avg env size
c [sweep-8-1] 1273 variables remain 11% (10314 retained 89%)
c [decomp-44] removed 2 variables
c [sweep-8-1] removed 2 vars (0 failed, 1 eqs, 1 impls)
c [sweep-8] 2 < 1/1000 * 11587 = 11 considered unsuccessful
c [sweep-8] removed 2 vars in TOTAL (1 rounds, 28 queries)
c [sort-queue-15] sorted 5070 enqueued variables after 46006 conflicts
c [score-dist-15] active 6515 (56%), one 3321 (29%), zero 1749 (15%)
c [score-dist-15] max exp 805, different 644 (80%)
c [score-dist-15] median active exp 712, avg 614.0
c [simplification-15] removed 5 variables 0.0% (11585 remain 6%)
c [simplification-15] removed 9 irredundant clauses 0.0% (73010 remain 13%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 20000
c [simplification-15] new conflict interval 33000
c [simplification-15] penalized conflict interval 33000 = 1 * 33000
c [simplification-15] hard conflict limit 95506 (soft 79006 + delta 16500)
c [simplification-15] new conflict limit 79006 (hard 95506)
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   44.1   11584    73010     56747   47399  36118  8669    6    49   26  12%    155   22    6    3  229%
c i   44.4   11578    73010     57715   48284  36170  8673    6    50   26  12%     46   22    6    3  219%
c i   44.4   11576    73010     57716   48284  36170  8673    6    50   26  12%     46   22    6    3  218%
c i   45.3   11575    73010     60755   51060  36321  8699    6    52   26  11%      5   23    6    3  218%
c i   45.8   11573    73010     62169   52344  36393  8713    6    52   26  11%    -12   22    5    3  164%
c i   45.8   11572    73010     62185   52351  36397  8714    6    52   26  11%    -13   22    5    3  160%
c i   46.7   11571    73010     65032   54974  36556  8727    6    51   27  12%     -0   21    6    3  204%
c i   47.4   11570    73010     67268   57029  36675  8734    6    52   27  12%     -6   21    6    3  180%
c i   48.0   11569    73010     68885   58528  36741  8740    6    54   27  12%    -13   23    6    3  189%
c 
c [simplification-16] limit of 780 binary hit after 787 binaries
c [quatres-12] found 32231 quaternary clauses 46% in total
c [quatres-12-1] removed 5 duplicate quaternary clauses
c [quatres-12-1] added 2 double-self-subsuming ternary resolvents
c [quatres-12-2] added 193 single-self-subsuming ternary resolvents
c [quatres-12-2] added 323 quaternary resolvents
c [ternres-12] limit 6361615 with penalty 0 = 0 + 0
c [ternres-12] all 11569 free variables schedulable
c [ternres-12] 1749 ternary resolvents (21 bin, 1728 trn)
c [ternres-12] 347 variables remain 3% (11222 retained 97%)
c [decomp-45] removed 19 variables
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 304 transitive binary clauses
c [transred-12] found 4 units
c [cce-11] limit of 15904038 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 3 clauses out of 293 (1%) of length 9
c [cce-11-1] eliminated 8 clauses out of 2249 (0%) of length 7
c [cce-11-1] eliminated 60 clauses out of 4211 (1%) of length 6
c [cce-11-1] eliminated 18 clauses out of 7592 (0%) of length 5
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 89 large clauses in 15904050 steps
c [cce-11-1] allowing another 7952025 steps for small clauses
c [cce-11-1] scheduling 20327 clauses = 9510 binary + 10817 ternary
c [cce-11-1] tried to eliminate 9117 small clauses 45%
c [cce-11-1] eliminated 37 binary clauses 0%
c [cce-11-1] eliminated 551 ternary clauses 5%
c [cce-11-1] eliminated 588 small clauses 3%
c [cce-11-1] eliminated 631 small clauses in 15904043 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 720 covered clauses in round 1
c [cce-11] eliminated 720 covered clauses in TOTAL during 1 rounds
c [cce-11] 720 < 1/100 * 72898 = 728 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 11559 variables 100%
c [elim-12] limit of 63616155 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 152 variables 1% in round 1 in 17133012 steps
c [elim-12-1] backward subsumption/strengthening limit 17133000
c [elim-12-1-1] backward checking 1064 touched variables 9%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 6 and strengthened 11 clauses in 462963 steps
c [elim-12-1] rescheduled 47 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 140217 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 152 = 1% variables out of 11559 scheduled
c [bca-12] limit of 10000000 steps and 144355 added (scaled 2)
c [bca-12] 6806 out of 22816 literals actually usable 30%
c [bca-12] added 5 blocked clauses in 80509 steps
c [sort-queue-16] sorted 4911 enqueued variables after 71667 conflicts
c [score-dist-16] active 6496 (57%), one 4068 (36%), zero 843 (7%)
c [score-dist-16] max exp 504, different 448 (89%)
c [score-dist-16] median active exp 399, avg 350.4
c [simplification-16] removed 162 variables 1.4% (11407 remain 6%)
c [simplification-16] removed 1191 irredundant clauses 1.6% (71819 remain 13%)
c [simplification-16] maximum reduction of 2% = max (1%, 2%)
c [simplification-16] forced so keeping old conflict interval 33000
c [simplification-16] conflict limit remains at 79016 (hard 95506)
c [simplification-16] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   50.6   11406    71819     72506   60620  37859  7961    6    55   30  12%     12   22    5    3  157%
c i   51.4   11405    71819     74947   62868  37968  7975    6    57   30  11%     -2   23    6    4  165%
c i   51.6   11403    71819     75477   63357  37996  7979    6    57   30  11%    -11   24    7    4  188%
c i   52.4   11402    71819     77622   65351  38086  7989    6    59   30  11%     -7   24    6    4  176%
c i   52.5   11401    71819     77888   65590  38102  7989    6    58   30  11%    -12   23    6    4  151%
c i   52.6   11400    71819     78085   65770  38112  7992    6    57   30  11%    -14   23    6    4  151%
c i   53.0   11399    71819     79106   66726  38156  7996    6    58   30  11%    -18   23    7    4  190%
c i   53.0   11398    71819     79117   66733  38156  7998    6    58   30  11%    -18   23    7    4  185%
c 
c [simplification-17] limit 79016 conflicts (hard 95506) hit after 81819 conflicts
c [quatres-13] found 32816 quaternary clauses 45% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 99 single-self-subsuming ternary resolvents
c [quatres-13-2] added 187 quaternary resolvents
c [ternres-13] limit 7562353 with penalty 0 = 0 + 0
c [ternres-13] 343 schedulable variables 3%
c [ternres-13] 1962 ternary resolvents (37 bin, 1925 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-46] removed 12 variables
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 216 transitive binary clauses
c [transred-13] found 2 units
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 11392 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 11 variables 0% in round 1 in 16999375 steps
c [elim-13-1] backward subsumption/strengthening limit 16999300
c [elim-13-1-1] backward checking 129 touched variables 1%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 2 clauses in 77350 steps
c [elim-13-1] rescheduled 5 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 16763 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 11 = 0% variables out of 11392 scheduled
c [elim-13] 11 < 1/100 * 11392 = 113 considered unsuccessful
c [bca-13] limit of 10000000 steps and 144118 added (scaled 2)
c [bca-13] 6165 out of 22764 literals actually usable 27%
c [bca-13] added 0 blocked clauses in 87928 steps
c [sort-queue-17] sorted 4715 enqueued variables after 81819 conflicts
c [score-dist-17] active 6666 (59%), one 4057 (36%), zero 658 (6%)
c [score-dist-17] max exp 659, different 529 (80%)
c [score-dist-17] median active exp 588, avg 508.0
c [simplification-17] removed 17 variables 0.1% (11381 remain 6%)
c [simplification-17] removed 120 irredundant clauses 0.2% (71699 remain 13%)
c [simplification-17] maximum reduction of 0% = max (0%, 0%)
c [simplification-17] full geometric conflict interval increment 33000
c [simplification-17] new conflict interval 66000
c [simplification-17] penalized conflict interval 66000 = 1 * 66000
c [simplification-17] hard conflict limit 180819 (soft 147819 + delta 33000)
c [simplification-17] new conflict limit 147819 (hard 180819)
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   55.7   11380    71699     83607   70903  40195  7825    7    59   32  11%     26   23    7    4  177%
c i   55.8   11379    71699     83651   70946  40195  7825    7    60   32  11%     24   23    7    4  181%
c i   56.1   11378    71699     84708   71930  40239  7832    7    59   32  12%     -4   22    7    4  174%
c i   56.6   11377    71699     85828   72978  40282  7836    7    58   32  12%    -13   21    7    4  170%
c i   56.8   11376    71699     86420   73526  40312  7841    7    57   32  12%    -18   19    7    4  170%
c i   57.2   11375    71699     87272   74320  40339  7845    7    57   32  12%    -19   20    7    4  163%
c i   57.2   11374    71699     87274   74320  40337  7847    7    57   32  12%    -19   20    7    4  162%
c i   57.2   11373    71699     87411   74446  40342  7848    7    58   32  12%    -20   20    7    4  158%
c i   57.6   11371    71699     88210   75196  40373  7851    7    58   32  12%    -20   20    7    4  160%
c i   58.1   11370    71699     89535   76412  40435  7861    7    58   32  12%    -16   20    6    4  147%
c i   58.1   11368    71699     89562   76435  40437  7861    7    58   32  12%    -16   19    6    4  143%
c i   58.2   11367    71699     89779   76639  40445  7861    7    58   32  12%    -18   19    7    4  166%
c i   58.2   11366    71699     89794   76651  40446  7861    7    57   32  12%    -18   19    7    4  160%
c i   59.3   11365    71699     92349   79038  40540  7871    7    59   32  12%     -1   19    6    4  140%
c 
c [simplification-18] limit of 53 iterations hit after 57 iterations
c [quatres-14] found 33599 quaternary clauses 43% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 65 single-self-subsuming ternary resolvents
c [quatres-14-2] added 124 quaternary resolvents
c [ternres-14] limit 9235252 with penalty 0 = 0 + 0
c [ternres-14] all 11364 free variables schedulable
c [ternres-14] 703 ternary resolvents (19 bin, 684 trn)
c [ternres-14] 39 variables remain 0% (11325 retained 100%)
c [decomp-47] removed 20 variables
c [treelook-6] limit 230881 penalty 2 = 2 + 0 boost 1
c [treelook-6] scheduled 7502 literals 33%
c [treelook-6] scheduling used 230888 steps
c [treelook-6] not fully scheduled
c [treelook-6] limit 230881 penalty 2 = 2 + 0 boost 1
c [treelook-6] used 232483 steps
c [treelook-6] 7317 literals remain 32%
c [treelook-6] 4045 variables remain to probed next time 36%
c [treelook-6] removed 0 variables, found 238 hbrs
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 215 transitive binary clauses
c [sort-queue-18] sorted 5013 enqueued variables after 94826 conflicts
c [score-dist-18] active 6348 (56%), one 4483 (39%), zero 530 (5%)
c [score-dist-18] max exp 562, different 500 (89%)
c [score-dist-18] median active exp 473, avg 409.6
c [simplification-18] removed 3 variables 0.0% (11361 remain 6%)
c [simplification-18] removed 147 irredundant clauses 0.2% (71552 remain 13%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] forced so keeping old conflict interval 66000
c [simplification-18] conflict limit remains at 147824 (hard 180819)
c [simplification-18] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   62.2   11360    71552     97735   83843  41202  7946    7    57   34  13%     41   16    9    5  190%
c i   62.2   11359    71552     97737   83844  41202  7946    7    57   34  13%     41   16    9    5  189%
c i   66.1   11358    71552    106598   92129  41552  7982    7    55   34  13%     91   12    9    5  179%
c i   66.2   11357    71552    106716   92229  41558  7987    7    54   34  13%     77   11    8    5  158%
c i   66.2   11355    71552    106718   92229  41559  7987    7    54   34  13%     77   11    8    5  157%
c i   66.5   11354    71552    107453   92917  41583  7992    7    55   34  13%     24   12    8    5  155%
c i   66.7   11353    71552    107893   93333  41598  7995    7    56   34  13%      5   14    8    5  154%
c i   67.3   11352    71552    109205   94561  41649  7998    7    55   34  13%    -13   12    8    5  165%
c i   67.4   11351    71552    109248   94590  41653  8002    7    54   34  13%    -14   11    8    5  152%
c i   68.3   11350    71552    111155   96384  41720  8008    7    52   34  14%    -13    9    7    5  135%
c i   68.3   11349    71552    111204   96425  41721  8011    7    52   34  14%    -14    9    7    5  145%
c -   69.5   11349    71552    113812   54476  41803  8020    7    55   27  13%     -4   11    8    5  152%
c i   69.8   11348    71552    114779   55362  41846  8025    7    55   29  13%      9   11    8    5  148%
c i   70.2   11347    71552    115684   56195  41882  8027    7    55   29  13%    -10   11    7    5  133%
c i   71.3   11345    71552    118670   58957  42023  8033    7    56   29  13%      2   11    6    5  122%
c i   71.3   11344    71552    118861   59136  42028  8035    7    55   29  13%     -4   11    6    5  118%
c i   71.4   11342    71552    119154   59406  42041  8038    7    55   29  13%    -10   10    6    5  111%
c i   73.2   11341    71552    124044   64010  42186  8067    7    57   30  13%     30   11    7    5  137%
c i   73.2   11340    71552    124046   64010  42186  8068    7    57   30  13%     30   11    7    5  136%
c i   73.2   11338    71552    124189   64146  42190  8068    7    56   30  13%     22   10    7    5  137%
c i   73.4   11337    71552    124633   64569  42205  8070    7    56   30  13%      5   11    7    5  124%
c i   73.4   11336    71552    124657   64583  42207  8070    7    56   30  13%      4   10    6    5  118%
c i   74.0   11331    71552    126397   66218  42265  8078    7    58   30  12%    -10   12    6    5  109%
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   74.0   11330    71552    126413   66228  42267  8080    7    58   30  12%    -11   12    6    5  105%
c i   74.0   11329    71552    126426   66234  42269  8082    7    58   30  12%    -11   12    6    5  103%
c i   74.0   11328    71552    126607   66403  42275  8085    7    58   30  12%    -14   12    7    6  119%
c i   74.1   11327    71552    126886   66655  42289  8089    7    60   30  12%    -17   14    6    6  110%
c i   74.6   11326    71552    128348   68024  42336  8097    7    61   30  11%    -16   15    6    6  112%
c i   75.2   11325    71552    129930   69532  42379  8103    7    59   30  12%    -15   13    7    6  131%
c i   75.3   11324    71552    130158   69749  42383  8103    7    59   30  12%    -17   12    7    6  123%
c i   76.6   11323    71552    133536   72947  42500  8110    7    62   30  11%      9   15    6    6  115%
c i   77.2   11322    71552    135054   74392  42544  8112    7    59   30  12%     -9   11    8    6  134%
c i   77.6   11321    71552    136117   75392  42574  8117    7    59   30  12%    -15   11    8    6  142%
c i   78.4   11319    71552    137949   77142  42621  8127    8    56   30  13%    -11    8    8    6  139%
c i   78.7   11318    71552    138779   77927  42644  8130    8    55   31  14%    -16    7    7    6  126%
c i   79.4   11315    71552    140267   79332  42696  8134    8    57   32  14%    -14    8    8    6  130%
c i   79.9   11314    71551    141629   80619  42741  8137    8    58   32  13%    -14   10    7    6  123%
c i   81.2   11313    71551    144470   83321  42828  8145    8    58   32  13%      3    9    8    6  133%
c i   81.6   11312    71551    145692   84452  42875  8153    7    62   32  12%    -10   13    7    6  110%
c 
c [simplification-19] limit 147839 conflicts (hard 180819) hit after 148229 conflicts
c [quatres-15] found 36227 quaternary clauses 39% in total
c [quatres-15-1] removed 2 duplicate quaternary clauses
c [quatres-15-2] added 170 single-self-subsuming ternary resolvents
c [quatres-15-2] added 235 quaternary resolvents
c [ternres-15] limit 16064384 with penalty 0 = 0 + 0
c [ternres-15] 37 schedulable variables 0%
c [ternres-15] 1749 ternary resolvents (30 bin, 1719 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 200804 penalty 4 = 4 + 0
c [gauss-5] extracted 63 xors of average arity 3.0
c [gauss-5] connected 188 occurrences of 91 variables (average 2.1)
c [gauss-5] limit 200804 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-49] removed 7 variables
c [basicprobe-6] limit 80321924 penalty 0 = 0 + 0
c [basicprobe-6-0] 2203 sched 20%, 25 failed, 1 lifted, 1055 hbrs
c [decomp-50] removed 50 variables
c [basicprobe-6-1] 5201 sched 46%, 20 failed, 0 lifted, 1461 hbrs
c [decomp-51] removed 26 variables
c [basicprobe-6-2] 5154 sched 46%, 12 failed, 0 lifted, 297 hbrs
c [decomp-52] removed 17 variables
c [basicprobe-6-3] 5139 sched 46%, 5 failed, 0 lifted, 159 hbrs
c [decomp-53] removed 5 variables
c [basicprobe-6-4] 5141 sched 46%, 2 failed, 0 lifted, 85 hbrs
c [decomp-54] removed 2 variables
c [basicprobe-6-5] 5143 sched 46%, 2 failed, 0 lifted, 34 hbrs
c [decomp-55] removed 2 variables
c [basicprobe-6-6] 5142 sched 46%, 1 failed, 0 lifted, 39 hbrs
c [decomp-56] removed 1 variables
c [basicprobe-6-7] 5141 sched 46%, 2 failed, 0 lifted, 26 hbrs
c [decomp-57] removed 2 variables
c [basicprobe-6-8] 5142 sched 46%, 1 failed, 0 lifted, 37 hbrs
c [basicprobe-6-8] round limit 8 hit
c [basicprobe-6-8] 71 units = 70 failed (99%) + 1 lifted (1%)
c [basicprobe-6-8] removed 106 variables, found 3193 hbrs
c [bate-4] eliminated 51 asymmetric tautologies during probing
c [unhide-13] limit 401609 with penalty 3 = 3 + 0
c [unhide-13-13] 0 units, 0 failed, 521 tauts, 0 hbrs, 21817 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 631 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 11198 variables 100%
c [block-5] limit of 10040240 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 92 blocked clauses
c [block-5] 92 < 1/100 * 70357 = 703 considered unsuccessful
c [cce-12] limit of 20080481 steps penalty 2 = 2 + 0
c [cce-12-1] eliminated 5 clauses out of 259 (2%) of length 9
c [cce-12-1] eliminated 9 clauses out of 669 (1%) of length 8
c [cce-12-1] eliminated 16 clauses out of 2230 (1%) of length 7
c [cce-12-1] eliminated 25 clauses out of 4026 (1%) of length 6
c [cce-12-1] eliminated 10 clauses out of 7505 (0%) of length 5
c [cce-12-1] incomplete large round (ATE)
c [cce-12-1] eliminated 65 large clauses in 20080519 steps
c [cce-12-1] allowing another 10040259 steps for small clauses
c [cce-12-1] scheduling 19233 clauses = 9329 binary + 9904 ternary
c [cce-12-1] tried to eliminate 15682 small clauses 82%
c [cce-12-1] eliminated 6 binary clauses 0%
c [cce-12-1] eliminated 89 ternary clauses 1%
c [cce-12-1] eliminated 95 small clauses 0%
c [cce-12-1] eliminated 95 small clauses in 20080544 steps
c [cce-12-1] incomplete small round (ATE)
c [cce-12-1] eliminated 160 covered clauses in round 1
c [cce-12] eliminated 160 covered clauses in TOTAL during 1 rounds
c [cce-12] 160 < 1/100 * 70265 = 702 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 11192 variables 100%
c [elim-14] limit of 160643849 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 94 variables 1% in round 1 in 16324689 steps
c [elim-14-1] backward subsumption/strengthening limit 16324600
c [elim-14-1-1] backward checking 629 touched variables 6%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 276339 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 94 = 1% variables out of 11192 scheduled
c [elim-14] 94 < 1/100 * 11192 = 111 considered unsuccessful
c [bca-14] limit of 10000000 steps and 140462 added (scaled 2)
c [bca-14] 4766 out of 22198 literals actually usable 21%
c [bca-14] added 15 blocked clauses in 99018 steps
c [sweep-9] limit 602414 penalty 3 = 3 + 0
c [sweep-9-1] 680 pos 56.1% + 532 neg 43.9% = 1212 sched 10.9% ret 9886
c [sweep-9-1] 602759 steps 14 queries 387.29 avg class size
c [sweep-9-1] 455 decisions 13 SAT calls 96.62 avg env size
c [sweep-9-1] 1165 variables remain 10% (9933 retained 90%)
c [sweep-9-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-9] removed 0 vars in TOTAL (1 rounds, 13 queries)
c [sort-queue-19] sorted 4458 enqueued variables after 148229 conflicts
c [score-dist-19] active 6640 (60%), one 4256 (38%), zero 202 (2%)
c [score-dist-19] max exp 532, different 469 (88%)
c [score-dist-19] median active exp 403, avg 375.9
c [simplification-19] removed 213 variables 1.9% (11098 remain 6%)
c [simplification-19] removed 1680 irredundant clauses 2.3% (69871 remain 13%)
c [simplification-19] maximum reduction of 2% = max (2%, 2%)
c [simplification-19] geometric conflict interval increment 22000 = 66000 / 3
c [simplification-19] new conflict interval 88000
c [simplification-19] penalized conflict interval 88000 = 1 * 88000
c [simplification-19] hard conflict limit 280229 (soft 236229 + delta 44000)
c [simplification-19] new conflict limit 236229 (hard 280229)
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   88.4   11097    69871    152373   88824  42958  9793    7    61   34  12%     60   11    8    6  129%
c i   88.4   11096    69871    152381   88830  42957  9794    7    61   34  12%     59   11    8    6  129%
c i   89.7   11095    69871    154925   91226  43049  9794    8    63   34  12%      4   12    8    6  131%
c i   91.1   11094    69871    158159   94275  43159  9801    8    60   34  13%      8    9    8    6  129%
c i   91.1   11093    69871    158199   94300  43168  9804    8    60   34  13%      7    8    7    6  116%
c i   91.3   11091    69871    158740   94809  43178  9805    8    58   34  13%     -6    7    8    6  134%
c i   91.3   11090    69871    158741   94809  43178  9805    8    58   34  13%     -6    6    8    6  133%
c i   91.8   11089    69871    159928   95936  43213  9807    8    56   34  14%    -14    5    8    6  125%
c i   92.3   11088    69871    161126   97079  43242  9812    8    58   34  13%    -16    7    8    6  128%
c i   92.8   11087    69871    162233   98101  43280  9823    8    57   34  13%    -17    6    6    6  100%
c i   93.3   11086    69871    163488   99302  43313  9824    8    58   34  13%    -16    6    8    6  118%
c i   93.3   11085    69871    163514   99321  43315  9826    8    58   34  13%    -16    6    7    6  111%
c i   94.8   11084    69871    167182  102805  43412  9833    8    63   34  12%     15   11    8    6  119%
c i   96.9   11083    69871    172089  107455  43557  9838    8    64   34  12%     34   11    8    7  119%
c i   98.5   11082    69871    176588  111757  43658  9850    8    74   34  10%     27   20    8    7  117%
c i   98.5   11081    69871    176674  111834  43662  9852    8    73   34  10%     23   20    8    7  118%
c i   98.5   11080    69871    176689  111847  43663  9852    8    73   34  10%     22   19    8    7  115%
c i   98.6   11079    69871    177002  112149  43669  9854    8    75   35  10%      9   21    7    7  112%
c i   98.6   11078    69871    177073  112195  43674  9855    7    75   35  10%      7   20    6    7   98%
c i   99.5   11076    69871    179704  114673  43738  9861    7    71   35  10%      1   16    8    7  116%
c i   99.5   11075    69871    179706  114673  43739  9861    7    71   35  10%      1   16    8    7  115%
c i  100.2   11074    69871    181168  116054  43791  9863    8    67   37  12%    -10   12    8    7  123%
c i  100.2   11071    69871    181174  116059  43791  9863    8    67   37  12%    -10   12    8    7  121%
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  100.6   11070    69871    181903  116745  43815  9867    8    65   37  12%    -16   10    8    7  116%
c i  100.9   11069    69871    182439  117249  43829  9871    8    65   37  12%    -19   10    8    7  121%
c i  100.9   11068    69871    182527  117314  43842  9873    8    64   37  12%    -19    9    7    7  101%
c i  100.9   11067    69871    182536  117316  43844  9876    8    64   37  12%    -19    9    7    7   99%
c -  100.9   11062    69871    182623   76551  43846  9876    8    65   28  12%    -20    9    8    7  116%
c i  101.2   11061    69871    183378   77277  43861  9878    8    63   31  13%    -20    7    8    7  120%
c i  101.3   11060    69871    183558   77413  43877  9884    8    61   31  13%    -20    6    6    7   90%
c i  101.3   11059    69871    183561   77414  43877  9885    8    61   31  13%    -20    6    6    7   89%
c i  101.9   11058    69871    185380   79144  43919  9888    8    65   31  12%    -10    9    8    7  111%
c i  102.4   11053    69871    187031   80714  43959  9892    8    61   31  13%    -10    5    8    7  120%
c i  102.4   11052    69871    187292   80950  43973  9892    8    63   31  12%    -13    7    7    7  107%
c i  103.1   11050    69871    189643   83203  44021  9900    8    65   32  12%     -2    8    7    7  107%
c i  103.1   11049    69871    189658   83214  44021  9901    8    65   32  12%     -3    8    7    7  104%
c i  103.4   11048    69871    190511   84015  44044  9906    8    62   32  13%    -11    6    9    7  136%
c i  103.4   11047    69871    190546   84043  44047  9908    8    62   32  13%    -12    5    9    7  127%
c i  103.4   11044    69871    190547   84043  44047  9908    8    62   32  13%    -12    5    9    7  127%
c i  103.5   11043    69871    190644   84117  44055  9914    8    61   32  13%    -13    5    8    7  111%
c i  103.5   11041    69871    191004   84453  44065  9915    8    63   32  12%    -16    7    8    7  118%
c i  103.5   11040    69871    191005   84453  44065  9915    8    63   32  12%    -16    7    8    7  118%
c i  104.1   11039    69871    192669   86034  44104  9926    8    64   32  12%    -10    8    8    7  110%
c i  104.6   11027    69871    194561   87852  44120  9926    7    57   32  13%     -6    1    8    7  114%
c i  104.6   11025    69871    194568   87857  44120  9927    7    57   32  13%     -7    1    8    7  113%
c i  104.6   11024    69871    194574   87857  44122  9929    7    57   32  13%     -7    0    8    7  111%
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  105.0   11022    69871    196137   89338  44148  9931    7    50   33  15%     -9   -7    7    7   98%
c i  105.2   11020    69871    196729   89900  44161  9934    7    53   33  14%    -13   -4    8    7  116%
c i  105.2   11019    69871    196896   90016  44183  9937    7    51   33  14%    -15   -6    6    7   86%
c i  106.5   11018    69871    201487   94368  44294  9942    7    58   33  13%     31    1    8    7  110%
c i  106.5   11015    69871    201489   94369  44294  9942    7    58   33  13%     31    1    8    7  110%
c i  106.5   11010    69871    201491   94369  44294  9943    7    58   33  13%     31    1    8    7  109%
c i  106.5   11007    69871    201492   94369  44294  9943    7    58   33  13%     31    1    7    7  109%
c i  106.5   11006    69871    201498   94374  44294  9943    7    57   33  13%     31    1    7    7  107%
c i  106.5   11005    69871    201501   94374  44295  9943    7    57   33  13%     31    1    7    7  106%
c i  107.0   11004    69870    203075   95881  44321  9948    8    69   33  11%     -1   12    8    7  115%
c i  107.0   11003    69870    203076   95881  44321  9948    8    69   33  11%     -1   12    8    7  115%
c i  107.0   11002    69870    203078   95882  44321  9948    8    69   33  11%     -1   12    8    7  114%
c i  107.8   11001    69870    205986   98670  44363  9948    8    81   33   9%      7   23    8    7  113%
c i  109.1   11000    69870    210287  102788  44451  9954    8    71   34  11%     27   12    8    7  108%
c i  109.4   10999    69870    210910  103387  44464  9955    8    69   34  12%      6    9    9    7  127%
c i  112.3   10998    69870    218582  110692  44641  9966    8    61   44  14%     76    1    9    7  122%
c i  112.3   10997    69870    218627  110732  44642  9967    8    61   44  14%     72    1    8    7  116%
c i  112.3   10996    69870    218628  110732  44642  9967    8    61   44  14%     71    1    8    7  116%
c i  113.1   10994    69870    220252  112297  44676  9970    9    60   44  14%      4    0    9    7  130%
c i  113.1   10993    69870    220341  112375  44683  9970    9    60   45  14%      2    1    9    7  129%
c i  113.1   10992    69870    220346  112379  44683  9970    9    60   45  14%      2    1    9    7  128%
c i  113.8   10991    69870    222633  114490  44727  9973    8    53   45  15%     -4   -6    9    7  118%
c i  113.8   10989    69870    222638  114491  44727  9976    8    53   45  15%     -4   -6    8    7  116%
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  114.7   10988    69870    225617  117345  44756  9980    8    55   47  15%      5   -5    8    7  116%
c i  115.5   10987    69870    228361  119963  44798  9983    8    61   47  13%      2    2   10    7  131%
c i  117.2   10985    69870    234089  125264  44898 10003    8    45   47  17%     45  -13    7    7   97%
c i  117.3   10984    69870    234290  125451  44907 10004    8    45   47  17%     32  -13    9    7  120%
c i  117.6   10983    69870    235055  126174  44924 10006    8    47   48  17%      4  -11    8    7  111%
c 
c [simplification-20] limit 236325 conflicts (hard 280229) hit after 237664 conflicts
c [quatres-16] found 38610 quaternary clauses 35% in total
c [quatres-16-1] removed 4 duplicate quaternary clauses
c [quatres-16-1] added 1 double-self-subsuming ternary resolvents
c [quatres-16-2] added 182 single-self-subsuming ternary resolvents
c [quatres-16-2] added 542 quaternary resolvents
c [ternres-16] limit 25931062 with penalty 0 = 0 + 0
c [ternres-16] all 10983 free variables schedulable
c [ternres-16] 2902 ternary resolvents (50 bin, 2852 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-59] removed 118 variables
c [simpleprobe-7] all 10980 free variables schedulable
c [simpleprobe-7] limit 103724251 penalty 0 = 0 + 0
c [decomp-60] removed 32 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 32 variables, found 3468 hbrs, 21 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 1402 transitive binary clauses
c [transred-16] found 1 units
c [bca-15] limit of 10000000 steps and 138307 added (scaled 2)
c [bca-15] 3783 out of 21894 literals actually usable 17%
c [bca-15] added 1 blocked clauses in 138158 steps
c [sort-queue-20] sorted 3998 enqueued variables after 237664 conflicts
c [score-dist-20] active 6948 (63%), one 3922 (36%), zero 76 (1%)
c [score-dist-20] max exp 949, different 671 (71%)
c [score-dist-20] median active exp 813, avg 705.2
c [simplification-20] removed 37 variables 0.3% (10946 remain 6%)
c [simplification-20] removed 1080 irredundant clauses 1.5% (68790 remain 13%)
c [simplification-20] maximum reduction of 2% = max (0%, 2%)
c [simplification-20] geometric conflict interval increment 29333 = 88000 / 3
c [simplification-20] new conflict interval 117333
c [simplification-20] penalized conflict interval 117333 = 1 * 117333
c [simplification-20] hard conflict limit 413663 (soft 354997 + delta 58666)
c [simplification-20] new conflict limit 354997 (hard 413663)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  119.6   10945    68790    238108  127619  47081 11887    8    72   43  11%      6   13    9    7  118%
c i  119.6   10944    68790    238162  127666  47082 11890    8    71   43  11%      4   13    8    7  109%
c i  120.2   10935    68790    239306  128754  47113 11896    8    69   43  12%    -11   10    8    7  110%
c i  120.2   10920    68790    239315  128750  47115 11897    8    69   43  12%    -11   10    8    7  107%
c i  120.2   10919    68790    239316  128750  47115 11897    8    69   43  12%    -11   10    8    7  107%
c i  120.3   10918    68790    239533  128955  47120 11898    8    67   43  12%    -14    9    8    7  107%
c i  120.3   10917    68790    239740  129126  47133 11901    8    65   43  12%    -16    6    7    7   92%
c -  121.4   10917    68790    241920   95349  47185 11901    8    59   31  14%     -6    0    9    7  115%
c i  121.7   10916    68790    242994   96375  47205 11902    8    60   35  14%      8    1    8    7  105%
c i  123.4   10911    68790    248828  101976  47311 11910    8    72   35  12%     47   12    9    8  114%
c i  124.9   10910    68790    254197  107100  47429 11916    8    58   36  14%     38   -2    8    8  112%
c i  125.1   10909    68790    254859  107737  47439 11917    8    58   36  14%      8   -2    9    8  116%
c i  125.1   10908    68790    254860  107737  47439 11917    8    58   36  14%      8   -2    9    8  115%
c i  125.1   10907    68790    254905  107757  47445 11921    8    58   36  14%      7   -2    8    8  105%
c i  125.1   10906    68790    254939  107780  47447 11923    8    58   36  14%      5   -3    7    8   96%
c i  126.2   10905    68790    258201  110878  47535 11927    8    63   36  13%      7    3    9    8  112%
c i  126.3   10904    68790    258584  111228  47546 11930    8    65   36  13%     -3    4    8    8  103%
c i  126.8   10903    68790    260063  112621  47581 11935    9    62   36  14%    -13    1    9    8  116%
c i  126.8   10902    68790    260064  112621  47581 11935    9    62   36  14%    -13    1    9    8  115%
c i  126.9   10901    68790    260093  112635  47589 11937    9    62   36  14%    -13    1    9    8  112%
c i  126.9   10900    68790    260139  112674  47590 11939    9    61   36  14%    -14    1    9    8  112%
c i  126.9   10899    68790    260149  112677  47590 11944    9    61   36  14%    -14    0    8    8  109%
c i  127.0   10897    68790    260465  112978  47598 11944    9    63   36  14%    -17    2    9    8  122%
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  127.4   10896    68790    261408  113870  47623 11949    9    61   36  14%    -19    0    8    8  100%
c i  128.8   10891    68790    266809  118987  47754 11959    8    75   38  11%     39   13    8    8  107%
c i  130.0   10890    68790    270830  122781  47845 11962    8    75   39  11%     19   13    9    8  120%
c i  130.9   10889    68790    273560  125422  47876 11965    8    65   39  13%      1    3    9    8  115%
c i  130.9   10888    68790    273564  125422  47879 11965    8    65   39  13%      1    3    9    8  113%
c i  134.3   10887    68789    286571  137504  48105 12002    7    58   39  13%    146   -2    5    8   67%
c -  136.6   10877    68789    292103  109072  48195 12013    8    52   32  16%     28   -8    9    8  117%
c i  138.3   10876    68789    298188  114735  48327 12023    9    55   37  16%    116   -4    8    8  107%
c i  144.0   10875    68789    317165  132789  48655 12058    8    51   38  17%    206   -7    7    8   93%
c i  144.1   10871    68789    317530  133143  48655 12058    9    53   38  16%    122   -5    9    8  115%
c i  144.1   10868    68789    317564  133170  48656 12060    9    53   38  16%    115   -5    9    8  113%
c i  145.9   10865    68789    323374  138620  48789 12070    8    56   41  14%      1   -2    4    8   53%
c i  146.5   10862    68789    325986  141115  48799 12072    8    35   41  22%    -41  -22    6    8   73%
c i  147.9   10856    68789    331502  146303  48881 12084    8    55   41  14%      0   -1    6    8   71%
c i  149.0   10855    68789    335984  150473  48993 12099    7    56   41  13%    -13   -1    9    8  120%
c i  149.0   10853    68789    335997  150485  48993 12099    7    56   41  13%    -14   -1    9    8  118%
c i  149.0   10852    68789    336034  150501  49000 12101    7    55   41  13%    -15   -1    9    8  110%
c i  149.1   10847    68789    336614  151058  49008 12102    8    55   41  14%    -36   -2    9    8  117%
c i  149.2   10838    68789    336619  151061  49009 12102    8    55   41  14%    -36   -2    9    8  116%
c i  149.2   10832    68786    336628  151063  49012 12103    8    55   41  14%    -36   -2    9    8  113%
c i  149.7   10825    68786    338669  153005  49041 12104    8    57   41  14%    -44    0    9    8  118%
c i  149.7   10824    68786    338676  153011  49041 12104    8    57   41  14%    -44    0    9    8  117%
c i  149.7   10822    68786    338700  153028  49044 12106    8    57   41  14%    -45    0    9    8  110%
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 -  149.9   10821    68786    338907  120029  49045 12107    8    57   32  14%    -48    0   10    8  127%
c i  151.1   10820    68786    344001  124771  49133 12120    7    43   37  16%      3  -13    5    8   58%
c 
c [simplification-21] limit 355035 conflicts (hard 413663) hit after 355035 conflicts
c [quatres-17] found 41513 quaternary clauses 32% in total
c [quatres-17-1] removed 7 duplicate quaternary clauses
c [quatres-17-1] added 2 double-self-subsuming ternary resolvents
c [quatres-17-2] added 251 single-self-subsuming ternary resolvents
c [quatres-17-2] added 456 quaternary resolvents
c [ternres-17] limit 37502815 with penalty 0 = 0 + 0
c [ternres-17] all 10820 free variables schedulable
c [ternres-17] 2472 ternary resolvents (43 bin, 2429 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 1171962 penalty 4 = 4 + 0
c [card-6] found 330 at-most-one constraints of average size 3.1
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1171962 for elimination
c [card-6] 330 out of 330 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-61] removed 133 variables
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 829 transitive binary clauses
c [transred-17] found 3 units
c [bca-16] limit of 10000000 steps and 136310 added (scaled 2)
c [bca-16] 3445 out of 21622 literals actually usable 16%
c [bca-16] added 11 blocked clauses in 142527 steps
c [sort-queue-21] sorted 4884 enqueued variables after 355035 conflicts
c [score-dist-21] active 5926 (55%), one 4831 (45%), zero 53 (0%)
c [score-dist-21] max exp 678, different 494 (73%)
c [score-dist-21] median active exp 338, avg 397.1
c [simplification-21] removed 10 variables 0.1% (10810 remain 6%)
c [simplification-21] removed 995 irredundant clauses 1.4% (67791 remain 12%)
c [simplification-21] maximum reduction of 1% = max (0%, 1%)
c [simplification-21] geometric conflict interval increment 58666 = 117333 / 2
c [simplification-21] new conflict interval 175999
c [simplification-21] penalized conflict interval 175999 = 1 * 175999
c [simplification-21] hard conflict limit 619033 (soft 531034 + delta 87999)
c [simplification-21] new conflict limit 531034 (hard 619033)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  156.2   10809    67791    358477  135956  50578 11109    8    47   40  16%    138   -8    5    8   61%
c i  156.5   10808    67791    359698  137073  50604 11113    7    40   40  17%     -1  -15    5    8   62%
c i  161.6   10807    67791    372010  148816  50791 11135    8    52   41  16%    100   -3    5    8   61%
c i  163.0   10806    67791    376092  152695  50845 11139    8    56   41  15%    -24    1    8    8   98%
c -  165.8   10806    67791    385292  127029  50972 11143    8    77   33  11%     54   22    9    8  117%
c i  170.0   10805    67791    399927  141107  51141 11153    8    59   39  14%    248    3    9    8  114%
c i  171.6   10804    67791    404519  145464  51220 11165    9    55   40  16%    -48   -1    9    8  113%
c i  171.6   10803    67791    404522  145463  51223 11165    9    55   40  16%    -48   -1    9    8  112%
c i  173.9   10802    67790    411241  151866  51316 11180    8    53   41  16%    -13   -3    5    8   63%
c i  173.9   10801    67790    411242  151866  51316 11180    8    53   41  16%    -13   -3    5    8   63%
c i  174.3   10800    67790    412386  152958  51332 11182    9    59   41  15%    -65    3    9    8  112%
c i  174.3   10799    67790    412389  152959  51333 11182    9    59   41  15%    -65    3    9    8  111%
c -  180.6   10795    67790    430166  134857  51619 11208    9    64   33  14%    153    7    9    8  107%
c i  182.4   10794    67790    435416  139910  51695 11211    9    67   39  14%    220   10   11    8  126%
c i  184.3   10781    67790    441153  145426  51753 11213    9    57   40  15%    -46   -2   10    8  121%
c i  184.3   10780    67790    441216  145460  51762 11219    9    56   40  16%    -50   -2    9    8  109%
c i  184.3   10779    67790    441221  145460  51764 11220    9    56   40  16%    -51   -2    9    8  107%
c i  184.3   10778    67790    441222  145460  51764 11220    9    56   40  16%    -51   -2    9    8  107%
c i  186.3   10777    67790    447836  151850  51809 11220    9    59   40  15%    -26    1   10    8  116%
c i  186.7   10776    67790    448570  152566  51819 11220    9    62   40  15%    -67    4   10    8  122%
c i  188.2   10775    67789    453411  157238  51854 11223    9    71   43  13%    -48   12    9    9  110%
c -  194.7   10772    67789    473534  141952  51987 11236    9    42   46  21%    179  -16    9    9  106%
c i  195.1   10771    67789    475032  143366  51996 11240    8    39   52  22%    198  -19    7    9   87%
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  203.5   10770    67789    501885  169264  52247 11251    9    44   57  21%    248  -12   10    9  116%
c i  205.7   10769    67788    508867  175947  52353 11263    9    49   58  18%    -56   -6   10    9  114%
c i  207.6   10768    67788    513707  180586  52418 11265   10    60   58  16%    -82    5   11    9  121%
c -  208.8   10768    67788    516352  147921  52443 11266   10    56   47  17%   -107    1    9    9  100%
c i  212.7   10767    67788    529262  160293  52542 11272    9    81   54  11%     90   26    7    9   75%
c i  212.7   10765    67788    529288  160311  52543 11272    9    81   54  11%     85   25    6    9   72%
c i  213.9   10764    67788    533472  164371  52571 11273    9    81   54  12%    -79   25   10    9  117%
c i  215.7   10763    67788    539018  169660  52602 11276    9    50   57  18%    -54   -8    8    9   91%
c i  216.3   10762    67788    540566  171159  52617 11276    9    53   57  17%    -96   -4   11    9  118%
c i  217.1   10761    67788    542812  173327  52647 11276    9    52   57  18%    -96   -5   10    9  115%
c 
c [simplification-22] limit 531062 conflicts (hard 619033) hit after 553985 conflicts
c [quatres-18] found 45594 quaternary clauses 29% in total
c [quatres-18-1] removed 7 duplicate quaternary clauses
c [quatres-18-1] added 2 double-self-subsuming ternary resolvents
c [quatres-18-2] added 249 single-self-subsuming ternary resolvents
c [quatres-18-2] added 419 quaternary resolvents
c [ternres-18] limit 59381887 with penalty 0 = 0 + 0
c [ternres-18] all 10761 free variables schedulable
c [ternres-18] 2363 ternary resolvents (39 bin, 2324 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-62] removed 53 variables
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 555 transitive binary clauses
c [transred-18] found 3 units
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 10754 variables 100%
c [elim-15] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 229 variables 2% in round 1 in 15172599 steps
c [elim-15-1] backward subsumption/strengthening limit 15172500
c [elim-15-1-1] backward checking 1325 touched variables 12%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 9 clauses in 548012 steps
c [elim-15-1] rescheduled 46 variables 0% by backward subsumption
c [elim-15-2] eliminated 7 variables 0% in round 2 in 199328 steps
c [elim-15-2] backward subsumption/strengthening limit 199300
c [elim-15-2-1] backward checking 28 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 1 clauses in 56603 steps
c [elim-15-2] rescheduled 6 variables 0% by backward subsumption
c [elim-15-3] no variable eliminated in round 3 in 39465 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 236 = 2% variables out of 10754 scheduled
c [bca-17] limit of 10000000 steps and 133669 added (scaled 2)
c [bca-17] 3035 out of 21038 literals actually usable 14%
c [bca-17] added 13 blocked clauses in 189660 steps
c [sort-queue-22] sorted 3904 enqueued variables after 553985 conflicts
c [score-dist-22] active 6614 (63%), one 3866 (37%), zero 38 (0%)
c [score-dist-22] max exp 798, different 618 (77%)
c [score-dist-22] median active exp 705, avg 587.3
c [simplification-22] removed 243 variables 2.3% (10518 remain 6%)
c [simplification-22] removed 1320 irredundant clauses 1.9% (66468 remain 12%)
c [simplification-22] maximum reduction of 2% = max (2%, 2%)
c [simplification-22] geometric conflict interval increment 58666 = 175999 / 3
c [simplification-22] new conflict interval 234665
c [simplification-22] penalized conflict interval 234665 = 1 * 234665
c [simplification-22] hard conflict limit 905982 (soft 788650 + delta 117332)
c [simplification-22] new conflict limit 788650 (hard 905982)
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 -  224.0   10518    66468    560971  152865  54014 10599    9    66   36  14%    144   10    9    9  100%
c i  230.7   10517    66468    581954  173088  54190 10609    9    72   45  13%    385   14   10    9  108%
c i  233.6   10514    66468    590680  181507  54277 10609   10    65   47  15%    -79    6   11    9  119%
c i  233.6   10510    66468    590713  181526  54279 10616   10    64   47  15%    -82    5   10    9  108%
c i  233.6   10505    66468    590714  181526  54279 10616   10    64   47  15%    -83    5   10    9  107%
c -  238.3   10500    66468    604190  158813  54377 10621    9    67   37  14%     13    7   11    9  115%
c -  254.0   10500    66468    647483  163686  54770 10635   10    60   37  17%    502   -0   11    9  115%
c -  269.3   10500    66468    691230  169372  55037 10648   10    46   37  21%    756  -14   10   10  103%
c i  274.7   10499    66468    708376  185895  55138 10658    9    70   46  13%    818   11    4   10   42%
c -  285.2   10499    66468    736958  176312  55335 10667    9    64   52  15%   -317    4    9    9   99%
c -  302.4   10499    66468    782013  182147  55554 10681    9    58   53  16%    350   -1   11    9  115%
c 
c [simplification-23] limit 788660 conflicts (hard 905982) hit after 788662 conflicts
c [quatres-19] found 48319 quaternary clauses 26% in total
c [quatres-19-1] removed 15 duplicate quaternary clauses
c [quatres-19-1] added 5 double-self-subsuming ternary resolvents
c [quatres-19-2] added 214 single-self-subsuming ternary resolvents
c [quatres-19-2] added 430 quaternary resolvents
c [ternres-19] limit 87474669 with penalty 0 = 0 + 0
c [ternres-19] all 10499 free variables schedulable
c [ternres-19] 2592 ternary resolvents (36 bin, 2556 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-63] removed 22 variables
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 363 transitive binary clauses
c [transred-19] found 2 units
c [cce-13] boosting limit by 10
c [cce-13] limit of 546716686 steps penalty 3 = 3 + 0
c [cce-13-1] eliminated 7 clauses out of 233 (3%) of length 9
c [cce-13-1] eliminated 14 clauses out of 563 (2%) of length 8
c [cce-13-1] eliminated 26 clauses out of 2105 (1%) of length 7
c [cce-13-1] eliminated 81 clauses out of 3827 (2%) of length 6
c [cce-13-1] eliminated 249 clauses out of 7107 (4%) of length 5
c [cce-13-1] eliminated 3023 clauses out of 18162 (17%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 3400 large clauses in 45919359 steps
c [cce-13-1] allowing another 22959679 steps for small clauses
c [cce-13-1] scheduling 18581 clauses = 9111 binary + 9470 ternary
c [cce-13-1] tried to eliminate 18581 small clauses 100%
c [cce-13-1] eliminated 238 binary clauses 3%
c [cce-13-1] eliminated 841 ternary clauses 9%
c [cce-13-1] eliminated 1079 small clauses 6%
c [cce-13-1] eliminated 1093 small clauses in 37126092 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] completed small and large (ACCE)
c [cce-13-1] eliminated 4493 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 226 (0%) of length 9
c [cce-13-2] eliminated 2 clauses out of 2079 (0%) of length 7
c [cce-13-2] eliminated 8 clauses out of 3746 (0%) of length 6
c [cce-13-2] eliminated 34 clauses out of 6858 (0%) of length 5
c [cce-13-2] eliminated 28 clauses out of 15139 (0%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 73 large clauses in 39516040 steps
c [cce-13-2] allowing another 19758020 steps for small clauses
c [cce-13-2] scheduling 17502 clauses = 8873 binary + 8629 ternary
c [cce-13-2] tried to eliminate 17502 small clauses 100%
c [cce-13-2] eliminated 18 binary clauses 0%
c [cce-13-2] eliminated 36 ternary clauses 0%
c [cce-13-2] eliminated 54 small clauses 0%
c [cce-13-2] eliminated 54 small clauses in 32911989 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 127 covered clauses in round 2
c [cce-13-3] eliminated 1 clauses out of 549 (0%) of length 8
c [cce-13-3] eliminated 3 clauses out of 2077 (0%) of length 7
c [cce-13-3] eliminated 3 clauses out of 3738 (0%) of length 6
c [cce-13-3] eliminated 3 clauses out of 6824 (0%) of length 5
c [cce-13-3] eliminated 5 clauses out of 15111 (0%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 15 large clauses in 39313683 steps
c [cce-13-3] allowing another 19656841 steps for small clauses
c [cce-13-3] scheduling 17448 clauses = 8855 binary + 8593 ternary
c [cce-13-3] tried to eliminate 17448 small clauses 100%
c [cce-13-3] eliminated 4 binary clauses 0%
c [cce-13-3] eliminated 4 small clauses 0%
c [cce-13-3] eliminated 4 small clauses in 32778541 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 19 covered clauses in round 3
c [cce-13] eliminated 4639 covered clauses in TOTAL during 3 rounds
c [bca-18] limit of 10000000 steps and 124060 added (scaled 2)
c [bca-18] 2967 out of 20990 literals actually usable 14%
c [bca-18] added 20 blocked clauses in 196671 steps
c [sort-queue-23] sorted 4015 enqueued variables after 788662 conflicts
c [score-dist-23] active 6479 (62%), one 3978 (38%), zero 37 (0%)
c [score-dist-23] max exp 810, different 567 (70%)
c [score-dist-23] median active exp 551, avg 574.5
c [simplification-23] removed 5 variables 0.0% (10494 remain 6%)
c [simplification-23] removed 4808 irredundant clauses 7.2% (61660 remain 11%)
c [simplification-23] maximum reduction of 7% = max (0%, 7%)
c [simplification-23] large reduction 7% >= 5% limit
c [simplification-23] next conflict interval 7886 = min (788662/100, 234665)
c [simplification-23] penalized conflict interval 7886 = 1 * 7886
c [simplification-23] hard conflict limit 806548 (soft 796548 + delta 10000)
c [simplification-23] new conflict limit 796548 (hard 806548)
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  313.3   10493    61660    802199  201376  59018 10658    8    42   48  20%    529  -16   11    9  119%
c 
c [simplification-24] limit 796548 conflicts (hard 806548) hit after 806549 conflicts
c [quatres-20] found 45741 quaternary clauses 25% in total
c [quatres-20-1] removed 1 duplicate quaternary clauses
c [quatres-20-1] added 2 double-self-subsuming ternary resolvents
c [quatres-20-2] added 71 single-self-subsuming ternary resolvents
c [quatres-20-2] added 124 quaternary resolvents
c [ternres-20] limit 89773464 with penalty 0 = 0 + 0
c [ternres-20] all 10492 free variables schedulable
c [ternres-20] 627 ternary resolvents (36 bin, 591 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-64] removed 3 variables
c [treelook-7] limit 1122168 penalty 3 = 3 + 0 boost 1
c [treelook-7] scheduled 12197 literals 58%
c [treelook-7] scheduling used 762007 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 1122168 penalty 3 = 3 + 0 boost 1
c [treelook-7] used 1122338 steps
c [treelook-7] 11653 literals remain 56%
c [treelook-7] 3923 variables remain to probed next time 37%
c [decomp-65] removed 2 variables
c [treelook-7] removed 6 variables, found 1629 hbrs
c [unhide-14] limit 1122168 with penalty 4 = 4 + 0
c [unhide-14-14] 0 units, 4 failed, 6167 tauts, 0 hbrs, 127259 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 451 transitive binary clauses
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 10481 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 696 variables 7% in round 1 in 14071780 steps
c [elim-16-1] backward subsumption/strengthening limit 14071700
c [elim-16-1-1] backward checking 3395 touched variables 32%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 4 and strengthened 14 clauses in 934324 steps
c [elim-16-1] rescheduled 80 variables 1% by backward subsumption
c [elim-16-2] eliminated 1 variables 0% in round 2 in 191253 steps
c [elim-16-2] backward subsumption/strengthening limit 191200
c [elim-16-2-1] backward checking 9 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 0 and strengthened 1 clauses in 64718 steps
c [elim-16-2] rescheduled 5 variables 0% by backward subsumption
c [elim-16-3] no variable eliminated in round 3 in 6428 steps
c [elim-16] fully completed in 3 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 697 = 7% variables out of 10481 scheduled
c [bca-19] limit of 10000000 steps and 121674 added (scaled 2)
c [bca-19] 2466 out of 19570 literals actually usable 13%
c [bca-19] added 20 blocked clauses in 204295 steps
c [sweep-10] limit 1683252 penalty 4 = 4 + 0
c [sweep-10-1] 595 pos 62.7% + 354 neg 37.3% = 949 sched 9.7% ret 8835
c [sweep-10-1] 1896183 steps 22 queries 181.59 avg class size
c [sweep-10-1] 1091 decisions 21 SAT calls 130.38 avg env size
c [sweep-10-1] 779 variables remain 8% (9004 retained 92%)
c [decomp-66] removed 4 variables
c [sweep-10-1] removed 4 vars (0 failed, 0 eqs, 0 impls)
c [sweep-10] 4 < 1/1000 * 9784 = 9 considered unsuccessful
c [sweep-10] removed 4 vars in TOTAL (1 rounds, 21 queries)
c [sort-queue-24] sorted 5039 enqueued variables after 806549 conflicts
c [score-dist-24] active 4741 (48%), one 5012 (51%), zero 27 (0%)
c [score-dist-24] max exp 518, different 341 (66%)
c [score-dist-24] median active exp 461, avg 350.1
c [simplification-24] removed 712 variables 6.8% (9780 remain 5%)
c [simplification-24] removed 1213 irredundant clauses 2.0% (60447 remain 11%)
c [simplification-24] maximum reduction of 7% = max (7%, 2%)
c [simplification-24] large reduction 7% >= 5% limit
c [simplification-24] next conflict interval 8065 = min (806549/100, 234665)
c [simplification-24] penalized conflict interval 8065 = 1 * 8065
c [simplification-24] hard conflict limit 824614 (soft 814614 + delta 10000)
c [simplification-24] new conflict limit 814614 (hard 824614)
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  321.3    9779    60447    817582  207990  52316 10069   10    60   50  16%   -545    2   11   10  111%
c 
c [simplification-25] limit 814614 conflicts (hard 824614) hit after 824614 conflicts
c [quatres-21] found 45023 quaternary clauses 25% in total
c [quatres-21-1] removed 45 duplicate quaternary clauses
c [quatres-21-2] added 168 single-self-subsuming ternary resolvents
c [quatres-21-2] added 441 quaternary resolvents
c [ternres-21] limit 91937876 with penalty 0 = 0 + 0
c [ternres-21] all 9779 free variables schedulable
c [ternres-21] 2842 ternary resolvents (28 bin, 2814 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-6] limit 1149223 penalty 4 = 4 + 0
c [gauss-6] extracted 306 xors of average arity 3.0
c [gauss-6] connected 918 occurrences of 251 variables (average 3.7)
c [gauss-6] limit 1149223 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 4311 sched 44%, 58 failed, 4 lifted, 2845 hbrs
c [decomp-68] removed 70 variables
c [basicprobe-7-1] 4195 sched 43%, 15 failed, 0 lifted, 883 hbrs
c [decomp-69] removed 27 variables
c [basicprobe-7-2] 4177 sched 43%, 5 failed, 1 lifted, 193 hbrs
c [decomp-70] removed 5 variables
c [basicprobe-7-3] 4182 sched 43%, 3 failed, 0 lifted, 63 hbrs
c [decomp-71] removed 3 variables
c [basicprobe-7-4] 4182 sched 43%, 3 failed, 0 lifted, 32 hbrs
c [decomp-72] removed 3 variables
c [basicprobe-7-5] 4182 sched 43%, 3 failed, 1 lifted, 32 hbrs
c [decomp-73] removed 3 variables
c [basicprobe-7-6] 4179 sched 43%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-7-7] 4180 sched 43%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-7-8] 4180 sched 43%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-7-8] round limit 8 hit
c [basicprobe-7-8] 93 units = 87 failed (94%) + 6 lifted (6%)
c [basicprobe-7-8] removed 111 variables, found 4058 hbrs
c [bate-5] eliminated 41 asymmetric tautologies during probing
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 677 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 9668 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 8 blocked clauses
c [block-6] 8 < 1/100 * 59688 = 596 considered unsuccessful
c [cce-14] limit of 114922345 steps penalty 2 = 2 + 0
c [cce-14-1] eliminated 12 clauses out of 225 (5%) of length 9
c [cce-14-1] eliminated 48 clauses out of 612 (8%) of length 8
c [cce-14-1] eliminated 59 clauses out of 2286 (3%) of length 7
c [cce-14-1] eliminated 100 clauses out of 3967 (3%) of length 6
c [cce-14-1] eliminated 151 clauses out of 6868 (2%) of length 5
c [cce-14-1] eliminated 263 clauses out of 14351 (2%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 633 large clauses in 33231057 steps
c [cce-14-1] allowing another 16615528 steps for small clauses
c [cce-14-1] scheduling 16469 clauses = 8403 binary + 8066 ternary
c [cce-14-1] tried to eliminate 16469 small clauses 100%
c [cce-14-1] eliminated 4 binary clauses 0%
c [cce-14-1] eliminated 76 ternary clauses 1%
c [cce-14-1] eliminated 80 small clauses 0%
c [cce-14-1] eliminated 80 small clauses in 25849489 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 713 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 16336841 steps for small clauses
c [cce-14-2] scheduling 16389 clauses = 8399 binary + 7990 ternary
c [cce-14-2] tried to eliminate 16389 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 713 covered clauses in TOTAL during 2 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 9666 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 97 variables 1% in round 1 in 13020763 steps
c [elim-17-1] backward subsumption/strengthening limit 13020700
c [elim-17-1-1] backward checking 1053 touched variables 11%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 9 clauses in 371132 steps
c [elim-17-1] rescheduled 33 variables 0% by backward subsumption
c [elim-17-2] eliminated 2 variables 0% in round 2 in 64234 steps
c [elim-17-2] backward subsumption/strengthening limit 64200
c [elim-17-2-1] backward checking 17 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 0 and strengthened 0 clauses in 39769 steps
c [elim-17] fully completed in 2 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 99 = 1% variables out of 9666 scheduled
c [bca-20] limit of 10000000 steps and 118400 added (scaled 2)
c [bca-20] 2320 out of 19136 literals actually usable 12%
c [bca-20] added 2 blocked clauses in 218518 steps
c [sort-queue-25] sorted 2996 enqueued variables after 824614 conflicts
c [score-dist-25] active 6571 (69%), one 2969 (31%), zero 27 (0%)
c [score-dist-25] max exp 754, different 578 (77%)
c [score-dist-25] median active exp 627, avg 541.0
c [simplification-25] removed 212 variables 2.2% (9567 remain 5%)
c [simplification-25] removed 1627 irredundant clauses 2.7% (58820 remain 11%)
c [simplification-25] maximum reduction of 3% = max (2%, 3%)
c [simplification-25] geometric conflict interval increment 58666 = 234665 / 4
c [simplification-25] new conflict interval 293331
c [simplification-25] penalized conflict interval 293331 = 1 * 293331
c [simplification-25] hard conflict limit 1264610 (soft 1117945 + delta 146665)
c [simplification-25] new conflict limit 1117945 (hard 1264610)
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 -  332.6    9567    58820    829739  178550  53198 11597   10    59   38  17%   -483    0   10   10  108%
c -  348.3    9567    58820    875781  185191  53387 11603    9    68   39  14%    278   21   10    9  110%
c -  364.9    9567    58820    920345  188358  53733 11613    9    56   39  17%    646    1    9   10   96%
c i  368.6    9566    58820    930735  198301  53779 11618    9    56   47  17%    701    0   10    9  101%
c -  384.2    9566    58820    968982  194528  53992 11623   10    58   55  18%   -158    4   11   10  116%
c -  403.3    9566    58820   1017395  200707  54253 11626    9    51   55  18%    459   -0   11   10  117%
c i  406.3    9565    58820   1025818  208844  54294 11631   10    55   64  18%    527    4   11   10  112%
c i  406.3    9564    58820   1025823  208844  54294 11633   10    55   64  18%    520    4   11   10  111%
c i  406.3    9563    58820   1025825  208845  54293 11634   10    55   64  18%    517    4   11   10  110%
c i  418.7    9561    58820   1059516  241225  54459 11649    8    47   69  17%   -176   -1    5    9   54%
c -  422.2    9561    58820   1067061  207872  54511 11652    9    47   56  18%   -521   -1    8    9   88%
c -  442.9    9561    58820   1116169  212817  54783 11661    9    45   56  20%    293   -1   11    9  117%
c 
c [simplification-26] limit 1117952 conflicts (hard 1264610) hit after 1117952 conflicts
c [quatres-22] found 47198 quaternary clauses 23% in total
c [quatres-22-1] removed 6 duplicate quaternary clauses
c [quatres-22-1] added 1 double-self-subsuming ternary resolvents
c [quatres-22-2] added 190 single-self-subsuming ternary resolvents
c [quatres-22-2] added 482 quaternary resolvents
c [ternres-22] limit 131049201 with penalty 0 = 0 + 0
c [ternres-22] all 9561 free variables schedulable
c [ternres-22] 2338 ternary resolvents (29 bin, 2309 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-76] removed 9 variables
c [simpleprobe-8] all 9558 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-77] removed 6 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 6 variables, found 3910 hbrs, 4 units
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 1616 transitive binary clauses
c [cce-15] limit of 327623003 steps penalty 1 = 1 + 0
c [cce-15-1] eliminated 3 clauses out of 236 (1%) of length 9
c [cce-15-1] eliminated 10 clauses out of 568 (2%) of length 8
c [cce-15-1] eliminated 22 clauses out of 2235 (1%) of length 7
c [cce-15-1] eliminated 144 clauses out of 3902 (4%) of length 6
c [cce-15-1] eliminated 274 clauses out of 6733 (4%) of length 5
c [cce-15-1] eliminated 269 clauses out of 14032 (2%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 722 large clauses in 37272612 steps
c [cce-15-1] allowing another 18636306 steps for small clauses
c [cce-15-1] scheduling 16226 clauses = 8382 binary + 7844 ternary
c [cce-15-1] tried to eliminate 16226 small clauses 100%
c [cce-15-1] eliminated 59 binary clauses 1%
c [cce-15-1] eliminated 89 ternary clauses 1%
c [cce-15-1] eliminated 148 small clauses 1%
c [cce-15-1] eliminated 148 small clauses in 30036016 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 870 covered clauses in round 1
c [cce-15-2] eliminated 6 clauses out of 6459 (0%) of length 5
c [cce-15-2] eliminated 11 clauses out of 13763 (0%) of length 4
c [cce-15-2] completed large round (ACCE)
c [cce-15-2] eliminated 17 large clauses in 36034006 steps
c [cce-15-2] allowing another 18017003 steps for small clauses
c [cce-15-2] scheduling 16078 clauses = 8323 binary + 7755 ternary
c [cce-15-2] tried to eliminate 16078 small clauses 100%
c [cce-15-2] eliminated 1 binary clauses 0%
c [cce-15-2] eliminated 2 ternary clauses 0%
c [cce-15-2] eliminated 3 small clauses 0%
c [cce-15-2] eliminated 3 small clauses in 29290648 steps
c [cce-15-2] completed small round (ACCE)
c [cce-15-2] eliminated 20 covered clauses in round 2
c [cce-15-3] eliminated 1 clauses out of 558 (0%) of length 8
c [cce-15-3] eliminated 2 clauses out of 2213 (0%) of length 7
c [cce-15-3] eliminated 1 clauses out of 3758 (0%) of length 6
c [cce-15-3] eliminated 3 clauses out of 6453 (0%) of length 5
c [cce-15-3] eliminated 6 clauses out of 13752 (0%) of length 4
c [cce-15-3] completed large round (ACCE)
c [cce-15-3] eliminated 13 large clauses in 35999266 steps
c [cce-15-3] allowing another 17999633 steps for small clauses
c [cce-15-3] scheduling 16075 clauses = 8322 binary + 7753 ternary
c [cce-15-3] tried to eliminate 16075 small clauses 100%
c [cce-15-3] eliminated 2 binary clauses 0%
c [cce-15-3] eliminated 1 ternary clauses 0%
c [cce-15-3] eliminated 3 small clauses 0%
c [cce-15-3] eliminated 3 small clauses in 29267328 steps
c [cce-15-3] completed small round (ACCE)
c [cce-15-3] eliminated 16 covered clauses in round 3
c [cce-15] eliminated 906 covered clauses in TOTAL during 3 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 9552 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 69 variables 1% in round 1 in 12582585 steps
c [elim-18-1] backward subsumption/strengthening limit 12582500
c [elim-18-1-1] backward checking 627 touched variables 7%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 1 and strengthened 2 clauses in 197627 steps
c [elim-18-1] rescheduled 13 variables 0% by backward subsumption
c [elim-18-2] no variable eliminated in round 2 in 25374 steps
c [elim-18] fully completed in 2 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 69 = 1% variables out of 9552 scheduled
c [elim-18] 69 < 1/100 * 9552 = 95 considered unsuccessful
c [bca-21] limit of 10000000 steps and 116227 added (scaled 2)
c [bca-21] 2252 out of 18968 literals actually usable 12%
c [bca-21] added 8 blocked clauses in 218387 steps
c [sort-queue-26] sorted 3303 enqueued variables after 1117952 conflicts
c [score-dist-26] active 6180 (65%), one 3281 (35%), zero 22 (0%)
c [score-dist-26] max exp 685, different 549 (80%)
c [score-dist-26] median active exp 591, avg 491.8
c [simplification-26] removed 78 variables 0.8% (9483 remain 5%)
c [simplification-26] removed 1087 irredundant clauses 1.8% (57733 remain 11%)
c [simplification-26] maximum reduction of 2% = max (1%, 2%)
c [simplification-26] geometric conflict interval increment 97777 = 293331 / 3
c [simplification-26] new conflict interval 391108
c [simplification-26] penalized conflict interval 391108 = 1 * 391108
c [simplification-26] hard conflict limit 1704614 (soft 1509060 + delta 195554)
c [simplification-26] new conflict limit 1509060 (hard 1704614)
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  461.4    9482    57733   1151959  244568  56728 13772    7    13   54  56%    601  -32    5    9   55%
c -  468.2    9473    57733   1168513  218013  56791 13779    9    48   40  19%   -444    4   11    9  118%
c i  471.7    9472    57733   1177514  226628  56829 13782    8    46   49  17%   -256    1    7    9   81%
c i  473.0    9471    57733   1180953  229871  56859 13787    8    43   50  19%   -561   -2    7    9   75%
c -  491.9    9468    57733   1223295  227038  57180 13794    9    45   57  19%    157   -2   10    9  113%
c -  516.6    9468    57733   1276142  233821  57394 13826    9    43   57  20%    637   -1    8    9   93%
c -  541.7    9468    57733   1328170  239341  57580 13845    9    42   57  22%    849   -3    9    9  103%
c i  554.2    9467    57733   1354613  264943  57686 13864    9    33   71  28%    907   -9   10    9  115%
c i  564.0    9466    57733   1374112  283830  57735 13872    9    26   74  35%  -1110  -13    9    9   99%
c -  567.2    9460    57733   1380480  245388  57748 13872    9    23   58  41%  -1193  -15    9    9  107%
c i  583.2    9459    57733   1412173  275809  57794 13881   10    24   74  41%   -343   -9   10    9  111%
c i  583.7    9458    57733   1413427  277009  57796 13882   10    23   74  42%   -732  -10    9    9  105%
c i  585.1    9457    57733   1415987  279359  57811 13893    9    20   74  46%   -839  -12    7    9   73%
c i  585.9    9431    57733   1417500  280725  57829 13899    9    19   74  48%   -839  -13    7    9   83%
c i  586.0    9421    57733   1417553  280767  57831 13900    9    19   74  48%   -839  -13    7    9   77%
c i  586.0    9398    57733   1417563  280770  57835 13901    9    19   74  48%   -839  -13    7    9   75%
c i  586.0    9384    57733   1417631  280818  57840 13904    9    19   74  48%   -839  -13    6    9   69%
c i  586.0    9371    57733   1417640  280816  57840 13908    9    19   74  48%   -839  -13    6    9   68%
c i  586.0    9343    57733   1417641  280815  57841 13908    9    19   74  48%   -839  -13    6    9   67%
c i  586.0    9315    57733   1417642  280815  57841 13908    9    19   74  48%   -840  -13    6    9   67%
c i  586.0    8796    57733   1417643  280815  57841 13908    9    19   74  48%   -840  -13    6    9   67%
c i  586.0    8704    57733   1417645  280816  57841 13908    9    19   74  48%   -840  -13    6    9   66%
c 0  586.0    8075    57733   1417645  280816  57841 13908    9    19   74  48%   -840  -13    6    9   66%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 771 basic ate = 321 trn 42% + 450 lrg 58% in 5 updates
c bcas: 21 count, 530 added (433 skipped), 2283789 steps
c bkwd: tried 80378 clauses, 160673 lits, 2.00 lits/clause
c bkwd: checked 2539049 occs, 31.59 occs/clause, 15.80 occs/lit
c bkwd: subsumed 0 binary, 6 ternary, 23 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 125 large (0% self)
c blkd: 6 bces, 723 removed, 2812120 resolutions, 7304732 steps
c blkd: 6913 blocking literals 2%, 9 pure
c bump: 1413412 bumped seen, 106466545 lits 75.3 on average
c card: 6 count, 0 units, 2 am1, 13901604 steps
c card: 2 rescheduled, 10 eliminated, 26 resolved, 8196 subsumed
c card: 2044 at-most-one constraints found, average size 3.02
c card: 2044 at-most-one constraints used 100%, average size 3.02
c card: 12 at-most-two constraints found, average size 4.00
c card: 12 at-most-two constraints used 100%, average size 4.00
c cces: 15 cces, 46547 eliminated, 37314 ate 80%, 9233 abce 20%
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: 1823044 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 181 gcs, 0 rescored clauses, 743 rescored vars
c dcps: 77 decompositions, 12820 equivalent 7%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 5370770 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 18 elims, 159821 eliminated 87%, 47 pure 0%
c elms: 34 rounds, 1.9 rounds/bve
c elms: 155737 small 97%, 4028 large 3%
c elms: 168615 tried small, 155737 succeeded 92%, 12878 failed 8%
c elms: 24760 subsumed, 44101 strengthened, 698 blocked
c elms: 6207533 copies, 8399886 resolutions, 2758512 ipos
c elms: 2285559 subchks, 1590944 strchks
c gaus: 6 extractions, 1761 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10205060 steps, 5102530 extr 50%, 79607 elim 1%
c glue: 8.6 orig avg, 8.6 real avg, 2.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 54965 = 26307 simple 48% + 27865 trn 51% + 793 lrg 1%, 2426 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1413412 clauses, 29.1 length
c lrnd: 41159199 lits = 61120630 orig - 19961431 removed 33%
c lrnd: 362729 uips 26%, 861810 flips 61%
c mins: 1379742 mins 98%, 1026 bin 0%, 32644 size 2%
c mins: 119126235 poisoned searches, 14712417 hits, 12% hit rate
c mins: 164013152 used twice searches, 4549739 hits, 3% hit rate
c move: moved 25895, 2929 bin 11%, 22966 trn 89%
c otfs: 6074 driving 26%, 17469 restarting 74%
c otfs: str 23543, 22467 red 95%, 1076 irr 5%
c otfs: str 23543, 0 bin 0%, 825 trn 4%, 22718 lrg 96%
c otfs: sub 182, 137 red 75%, 45 irr 25%
c otfs: sub 182, 0 bin 0%, 82 trn 45%, 100 lrg 55%
c phas: 8 computed, 23291 set, 6317 pos (27%), 16974 neg (73%)
c prbs: 7 basic, 289077 probed, 326 failed, 10 lifted
c prbs: 8 simple, 428114 probed, 31 failed, 20263 eqs
c prbs: 7 treelook, 1432 probed, 5 failed, 0 lifted
c prom: 388282 locked 16% out of 2445186 tried
c prps: 581297999 props, 107 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 22 count, 12185 quat, 6117 self1, 105 self2, 218 dup
c queu: 26 sorted, 5370770 next (2121002 steps 0.39)
c queu: 111350930 enq (115766545 steps 1.04), 106466545 deq 96%
c redc: 65718 clauses 14%, 473618 tried 33%, 35 sat 0%
c redc: 88103 lits 2%, 5862057 tried 10%, 35 sat 0%
c redc: 2603 times jump level reduced, 4.0 levels on average
c reds: 27 count, 52505.4 conflicts per reduce
c reds: 0 memlim 0%, 27 arith 100%
c reds: 850718 collected 81%, 195247 retired 19%
c rmbd: 5547 removed, 2642 red 48%
c rsts: 34154 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 26 count, 23 confs 88%, 0 vars 0%
c simp: 1 its 4%, 1 bin 4%, 1 trns 4%
c subl: 1413412 count (652302 tried 0.5), 36668 sub out of 1390734 (2.6%)
c swps: 10 count, 11 rounds, 3134 queries (284.9/round)
c swps: 3089 sat calls, 49 unsat (0.6% success rate)
c swps: 52517 decisions 17.0, 1841 conflicts 0.6
c swps; 528.0 avg class size, 33.0 avg environment size
c swps: 0 failed, 216 impls, 93 equivs
c swp0: 1042 type 0 queries, 118 unsat (11.3%), 1018 sat (97.7%)
c swp1: 2092 type 1 queries, 470 unsat (22.5%), 2023 sat (96.7%)
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: 13570623 calls to obtain time
c tops: 2609 fixed 1%, 271 its, 5231.16 confs/it
c trds: 22 transitive reductions, 15154 removed, 27 failed
c trds: 528768 nodes, 397304 edges, 11065111 steps
c trim: 515820 words, 2.0 MB
c trnr: 22 count, 2209 bin, 101286 trn, 309781375 steps
c unhd: 14 count, 14 rounds, 17961043 steps
c unhd: 112 non-trivial sccs of average size 2.0
c unhd: 38 units, 38 bin, 0 trn, 0 lrg
c unhd: 383 failed, 374 stamp, 0 lits, 1 bin, 7 trn, 0 lrg
c unhd: 45646 tauts, 230 bin 1%, 30311 trn 66%, 9175 lrg 20%
c unhd: 45646 tauts, 5930 stamp 13%, 35973 red 79%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 260145 str, 38 bin 0%, 7473 trn 3%, 252634 lrg 97%, 177196 red 68%
c vars: 8075 remaining 4% and 175250 removed 96% out of 183325
c vars: 2609 fixed 1%, 159821 eliminated 87%, 12820 equivalent 7%
c vsts: 17817919674 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 30.7 search visits per propagation, 12491.9 per conflict
c wchs: 5200556456 pushed, 22453897 enlarged, 284 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1402919        850718        195247     114062858      18322833        887761
c 
c  0 0        302852  22     52354   6         0   0  97630601  86< 13783694  75<   543226  61     8.1
c  1 5        124618   9     76865   9     26384  14   7490560   7   1644912   9     94067  11<    1.1
c  2 6        364978  26<   268274  32     58790  30   6759639   6   1872473  10    151505  17     2.6
c  3 9        396631  28    302882  36<    61923  32<  1771325   2    785356   4     79352   9     3.0
c  4 14       171580  12    124186  15     34694  18    345774   0    199929   1     16872   2     1.8
c  5 21        35192   3     22364   3     10471   5     54366   0     31528   0      2442   0     0.5
c  6 30         5886   0      3204   0      2414   1      9130   0      4262   0       252   0     0.1
c  7 41          961   0       491   0       451   0      1204   0       568   0        41   0     0.0
c  8 54          164   0        67   0        95   0       191   0        76   0         4   0     0.0
c  9 69           44   0        21   0        22   0        55   0        25   0         0   0     0.0
c 10 86           13   0        10   0         3   0        13   0        10   0         0   0     0.0
c 
c avg                  2.1           2.5           2.8           0.2           0.5           0.8
c std                  1.4           1.1           1.2           0.7           0.9           1.2
c 
c   18.781   3% cce
c   11.183   2% probe
c   10.720   2% bump
c    9.477   2% elim
c    4.135   1% quatres
c    3.296   1% decide
c    2.596   0% ternres
c    1.915   0% sweep
c 
c    6.863 < 1% rest (below)
c 
c    1.846   0% unhide
c    1.447   0% bca
c    0.953   0% transred
c    0.815   0% block
c    0.806   0% rescore
c    0.657   0% gauss
c    0.338   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    4.405   1% preprocessing     7%
c   54.540   9% inprocessing     93%
c ==================================
c   58.946  10% simplifying
c  527.055  90% search
c ==================================
c  586.004 100% all
c 
c       1417645 conflicts,        2419.2 confs/sec
c         20011 ternaries,          70.8 confs/ternary
c          1815 binaries,          781.1 confs/binary
c           271 iterations,       5231.2 confs/iteration
c 
c            27 reductions,          0.0 redus/sec,  52505.4 confs/reduction
c         34154 restarts,           58.3 rests/sec,     41.5 confs/restart
c       5370770 decisions,        9165.1 decis/sec,      3.8 decis/conflict
c     581297999 propagations,   991969.2 props/sec,    108.2 props/decision
c 
c 586.0 seconds, 81.5 MB
c launch: done
