c launch: /data/cnf/sc2014/app/manol-pipe-c10nidw.cnf.bz2
c host: atom28
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/manol-pipe-c10nidw.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/manol-pipe-c10nidw.cnf.bz2
c no embedded options
c found 'p cnf 433601 1291714' header
c read 433601 variables, 1291714 clauses, 3013998 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=2
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 433600 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] VMTF (--score=2)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  433600  1291713         0       0      0     0    0     0   73   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 2 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 2 out of 2 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 433600 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 506 variables
c [simpleprobe-1] 181013 variables remain 42% (252081 retained 58%)
c [simpleprobe-1] removed 506 variables, found 1058 hbrs, 10 units
c [unhide-1] limit 80637 based on 1290202 irredundant clauses
c [unhide-1-1] 0 units, 64 failed, 105 tauts, 0 hbrs, 114 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 431402 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 189604 not tried 44% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 241798 = 56% variables out of 431402 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 744044 negative 95.9% of 775692 except 31648 4.1%
c [phase-count-1] 716116 positive 92.3% of 775692 except 59576 7.7%
c [phase-1] phase bias: 59937 positive 32%, 129667 negative 68%
c [sort-queue-1] sorted 189604 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 189604 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 243996 variables 56.3% (189604 remain 44%)
c [simplification-1] removed 516021 irredundant clauses 39.9% (775692 remain 60%)
c [simplification-1] maximum reduction of 56% = max (56%, 40%)
c [simplification-1] large reduction 56% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    7.6  189603   775692         1       0      0   154    0     0   65   0%      0    0    0    0    0%
c i    7.9  189477   775692       132      90     24   161    0     6   67   2%      0    6    2    0 20851%
c i    8.4  189418   775692       531     392     65   181    1    22   67   3%      1   22    5    0 11795%
c i    8.4  189363   775692       532     392     65   181    1    22   67   3%      1   22    5    0 11749%
c i    8.9  189105   775692       805     600     96   197    1    37   67   3%      1   37    6    0 8335%
c i    9.1  189095   775692       913     669    111   204    1    38   67   3%      1   38    5    0 6931%
c i    9.1  189072   775692       929     674    114   207    1    38   67   3%      1   38    5    0 6715%
c i    9.1  188803   775692       931     674    114   208    1    38   67   3%      1   37    5    0 6667%
c i    9.2  188529   775692      1011     735    122   211    1    42   67   3%      1   42    5    0 6586%
c 
c [simplification-2] limit 1025 conflicts (hard 11000) hit after 1026 conflicts
c [decomp-3] removed 2155 variables
c [simpleprobe-2] 78193 schedulable variables 42%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 21 variables
c [simpleprobe-2] 73408 variables remain 39% (114020 retained 61%)
c [simpleprobe-2] removed 21 variables, found 40 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 46233 literals 12%
c [treelook-1] scheduling used 300117 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 335897 steps
c [treelook-1] 46025 literals remain 12%
c [treelook-1] 45049 variables remain to probed next time 24%
c [treelook-1] removed 0 variables, found 768 hbrs
c [basicprobe-1] limit 6122344 based on 765293 irredundant clauses
c [basicprobe-1-0] 140685 probes remain 76% after last round
c [basicprobe-1-0] 126 units = 86 failed (68%) + 40 lifted (32%)
c [basicprobe-1-0] removed 3168 variables, found 5070 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 16 units, 18 failed, 467 tauts, 0 hbrs, 2086 literals
c [elim-2] 183981 variables 100% will be scheduled this time
c [elim-2] scheduled 183981 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 74169 not tried 40% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 109651 = 60% variables out of 183981 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 464061 negative 97.4% of 476626 except 12565 2.6%
c [phase-count-2] 459105 positive 96.3% of 476626 except 17521 3.7%
c [phase-2] phase bias: 13 positive 15%, 73 negative 85%
c [sort-queue-2] sorted 74330 enqueued variables after 1026 conflicts
c [score-dist-2] active 0 (0%), one 6194 (8%), zero 68136 (92%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 114146 variables 60.6% (74330 remain 17%)
c [simplification-2] removed 299066 irredundant clauses 38.6% (476626 remain 37%)
c [simplification-2] maximum reduction of 61% = max (61%, 39%)
c [simplification-2] large reduction 61% >= 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 13026 (soft 3026 + delta 10000)
c [simplification-2] new conflict limit 3026 (hard 13026)
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   14.6   74329   476626      1296     343     70   890    2    56   57   3%      2   56    7    0 5936%
c i   15.0   74326   476626      2626    1235    166   914    3    69   57   5%      9   67   10    0 3760%
c i   15.0   74311   476626      2627    1235    166   914    3    69   57   5%      9   67   10    0 3746%
c i   15.0   74182   476626      2632    1237    167   914    3    69   57   5%      9   67    9    0 3692%
c i   15.0   74177   476626      2641    1240    170   915    3    69   57   5%      9   67    9    0 3600%
c i   15.1   74173   476626      2919    1390    198   919    3    72   57   5%      8   70    7    0 2610%
c 
c [simplification-3] limit 3039 conflicts (hard 13026) hit after 3040 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 31 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 31 out of 31 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 277 variables
c [unhide-3] limit 110946 with penalty 0 = 0 + 0
c [unhide-3-3] 3 units, 11 failed, 1706 tauts, 0 hbrs, 5240 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 74029 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 20651 not tried 28% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 13540 = 18% variables out of 74029 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 434968 negative 97.3% of 447262 except 12294 2.7%
c [phase-count-3] 434299 positive 97.1% of 447262 except 12963 2.9%
c [phase-3] phase bias: 4 positive 10%, 35 negative 90%
c [sort-queue-3] sorted 60489 enqueued variables after 3040 conflicts
c [score-dist-3] active 0 (0%), one 8402 (14%), zero 52087 (86%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 13682 variables 18.4% (60489 remain 14%)
c [simplification-3] removed 29364 irredundant clauses 6.2% (447262 remain 35%)
c [simplification-3] maximum reduction of 18% = max (18%, 6%)
c [simplification-3] large reduction 18% >= 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 15040 (soft 5040 + delta 10000)
c [simplification-3] new conflict limit 5040 (hard 15040)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   18.3   60488   447262      3137     979    178   497    4    77   56   5%      6   75    7    0 2302%
c i   18.5   60458   447262      3548    1258    191   499    4    80   56   5%      5   78    8    0 2321%
c i   18.7   60455   447261      4029    1587    228   512    4    86   57   5%      5   82    9    0 2248%
c i   18.7   60339   447261      4043    1598    229   512    4    85   57   5%      5   82    8    0 2170%
c i   18.7   60336   447261      4059    1608    232   514    4    85   57   5%      5   82    8    0 2076%
c i   18.8   60326   447260      4390    1840    246   516    5    88   57   5%      4   84    8    0 1983%
c i   18.8   60321   447260      4545    1939    257   520    5    88   57   5%      4   85    9    0 1955%
c i   18.9   60316   447260      4943    2186    287   523    5    89   57   5%      3   85    7    0 1478%
c 
c [simplification-4] limit 5040 conflicts (hard 15040) hit after 5040 conflicts
c [decomp-7] removed 260 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 9697 literals 8%
c [treelook-2] scheduling used 150102 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 189471 steps
c [treelook-2] 9665 literals remain 8%
c [treelook-2] 5576 variables remain to probed next time 9%
c [treelook-2] removed 1 variables, found 88 hbrs
c [unhide-4] limit 147999 with penalty 0 = 0 + 0
c [unhide-4-4] 2 units, 36 failed, 59 tauts, 0 hbrs, 7495 literals
c [elim-4] 20517 variables 34% will be scheduled this time
c [elim-4] scheduled 20517 variables 34%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 1660 variables 3% in round 1 in 275981355 steps
c [elim-4-1] backward subsumption/strengthening limit 124018645
c [elim-4-1-1] backward checking 13073 touched variables 22%
c [elim-4-1-1] incomplete backward checking 14185 remain 109%
c [elim-4-1] subsumed 928 and strengthened 1869 clauses in 124019104 steps
c [elim-4] incomplete 1583 not tried 3% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 1668 = 8% variables out of 20517 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 424834 negative 97.2% of 437016 except 12182 2.8%
c [phase-count-4] 425852 positive 97.4% of 437016 except 11164 2.6%
c [phase-4] phase bias: 8 positive 47%, 9 negative 53%
c [sort-queue-4] sorted 58519 enqueued variables after 5040 conflicts
c [score-dist-4] active 0 (0%), one 9860 (17%), zero 48659 (83%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 1795 variables 3.0% (58519 remain 13%)
c [simplification-4] removed 10244 irredundant clauses 2.3% (437016 remain 34%)
c [simplification-4] maximum reduction of 3% = max (3%, 2%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 5000
c [simplification-4] penalized conflict interval 5000 = 1 * 5000
c [simplification-4] hard conflict limit 20040 (soft 10040 + delta 10000)
c [simplification-4] new conflict limit 10040 (hard 20040)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   26.0   58518   437016      5079    2141    271   527    5    90   57   5%      3   86    7    0 1513%
c i   26.1   58515   437016      5560    2474    299   529    5    91   57   6%      3   86    6    1 1203%
c i   26.1   58514   437016      5577    2484    302   529    5    91   57   6%      3   86    6    1 1170%
c i   26.2   58443   437016      5946    2759    320   544    5    94   57   6%      3   89    8    1 1347%
c i   26.3   58441   437016      6143    2884    337   546    5    94   57   6%      3   88    7    1 1280%
c i   26.3   58438   437016      6374    3054    347   549    5    94   57   6%      2   88    8    1 1348%
c i   26.5   58435   437016      6854    3395    369   554    6    95   57   6%      3   88    8    1 1256%
c i   26.6   58365   437016      7280    3702    396   558    6    97   57   6%      3   90    8    1 1146%
c i   26.7   58363   437016      7473    3830    401   558    6    97   57   6%      3   90    8    1 1169%
c i   26.8   58361   437016      8035    4212    429   565    6    99   57   6%      3   91    9    1 1114%
c 
c [simplification-5] limit of 33 iterations hit after 33 iterations
c [quatres-1] found 37984 quaternary clauses 18% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 468 single-self-subsuming ternary resolvents
c [quatres-1-2] added 4650 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 58355 free variables schedulable
c [ternres-1] 8363 ternary resolvents (100 bin, 8263 trn)
c [ternres-1] 1090 variables remain 2% (57265 retained 98%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 16041 xors of average arity 3.0
c [gauss-1] connected 48092 occurrences of 5870 variables (average 8.2)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-9] removed 41 variables
c [basicprobe-2] limit 4965663 penalty 0 = 0 + 0
c [basicprobe-2-0] 4151 probes remain 7% after last round
c [basicprobe-2-0] 174 units = 174 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 990 variables, found 3767 hbrs
c [bate-1] eliminated 135 asymmetric tautologies during probing
c [unhide-5] limit 198626 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 5 failed, 1731 tauts, 0 hbrs, 5869 literals
c [transred-1] limit 993132 with penalty 0 = 0 + 0
c [transred-1] removed 279 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 57318 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 13110 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 38
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 37
c [cce-1-1] eliminated 1 clauses out of 51 (2%) of length 30
c [cce-1-1] eliminated 1 clauses out of 68 (1%) of length 29
c [cce-1-1] eliminated 12 clauses out of 168 (7%) of length 27
c [cce-1-1] eliminated 2 clauses out of 78 (3%) of length 26
c [cce-1-1] eliminated 1 clauses out of 139 (1%) of length 25
c [cce-1-1] eliminated 20 clauses out of 297 (7%) of length 24
c [cce-1-1] eliminated 7 clauses out of 233 (3%) of length 23
c [cce-1-1] eliminated 6 clauses out of 275 (2%) of length 22
c [cce-1-1] eliminated 10 clauses out of 279 (4%) of length 21
c [cce-1-1] eliminated 6 clauses out of 273 (2%) of length 20
c [cce-1-1] eliminated 33 clauses out of 507 (7%) of length 19
c [cce-1-1] eliminated 24 clauses out of 640 (4%) of length 18
c [cce-1-1] eliminated 47 clauses out of 625 (8%) of length 17
c [cce-1-1] eliminated 54 clauses out of 942 (6%) of length 16
c [cce-1-1] eliminated 93 clauses out of 944 (10%) of length 15
c [cce-1-1] eliminated 108 clauses out of 1043 (10%) of length 14
c [cce-1-1] eliminated 137 clauses out of 1454 (9%) of length 13
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 564 large clauses in 30000001 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 126297 clauses = 53379 binary + 72918 ternary
c [cce-1-1] tried to eliminate 9541 small clauses 8%
c [cce-1-1] eliminated 70 binary clauses 0%
c [cce-1-1] eliminated 89 ternary clauses 0%
c [cce-1-1] eliminated 159 small clauses 0%
c [cce-1-1] eliminated 159 small clauses in 30000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 723 covered clauses in round 1
c [cce-1] eliminated 723 covered clauses in TOTAL during 1 rounds
c [cce-1] 723 < 1/100 * 407317 = 4073 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 56196 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 7662 not tried 14% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2614 = 5% variables out of 56196 scheduled
c [bca-1] limit of 10000000 steps and 800134 added (scaled 2)
c [bca-1] 94058 out of 107166 literals actually usable 88%
c [bca-1] added 528 blocked clauses in 289433 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 18973 pos 35.4% + 34609 neg 64.6% = 53582 sched 100.0% ret 0
c [sweep-1-1] 1004436 steps 69 queries 10494.78 avg class size
c [sweep-1-1] 2111 decisions 68 SAT calls 48.10 avg env size
c [sweep-1-1] 52567 variables remain 98% (1014 retained 2%)
c [decomp-10] removed 52 variables
c [sweep-1-1] removed 52 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 52 vars in TOTAL (1 rounds, 68 queries)
c [phase-count-5] 388021 negative 97.1% of 399468 except 11447 2.9%
c [phase-count-5] 390797 positive 97.8% of 399468 except 8671 2.2%
c [phase-5] phase bias: 7 positive 70%, 3 negative 30%
c [sort-queue-5] sorted 53530 enqueued variables after 8035 conflicts
c [score-dist-5] active 0 (0%), one 12028 (22%), zero 41502 (78%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 4825 variables 8.3% (53530 remain 12%)
c [simplification-5] removed 37548 irredundant clauses 8.6% (399468 remain 31%)
c [simplification-5] maximum reduction of 9% = max (8%, 9%)
c [simplification-5] forced so keeping old conflict interval 5000
c [simplification-5] conflict limit remains at 10040 (hard 20040)
c [simplification-5] new iteration interval 100
c 
c [simplification-6] limit 10040 conflicts (hard 20040) hit after 10040 conflicts
c [quatres-2] found 38829 quaternary clauses 19% in total
c [quatres-2-1] added 10 double-self-subsuming ternary resolvents
c [quatres-2-2] added 1026 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1334 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 992 schedulable variables 2%
c [ternres-2] 2893 ternary resolvents (116 bin, 2777 trn)
c [ternres-2] 305 variables remain 1% (53225 retained 99%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 164 at-most-one constraints of average size 3.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 164 out of 164 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 16742 xors of average arity 3.0
c [gauss-2] connected 50222 occurrences of 7588 variables (average 6.6)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 8 variables
c [simpleprobe-3] 20833 schedulable variables 39%
c [simpleprobe-3] limit 4655269 penalty 0 = 0 + 0
c [decomp-12] removed 2 variables
c [simpleprobe-3] 20493 variables remain 38% (33027 retained 62%)
c [simpleprobe-3] removed 2 variables, found 47 hbrs, 1 units
c [unhide-6] limit 232763 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 2 failed, 583 tauts, 0 hbrs, 4400 literals
c [transred-2] limit 1163817 with penalty 0 = 0 + 0
c [transred-2] removed 98 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 53518 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 507 blocked clauses
c [block-2] 507 < 1/100 * 399387 = 3993 considered unsuccessful
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 53444 variables 100%
c [elim-6] limit of 23276346 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 6375 not tried 12% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 257 = 0% variables out of 53444 scheduled
c [elim-6] 257 < 1/100 * 53444 = 534 considered unsuccessful
c [bca-2] limit of 10000000 steps and 797074 added (scaled 2)
c [bca-2] 90704 out of 106376 literals actually usable 85%
c [bca-2] added 6 blocked clauses in 280578 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 18323 pos 35.1% + 33862 neg 64.9% = 52185 sched 98.1% ret 1002
c [sweep-2-1] 1005739 steps 100 queries 12870.37 avg class size
c [sweep-2-1] 2667 decisions 97 SAT calls 49.67 avg env size
c [sweep-2-1] 51050 variables remain 96% (2133 retained 4%)
c [decomp-13] removed 11 variables
c [sweep-2-1] removed 11 vars (0 failed, 2 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 11 vars in TOTAL (1 rounds, 99 queries)
c [phase-count-6] 386592 negative 97.1% of 398017 except 11425 2.9%
c [phase-count-6] 389287 positive 97.8% of 398017 except 8730 2.2%
c [phase-6] phase bias: 3 positive 100%, 0 negative 0%
c [sort-queue-6] sorted 53176 enqueued variables after 10040 conflicts
c [score-dist-6] active 0 (0%), one 13356 (25%), zero 39820 (75%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 354 variables 0.7% (53176 remain 12%)
c [simplification-6] removed 1451 irredundant clauses 0.4% (398017 remain 31%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 15000
c [simplification-6] penalized conflict interval 15000 = 1 * 15000
c [simplification-6] hard conflict limit 35040 (soft 25040 + delta 10000)
c [simplification-6] new conflict limit 25040 (hard 35040)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   40.4   53175   398017     18720   15599  12346  3239    7   110   57   7%    140   88    7    2  434%
c i   41.7   53172   398016     23130   18646  12575  3261    8   114   57   7%     41   87    7    2  336%
c 
c [simplification-7] limit 25040 conflicts (hard 35040) hit after 25040 conflicts
c [quatres-3] found 39837 quaternary clauses 20% in total
c [quatres-3-1] added 3 double-self-subsuming ternary resolvents
c [quatres-3-2] added 87 single-self-subsuming ternary resolvents
c [quatres-3-2] added 619 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 301 schedulable variables 1%
c [ternres-3] 2898 ternary resolvents (95 bin, 2803 trn)
c [ternres-3] 43 variables remain 0% (53128 retained 100%)
c [decomp-14] removed 23 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 8260 literals 8%
c [treelook-3] scheduling used 300003 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 325833 steps
c [treelook-3] 8248 literals remain 8%
c [treelook-3] 3212 variables remain to probed next time 6%
c [treelook-3] removed 1 variables, found 104 hbrs
c [unhide-7] limit 482092 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 5 failed, 655 tauts, 0 hbrs, 4741 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 96 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 72 (1%) of length 29
c [cce-2-1] eliminated 2 clauses out of 66 (3%) of length 28
c [cce-2-1] eliminated 2 clauses out of 165 (1%) of length 27
c [cce-2-1] eliminated 1 clauses out of 90 (1%) of length 26
c [cce-2-1] eliminated 4 clauses out of 149 (3%) of length 25
c [cce-2-1] eliminated 1 clauses out of 304 (0%) of length 22
c [cce-2-1] eliminated 4 clauses out of 320 (1%) of length 21
c [cce-2-1] eliminated 5 clauses out of 337 (1%) of length 20
c [cce-2-1] eliminated 14 clauses out of 537 (3%) of length 19
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 34 large clauses in 15000015 steps
c [cce-2-1] allowing another 7500007 steps for small clauses
c [cce-2-1] scheduling 121862 clauses = 50325 binary + 71537 ternary
c [cce-2-1] tried to eliminate 8001 small clauses 7%
c [cce-2-1] eliminated 38 binary clauses 0%
c [cce-2-1] eliminated 96 ternary clauses 0%
c [cce-2-1] eliminated 134 small clauses 0%
c [cce-2-1] eliminated 205 small clauses in 15000048 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 239 covered clauses in round 1
c [cce-2] eliminated 239 covered clauses in TOTAL during 1 rounds
c [cce-2] 239 < 1/100 * 397078 = 3970 considered unsuccessful
c [bca-3] limit of 10000000 steps and 794445 added (scaled 2)
c [bca-3] 85174 out of 106292 literals actually usable 80%
c [bca-3] added 3 blocked clauses in 272094 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 18189 pos 35.7% + 32829 neg 64.3% = 51018 sched 96.0% ret 2127
c [sweep-3-1] 1000454 steps 88 queries 11869.90 avg class size
c [sweep-3-1] 2446 decisions 85 SAT calls 40.33 avg env size
c [sweep-3-1] 50174 variables remain 94% (2962 retained 6%)
c [decomp-16] removed 22 variables
c [sweep-3-1] removed 22 vars (0 failed, 3 eqs, 4 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 22 vars in TOTAL (1 rounds, 87 queries)
c [phase-count-7] 385238 negative 97.1% of 396644 except 11406 2.9%
c [phase-count-7] 387920 positive 97.8% of 396644 except 8724 2.2%
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-7] sorted 53123 enqueued variables after 25040 conflicts
c [score-dist-7] active 0 (0%), one 17280 (33%), zero 35843 (67%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 48 variables 0.1% (53123 remain 12%)
c [simplification-7] removed 1372 irredundant clauses 0.3% (396644 remain 31%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20000
c [simplification-7] new conflict interval 35000
c [simplification-7] penalized conflict interval 35000 = 1 * 35000
c [simplification-7] hard conflict limit 77540 (soft 60040 + delta 17500)
c [simplification-7] new conflict limit 60040 (hard 77540)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   45.5   53122   396644     26685   21603  15428  3522    8   114   58   7%     27   83    7    2  296%
c i   45.9   53121   396644     27837   22436  15477  3524    8   117   58   7%      6   84    8    2  348%
c i   45.9   53120   396644     27882   22474  15479  3528    8   116   58   7%      5   84    8    2  327%
c i   47.3   53112   396644     32312   25727  15694  3547    8   122   58   7%     38   85   10    3  380%
c i   47.5   53111   396644     32628   25934  15711  3550    8   121   58   7%     24   84    9    3  344%
c i   47.5   53108   396644     32629   25934  15711  3550    8   121   58   7%     24   84    9    3  343%
c i   50.6   53107   396644     42604   32510  16098  3585    8   134   58   6%    116   88    8    3  222%
c i   53.0   53099   396644     48838   37265  16334  3594    8   126   60   6%     55   73    7    4  181%
c 
c [simplification-8] limit 60050 conflicts (hard 77540) hit after 60050 conflicts
c [quatres-4] found 42112 quaternary clauses 20% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-1] added 2 double-self-subsuming ternary resolvents
c [quatres-4-2] added 73 single-self-subsuming ternary resolvents
c [quatres-4-2] added 412 quaternary resolvents
c [ternres-4] limit 6078470 with penalty 0 = 0 + 0
c [ternres-4] 41 schedulable variables 0%
c [ternres-4] 6748 ternary resolvents (25 bin, 6723 trn)
c [ternres-4] 6 variables remain 0% (53087 retained 100%)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 8031 xors of average arity 3.0
c [gauss-3] connected 24088 occurrences of 5679 variables (average 4.2)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 15 variables
c [basicprobe-3] limit 30392350 penalty 0 = 0 + 0
c [basicprobe-3-0] 4548 sched 9%, 41 failed, 0 lifted, 867 hbrs
c [decomp-18] removed 157 variables
c [basicprobe-3-1] 28368 sched 54%, 92 failed, 8 lifted, 1600 hbrs
c [decomp-19] removed 180 variables
c [basicprobe-3-2] 28210 sched 53%, 7 failed, 0 lifted, 55 hbrs
c [decomp-20] removed 15 variables
c [basicprobe-3-3] 28215 sched 54%, 2 failed, 0 lifted, 5 hbrs
c [decomp-21] removed 4 variables
c [basicprobe-3-4] 28211 sched 54%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-4] fully completed probing
c [basicprobe-3-4] 150 units = 142 failed (95%) + 8 lifted (5%)
c [basicprobe-3-4] removed 356 variables, found 2527 hbrs
c [bate-2] eliminated 187 asymmetric tautologies during probing
c [unhide-8] limit 1215694 with penalty 0 = 0 + 0
c [unhide-8-8] 0 units, 0 failed, 1905 tauts, 0 hbrs, 16129 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 250 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 52722 variables 100%
c [block-3] limit of 30392350 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1475 blocked clauses
c [block-3] 1475 < 1/100 * 392665 = 3926 considered unsuccessful
c [elim-7] 6203 variables 12% will be scheduled this time
c [elim-7] scheduled 6203 variables 12%
c [elim-7] limit of 60784700 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 2425 not tried 5% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 0 = 0% variables out of 6203 scheduled
c [bca-4] limit of 10000000 steps and 782322 added (scaled 2)
c [bca-4] 77123 out of 105078 literals actually usable 73%
c [bca-4] added 28 blocked clauses in 269635 steps
c [sweep-4] limit 1823541 penalty 0 = 0 + 0
c [sweep-4-1] 18020 pos 36.3% + 31666 neg 63.7% = 49686 sched 94.6% ret 2852
c [sweep-4-1] 1827994 steps 97 queries 7970.08 avg class size
c [sweep-4-1] 2950 decisions 97 SAT calls 68.81 avg env size
c [sweep-4-1] 48231 variables remain 92% (4307 retained 8%)
c [decomp-22] removed 12 variables
c [sweep-4-1] removed 12 vars (0 failed, 1 eqs, 2 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 12 vars in TOTAL (1 rounds, 96 queries)
c [sort-queue-8] sorted 52526 enqueued variables after 60050 conflicts
c [score-dist-8] active 0 (0%), one 23695 (45%), zero 28831 (55%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 567 variables 1.1% (52526 remain 12%)
c [simplification-8] removed 6066 irredundant clauses 1.5% (390578 remain 30%)
c [simplification-8] maximum reduction of 2% = max (1%, 2%)
c [simplification-8] geometric conflict interval increment 11666 = 35000 / 3
c [simplification-8] new conflict interval 46666
c [simplification-8] penalized conflict interval 46666 = 1 * 46666
c [simplification-8] hard conflict limit 130049 (soft 106716 + delta 23333)
c [simplification-8] new conflict limit 106716 (hard 130049)
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   83.2   52525   390578    102036   77281  22840  4688    7   111   62   7%    550   22    7    6  117%
c i   83.2   52522   390578    102037   77281  22840  4688    7   111   62   7%    549   22    7    6  117%
c i   83.2   52521   390578    102176   77400  22846  4688    7   109   62   7%    444   20    6    6  103%
c -   84.4   52513   390578    104568   35254  22954  4694    8   119   58   6%   -176   30    7    6  116%
c i   87.6   52512   390578    113328   41749  23365  4774    7   128   60   6%    -88   33    6    6  105%
c i   88.4   52470   390578    115761   43539  23465  4785    8   128   60   6%   -202   32   10    6  162%
c i   89.7   52467   390578    119912   46810  23609  4794    7   121   60   6%   -177   24    8    6  135%
c 
c [simplification-9] limit 106726 conflicts (hard 130049) hit after 130049 conflicts
c [quatres-5] found 45939 quaternary clauses 21% in total
c [quatres-5-1] removed 4 duplicate quaternary clauses
c [quatres-5-1] added 6 double-self-subsuming ternary resolvents
c [quatres-5-2] added 181 single-self-subsuming ternary resolvents
c [quatres-5-2] added 540 quaternary resolvents
c [ternres-5] limit 14003197 with penalty 0 = 0 + 0
c [ternres-5] 5 schedulable variables 0%
c [ternres-5] 3752 ternary resolvents (65 bin, 3687 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-23] removed 190 variables
c [simpleprobe-4] 20051 schedulable variables 38%
c [simpleprobe-4] limit 56012788 penalty 0 = 0 + 0
c [decomp-24] removed 89 variables
c [simpleprobe-4] 6779 variables remain 13% (45468 retained 87%)
c [simpleprobe-4] removed 89 variables, found 634 hbrs, 5 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 441 transitive binary clauses
c [transred-5] found 2 units
c [bca-5] limit of 10000000 steps and 777056 added (scaled 2)
c [bca-5] 77855 out of 104472 literals actually usable 75%
c [bca-5] added 41 blocked clauses in 287033 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 42009590 penalty 0 = 0 + 0
c [sweep-5-1] 20972 pos 43.7% + 27017 neg 56.3% = 47989 sched 91.9% ret 4246
c [sweep-5-1] 42011819 steps 3888 queries 944.47 avg class size
c [sweep-5-1] 67543 decisions 3858 SAT calls 26.30 avg env size
c [sweep-5-1] 11743 variables remain 22% (40480 retained 78%)
c [decomp-25] removed 130 variables
c [sweep-5-1] removed 130 vars (0 failed, 81 eqs, 55 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 130 vars in TOTAL (1 rounds, 3887 queries)
c [sort-queue-9] sorted 52105 enqueued variables after 130049 conflicts
c [score-dist-9] active 0 (0%), one 27855 (53%), zero 24250 (47%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 358 variables 0.7% (52105 remain 12%)
c [simplification-9] removed 2972 irredundant clauses 0.8% (387606 remain 30%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 23333 = 46666 / 2
c [simplification-9] new conflict interval 69999
c [simplification-9] penalized conflict interval 69999 = 1 * 69999
c [simplification-9] hard conflict limit 235047 (soft 200048 + delta 34999)
c [simplification-9] new conflict limit 200048 (hard 235047)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  102.7   52104   387606    140737   62167  26328  5488    7   112   62   7%    101    7    7    6  114%
c i  112.9   52098   387606    169326   85589  27212  5523    8   105   64   8%    214   -2    9    7  129%
c -  119.4   52094   387606    187510   58783  27689  5551    8    91   60   9%     66  -12    6    7   89%
c 
c [simplification-10] limit 200048 conflicts (hard 235047) hit after 200048 conflicts
c [quatres-6] found 49523 quaternary clauses 21% in total
c [quatres-6-1] removed 5 duplicate quaternary clauses
c [quatres-6-1] added 2 double-self-subsuming ternary resolvents
c [quatres-6-2] added 147 single-self-subsuming ternary resolvents
c [quatres-6-2] added 352 quaternary resolvents
c [ternres-6] limit 20791624 with penalty 0 = 0 + 0
c [ternres-6] all 52094 free variables schedulable
c [ternres-6] 4128 ternary resolvents (91 bin, 4037 trn)
c [ternres-6] 876 variables remain 2% (51218 retained 98%)
c [card-4] limit 1299476 penalty 3 = 3 + 0
c [card-4] found 230 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1299476 for elimination
c [card-4] 230 out of 230 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-26] removed 29 variables
c [treelook-4] limit 2079162 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 14581 literals 14%
c [treelook-4] scheduling used 951296 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 2079162 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 2081371 steps
c [treelook-4] 14091 literals remain 14%
c [treelook-4] 2843 variables remain to probed next time 5%
c [decomp-27] removed 28 variables
c [treelook-4] removed 77 variables, found 1375 hbrs
c [unhide-9] limit 2079162 with penalty 1 = 1 + 0
c [unhide-9-9] 0 units, 9 failed, 1217 tauts, 0 hbrs, 21118 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 427 transitive binary clauses
c [transred-6] found 2 units
c [cce-3] limit of 25989530 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 56
c [cce-3-1] eliminated 4 clauses out of 162 (2%) of length 27
c [cce-3-1] eliminated 15 clauses out of 84 (18%) of length 26
c [cce-3-1] eliminated 6 clauses out of 133 (5%) of length 25
c [cce-3-1] eliminated 23 clauses out of 258 (9%) of length 24
c [cce-3-1] eliminated 9 clauses out of 191 (5%) of length 23
c [cce-3-1] eliminated 26 clauses out of 299 (9%) of length 22
c [cce-3-1] eliminated 29 clauses out of 311 (9%) of length 21
c [cce-3-1] eliminated 15 clauses out of 337 (4%) of length 20
c [cce-3-1] eliminated 21 clauses out of 453 (5%) of length 19
c [cce-3-1] eliminated 38 clauses out of 731 (5%) of length 18
c [cce-3-1] eliminated 42 clauses out of 620 (7%) of length 17
c [cce-3-1] eliminated 54 clauses out of 1007 (5%) of length 16
c [cce-3-1] eliminated 12 clauses out of 955 (1%) of length 15
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 295 large clauses in 25989572 steps
c [cce-3-1] allowing another 12994786 steps for small clauses
c [cce-3-1] scheduling 117840 clauses = 48210 binary + 69630 ternary
c [cce-3-1] tried to eliminate 10788 small clauses 9%
c [cce-3-1] eliminated 137 binary clauses 0%
c [cce-3-1] eliminated 248 ternary clauses 0%
c [cce-3-1] eliminated 385 small clauses 0%
c [cce-3-1] eliminated 475 small clauses in 25990386 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 770 covered clauses in round 1
c [cce-3] eliminated 770 covered clauses in TOTAL during 1 rounds
c [cce-3] 770 < 1/100 * 386202 = 3862 considered unsuccessful
c [bca-6] limit of 10000000 steps and 771667 added (scaled 2)
c [bca-6] 76826 out of 103974 literals actually usable 74%
c [bca-6] added 16 blocked clauses in 301292 steps
c [sweep-6] limit 6237487 penalty 0 = 0 + 0
c [sweep-6-1] 4632 pos 39.6% + 7070 neg 60.4% = 11702 sched 22.5% ret 40284
c [sweep-6-1] 6237633 steps 924 queries 1956.03 avg class size
c [sweep-6-1] 12432 decisions 897 SAT calls 21.20 avg env size
c [sweep-6-1] 9424 variables remain 18% (42550 retained 82%)
c [decomp-28] removed 101 variables
c [sweep-6-1] removed 101 vars (0 failed, 65 eqs, 33 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 101 vars in TOTAL (1 rounds, 923 queries)
c [sort-queue-10] sorted 51885 enqueued variables after 200048 conflicts
c [score-dist-10] active 0 (0%), one 30332 (58%), zero 21553 (42%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 209 variables 0.4% (51885 remain 12%)
c [simplification-10] removed 2646 irredundant clauses 0.7% (384960 remain 30%)
c [simplification-10] maximum reduction of 1% = max (0%, 1%)
c [simplification-10] geometric conflict interval increment 34999 = 69999 / 2
c [simplification-10] new conflict interval 104998
c [simplification-10] penalized conflict interval 104998 = 1 * 104998
c [simplification-10] hard conflict limit 357545 (soft 305046 + delta 52499)
c [simplification-10] new conflict limit 305046 (hard 357545)
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  135.5   51884   384960    233469   96420  31307  6616    8    83   67   9%    549  -23    6    8   83%
c i  135.5   51851   384960    233471   96420  31307  6617    8    83   67   9%    547  -23    6    8   82%
c i  137.1   51742   384960    240209  101679  31563  6655    8   178   67   4%   -322   70    8    8  103%
c i  137.8   51736   384960    243256  104081  31683  6668    7   137   67   5%   -359   26    5    8   69%
c i  140.0   51711   384960    252341  111289  32046  6720    8   125   68   6%   -227   13    9    8  112%
c i  140.2   51706   384960    252879  111732  32069  6725    7   121   68   6%   -274    8    7    8   87%
c i  140.3   51691   384960    253955  112410  32090  6729    8   222   68   3%   -312  108    8    8  106%
c i  142.1   51683   384960    259463  116773  32257  6763    8   203   68   4%   -250   83    9    8  113%
c -  142.6   51680   384960    261689   80358  32306  6769    8   204   62   4%   -283   81    7    8   91%
c i  142.7   51679   384960    261973   80569  32314  6775    8   207   65   4%   -279   83    9    8  123%
c i  143.4   51678   384960    263981   82193  32369  6783    8   193   65   4%   -279   67   10    8  133%
c i  144.7   51676   384960    268850   86043  32530  6794    9   179   65   5%   -221   50   10    8  124%
c i  145.3   51671   384960    269882   86818  32566  6798    9   197   65   4%   -250   67    8    8  105%
c i  145.5   51666   384960    270399   87249  32587  6800    8   191   65   4%   -257   60    8    8  101%
c i  146.2   51665   384960    273831   89920  32720  6812    8   158   65   5%   -224   26    8    8  102%
c 
c [simplification-11] limit of 4702 ternary hit after 4808 ternaries
c [quatres-7] found 50943 quaternary clauses 21% in total
c [quatres-7-1] removed 12 duplicate quaternary clauses
c [quatres-7-1] added 2 double-self-subsuming ternary resolvents
c [quatres-7-2] added 206 single-self-subsuming ternary resolvents
c [quatres-7-2] added 429 quaternary resolvents
c [ternres-7] limit 27864378 with penalty 0 = 0 + 0
c [ternres-7] 843 schedulable variables 2%
c [ternres-7] 5336 ternary resolvents (325 bin, 5011 trn)
c [ternres-7] 7 variables remain 0% (51654 retained 100%)
c [gauss-4] limit 1393218 penalty 2 = 2 + 0
c [gauss-4] extracted 10186 xors of average arity 3.0
c [gauss-4] connected 30212 occurrences of 6648 variables (average 4.5)
c [gauss-4] limit 1393218 penalty 2 = 2 + 0
c [decomp-29] removed 636 variables
c [gauss-4] exported 0 unary, 1 binary and 3 ternary equations
c [decomp-30] removed 7 variables
c [basicprobe-4] limit 139321893 penalty 0 = 0 + 0
c [basicprobe-4-0] 27068 sched 53%, 63 failed, 0 lifted, 4375 hbrs
c [decomp-31] removed 313 variables
c [basicprobe-4-1] 26889 sched 53%, 14 failed, 0 lifted, 341 hbrs
c [decomp-32] removed 46 variables
c [basicprobe-4-2] 26866 sched 53%, 3 failed, 0 lifted, 44 hbrs
c [decomp-33] removed 8 variables
c [basicprobe-4-3] 26865 sched 53%, 1 failed, 0 lifted, 14 hbrs
c [decomp-34] removed 3 variables
c [basicprobe-4-4] 26861 sched 53%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-5] 26861 sched 53%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-6] 26861 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-6] fully completed probing
c [basicprobe-4-6] 81 units = 81 failed (100%) + 0 lifted (0%)
c [basicprobe-4-6] removed 370 variables, found 4778 hbrs
c [bate-3] eliminated 323 asymmetric tautologies during probing
c [unhide-10] limit 5572875 with penalty 0 = 0 + 0
c [unhide-10-11] 0 units, 0 failed, 5593 tauts, 0 hbrs, 41548 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 525 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 50648 variables 100%
c [block-4] limit of 69660946 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 13694 blocked clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 49059 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2786437865 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 2487 variables 5% in round 1 in 323288056 steps
c [elim-8-1] backward subsumption/strengthening limit 323288000
c [elim-8-1-1] backward checking 7279 touched variables 15%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 86 and strengthened 145 clauses in 23497979 steps
c [elim-8-1] rescheduled 392 variables 1% by backward subsumption
c [elim-8-2] eliminated 40 variables 0% in round 2 in 67510835 steps
c [elim-8-2] backward subsumption/strengthening limit 67510800
c [elim-8-2-1] backward checking 285 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 3 and strengthened 22 clauses in 2591637 steps
c [elim-8-2] rescheduled 76 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 22740437 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 2527 = 5% variables out of 49059 scheduled
c [bca-7] limit of 10000000 steps and 699639 added (scaled 2)
c [bca-7] 65171 out of 93066 literals actually usable 70%
c [bca-7] added 307 blocked clauses in 273714 steps
c [sweep-7] limit 8359313 penalty 0 = 0 + 0
c [sweep-7-1] 3811 pos 44.7% + 4716 neg 55.3% = 8527 sched 18.3% ret 38005
c [sweep-7-1] 8360057 steps 2347 queries 1232.86 avg class size
c [sweep-7-1] 30846 decisions 2350 SAT calls 18.57 avg env size
c [sweep-7-1] 3601 variables remain 8% (42921 retained 92%)
c [decomp-37] removed 85 variables
c [sweep-7-1] removed 85 vars (2 failed, 28 eqs, 7 impls)
c [sweep-7] removed 85 vars in TOTAL (1 rounds, 2346 queries)
c [sort-queue-11] sorted 46447 enqueued variables after 289663 conflicts
c [score-dist-11] active 0 (0%), one 29284 (63%), zero 17163 (37%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 5214 variables 10.1% (46447 remain 11%)
c [simplification-11] removed 35773 irredundant clauses 9.3% (349187 remain 27%)
c [simplification-11] maximum reduction of 10% = max (10%, 9%)
c [simplification-11] forced so keeping old conflict interval 104998
c [simplification-11] conflict limit remains at 305051 (hard 357545)
c [simplification-11] new ternary interval 10000
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  166.4   46446   349187    294109   78140  23512  4769    8   169   63   5%     67   26   10    8  129%
c i  167.0   46445   349187    297855   81119  23617  4781    8   132   63   6%   -175  -12    9    8  114%
c i  167.6   46444   349187    299167   82179  23666  4786    8   138   63   6%   -199   -6    9    8  116%
c 
c [simplification-12] limit 305051 conflicts (hard 357545) hit after 312907 conflicts
c [quatres-8] found 47360 quaternary clauses 21% in total
c [quatres-8-1] removed 169 duplicate quaternary clauses
c [quatres-8-1] added 5 double-self-subsuming ternary resolvents
c [quatres-8-2] added 285 single-self-subsuming ternary resolvents
c [quatres-8-2] added 905 quaternary resolvents
c [ternres-8] limit 29448279 with penalty 0 = 0 + 0
c [ternres-8] 4 schedulable variables 0%
c [ternres-8] 13278 ternary resolvents (975 bin, 12303 trn)
c [ternres-8] 1 variables remain 0% (46442 retained 100%)
c [decomp-38] removed 94 variables
c [simpleprobe-5] 5886 schedulable variables 13%
c [simpleprobe-5] limit 117793119 penalty 0 = 0 + 0
c [decomp-39] removed 88 variables
c [simpleprobe-5] 81 variables remain 0% (46184 retained 100%)
c [simpleprobe-5] removed 88 variables, found 1864 hbrs, 37 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 750 transitive binary clauses
c [transred-8] found 3 units
c [bca-8] limit of 10000000 steps and 696994 added (scaled 2)
c [bca-8] 61936 out of 92504 literals actually usable 67%
c [bca-8] added 17 blocked clauses in 280804 steps
c [sweep-8] limit 8834483 penalty 0 = 0 + 0
c [sweep-8-1] 1422 pos 39.6% + 2168 neg 60.4% = 3590 sched 7.8% ret 42661
c [sweep-8-1] 4588215 steps 2162 queries 584.93 avg class size
c [sweep-8-1] 27793 decisions 2179 SAT calls 17.41 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-40] removed 59 variables
c [sweep-8-1] removed 59 vars (0 failed, 22 eqs, 5 impls)
c [sweep-8-2] 16545 pos 35.8% + 29647 neg 64.2% = 46192 sched 100.0% ret 0
c [sweep-8-2] 4260454 steps 268 queries 6034.76 avg class size
c [sweep-8-2] 8128 decisions 269 SAT calls 55.36 avg env size
c [sweep-8-2] 39770 variables remain 86% (6418 retained 14%)
c [decomp-41] removed 17 variables
c [sweep-8-2] removed 17 vars (0 failed, 9 eqs, 7 impls)
c [sweep-8] removed 76 vars in TOTAL (2 rounds, 2428 queries)
c [sort-queue-12] sorted 46175 enqueued variables after 312907 conflicts
c [score-dist-12] active 0 (0%), one 29793 (65%), zero 16382 (35%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 268 variables 0.6% (46175 remain 11%)
c [simplification-12] removed 1652 irredundant clauses 0.5% (347535 remain 27%)
c [simplification-12] maximum reduction of 1% = max (1%, 0%)
c [simplification-12] geometric conflict interval increment 52499 = 104998 / 2
c [simplification-12] new conflict interval 157497
c [simplification-12] penalized conflict interval 157497 = 1 * 157497
c [simplification-12] hard conflict limit 549152 (soft 470404 + delta 78748)
c [simplification-12] new conflict limit 470404 (hard 549152)
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  174.6   46174   347535    314409   94636  35337  6586    9   145   67   6%     23    2    9    8  117%
c i  177.2   46169   347535    325501  103869  35653  6612    8   105   67   8%    -25  -39    9    8  116%
c i  178.4   46167   347535    330392  107779  35828  6645    8   148   67   5%   -112    5    7    8   83%
c i  180.6   46166   347535    339269  115141  36035  6660    9   138   67   6%    -37   -9    9    8  105%
c -  181.4   46165   347535    342785   79681  36144  6664    8   153   61   5%   -110    7    9    8  117%
c i  189.4   46164   347535    375344  106396  37047  6770    9   293   66   3%    331  125   10    8  116%
c 
c [simplification-13] limit of 861 binary hit after 861 binaries
c [quatres-9] found 49670 quaternary clauses 21% in total
c [quatres-9-1] removed 68 duplicate quaternary clauses
c [quatres-9-1] added 9 double-self-subsuming ternary resolvents
c [quatres-9-2] added 192 single-self-subsuming ternary resolvents
c [quatres-9-2] added 272 quaternary resolvents
c [ternres-9] limit 34127076 with penalty 0 = 0 + 0
c [ternres-9] 1 schedulable variables 0%
c [ternres-9] 6952 ternary resolvents (629 bin, 6323 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-5] limit 3412707 penalty 1 = 1 + 0
c [gauss-5] extracted 19710 xors of average arity 3.0
c [gauss-5] connected 59028 occurrences of 8271 variables (average 7.1)
c [gauss-5] limit 3412707 penalty 1 = 1 + 0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-42] removed 95 variables
c [treelook-5] limit 3412707 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 12355 literals 13%
c [treelook-5] scheduling used 901049 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 3412707 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 3466473 steps
c [treelook-5] 12174 literals remain 13%
c [treelook-5] 2273 variables remain to probed next time 5%
c [decomp-43] removed 2 variables
c [treelook-5] removed 2 variables, found 2485 hbrs
c [unhide-11] limit 3412707 with penalty 1 = 1 + 0
c [unhide-11-12] 0 units, 3 failed, 1057 tauts, 0 hbrs, 40092 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 895 transitive binary clauses
c [transred-9] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 46030 variables 100%
c [block-5] limit of 170635384 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 7632 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 45052 variables 100%
c [elim-9] limit of 341270769 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 637 variables 1% in round 1 in 289173330 steps
c [elim-9-1] backward subsumption/strengthening limit 52097439
c [elim-9-1-1] backward checking 2590 touched variables 6%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 20 and strengthened 33 clauses in 11631033 steps
c [elim-9-1] rescheduled 88 variables 0% by backward subsumption
c [elim-9-2] no variable eliminated in round 2 in 40254934 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 637 = 1% variables out of 45052 scheduled
c [bca-9] limit of 10000000 steps and 672793 added (scaled 2)
c [bca-9] 58896 out of 88832 literals actually usable 66%
c [bca-9] added 142 blocked clauses in 280146 steps
c [sweep-9] limit 10238123 penalty 0 = 0 + 0
c [sweep-9-1] 14935 pos 39.0% + 23407 neg 61.0% = 38342 sched 86.3% ret 6073
c [sweep-9-1] 10250573 steps 665 queries 3947.60 avg class size
c [sweep-9-1] 16420 decisions 667 SAT calls 41.26 avg env size
c [sweep-9-1] 28415 variables remain 64% (15993 retained 36%)
c [decomp-44] removed 53 variables
c [sweep-9-1] removed 53 vars (0 failed, 25 eqs, 9 impls)
c [sweep-9] removed 53 vars in TOTAL (1 rounds, 664 queries)
c [sort-queue-13] sorted 44362 enqueued variables after 376090 conflicts
c [score-dist-13] active 0 (0%), one 29043 (65%), zero 15319 (35%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 1802 variables 3.9% (44362 remain 10%)
c [simplification-13] removed 11846 irredundant clauses 3.4% (335689 remain 26%)
c [simplification-13] maximum reduction of 4% = max (4%, 3%)
c [simplification-13] forced so keeping old conflict interval 157497
c [simplification-13] conflict limit remains at 470404 (hard 549152)
c [simplification-13] 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 -  206.8   44362   335689    410161   90801  38160  7674    8   110   61   8%    280  -57   10    8  116%
c -  220.2   44362   335689    469165  105469  39301  7783    9   170   62   5%    722   -5   10    8  124%
c 
c [simplification-14] limit 470404 conflicts (hard 549152) hit after 484665 conflicts
c [quatres-10] found 51061 quaternary clauses 20% in total
c [quatres-10-1] removed 32 duplicate quaternary clauses
c [quatres-10-1] added 8 double-self-subsuming ternary resolvents
c [quatres-10-2] added 192 single-self-subsuming ternary resolvents
c [quatres-10-2] added 398 quaternary resolvents
c [ternres-10] limit 41602424 with penalty 0 = 0 + 0
c [ternres-10] all 44362 free variables schedulable
c [ternres-10] 7582 ternary resolvents (883 bin, 6699 trn)
c [ternres-10] 25 variables remain 0% (44337 retained 100%)
c [decomp-45] removed 91 variables
c [basicprobe-5] limit 208012121 penalty 0 = 0 + 0
c [basicprobe-5-0] 23553 sched 53%, 51 failed, 0 lifted, 1061 hbrs
c [decomp-46] removed 181 variables
c [basicprobe-5-1] 23468 sched 53%, 11 failed, 0 lifted, 108 hbrs
c [decomp-47] removed 40 variables
c [basicprobe-5-2] 23449 sched 53%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-5-3] 23449 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-3] fully completed probing
c [basicprobe-5-3] 62 units = 62 failed (100%) + 0 lifted (0%)
c [basicprobe-5-3] removed 221 variables, found 1172 hbrs
c [bate-4] eliminated 171 asymmetric tautologies during probing
c [unhide-12] limit 8320484 with penalty 0 = 0 + 0
c [unhide-12-15] 0 units, 0 failed, 12037 tauts, 0 hbrs, 55111 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 381 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 44050 variables 100%
c [block-6] limit of 416024242 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 2738 blocked clauses
c [block-6] 2738 < 1/100 * 332928 = 3329 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 260015151 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 33
c [cce-4-1] eliminated 1 clauses out of 68 (1%) of length 27
c [cce-4-1] eliminated 1 clauses out of 93 (1%) of length 26
c [cce-4-1] eliminated 1 clauses out of 126 (1%) of length 25
c [cce-4-1] eliminated 3 clauses out of 207 (1%) of length 23
c [cce-4-1] eliminated 5 clauses out of 263 (2%) of length 22
c [cce-4-1] eliminated 10 clauses out of 277 (4%) of length 21
c [cce-4-1] eliminated 7 clauses out of 307 (2%) of length 20
c [cce-4-1] eliminated 17 clauses out of 388 (4%) of length 19
c [cce-4-1] eliminated 35 clauses out of 651 (5%) of length 18
c [cce-4-1] eliminated 37 clauses out of 503 (7%) of length 17
c [cce-4-1] eliminated 57 clauses out of 926 (6%) of length 16
c [cce-4-1] eliminated 64 clauses out of 775 (8%) of length 15
c [cce-4-1] eliminated 69 clauses out of 813 (8%) of length 14
c [cce-4-1] eliminated 117 clauses out of 1114 (11%) of length 13
c [cce-4-1] eliminated 254 clauses out of 1853 (14%) of length 12
c [cce-4-1] eliminated 382 clauses out of 2777 (14%) of length 11
c [cce-4-1] eliminated 561 clauses out of 4022 (14%) of length 10
c [cce-4-1] eliminated 890 clauses out of 6065 (15%) of length 9
c [cce-4-1] eliminated 1596 clauses out of 10896 (15%) of length 8
c [cce-4-1] eliminated 2556 clauses out of 22518 (11%) of length 7
c [cce-4-1] eliminated 2299 clauses out of 50374 (5%) of length 6
c [cce-4-1] eliminated 1511 clauses out of 27823 (5%) of length 5
c [cce-4-1] eliminated 936 clauses out of 29040 (3%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 11410 large clauses in 248977773 steps
c [cce-4-1] allowing another 124488886 steps for small clauses
c [cce-4-1] scheduling 108530 clauses = 40248 binary + 68282 ternary
c [cce-4-1] tried to eliminate 108530 small clauses 100%
c [cce-4-1] eliminated 355 binary clauses 1%
c [cce-4-1] eliminated 1348 ternary clauses 2%
c [cce-4-1] eliminated 1703 small clauses 2%
c [cce-4-1] eliminated 1703 small clauses in 213410633 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 13113 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 23302330 steps for small clauses
c [cce-4-2] scheduling 106833 clauses = 39893 binary + 66940 ternary
c [cce-4-2] tried to eliminate 37285 small clauses 35%
c [cce-4-2] eliminated 1 ternary clauses 0%
c [cce-4-2] eliminated 1 small clauses 0%
c [cce-4-2] eliminated 1 small clauses in 46604525 steps
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 1 covered clauses in round 2
c [cce-4] eliminated 13114 covered clauses in TOTAL during 2 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 43743 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 3328 variables 8% in round 1 in 246209778 steps
c [elim-10-1] backward subsumption/strengthening limit 246209700
c [elim-10-1-1] backward checking 12045 touched variables 28%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 6 and strengthened 17 clauses in 12799411 steps
c [elim-10-1] rescheduled 67 variables 0% by backward subsumption
c [elim-10-2] eliminated 7 variables 0% in round 2 in 15013423 steps
c [elim-10-2] backward subsumption/strengthening limit 15013400
c [elim-10-2-1] backward checking 50 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 506023 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 3335 = 8% variables out of 43743 scheduled
c [bca-10] limit of 10000000 steps and 616852 added (scaled 2)
c [bca-10] 53347 out of 80818 literals actually usable 66%
c [bca-10] added 263 blocked clauses in 276785 steps
c [sweep-10] limit 12480727 penalty 0 = 0 + 0
c [sweep-10-1] 11849 pos 46.2% + 13814 neg 53.8% = 25663 sched 63.5% ret 14745
c [sweep-10-1] 12483354 steps 1286 queries 2040.24 avg class size
c [sweep-10-1] 27782 decisions 1283 SAT calls 32.35 avg env size
c [sweep-10-1] 16011 variables remain 40% (24392 retained 60%)
c [decomp-49] removed 72 variables
c [sweep-10-1] removed 72 vars (1 failed, 45 eqs, 21 impls)
c [sweep-10] removed 72 vars in TOTAL (1 rounds, 1285 queries)
c [sort-queue-14] sorted 40336 enqueued variables after 484665 conflicts
c [score-dist-14] active 0 (0%), one 27117 (67%), zero 13219 (33%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 4026 variables 9.1% (40336 remain 9%)
c [simplification-14] removed 27916 irredundant clauses 8.3% (307773 remain 24%)
c [simplification-14] maximum reduction of 9% = max (9%, 8%)
c [simplification-14] large reduction 9% >= 5% limit
c [simplification-14] next conflict interval 4846 = min (484665/100, 157497)
c [simplification-14] penalized conflict interval 4846 = 1 * 4846
c [simplification-14] hard conflict limit 499511 (soft 489511 + delta 10000)
c [simplification-14] new conflict limit 489511 (hard 499511)
c 
c [simplification-15] limit 489511 conflicts (hard 499511) hit after 490431 conflicts
c [quatres-11] found 44768 quaternary clauses 19% in total
c [quatres-11-1] removed 56 duplicate quaternary clauses
c [quatres-11-1] added 3 double-self-subsuming ternary resolvents
c [quatres-11-2] added 139 single-self-subsuming ternary resolvents
c [quatres-11-2] added 352 quaternary resolvents
c [ternres-11] limit 42097534 with penalty 0 = 0 + 0
c [ternres-11] 25 schedulable variables 0%
c [ternres-11] 4525 ternary resolvents (178 bin, 4347 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1315547 penalty 4 = 4 + 0
c [card-5] found 183 at-most-one constraints of average size 3.1
c [card-5] found 21 at-most-two constraints of average size 4.0
c [card-5] using previous limit 1315547 for elimination
c [card-5] 204 out of 204 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-50] removed 13 variables
c [simpleprobe-6] 64 schedulable variables 0%
c [simpleprobe-6] limit 168390138 penalty 0 = 0 + 0
c [decomp-51] removed 19 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 19 variables, found 1489 hbrs, 7 units
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 611 transitive binary clauses
c [transred-11] found 1 units
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 40302 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 555 variables 1% in round 1 in 238468796 steps
c [elim-11-1] backward subsumption/strengthening limit 238468700
c [elim-11-1-1] backward checking 1569 touched variables 4%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 1 clauses in 6545543 steps
c [elim-11-1] rescheduled 12 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 296513 steps
c [elim-11-2] backward subsumption/strengthening limit 296500
c [elim-11-2-1] backward checking 12 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 2 clauses in 222693 steps
c [elim-11-2] rescheduled 12 variables 0% by backward subsumption
c [elim-11-3] eliminated 1 variables 0% in round 3 in 764418 steps
c [elim-11-3] backward subsumption/strengthening limit 764400
c [elim-11-3-1] backward checking 15 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 0 and strengthened 0 clauses in 217352 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 557 = 1% variables out of 40302 scheduled
c [bca-11] limit of 10000000 steps and 611329 added (scaled 2)
c [bca-11] 51115 out of 79492 literals actually usable 64%
c [bca-11] added 100 blocked clauses in 270902 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 126292600 penalty 0 = 0 + 0
c [sweep-11-1] 6518 pos 41.5% + 9175 neg 58.5% = 15693 sched 39.5% ret 24052
c [sweep-11-1] 25260439 steps 6461 queries 797.65 avg class size
c [sweep-11-1] 97072 decisions 6492 SAT calls 20.94 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-52] removed 128 variables
c [sweep-11-1] removed 128 vars (1 failed, 138 eqs, 56 impls)
c [sweep-11-2] 14891 pos 37.6% + 24726 neg 62.4% = 39617 sched 100.0% ret 0
c [sweep-11-2] 43456500 steps 5779 queries 400.48 avg class size
c [sweep-11-2] 106991 decisions 5802 SAT calls 27.49 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-53] removed 162 variables
c [sweep-11-2] removed 162 vars (1 failed, 158 eqs, 54 impls)
c [sweep-11-3] 14843 pos 37.6% + 24612 neg 62.4% = 39455 sched 100.0% ret 0
c [sweep-11-3] 42327793 steps 5730 queries 304.87 avg class size
c [sweep-11-3] 106162 decisions 5744 SAT calls 27.62 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-54] removed 110 variables
c [sweep-11-3] removed 110 vars (1 failed, 118 eqs, 26 impls)
c [sweep-11] removed 400 vars in TOTAL (3 rounds, 17967 queries)
c [sort-queue-15] sorted 39345 enqueued variables after 490431 conflicts
c [score-dist-15] active 0 (0%), one 27481 (70%), zero 11864 (30%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 991 variables 2.5% (39345 remain 9%)
c [simplification-15] removed 3726 irredundant clauses 1.2% (304047 remain 24%)
c [simplification-15] maximum reduction of 2% = max (2%, 1%)
c [simplification-15] geometric conflict interval increment 52499 = 157497 / 3
c [simplification-15] new conflict interval 209996
c [simplification-15] penalized conflict interval 209996 = 1 * 209996
c [simplification-15] hard conflict limit 805425 (soft 700427 + delta 104998)
c [simplification-15] new conflict limit 700427 (hard 805425)
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 -  265.5   39345   304047    527725  108707  34648  6882    8   135   60   6%    900  -28    6    9   68%
c -  279.4   39345   304047    585164  119482  35794  6933   10   109   61   9%    972  -29   11    9  118%
c -  294.5   39345   304047    642761  131235  36875  6984    9    45   61  20%   1003  -57    9    9   93%
c i  298.3   39344   304047    657765  144872  37050  6992    9    57   90  16%   1007  -34    9    9  104%
c i  299.0   39343   304047    659868  146787  37077  6996   10    73   90  13%  -2759  -17   11    9  117%
c i  299.1   39202   304046    660032  146930  37079  6999   10    74   90  13%  -2838  -16   10    9  108%
c i  299.2   39199   304046    660442  147297  37088  7000   10    76   90  13%  -2983  -14   11    9  116%
c i  300.9   39190   304046    669806  155252  37210  7020    9   129   92   7%  -2757   35    8    9   92%
c i  301.7   39185   304046    675944  160672  37267  7031    9    95   92   9%  -2554    1    9    9   96%
c i  301.7   39169   304046    676258  160904  37271  7034    9    96   92   9%  -2562    1    9    9   95%
c i  303.3   39168   304046    683253  167069  37386  7060   10    83   93  12%  -2268  -11   11    9  118%
c i  303.6   39164   304046    683981  167708  37400  7063   10    82   93  12%  -2287  -12   11    9  118%
c i  305.0   39160   304046    690874  173895  37515  7090    9    47   93  19%  -2016  -44   11    9  117%
c -  307.0   39158   304046    698145  143016  37677  7116    9    40   84  23%  -1795  -46   11    9  118%
c i  308.3   39157   304046    702297  146729  37778  7128   10    42   90  23%  -1622  -41    9    9   94%
c i  309.0   39156   304046    704866  148970  37818  7140    9    36   90  26%  -1680  -46    6    9   63%
c i  309.0   39152   304046    704867  148970  37818  7140    9    36   90  26%  -1680  -46    6    9   63%
c i  310.8   39146   304046    711832  155399  37911  7156    9    26   91  33%  -1457  -50    7    9   78%
c i  311.9   39145   304046    715949  159073  37947  7165    9    23   91  37%  -1408  -50   11    9  121%
c i  312.8   39139   304046    718975  161772  37955  7170    8    18   91  46%  -1359  -53    6    9   64%
c i  312.9   39134   304046    719573  162289  37961  7172    8    17   92  48%  -1360  -54    6    9   67%
c i  312.9   39115   304046    719585  162296  37962  7174    8    17   92  48%  -1360  -54    6    9   65%
c i  313.0   39096   304046    719954  162578  37974  7180    8    16   92  49%  -1357  -54    6    9   69%
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.0   39018   304046    719965  162584  37974  7181    8    16   92  49%  -1357  -54    6    9   67%
c i  313.1   39017   304046    720114  162671  37981  7185    8    16   92  49%  -1356  -54    6    9   63%
c i  313.1   39015   304046    720138  162687  37985  7185    8    16   92  49%  -1356  -54    6    9   62%
c i  313.1   38970   304046    720188  162724  37988  7185    8    16   92  50%  -1356  -54    5    9   60%
c i  313.1   38968   304046    720212  162736  37990  7186    8    16   92  50%  -1355  -54    5    9   59%
c i  313.1   38948   304046    720232  162752  37991  7187    8    16   92  50%  -1355  -54    5    9   57%
c 0  313.1   38752   304046    720232  162752  37991  7187    8    16   92  50%  -1355  -54    5    9   57%
c 
s UNSATISFIABLE
c
c bate: 816 basic ate = 319 trn 39% + 497 lrg 61% in 4 updates
c bcas: 11 count, 1451 added (911 skipped), 3082416 steps
c bkwd: tried 462434 clauses, 922588 lits, 2.00 lits/clause
c bkwd: checked 117268502 occs, 253.59 occs/clause, 127.11 occs/lit
c bkwd: subsumed 2 binary, 11 ternary, 1032 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 2088 large (0% self)
c blkd: 6 bces, 39156 removed, 15863918 resolutions, 41615106 steps
c blkd: 11240 blocking literals 1%, 4254 pure
c bump: 680203 bumped seen, 26155651 lits 38.5 on average
c card: 5 count, 0 units, 0 am1, 16016059 steps
c card: 1 rescheduled, 4 eliminated, 211 resolved, 4317 subsumed
c card: 610 at-most-one constraints found, average size 3.15
c card: 610 at-most-one constraints used 100%, average size 3.15
c card: 21 at-most-two constraints found, average size 4.05
c card: 21 at-most-two constraints used 100%, average size 4.05
c cces: 4 cces, 14685 eliminated, 14481 ate 99%, 204 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 4305712 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 111 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 54 decompositions, 4184 equivalent 1%
c deco: 1 decision-only clauses 0%, 59% reduction
c decs: 10124082 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 11 elims, 380828 eliminated 88%, 426 pure 0%
c elms: 20 rounds, 1.8 rounds/bve
c elms: 356100 small 94%, 20048 large 5%
c elms: 490518 tried small, 356100 succeeded 73%, 134418 failed 27%
c elms: 13150 subsumed, 9368 strengthened, 1636 blocked
c elms: 14912449 copies, 26567326 resolutions, 9804087 ipos
c elms: 14841769 subchks, 12885367 strchks
c gaus: 5 extractions, 70710 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 1 binary and 4 ternary equations
c gaus: 0 gc, 19626418 steps, 9813209 extr 50%, 9890090 elim 50%
c glue: 8.4 orig avg, 8.4 real avg, 1.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 29649 = 5132 simple 17% + 22278 trn 75% + 2239 lrg 8%, 2469 sub 8%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 680203 clauses, 19.5 length
c lrnd: 13242964 lits = 17210081 orig - 3967117 removed 23%
c lrnd: 219066 uips 32%, 292952 flips 43%
c mins: 643585 mins 95%, 978 bin 0%, 35639 size 5%
c mins: 17604436 poisoned searches, 2826656 hits, 16% hit rate
c mins: 31126152 used twice searches, 2680785 hits, 9% hit rate
c move: moved 26312, 5729 bin 22%, 20583 trn 78%
c otfs: 48210 driving 51%, 45528 restarting 49%
c otfs: str 93738, 93333 red 100%, 405 irr 0%
c otfs: str 93738, 0 bin 0%, 1055 trn 1%, 92683 lrg 99%
c otfs: sub 1219, 1211 red 99%, 8 irr 1%
c otfs: sub 1219, 0 bin 0%, 156 trn 13%, 1063 lrg 87%
c phas: 7 computed, 189759 set, 59972 pos (32%), 129787 neg (68%)
c prbs: 5 basic, 861144 probed, 545 failed, 48 lifted
c prbs: 6 simple, 702277 probed, 61 failed, 271 eqs
c prbs: 5 treelook, 844 probed, 14 failed, 0 lifted
c prom: 90745 locked 19% out of 490181 tried
c prps: 439179976 props, 42 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 11 count, 10263 quat, 2996 self1, 51 self2, 524 dup
c queu: 15 sorted, 10124082 next (144 steps 0.00)
c queu: 27505204 enq (27505173 steps 1.00), 26155651 deq 95%
c redc: 24774 clauses 8%, 300901 tried 42%, 17 sat 0%
c redc: 32905 lits 1%, 2707152 tried 16%, 17 sat 0%
c redc: 840 times jump level reduced, 7.4 levels on average
c reds: 10 count, 72023.2 conflicts per reduce
c reds: 0 memlim 0%, 10 arith 100%
c reds: 269338 collected 69%, 118286 retired 31%
c rmbd: 2377 removed, 1281 red 54%
c rsts: 23594 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 15 count, 12 confs 80%, 0 vars 0%
c simp: 1 its 7%, 1 bin 7%, 1 trns 7%
c subl: 680203 count (281153 tried 0.4), 58592 sub out of 667492 (8.8%)
c swps: 11 count, 14 rounds, 29850 queries (2132.1/round)
c swps: 29888 sat calls, 742 unsat (0.3% success rate)
c swps: 511343 decisions 17.1, 8181 conflicts 0.3
c swps; 989.9 avg class size, 25.4 avg environment size
c swps: 6 failed, 281 impls, 695 equivs
c swp0: 9946 type 0 queries, 1041 unsat (10.5%), 9831 sat (98.8%)
c swp1: 19904 type 1 queries, 5591 unsat (28.1%), 19324 sat (97.1%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 21608965 calls to obtain time
c tops: 9837 fixed 2%, 98 its, 7349.31 confs/it
c trds: 11 transitive reductions, 4753 removed, 9 failed
c trds: 1078819 nodes, 559531 edges, 8499834 steps
c trim: 800901 words, 3.1 MB
c trnr: 11 count, 3482 bin, 62973 trn, 244012987 steps
c unhd: 12 count, 15 rounds, 56665813 steps
c unhd: 2764 non-trivial sccs of average size 2.6
c unhd: 21 units, 21 bin, 0 trn, 0 lrg
c unhd: 153 failed, 139 stamp, 0 lits, 4 bin, 3 trn, 0 lrg
c unhd: 27115 tauts, 278 bin 1%, 14903 trn 55%, 8352 lrg 31%
c unhd: 27115 tauts, 3582 stamp 13%, 22182 red 82%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 203943 str, 21 bin 0%, 2283 trn 1%, 201639 lrg 99%, 164137 red 80%
c vars: 38752 remaining 9% and 394849 removed 91% out of 433601
c vars: 9837 fixed 2%, 380828 eliminated 88%, 4184 equivalent 1%
c vsts: 6229931812 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 14.1 search visits per propagation, 8318.3 per conflict
c wchs: 1426263564 pushed, 51967006 enlarged, 180 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         677755        269338        118286      29930079       2879597        300765
c 
c  0 0        201888  30      7059   3         0   0  23242405  78<  1674589  58    162339  54     4.0
c  1 5         73270  11     36593  14     15674  13   2675180   9    331267  12<    41297  14<    0.6
c  2 6        155985  23<    88241  33     34937  30   2567202   9    473749  16     54254  18     1.5
c  3 9        142827  21     80603  30<    35161  30<  1076471   4    277512  10     29695  10     2.1
c  4 14        70072  10     39396  15     20320  17    279465   1     90690   3      9844   3     1.4
c  5 21        24086   4     12824   5      8232   7     72197   0     24180   1      2525   1     0.7
c  6 30         6905   1      3434   1      2715   2     12454   0      5668   0       623   0     0.3
c  7 41         1882   0       842   0       837   1      2803   0      1264   0       130   0     0.1
c  8 54          541   0       233   0       257   0      1489   0       501   0        40   0     0.0
c  9 69          175   0        69   0        88   0       255   0       114   0        15   0     0.0
c 10 86          119   0        42   0        62   0       153   0        61   0         3   0     0.0
c 11 126           5   0         2   0         3   0         5   0         2   0         0   0     0.0
c 
c avg                  1.9           2.6           2.9           0.4           0.9           1.0
c std                  1.6           1.2           1.3           0.9           1.3           1.3
c 
c   37.365  12% elim
c   21.437   7% sweep
c   17.510   6% probe
c    7.286   2% decide
c    6.741   2% cce
c    5.500   2% unhide
c    4.009   1% block
c    2.790   1% quatres
c    2.552   1% bca
c    2.459   1% gauss
c    2.337   1% ternres
c 
c    3.240 < 1% rest (below)
c 
c    2.073   1% bump
c    0.738   0% transred
c    0.429   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    7.561   2% preprocessing     7%
c  103.675  33% inprocessing     93%
c ==================================
c  111.236  36% simplifying
c  201.874  64% search
c ==================================
c  313.118 100% all
c 
c        720232 conflicts,        2300.2 confs/sec
c          8749 ternaries,          82.3 confs/ternary
c          1263 binaries,          570.3 confs/binary
c            98 iterations,       7349.3 confs/iteration
c 
c            10 reductions,          0.0 redus/sec,  72023.2 confs/reduction
c         23594 restarts,           75.4 rests/sec,     30.5 confs/restart
c      10124082 decisions,       32333.1 decis/sec,     14.1 decis/conflict
c     439179976 propagations,  1402603.0 props/sec,     43.4 props/decision
c 
c 313.1 seconds, 119.1 MB
c launch: done
