c launch: /data/cnf/sc2014/app/ACG-15-10p0.cnf.bz2
c host: atom20
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/ACG-15-10p0.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/ACG-15-10p0.cnf.bz2
c no embedded options
c found 'p cnf 262253 1131732' header
c read 262253 variables, 1131732 clauses, 2644763 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 252004 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  252004  1120813         0       0      0     0    0     0   61   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 5064 at-most-one constraints of average size 5.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 5064 out of 5064 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 54025 variables
c [simpleprobe-1] all 208228 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 417 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 417 variables, found 11185 hbrs, 20 units
c [unhide-1] limit 53492 based on 855883 irredundant clauses
c [unhide-1-1] 6 units, 1919 failed, 14578 tauts, 0 hbrs, 5999 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 200713 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 59076 not tried 29% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 85192 = 42% variables out of 200713 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 676017 negative 99.3% of 680813 except 4796 0.7%
c [phase-count-1] 547738 positive 80.5% of 680813 except 133075 19.5%
c [phase-count-1] less non-negative clauses 4796 than limit 68000 (10.0%)
c [phase-count-1] non-pos/non-neg = 133075/4796 = 27.75 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 115521 negative 100%
c [sort-queue-1] sorted 115521 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 115521 (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 98588 variables 46.0% (115521 remain 46%)
c [simplification-1] removed 440000 irredundant clauses 39.3% (680813 remain 61%)
c [simplification-1] maximum reduction of 46% = max (46%, 39%)
c [simplification-1] large reduction 46% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.4  115520   680813        67      58      3  5533    0     8   52   3%      0    8    4    0 22574%
c i    5.5  115445   680813       130      94     15  5542    0    10   52   4%      0    9    5    0 19029%
c i    5.5  115072   680813       141      99     18  5543    0    10   52   4%      0   10    5    0 18459%
c i    5.9  114945   680813       354     275     38  5556    1    15   52   4%      0   15    5    0 12487%
c i    6.1  114892   680813       580     441     62  5581    1    18   52   5%      1   18    6    0 9009%
c i    6.5  114579   680813       898     680    100  5615    2    24   52   7%      1   23    9    0 8454%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 1090 variables
c [simpleprobe-2] all 114431 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 75 variables
c [simpleprobe-2] 112482 variables remain 98% (1874 retained 2%)
c [simpleprobe-2] removed 75 variables, found 4098 hbrs, 9 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 69959 literals 31%
c [treelook-1] scheduling used 316209 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 362207 steps
c [treelook-1] 68851 literals remain 30%
c [treelook-1] 66926 variables remain to probed next time 59%
c [decomp-5] removed 127 variables
c [treelook-1] removed 1234 variables, found 2565 hbrs
c [basicprobe-1] limit 5327616 based on 665952 irredundant clauses
c [basicprobe-1-0] 32779 probes remain 30% after last round
c [basicprobe-1-0] 23 units = 23 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3473 variables, found 16751 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 13 units, 2167 failed, 2386 tauts, 0 hbrs, 16962 literals
c [elim-2] 55085 variables 52% will be scheduled this time
c [elim-2] scheduled 55085 variables 52%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 10981 not tried 10% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 1541 = 3% variables out of 55085 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 599938 negative 99.2% of 604733 except 4795 0.8%
c [phase-count-2] 481117 positive 79.6% of 604733 except 123616 20.4%
c [phase-count-2] less non-negative clauses 4795 than limit 60400 (10.0%)
c [phase-count-2] non-pos/non-neg = 123616/4795 = 25.78 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 9408 negative 100%
c [sort-queue-2] sorted 94479 enqueued variables after 1001 conflicts
c [score-dist-2] active 10625 (10%), one 0 (0%), zero 94479 (90%)
c [score-dist-2] max exp 766, different 218 (28%)
c [score-dist-2] median active exp 706, avg 691.6
c [simplification-2] removed 9466 variables 8.3% (105104 remain 42%)
c [simplification-2] removed 76080 irredundant clauses 11.2% (604733 remain 54%)
c [simplification-2] maximum reduction of 11% = max (8%, 11%)
c [simplification-2] large reduction 11% >= 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 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
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.4  105103   604733      1110     818    110 20136    2    28   47   7%      1   28   10    0 7127%
c i   10.5  105070   604733      1205     899    118 20139    2    30   48   7%      1   30   10    0 6235%
c i   10.5  104680   604733      1213     904    119 20140    2    31   48   7%      1   30    9    0 6135%
c i   10.7  104608   604733      1315     977    134 20151    2    34   48   7%      1   34   10    0 5997%
c i   10.9  104580   604733      1442    1078    147 20162    3    39   48   7%      1   39   10    0 5397%
c i   11.0  103796   604733      1471    1101    151 20163    3    39   48   7%      1   39   10    0 4985%
c i   11.1  103435   604733      1505    1132    153 20163    3    41   48   7%      1   41   10    0 4987%
c i   11.6  103395   604733      1738    1324    166 20185    4    51   48   7%      1   50   13    0 5120%
c i   11.7  103181   604733      1768    1350    167 20187    4    52   48   7%      1   52   13    0 5082%
c i   11.8  103180   604733      1813    1393    168 20187    4    56   48   7%      1   55   14    0 5071%
c 
c [simplification-3] limit of 16 iterations hit after 16 iterations
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4740 at-most-one constraints of average size 4.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4740 out of 4740 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 3105 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 65529 literals 32%
c [treelook-2] scheduling used 303586 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 731314 steps
c [treelook-2] 65513 literals remain 32%
c [treelook-2] 45601 variables remain to probed next time 45%
c [decomp-7] removed 6 variables
c [treelook-2] removed 18 variables, found 5038 hbrs
c [unhide-3] limit 130215 with penalty 0 = 0 + 0
c [unhide-3-3] 13 units, 904 failed, 8163 tauts, 0 hbrs, 6618 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 99876 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 19323 not tried 19% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 4418 = 4% variables out of 99876 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 553326 negative 99.2% of 557954 except 4628 0.8%
c [phase-count-3] 442294 positive 79.3% of 557954 except 115660 20.7%
c [phase-count-3] less non-negative clauses 4628 than limit 55700 (10.0%)
c [phase-count-3] non-pos/non-neg = 115660/4628 = 24.99 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 2085 negative 100%
c [sort-queue-3] sorted 70643 enqueued variables after 1813 conflicts
c [score-dist-3] active 24815 (26%), one 0 (0%), zero 70643 (74%)
c [score-dist-3] max exp 978, different 350 (36%)
c [score-dist-3] median active exp 933, avg 905.7
c [simplification-3] removed 7715 variables 7.5% (95458 remain 38%)
c [simplification-3] removed 46779 irredundant clauses 7.7% (557954 remain 50%)
c [simplification-3] maximum reduction of 8% = max (7%, 8%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3002 (hard 13001)
c [simplification-3] 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   15.0   95457   557954      1815    1332    156 20278    4    56   45   7%      1   55   14    0 5035%
c i   15.0   95443   557954      1818    1334    156 20278    4    56   45   7%      1   55   14    0 5029%
c i   15.1   95436   557954      1879    1376    164 20286    4    57   46   7%      1   56   12    0 4282%
c i   15.1   95323   557954      1890    1380    168 20288    4    57   46   7%      1   56   12    0 4133%
c i   15.3   95318   557954      1963    1437    172 20296    4    59   46   7%      1   59   12    0 4031%
c i   15.3   95245   557954      1966    1438    173 20296    4    59   46   7%      1   59   12    0 3988%
c i   15.3   95239   557954      2029    1483    177 20304    4    60   46   7%      1   59   11    0 3682%
c i   15.4   95223   557954      2052    1505    177 20304    4    61   46   7%      1   60   11    0 3539%
c i   15.4   95222   557954      2069    1520    177 20304    4    61   46   7%      1   60   12    0 3923%
c i   15.6   95219   557954      2212    1642    186 20312    4    66   46   7%      1   65   13    0 3704%
c i   15.6   95182   557954      2228    1655    187 20312    5    66   46   7%      1   65   15    0 4194%
c i   15.6   95181   557954      2240    1656    190 20315    5    66   46   7%      1   65   16    0 4309%
c i   15.7   94971   557954      2320    1717    198 20321    5    67   46   8%      1   66   18    0 4588%
c i   15.9   94956   557954      2424    1801    204 20330    6    71   46   8%      1   70   21    0 4897%
c i   16.5   94790   557954      2795    2118    227 20354    6    81   46   8%      2   79   17    1 3326%
c i   16.5   94784   557954      2813    2132    229 20355    6    84   46   8%      2   82   17    1 3233%
c i   16.5   94783   557954      2823    2139    230 20356    6    84   46   8%      2   82   16    1 3155%
c i   16.6   94773   557954      2853    2163    233 20358    6    86   46   8%      1   84   15    1 2930%
c i   16.9   94677   557954      2999    2280    240 20376    7    93   46   7%      1   91   15    1 2678%
c i   16.9   94665   557954      3011    2288    241 20378    7    94   46   7%      1   92   15    1 2683%
c 
c [simplification-4] limit of 250 binary hit after 250 binaries
c [decomp-8] removed 992 variables
c [basicprobe-2] limit 5593854 penalty 0 = 0 + 0
c [basicprobe-2-0] 29098 probes remain 31% after last round
c [basicprobe-2-0] 30 units = 30 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1156 variables, found 14145 hbrs
c [unhide-4] limit 223754 with penalty 0 = 0 + 0
c [unhide-4-4] 5 units, 1165 failed, 4039 tauts, 0 hbrs, 7185 literals
c [elim-4] 10592 variables 12% will be scheduled this time
c [elim-4] scheduled 10592 variables 12%
c [elim-4] boosting limit by 20
c [elim-4] limit of 447508380 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 18972919 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 10592 scheduled
c [phase-count-4] 525571 negative 99.1% of 530200 except 4629 0.9%
c [phase-count-4] 419191 positive 79.1% of 530200 except 111009 20.9%
c [phase-count-4] less non-negative clauses 4629 than limit 53000 (10.0%)
c [phase-count-4] non-pos/non-neg = 111009/4629 = 23.98 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 468 negative 100%
c [sort-queue-4] sorted 57256 enqueued variables after 3011 conflicts
c [score-dist-4] active 34677 (38%), one 0 (0%), zero 57256 (62%)
c [score-dist-4] max exp 791, different 549 (69%)
c [score-dist-4] median active exp 726, avg 639.4
c [simplification-4] removed 2634 variables 2.8% (91933 remain 36%)
c [simplification-4] removed 27754 irredundant clauses 5.0% (530200 remain 47%)
c [simplification-4] maximum reduction of 5% = max (3%, 5%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3014 (hard 13001)
c [simplification-4] new binary interval 1000
c 
c [simplification-5] limit 3014 conflicts (hard 13001) hit after 3014 conflicts
c [quatres-1] found 35844 quaternary clauses 41% in total
c [quatres-1-2] added 7 single-self-subsuming ternary resolvents
c [quatres-1-2] added 30 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 91933 free variables schedulable
c [ternres-1] 1594 ternary resolvents (4 bin, 1590 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 676 xors of average arity 2.1
c [gauss-1] connected 1397 occurrences of 1082 variables (average 1.3)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 647 variables
c [gauss-1] exported 0 unary, 1 binary and 0 ternary equations
c [simpleprobe-3] 89777 schedulable variables 98%
c [simpleprobe-3] limit 4487896 penalty 0 = 0 + 0
c [decomp-11] removed 1515 variables
c [simpleprobe-3] 55085 variables remain 61% (34686 retained 39%)
c [simpleprobe-3] removed 1515 variables, found 12956 hbrs, 239 units
c [unhide-5] limit 224394 with penalty 0 = 0 + 0
c [unhide-5-5] 3 units, 295 failed, 8021 tauts, 0 hbrs, 2246 literals
c [transred-1] limit 1121974 with penalty 0 = 0 + 0
c [transred-1] removed 107 transitive binary clauses
c [transred-1] found 4 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 89052 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 9229 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 8 clauses out of 351 (2%) of length 10
c [cce-1-1] eliminated 124 clauses out of 1925 (6%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 132 large clauses in 30000007 steps
c [cce-1-1] allowing another 15000003 steps for small clauses
c [cce-1-1] scheduling 318326 clauses = 269619 binary + 48707 ternary
c [cce-1-1] tried to eliminate 316 small clauses 0%
c [cce-1-1] eliminated 63 binary clauses 0%
c [cce-1-1] eliminated 22 ternary clauses 0%
c [cce-1-1] eliminated 85 small clauses 0%
c [cce-1-1] eliminated 85 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 217 covered clauses in round 1
c [cce-1] eliminated 217 covered clauses in TOTAL during 1 rounds
c [cce-1] 217 < 1/100 * 498034 = 4980 considered unsuccessful
c [bca-1] limit of 10000000 steps and 996134 added (scaled 2)
c [bca-1] 161099 out of 178106 literals actually usable 90%
c [bca-1] added 165 blocked clauses in 456823 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 4006 pos 4.5% + 85046 neg 95.5% = 89052 sched 100.0% ret 0
c [sweep-1-1] 1044664 steps 14 queries 24058.21 avg class size
c [sweep-1-1] 192 decisions 12 SAT calls 90.75 avg env size
c [sweep-1-1] 89019 variables remain 100% (33 retained 0%)
c [decomp-12] removed 282 variables
c [sweep-1-1] removed 282 vars (0 failed, 1 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 282 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-5] 492647 negative 99.1% of 497254 except 4607 0.9%
c [phase-count-5] 398361 positive 80.1% of 497254 except 98893 19.9%
c [phase-count-5] less non-negative clauses 4607 than limit 49700 (10.0%)
c [phase-count-5] non-pos/non-neg = 98893/4607 = 21.47 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 463 negative 100%
c [sort-queue-5] sorted 54119 enqueued variables after 3014 conflicts
c [score-dist-5] active 34651 (39%), one 0 (0%), zero 54119 (61%)
c [score-dist-5] max exp 792, different 550 (69%)
c [score-dist-5] median active exp 726, avg 639.5
c [simplification-5] removed 3163 variables 3.4% (88770 remain 35%)
c [simplification-5] removed 32946 irredundant clauses 6.2% (497254 remain 44%)
c [simplification-5] maximum reduction of 6% = max (3%, 6%)
c [simplification-5] large reduction 6% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 15014 (soft 5014 + delta 10000)
c [simplification-5] new conflict limit 5014 (hard 15014)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   22.3   88769   497254      3020    2307   1319 50702    7    94   44   7%      1   92   15    1 2635%
c i   22.7   88492   497254      3266    2500   1335 50724   10   107   44   9%      2  104   41    1 5298%
c i   22.7   88486   497254      3302    2533   1336 50725   10   107   44   9%      1  105   37    1 4775%
c i   22.8   88482   497254      3307    2537   1336 50725   10   107   44   9%      1  105   36    1 4697%
c i   22.8   88475   497254      3308    2537   1336 50725   10   107   44   9%      1  105   36    1 4679%
c i   22.8   88450   497254      3376    2598   1337 50730   10   108   44   9%      1  105   36    1 4398%
c i   23.1   88449   497254      3595    2788   1344 50748   10   110   44  10%      1  107   25    1 2929%
c i   23.2   88448   497254      3674    2860   1345 50751   11   111   44  10%      1  108   23    1 2592%
c i   23.2   88439   497254      3676    2861   1345 50751   11   111   44  10%      1  108   23    1 2574%
c i   23.3   88432   497254      3785    2959   1351 50753   11   114   44  10%      1  110   27    1 2889%
c i   23.4   88404   497254      3859    3020   1354 50760   11   116   44  10%      1  113   24    1 2539%
c i   23.4   88393   497254      3862    3020   1354 50762   11   116   44  10%      1  113   24    1 2510%
c i   23.4   88371   497254      3864    3020   1355 50762   11   116   44  10%      1  113   24    1 2491%
c i   23.5   88244   497254      3910    3050   1360 50770   11   116   44  10%      1  113   21    1 2146%
c i   23.9   88174   497254      4124    3206   1380 50800   11   123   44   9%      1  119   18    1 1824%
c i   23.9   88164   497254      4125    3206   1380 50800   11   123   44   9%      1  119   18    1 1817%
c i   23.9   88150   497254      4131    3206   1381 50801   11   123   44   9%      1  119   18    1 1797%
c i   23.9   88122   497254      4135    3209   1381 50801   11   123   44   9%      1  119   18    1 1772%
c i   24.2   88108   497254      4309    3352   1393 50817   13   130   45  10%      1  126   30    1 2679%
c i   24.2   88106   497254      4341    3376   1397 50820   13   133   45  10%      1  129   29    1 2594%
c i   24.4   88105   497254      4404    3432   1398 50821   13   136   45   9%      1  132   29    1 2508%
c i   24.4   88092   497254      4414    3441   1398 50821   13   138   45   9%      1  133   30    1 2583%
c i   24.6   88088   497254      4564    3571   1404 50832   14   138   45  10%      1  133   28    1 2328%
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   24.6   88080   497254      4577    3578   1409 50832   14   139   45  10%      1  134   28    1 2272%
c i   24.7   88079   497254      4614    3610   1410 50834   14   141   45  10%      1  136   27    1 2226%
c i   24.8   88076   497254      4708    3690   1415 50841   14   142   45  10%      1  137   25    1 1974%
c i   25.1   87216   497254      4854    3801   1427 50862   14   147   45   9%      1  142   20    1 1572%
c i   25.1   87202   497254      4855    3801   1427 50862   14   147   45   9%      1  142   20    1 1566%
c i   25.1   87189   497254      4865    3808   1428 50863   14   147   45   9%      1  142   21    1 1641%
c i   25.1   87179   497254      4866    3808   1428 50863   14   147   45   9%      1  142   21    1 1635%
c i   25.2   87164   497254      4928    3859   1432 50868   14   152   45   9%      1  146   25    1 1869%
c i   25.3   87159   497254      4969    3896   1433 50869   14   152   45   9%      1  146   24    1 1783%
c i   25.3   87147   497254      5007    3914   1444 50877   14   152   45   9%      1  146   22    1 1644%
c 
c [simplification-6] limit 5075 conflicts (hard 15014) hit after 5078 conflicts
c [quatres-2] found 30848 quaternary clauses 38% in total
c [quatres-2-2] added 6 single-self-subsuming ternary resolvents
c [quatres-2-2] added 46 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 87139 free variables schedulable
c [ternres-2] 42 ternary resolvents (0 bin, 42 trn)
c [ternres-2] 29523 variables remain 34% (57616 retained 66%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2482 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2482 out of 2482 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 146 xors of average arity 2.3
c [gauss-2] connected 335 occurrences of 211 variables (average 1.6)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [decomp-13] removed 88 variables
c [gauss-2] exported 0 unary, 1 binary and 0 ternary equations
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 69352 literals 40%
c [treelook-3] scheduling used 361806 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 300137 steps
c [treelook-3] 69344 literals remain 40%
c [treelook-3] 35777 variables remain to probed next time 41%
c [treelook-3] removed 3 variables, found 2002 hbrs
c [unhide-6] limit 374175 with penalty 0 = 0 + 0
c [unhide-6-6] 5 units, 483 failed, 4300 tauts, 0 hbrs, 7309 literals
c [transred-2] limit 1870877 with penalty 0 = 0 + 0
c [transred-2] removed 157 transitive binary clauses
c [transred-2] found 7 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 86155 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 746 blocked clauses
c [block-2] 746 < 1/100 * 489024 = 4890 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 86155 variables 100%
c [elim-5] limit of 18708775 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 13336 not tried 15% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 3287 = 4% variables out of 86155 scheduled
c [bca-2] limit of 10000000 steps and 954022 added (scaled 2)
c [bca-2] 146073 out of 165738 literals actually usable 88%
c [bca-2] added 82 blocked clauses in 408722 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 3975 pos 4.8% + 78864 neg 95.2% = 82839 sched 100.0% ret 29
c [sweep-2-1] 1004845 steps 10 queries 24215.60 avg class size
c [sweep-2-1] 48 decisions 8 SAT calls 65.88 avg env size
c [sweep-2-1] 82828 variables remain 100% (40 retained 0%)
c [decomp-16] removed 9 variables
c [sweep-2-1] removed 9 vars (0 failed, 1 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 9 vars in TOTAL (1 rounds, 9 queries)
c [phase-count-6] 472137 negative 99.0% of 476704 except 4567 1.0%
c [phase-count-6] 379854 positive 79.7% of 476704 except 96850 20.3%
c [phase-count-6] less non-negative clauses 4567 than limit 47600 (10.0%)
c [phase-count-6] non-pos/non-neg = 96850/4567 = 21.21 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 141 negative 100%
c [sort-queue-6] sorted 48445 enqueued variables after 5078 conflicts
c [score-dist-6] active 34414 (42%), one 4129 (5%), zero 44316 (53%)
c [score-dist-6] max exp 834, different 604 (72%)
c [score-dist-6] median active exp 731, avg 631.4
c [simplification-6] removed 4280 variables 4.9% (82859 remain 33%)
c [simplification-6] removed 20550 irredundant clauses 4.1% (476704 remain 43%)
c [simplification-6] maximum reduction of 5% = max (5%, 4%)
c [simplification-6] large reduction 5% >= 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 17078 (soft 7078 + delta 10000)
c [simplification-6] new conflict limit 7078 (hard 17078)
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   29.8   82858   476704      5297    3849   1231 45161   14   155   44   9%      1  148   18    1 1275%
c i   29.8   82834   476704      5298    3849   1231 45161   14   154   44   9%      1  148   18    1 1270%
c i   29.8   82827   476704      5304    3854   1231 45161   14   155   44   9%      1  149   19    1 1372%
c i   29.9   82810   476704      5359    3899   1236 45165   14   160   44   9%      1  154   19    1 1318%
c i   30.0   82801   476704      5411    3949   1237 45165   15   163   44   9%      1  157   23    1 1569%
c i   30.2   82800   476704      5604    4114   1249 45173   16   169   44   9%      1  162   29    2 1867%
c i   30.2   82799   476704      5605    4114   1249 45173   16   168   44   9%      1  161   29    2 1860%
c i   30.2   82786   476704      5606    4114   1249 45173   16   168   44   9%      1  161   29    2 1853%
c i   30.4   82772   476704      5718    4220   1249 45174   16   168   44  10%      1  161   36    2 2198%
c i   30.4   82763   476704      5729    4228   1250 45175   16   168   44  10%      1  161   35    2 2140%
c i   30.6   82759   476704      5889    4371   1259 45181   17   170   44  10%      1  162   28    2 1703%
c i   30.9   82748   476704      6013    4470   1266 45193   17   179   45   9%      1  171   28    2 1653%
c i   31.1   82745   476704      6151    4586   1276 45202   18   185   45  10%      1  177   33    2 1817%
c i   31.4   82717   476704      6336    4737   1285 45219   19   194   45  10%      1  185   36    2 1889%
c i   31.4   82709   476704      6378    4774   1288 45219   19   194   45  10%      1  185   35    2 1805%
c i   31.6   82708   476704      6513    4891   1290 45222   19   193   45  10%      1  184   36    2 1806%
c i   31.8   82703   476704      6607    4970   1295 45230   20   202   45  10%      1  192   34    2 1650%
c i   31.8   82699   476704      6622    4984   1295 45230   20   203   45  10%      1  193   33    2 1624%
c i   32.2   82696   476704      6899    5223   1313 45238   20   204   45  10%      1  194   32    2 1459%
c i   32.3   82695   476704      7003    5315   1319 45240   21   205   45  10%      1  194   29    2 1316%
c i   32.4   82444   476704      7033    5333   1322 45246   20   205   45  10%      1  194   27    2 1209%
c i   32.4   82427   476704      7036    5335   1322 45246   20   205   45  10%      1  194   26    2 1196%
c i   32.4   82426   476704      7054    5349   1323 45248   20   204   45  10%      1  193   26    2 1163%
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.4   82422   476704      7066    5358   1324 45249   20   205   45  10%      1  194   26    2 1167%
c i   32.5   82322   476704      7097    5380   1327 45253   21   207   45  10%      1  196   28    2 1253%
c i   32.5   82321   476704      7099    5381   1327 45253   21   207   45  10%      1  196   28    2 1244%
c 
c [simplification-7] limit 7117 conflicts (hard 17078) hit after 7118 conflicts
c [quatres-3] found 32555 quaternary clauses 40% in total
c [quatres-3-2] added 14 single-self-subsuming ternary resolvents
c [quatres-3-2] added 19 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 27926 schedulable variables 34%
c [ternres-3] 998 ternary resolvents (2 bin, 996 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 108 xors of average arity 2.4
c [gauss-3] connected 262 occurrences of 188 variables (average 1.4)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [decomp-17] removed 84 variables
c [gauss-3] exported 0 unary, 2 binary and 0 ternary equations
c [basicprobe-3] limit 12978212 penalty 0 = 0 + 0
c [basicprobe-3-0] 25935 probes remain 32% after last round
c [basicprobe-3-0] 50 units = 50 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 997 variables, found 26413 hbrs
c [bate-1] eliminated 31 asymmetric tautologies during probing
c [unhide-7] limit 519128 with penalty 0 = 0 + 0
c [unhide-7-7] 3 units, 138 failed, 7831 tauts, 0 hbrs, 10589 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 125 transitive binary clauses
c [transred-3] found 3 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7500002 steps for small clauses
c [cce-2-1] scheduling 333012 clauses = 243663 binary + 89349 ternary
c [cce-2-1] tried to eliminate 138 small clauses 0%
c [cce-2-1] eliminated 20 binary clauses 0%
c [cce-2-1] eliminated 24 ternary clauses 0%
c [cce-2-1] eliminated 44 small clauses 0%
c [cce-2-1] eliminated 2412 small clauses in 15000002 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2412 covered clauses in round 1
c [cce-2] eliminated 2412 covered clauses in TOTAL during 1 rounds
c [cce-2] 2412 < 1/100 * 461787 = 4617 considered unsuccessful
c [elim-6] 13187 variables 16% will be scheduled this time
c [elim-6] scheduled 13187 variables 16%
c [elim-6] limit of 51912848 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 5 variables 0% in round 1 in 19440044 steps
c [elim-6-1] backward subsumption/strengthening limit 19440000
c [elim-6-1-1] backward checking 1433 touched variables 2%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 23 and strengthened 2 clauses in 364523 steps
c [elim-6-1] rescheduled 75 variables 0% by backward subsumption
c [elim-6-2] eliminated 1 variables 0% in round 2 in 42519 steps
c [elim-6-2] backward subsumption/strengthening limit 42500
c [elim-6-2-1] backward checking 10 touched variables 0%
c [elim-6-2-1] incomplete backward checking 0 remain 0%
c [elim-6-2] subsumed 2 and strengthened 0 clauses in 42501 steps
c [elim-6-2] rescheduled 6 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 2135 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 15 = 0% variables out of 13187 scheduled
c [elim-6] 15 < 1/100 * 13187 = 131 considered unsuccessful
c [bca-3] limit of 10000000 steps and 917157 added (scaled 2)
c [bca-3] 139765 out of 161788 literals actually usable 86%
c [bca-3] added 39 blocked clauses in 380651 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 3873 pos 4.8% + 76981 neg 95.2% = 80854 sched 100.0% ret 39
c [sweep-3-1] 1150948 steps 11 queries 20257.45 avg class size
c [sweep-3-1] 197 decisions 10 SAT calls 92.20 avg env size
c [sweep-3-1] 80813 variables remain 100% (74 retained 0%)
c [decomp-19] removed 211 variables
c [sweep-3-1] removed 211 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 211 vars in TOTAL (1 rounds, 10 queries)
c [phase-count-7] 453246 negative 99.0% of 457809 except 4563 1.0%
c [phase-count-7] 364904 positive 79.7% of 457809 except 92905 20.3%
c [phase-count-7] less non-negative clauses 4563 than limit 45700 (10.0%)
c [phase-count-7] non-pos/non-neg = 92905/4563 = 20.36 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 71 negative 100%
c [sort-queue-7] sorted 46264 enqueued variables after 7118 conflicts
c [score-dist-7] active 34418 (43%), one 6561 (8%), zero 39703 (49%)
c [score-dist-7] max exp 871, different 644 (74%)
c [score-dist-7] median active exp 778, avg 677.7
c [simplification-7] removed 1629 variables 2.0% (80682 remain 32%)
c [simplification-7] removed 18895 irredundant clauses 4.0% (457809 remain 41%)
c [simplification-7] maximum reduction of 4% = max (2%, 4%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 4000
c [simplification-7] penalized conflict interval 4000 = 1 * 4000
c [simplification-7] hard conflict limit 21118 (soft 11118 + delta 10000)
c [simplification-7] new conflict limit 11118 (hard 21118)
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   36.3   80681   457809      7266    5523   1991 70026   21   205   46  10%      1  193   28    2 1206%
c i   36.4   80675   457809      7323    5574   1996 70026   21   206   46  10%      1  194   30    2 1297%
c i   36.4   80522   457809      7328    5576   1996 70028   21   205   46  10%      1  194   30    2 1275%
c i   37.0   80518   457809      7712    5905   2015 70057   22   208   46  11%      2  195   30    2 1224%
c i   37.0   80511   457809      7722    5913   2016 70057   22   208   46  11%      2  195   33    3 1302%
c i   37.0   80503   457809      7723    5913   2016 70057   22   208   46  11%      2  195   32    3 1297%
c i   37.0   80502   457809      7724    5913   2016 70057   22   208   46  11%      2  195   32    3 1292%
c i   37.0   80496   457809      7727    5914   2016 70058   22   208   46  11%      2  195   33    3 1315%
c i   37.1   80495   457809      7782    5954   2021 70066   22   208   46  11%      2  195   31    3 1243%
c i   37.3   80491   457809      7974    6129   2024 70075   22   206   46  11%      2  193   30    3 1140%
c i   37.4   80488   457809      8023    6174   2027 70075   23   209   46  11%      1  195   31    3 1184%
c i   37.8   80487   457809      8310    6422   2044 70092   23   211   46  11%      2  196   30    3 1098%
c i   37.9   80476   457809      8321    6431   2044 70093   23   211   46  11%      2  196   30    3 1109%
c i   37.9   80465   457809      8338    6444   2046 70094   23   212   46  11%      2  197   29    3 1065%
c i   38.0   80454   457809      8443    6537   2051 70095   24   210   46  11%      2  195   36    3 1276%
c i   38.2   80453   457809      8643    6703   2062 70108   24   211   46  11%      2  195   31    3 1059%
c i   38.2   79787   457809      8644    6703   2062 70108   24   211   46  11%      2  195   30    3 1055%
c i   38.2   79768   457809      8645    6703   2062 70108   24   211   46  11%      2  195   30    3 1051%
c i   38.2   79764   457809      8652    6704   2064 70111   24   211   46  11%      1  195   30    3 1024%
c i   38.2   79761   457809      8657    6705   2065 70112   24   211   46  11%      1  195   29    3 1021%
c i   38.3   79646   457809      8701    6727   2072 70123   24   212   46  11%      1  196   27    3  921%
c i   38.3   79612   457809      8710    6731   2074 70124   23   212   46  11%      1  196   26    3  904%
c i   38.3   79570   457809      8711    6731   2074 70124   23   211   46  11%      1  196   26    3  900%
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   38.8   79563   457809      9139    7113   2090 70141   26   208   46  12%      2  191   43    3 1366%
c i   38.9   79561   457809      9215    7185   2090 70141   26   208   46  13%      2  191   46    3 1431%
c i   39.1   79560   457809      9301    7261   2094 70145   26   210   47  12%      2  192   39    3 1208%
c i   39.2   79559   457809      9363    7313   2096 70145   28   216   47  13%      2  198   69    3 2026%
c i   39.2   79558   457809      9415    7362   2097 70146   28   216   47  13%      2  198   63    3 1830%
c i   39.9   79549   457809      9953    7819   2122 70166   30   219   47  14%      3  199   48    4 1264%
c i   40.1   79548   457809     10112    7957   2129 70176   31   222   47  14%      3  202   46    4 1175%
c i   40.1   79544   457809     10153    7993   2131 70178   31   222   47  14%      2  202   47    4 1192%
c i   40.3   79543   457809     10258    8086   2136 70180   32   227   47  14%      2  206   58    4 1448%
c i   40.3   79537   457809     10263    8088   2137 70181   32   227   47  14%      2  206   57    4 1422%
c i   40.4   79534   457809     10352    8167   2137 70183   35   229   47  15%      2  208   87    4 2070%
c i   40.4   79528   457809     10353    8167   2137 70183   35   229   47  15%      2  208   87    4 2062%
c i   40.4   79519   457809     10354    8167   2137 70183   35   228   47  15%      2  208   87    4 2054%
c i   40.4   79510   457809     10355    8167   2137 70183   35   228   47  15%      2  208   86    4 2046%
c i   40.4   79506   457809     10356    8167   2137 70183   35   228   47  15%      2  208   86    4 2038%
c 
c [simplification-8] limit 11220 conflicts (hard 21118) hit after 11222 conflicts
c [quatres-4] found 30916 quaternary clauses 41% in total
c [quatres-4-2] added 2 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 79503 free variables schedulable
c [ternres-4] 161 ternary resolvents (0 bin, 161 trn)
c [ternres-4] 24543 variables remain 31% (54960 retained 69%)
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] extracted 162 xors of average arity 2.4
c [gauss-4] connected 391 occurrences of 276 variables (average 1.4)
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [decomp-20] removed 103 variables
c [gauss-4] exported 0 unary, 2 binary and 0 ternary equations
c [simpleprobe-4] 48670 schedulable variables 61%
c [simpleprobe-4] limit 15363871 penalty 0 = 0 + 0
c [decomp-22] removed 1532 variables
c [simpleprobe-4] 12112 variables remain 16% (65756 retained 84%)
c [simpleprobe-4] removed 1532 variables, found 42668 hbrs, 299 units
c [unhide-8] limit 768193 with penalty 0 = 0 + 0
c [unhide-8-8] 8 units, 218 failed, 10222 tauts, 0 hbrs, 22895 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 167 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 77287 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 43 blocked clauses
c [block-3] 43 < 1/100 * 440797 = 4407 considered unsuccessful
c [bca-4] limit of 10000000 steps and 873609 added (scaled 2)
c [bca-4] 129821 out of 154576 literals actually usable 84%
c [bca-4] added 101 blocked clauses in 350839 steps
c [sweep-4] limit 1152290 penalty 0 = 0 + 0
c [sweep-4-1] 3659 pos 4.7% + 73556 neg 95.3% = 77215 sched 99.9% ret 72
c [sweep-4-1] 1186755 steps 8 queries 17955.50 avg class size
c [sweep-4-1] 145 decisions 7 SAT calls 113.29 avg env size
c [sweep-4-1] 77105 variables remain 100% (84 retained 0%)
c [decomp-23] removed 349 variables
c [sweep-4-1] removed 349 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 349 vars in TOTAL (1 rounds, 7 queries)
c [phase-count-8] 431052 negative 99.0% of 435615 except 4563 1.0%
c [phase-count-8] 345050 positive 79.2% of 435615 except 90565 20.8%
c [phase-count-8] less non-negative clauses 4563 than limit 43500 (10.0%)
c [phase-count-8] non-pos/non-neg = 90565/4563 = 19.85 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 71 negative 100%
c [sort-queue-8] sorted 46151 enqueued variables after 11222 conflicts
c [score-dist-8] active 30787 (40%), one 10992 (14%), zero 35159 (46%)
c [score-dist-8] max exp 949, different 615 (65%)
c [score-dist-8] median active exp 858, avg 737.7
c [simplification-8] removed 2565 variables 3.2% (76938 remain 31%)
c [simplification-8] removed 22194 irredundant clauses 4.8% (435615 remain 39%)
c [simplification-8] maximum reduction of 5% = max (3%, 5%)
c [simplification-8] large reduction 5% >= 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 23222 (soft 13222 + delta 10000)
c [simplification-8] new conflict limit 13222 (hard 23222)
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.0   76937   435615     11542    9112   1848 99448   38   224   49  17%      8  199   57    5 1136%
c i   45.1   76936   435615     11603    9163   1851 99452   38   224   49  17%      8  199   52    5 1036%
c i   45.1   76935   435615     11608    9166   1851 99452   38   224   49  17%      8  199   51    5 1018%
c i   45.9   76934   435615     12223    9712   1869 99471   39   226   49  17%      6  200   47    5  876%
c i   46.4   76926   435615     12625   10078   1877 99480   40   231   49  17%      5  203   54    6  947%
c i   46.4   76925   435615     12631   10080   1880 99480   40   231   49  17%      5  203   53    6  930%
c i   46.5   76917   435615     12683   10121   1883 99482   41   233   49  18%      5  205   58    6 1013%
c i   46.7   76912   435615     12822   10214   1901 99505   40   229   49  17%      4  201   36    6  635%
c i   46.8   76905   435615     12917   10279   1910 99515   39   227   49  17%      4  199   30    6  524%
c i   46.8   76901   435615     12918   10279   1910 99515   39   227   49  17%      4  199   30    6  522%
c i   46.8   76509   435615     12919   10279   1910 99515   39   227   49  17%      4  199   30    6  520%
c i   46.9   76499   435615     12977   10331   1911 99518   39   227   49  17%      4  198   35    6  607%
c 
c [simplification-9] limit 13245 conflicts (hard 23222) hit after 13245 conflicts
c [quatres-5] found 30493 quaternary clauses 41% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 1 quaternary resolvents
c [ternres-5] limit 4463607 with penalty 0 = 0 + 0
c [ternres-5] 23575 schedulable variables 31%
c [ternres-5] 191 ternary resolvents (3 bin, 188 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] extracted 161 xors of average arity 2.6
c [gauss-5] connected 420 occurrences of 287 variables (average 1.5)
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] fully completed
c [decomp-24] removed 64 variables
c [gauss-5] exported 0 unary, 5 binary and 0 ternary equations
c [treelook-4] limit 446360 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 75183 literals 49%
c [treelook-4] scheduling used 446949 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 446360 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 759778 steps
c [treelook-4] 75146 literals remain 49%
c [treelook-4] 30608 variables remain to probed next time 40%
c [treelook-4] removed 22 variables, found 122 hbrs
c [unhide-9] limit 892721 with penalty 0 = 0 + 0
c [unhide-9-9] 2 units, 85 failed, 5078 tauts, 0 hbrs, 23631 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 135 transitive binary clauses
c [transred-5] found 3 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 76195 variables 100%
c [elim-7] limit of 44636079 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 2475 variables 3% in round 1 in 35796115 steps
c [elim-7-1] backward subsumption/strengthening limit 8839964
c [elim-7-1-1] backward checking 9626 touched variables 13%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 36 and strengthened 119 clauses in 2487492 steps
c [elim-7-1] rescheduled 402 variables 1% by backward subsumption
c [elim-7-2] eliminated 44 variables 0% in round 2 in 358009 steps
c [elim-7-2] backward subsumption/strengthening limit 358000
c [elim-7-2-1] backward checking 342 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 4 and strengthened 5 clauses in 214373 steps
c [elim-7-2] rescheduled 24 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 14914 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 2519 = 3% variables out of 76195 scheduled
c [bca-5] limit of 10000000 steps and 844341 added (scaled 2)
c [bca-5] 124454 out of 147354 literals actually usable 84%
c [bca-5] added 50 blocked clauses in 339914 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 13390820 penalty 0 = 0 + 0
c [sweep-5-1] 3563 pos 4.8% + 70032 neg 95.2% = 73595 sched 99.9% ret 81
c [sweep-5-1] 13457103 steps 132 queries 4250.24 avg class size
c [sweep-5-1] 841 decisions 99 SAT calls 52.56 avg env size
c [sweep-5-1] 71135 variables remain 97% (2363 retained 3%)
c [decomp-27] removed 306 variables
c [sweep-5-1] removed 306 vars (0 failed, 39 eqs, 55 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 306 vars in TOTAL (1 rounds, 131 queries)
c [phase-count-9] 415655 negative 98.9% of 420204 except 4549 1.1%
c [phase-count-9] 331736 positive 78.9% of 420204 except 88468 21.1%
c [phase-count-9] less non-negative clauses 4549 than limit 42000 (10.0%)
c [phase-count-9] non-pos/non-neg = 88468/4549 = 19.45 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 65 negative 100%
c [sort-queue-9] sorted 40436 enqueued variables after 13245 conflicts
c [score-dist-9] active 32934 (45%), one 9351 (13%), zero 31085 (42%)
c [score-dist-9] max exp 995, different 640 (64%)
c [score-dist-9] median active exp 920, avg 807.7
c [simplification-9] removed 3089 variables 4.0% (73370 remain 29%)
c [simplification-9] removed 15411 irredundant clauses 3.5% (420204 remain 37%)
c [simplification-9] maximum reduction of 4% = max (4%, 4%)
c [simplification-9] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-9] new conflict interval 8000
c [simplification-9] penalized conflict interval 8000 = 1 * 8000
c [simplification-9] hard conflict limit 31245 (soft 21245 + delta 10000)
c [simplification-9] new conflict limit 21245 (hard 31245)
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   52.3   73369   420204     13419    7627   1784 102286   39   229   45  17%      4  199   42    6  695%
c i   52.4   73363   420204     13469    7671   1787 102288   39   229   45  17%      3  199   37    6  618%
c i   52.8   73362   420204     13835    7976   1810 102309   38   222   45  17%      3  190   25    6  403%
c i   52.8   73357   420204     13843    7980   1811 102311   38   222   45  17%      3  190   24    6  392%
c i   53.0   73353   420204     14065    8172   1815 102329   37   217   45  17%      3  185   31    6  501%
c i   53.1   73352   420204     14110    8214   1817 102329   38   220   45  17%      3  188   42    6  672%
c i   53.4   73351   420204     14351    8420   1825 102342   39   229   46  17%      2  196   49    6  763%
c i   53.8   73344   420204     14627    8677   1830 102348   39   232   46  17%      2  198   42    7  632%
c i   54.2   73336   420204     14938    8959   1841 102354   40   234   46  17%      2  200   55    7  803%
c i   54.5   73335   420204     15188    9181   1848 102366   40   236   46  17%      2  201   40    7  579%
c i   54.8   73334   420204     15358    9333   1851 102377   39   237   46  17%      2  201   31    7  447%
c i   55.0   73333   420204     15517    9470   1858 102387   39   237   46  16%      2  200   32    7  459%
c i   55.0   73321   420204     15520    9472   1858 102387   39   237   46  16%      2  200   33    7  462%
c i   55.1   73315   420204     15521    9472   1858 102387   39   236   46  16%      2  200   32    7  461%
c i   55.5   73308   420204     15874    9780   1873 102404   38   234   46  16%      2  196   37    7  509%
c i   55.6   73305   420204     15950    9844   1876 102408   39   234   46  17%      2  196   49    7  669%
c i   55.8   73304   420204     16037    9923   1879 102411   39   236   46  17%      2  198   48    7  653%
c i   56.4   73303   420204     16426   10269   1889 102423   40   237   46  17%      2  198   55    8  727%
c i   56.4   73294   420204     16453   10292   1890 102423   40   236   46  17%      2  197   53    8  704%
c i   56.7   73293   420204     16611   10439   1895 102427   41   243   46  17%      2  203   60    8  778%
c i   56.9   73292   420204     16788   10591   1903 102434   41   244   47  17%      2  203   50    8  635%
c i   57.4   73027   420204     17095   10847   1916 102462   41   240   47  17%      2  199   38    8  476%
c i   57.4   73015   420204     17112   10859   1916 102465   41   240   47  17%      2  198   36    8  452%
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   57.7   73014   420204     17283   11004   1930 102472   41   239   47  17%      2  197   39    8  491%
c i   57.7   72994   420204     17303   11018   1934 102473   41   238   47  17%      1  196   38    8  469%
c i   57.7   72986   420204     17319   11024   1936 102477   41   238   47  17%      1  196   36    8  444%
c i   58.0   72981   420204     17551   11236   1944 102481   40   234   48  17%      1  192   36    8  444%
c i   58.6   72969   420204     18066   11665   1970 102510   38   226   49  17%      2  182   28    8  338%
c i   59.0   72968   420204     18357   11908   1979 102533   39   226   49  17%      2  181   50    8  597%
c i   59.1   72967   420204     18403   11946   1980 102535   39   228   49  17%      2  183   55    8  652%
c i   59.2   72966   420204     18448   11986   1981 102535   39   228   49  17%      2  183   53    8  626%
c i   59.2   72961   420204     18450   11987   1981 102535   39   228   49  17%      2  183   53    8  628%
c i   59.2   72954   420204     18461   11996   1981 102536   40   229   49  17%      2  184   57    9  672%
c i   59.3   72953   420204     18502   12035   1981 102536   40   230   49  17%      2  185   55    9  650%
c i   59.7   72952   420204     18820   12322   1988 102546   41   232   49  18%      2  186   49    9  556%
c i   59.8   72930   420204     18862   12356   1989 102551   41   232   49  18%      2  186   44    9  498%
c i   60.0   72928   420204     19001   12477   1999 102555   40   233   49  17%      2  186   36    9  408%
c i   60.5   72920   420204     19371   12806   2012 102568   40   229   50  18%      2  182   37    9  407%
c i   60.5   72913   420204     19377   12809   2012 102568   40   229   50  18%      2  181   38    9  427%
c i   60.6   72905   420204     19433   12855   2012 102568   41   230   50  18%      2  182   55    9  600%
c i   60.7   72790   420204     19464   12883   2012 102569   42   231   50  18%      2  183   58    9  639%
c i   61.6   72787   420204     19997   13356   2028 102584   43   233   50  19%      3  184   53    9  557%
c i   61.7   72785   420204     20064   13414   2032 102585   43   233   50  18%      2  183   46   10  485%
c i   61.7   72782   420204     20090   13439   2032 102585   44   235   50  19%      2  185   60   10  632%
c i   62.2   72768   420204     20402   13721   2035 102590   45   236   50  19%      2  186   56   10  571%
c i   62.5   72762   420204     20550   13853   2037 102599   45   237   50  19%      2  186   60   10  605%
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.8   72761   420204     20762   14041   2042 102607   45   234   50  19%      2  183   49   10  493%
c i   63.2   72758   420204     21022   14278   2044 102613   45   235   51  19%      2  182   45   10  448%
c i   63.3   72757   420204     21079   14330   2046 102614   46   236   51  19%      2  183   57   10  554%
c i   63.4   72756   420204     21149   14395   2048 102614   46   235   51  19%      2  183   52   10  511%
c i   63.6   72716   420204     21225   14467   2047 102616   45   236   51  19%      1  184   48   10  466%
c 
c [simplification-10] limit 21265 conflicts (hard 31245) hit after 21265 conflicts
c [quatres-6] found 31008 quaternary clauses 42% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 2 single-self-subsuming ternary resolvents
c [quatres-6-2] added 4 quaternary resolvents
c [ternres-6] limit 7141158 with penalty 0 = 0 + 0
c [ternres-6] all 72713 free variables schedulable
c [ternres-6] 826 ternary resolvents (7 bin, 819 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 446322 penalty 3 = 3 + 0
c [card-4] found 1735 at-most-one constraints of average size 3.9
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 446322 for elimination
c [card-4] 1735 out of 1735 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-6] limit 2000000 penalty 0 = 0 + 0
c [gauss-6] extracted 155 xors of average arity 2.5
c [gauss-6] connected 384 occurrences of 199 variables (average 1.9)
c [gauss-6] limit 2000000 penalty 0 = 0 + 0
c [gauss-6] fully completed
c [decomp-28] removed 90 variables
c [gauss-6] exported 1 unary, 2 binary and 0 ternary equations
c [basicprobe-4] limit 35705793 penalty 0 = 0 + 0
c [basicprobe-4-0] 22654 probes remain 32% after last round
c [basicprobe-4-0] 131 units = 131 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 743 variables, found 38882 hbrs
c [bate-2] eliminated 54 asymmetric tautologies during probing
c [unhide-10] limit 1428231 with penalty 0 = 0 + 0
c [unhide-10-10] 10 units, 305 failed, 8630 tauts, 0 hbrs, 47789 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 146 transitive binary clauses
c [cce-3] limit of 8926448 steps penalty 2 = 2 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 4463226 steps for small clauses
c [cce-3-1] scheduling 259191 clauses = 217735 binary + 41456 ternary
c [cce-3-1] tried to eliminate 123 small clauses 0%
c [cce-3-1] eliminated 23 binary clauses 0%
c [cce-3-1] eliminated 7 ternary clauses 0%
c [cce-3-1] eliminated 30 small clauses 0%
c [cce-3-1] eliminated 3858 small clauses in 8926452 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 3858 covered clauses in round 1
c [cce-3] eliminated 3858 covered clauses in TOTAL during 1 rounds
c [cce-3] 3858 < 1/100 * 409894 = 4098 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 71397 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2856463480 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1582 variables 2% in round 1 in 34102708 steps
c [elim-8-1] backward subsumption/strengthening limit 34102700
c [elim-8-1-1] backward checking 5992 touched variables 8%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 75 and strengthened 141 clauses in 1688446 steps
c [elim-8-1] rescheduled 459 variables 1% by backward subsumption
c [elim-8-2] eliminated 52 variables 0% in round 2 in 787924 steps
c [elim-8-2] backward subsumption/strengthening limit 787900
c [elim-8-2-1] backward checking 404 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 8 and strengthened 4 clauses in 315366 steps
c [elim-8-2] rescheduled 27 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 1007909 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1640 = 2% variables out of 71397 scheduled
c [bca-6] limit of 10000000 steps and 803084 added (scaled 2)
c [bca-6] 114879 out of 139516 literals actually usable 82%
c [bca-6] added 70 blocked clauses in 314711 steps
c [sweep-6] limit 2142347 penalty 0 = 0 + 0
c [sweep-6-1] 3092 pos 4.6% + 64618 neg 95.4% = 67710 sched 97.1% ret 2047
c [sweep-6-1] 2205695 steps 30 queries 9310.60 avg class size
c [sweep-6-1] 277 decisions 26 SAT calls 153.31 avg env size
c [sweep-6-1] 67500 variables remain 97% (2257 retained 3%)
c [decomp-30] removed 44 variables
c [sweep-6-1] removed 44 vars (0 failed, 3 eqs, 6 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 44 vars in TOTAL (1 rounds, 29 queries)
c [phase-count-10] 396690 negative 98.9% of 401126 except 4436 1.1%
c [phase-count-10] 314897 positive 78.5% of 401126 except 86229 21.5%
c [phase-count-10] less non-negative clauses 4436 than limit 40100 (10.0%)
c [phase-count-10] non-pos/non-neg = 86229/4436 = 19.44 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 24 negative 100%
c [sort-queue-10] sorted 41157 enqueued variables after 21265 conflicts
c [score-dist-10] active 28556 (41%), one 14963 (21%), zero 26194 (38%)
c [score-dist-10] max exp 598, different 444 (74%)
c [score-dist-10] median active exp 564, avg 479.9
c [simplification-10] removed 3000 variables 4.1% (69713 remain 28%)
c [simplification-10] removed 19078 irredundant clauses 4.5% (401126 remain 36%)
c [simplification-10] maximum reduction of 5% = max (4%, 5%)
c [simplification-10] large reduction 5% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 33265 (soft 23265 + delta 10000)
c [simplification-10] new conflict limit 23265 (hard 33265)
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   70.0   69712   401126     21635   11582   2333 129746   45   231   49  19%      2  177   36   10  342%
c i   70.0   69711   401126     21654   11598   2333 129747   45   231   49  19%      2  177   34   10  329%
c i   70.1   69710   401126     21721   11654   2335 129754   44   231   49  19%      2  177   32   10  304%
c i   70.1   69598   401126     21722   11654   2335 129754   44   231   49  19%      2  177   32   10  303%
c i   70.1   69597   401126     21723   11654   2335 129754   44   231   49  19%      2  177   32   10  302%
c i   70.3   69596   401126     21819   11741   2339 129756   44   230   49  19%      2  176   32   11  307%
c i   70.4   69595   401126     21938   11838   2342 129768   43   227   49  19%      1  172   26   11  245%
c i   71.4   69572   401126     22625   12447   2356 129804   44   225   49  19%      3  168   51   11  468%
c i   71.6   69571   401126     22744   12551   2359 129806   44   223   49  20%      3  166   58   11  527%
c 
c [simplification-11] limit 23285 conflicts (hard 33265) hit after 23285 conflicts
c [quatres-7] found 32161 quaternary clauses 44% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 2 single-self-subsuming ternary resolvents
c [quatres-7-2] added 24 quaternary resolvents
c [ternres-7] limit 7810764 with penalty 0 = 0 + 0
c [ternres-7] all 69499 free variables schedulable
c [ternres-7] 832 ternary resolvents (4 bin, 828 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-7] limit 2000000 penalty 0 = 0 + 0
c [gauss-7] extracted 49 xors of average arity 3.0
c [gauss-7] connected 147 occurrences of 129 variables (average 1.1)
c [gauss-7] limit 2000000 penalty 0 = 0 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 1 variables
c [simpleprobe-5] 10928 schedulable variables 16%
c [simpleprobe-5] limit 31243058 penalty 0 = 0 + 0
c [decomp-32] removed 673 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 673 variables, found 28174 hbrs, 191 units
c [unhide-11] limit 1562152 with penalty 0 = 0 + 0
c [unhide-11-11] 1 units, 36 failed, 4011 tauts, 0 hbrs, 24842 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 147 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 68726 variables 100%
c [block-4] limit of 19526911 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 159 blocked clauses
c [block-4] 159 < 1/100 * 392766 = 3927 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 68726 variables 100%
c [elim-9] limit of 156215291 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 916 variables 1% in round 1 in 32817414 steps
c [elim-9-1] backward subsumption/strengthening limit 32817400
c [elim-9-1-1] backward checking 4248 touched variables 6%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 36 and strengthened 32 clauses in 1180751 steps
c [elim-9-1] rescheduled 156 variables 0% by backward subsumption
c [elim-9-2] eliminated 12 variables 0% in round 2 in 103333 steps
c [elim-9-2] backward subsumption/strengthening limit 103300
c [elim-9-2-1] backward checking 89 touched variables 0%
c [elim-9-2-1] incomplete backward checking 0 remain 0%
c [elim-9-2] subsumed 4 and strengthened 3 clauses in 103301 steps
c [elim-9-2] rescheduled 21 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 15586 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 928 = 1% variables out of 68726 scheduled
c [bca-7] limit of 10000000 steps and 780115 added (scaled 2)
c [bca-7] 110556 out of 135598 literals actually usable 82%
c [bca-7] added 37 blocked clauses in 299739 steps
c [sweep-7] limit 2343229 penalty 0 = 0 + 0
c [sweep-7-1] 3577 pos 5.4% + 62107 neg 94.6% = 65684 sched 96.9% ret 2114
c [sweep-7-1] 2493767 steps 20 queries 8255.55 avg class size
c [sweep-7-1] 174 decisions 17 SAT calls 129.12 avg env size
c [sweep-7-1] 65601 variables remain 97% (2196 retained 3%)
c [decomp-33] removed 19 variables
c [sweep-7-1] removed 19 vars (0 failed, 2 eqs, 3 impls)
c [sweep-7] 19 < 1/1000 * 67798 = 67 considered unsuccessful
c [sweep-7] removed 19 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-11] 385297 negative 98.9% of 389615 except 4318 1.1%
c [phase-count-11] 305415 positive 78.4% of 389615 except 84200 21.6%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-11] sorted 38788 enqueued variables after 23285 conflicts
c [score-dist-11] active 28991 (43%), one 14334 (21%), zero 24454 (36%)
c [score-dist-11] max exp 626, different 483 (77%)
c [score-dist-11] median active exp 532, avg 469.6
c [simplification-11] removed 1720 variables 2.5% (67779 remain 27%)
c [simplification-11] removed 11511 irredundant clauses 2.9% (389615 remain 35%)
c [simplification-11] maximum reduction of 3% = max (2%, 3%)
c [simplification-11] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-11] new conflict interval 13000
c [simplification-11] penalized conflict interval 13000 = 1 * 13000
c [simplification-11] hard conflict limit 46285 (soft 36285 + delta 10000)
c [simplification-11] new conflict limit 36285 (hard 46285)
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   77.0   67778   389615     23432   11778   2586 151852   46   214   49  21%      4  155   51   11  446%
c i   77.0   67777   389615     23446   11788   2587 151853   46   214   49  21%      4  156   52   11  452%
c i   77.4   67776   389615     23699   12019   2595 151858   46   217   49  21%      3  158   48   12  415%
c i   77.5   67771   389615     23769   12081   2596 151861   46   217   49  21%      3  158   43   12  373%
c i   78.6   67770   389615     24489   12741   2611 151870   47   215   49  22%      4  153   50   12  412%
c i   78.7   67735   389615     24556   12806   2611 151870   46   213   49  22%      4  151   47   12  388%
c i   80.2   67734   389615     25547   13726   2627 151882   48   216   49  22%      7  152   51   13  402%
c i   80.3   67692   389615     25617   13793   2628 151883   47   215   49  22%      6  151   44   13  349%
c i   80.5   67691   389615     25723   13889   2630 151885   48   217   49  22%      5  153   48   13  376%
c i   80.5   67690   389615     25733   13898   2630 151885   48   216   49  22%      5  152   48   13  375%
c i   81.0   67689   389615     26039   14181   2637 151890   47   212   49  22%      4  147   40   13  312%
c i   81.2   67688   389615     26162   14293   2642 151893   46   211   50  22%      4  146   34   13  266%
c i   81.3   67687   389615     26265   14383   2647 151896   46   209   50  22%      4  144   34   13  265%
c i   81.5   67686   389615     26370   14478   2651 151897   46   208   50  22%      3  143   35   13  271%
c i   82.1   67685   389615     26729   14799   2653 151901   48   209   50  23%      3  143   68   13  510%
c i   82.7   67684   389615     27052   15093   2655 151907   49   209   50  24%      3  142   64   14  475%
c i   82.9   67683   389615     27193   15221   2656 151908   50   209   50  24%      2  142   61   14  444%
c i   83.1   67682   389615     27375   15361   2660 151910   51   209   51  24%      2  141   71   14  515%
c i   83.6   67681   389615     27759   15699   2666 151918   51   208   51  24%      2  140   54   14  385%
c i   83.7   67680   389615     27871   15794   2669 151920   52   207   51  25%      2  138   70   14  491%
c i   83.8   67677   389615     27971   15882   2670 151925   51   205   51  25%      2  136   57   14  404%
c i   84.0   67676   389615     28084   15990   2670 151926   51   203   51  25%      1  134   51   14  360%
c i   84.7   67675   389615     28481   16354   2676 151928   52   204   51  26%      2  134   59   15  407%
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   85.5   67674   389615     28968   16799   2684 151937   50   197   52  25%      2  126   33   15  227%
c i   85.7   67673   389615     29061   16881   2684 151937   49   195   52  25%      2  124   31   15  209%
c i   86.1   67672   389615     29350   17154   2688 151938   49   194   52  25%      2  123   45   15  305%
c i   86.4   67671   389615     29543   17332   2689 151939   49   190   52  26%      2  118   43   15  291%
c i   86.9   67670   389615     29974   17686   2693 151944   51   184   54  28%      2  111   61   15  400%
c i   87.3   67666   389615     30229   17913   2698 151950   50   182   54  28%      2  109   48   15  315%
c i   87.3   67157   389615     30252   17934   2698 151950   50   182   54  28%      2  109   46   15  300%
c i   87.4   67116   389615     30259   17936   2698 151953   50   182   54  28%      2  109   45   15  294%
c i   87.7   67067   389615     30418   18081   2700 151955   50   181   54  27%      1  108   46   15  298%
c i   87.8   67066   389615     30474   18131   2701 151955   50   180   54  28%      1  107   46   15  296%
c i   87.8   67052   389615     30478   18134   2701 151955   50   180   54  28%      1  107   45   15  292%
c i   88.1   67051   389615     30645   18285   2704 151958   50   179   54  28%      1  105   49   16  313%
c i   89.1   67049   389615     31230   18809   2711 151971   52   182   55  28%      2  107   53   16  334%
c i   89.7   67048   389615     31560   19107   2723 151973   52   181   56  29%      2  105   53   16  329%
c i   90.0   67047   389615     31836   19355   2724 151973   52   177   56  30%      2  101   56   16  343%
c i   90.6   67046   389615     32147   19634   2727 151979   53   178   57  30%      2  101   63   17  378%
c i   90.8   67044   389615     32266   19739   2728 151979   53   177   57  30%      2  100   60   17  360%
c i   93.4   67043   389615     33678   21047   2747 151990   48   164   57  29%     10   85   32   17  188%
c i   93.9   67042   389615     34059   21390   2757 151991   47   159   57  30%      7   80   35   17  203%
c i   94.0   67041   389615     34109   21434   2757 151992   47   159   57  30%      7   80   37   17  217%
c i   94.6   67040   389615     34511   21779   2762 151993   49   154   57  32%      5   75   54   18  309%
c i   94.7   67039   389615     34585   21849   2763 151993   49   154   57  32%      5   75   53   18  302%
c i   96.7   67038   389615     35682   22835   2787 152004   48   145   57  33%      7   64   41   18  228%
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   96.8   67037   389615     35700   22849   2787 152004   48   144   57  33%      7   64   40   18  225%
c 
c [simplification-12] limit 36289 conflicts (hard 46285) hit after 36289 conflicts
c [quatres-8] found 30810 quaternary clauses 44% in total
c [quatres-8-2] added 17 single-self-subsuming ternary resolvents
c [quatres-8-2] added 5 quaternary resolvents
c [ternres-8] limit 12667233 with penalty 0 = 0 + 0
c [ternres-8] all 67037 free variables schedulable
c [ternres-8] 470 ternary resolvents (3 bin, 467 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-34] removed 982 variables
c [treelook-5] limit 1266723 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 115807 literals 87%
c [treelook-5] scheduling used 1266725 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 1266723 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1278385 steps
c [treelook-5] 115782 literals remain 87%
c [treelook-5] 25751 variables remain to probed next time 39%
c [treelook-5] removed 0 variables, found 9809 hbrs
c [unhide-12] limit 2533446 with penalty 0 = 0 + 0
c [unhide-12-12] 8 units, 207 failed, 17115 tauts, 0 hbrs, 113570 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 106 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 66555 variables 100%
c [elim-10] limit of 253344676 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 570 variables 1% in round 1 in 31667917 steps
c [elim-10-1] backward subsumption/strengthening limit 31667900
c [elim-10-1-1] backward checking 2640 touched variables 4%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 22 and strengthened 28 clauses in 788741 steps
c [elim-10-1] rescheduled 117 variables 0% by backward subsumption
c [elim-10-2] eliminated 11 variables 0% in round 2 in 84291 steps
c [elim-10-2] backward subsumption/strengthening limit 84200
c [elim-10-2-1] backward checking 69 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 2 and strengthened 3 clauses in 84201 steps
c [elim-10-2] rescheduled 15 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 7832 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 592 = 1% variables out of 66555 scheduled
c [elim-10] 592 < 1/100 * 66555 = 665 considered unsuccessful
c [bca-8] limit of 10000000 steps and 761370 added (scaled 2)
c [bca-8] 105771 out of 131928 literals actually usable 80%
c [bca-8] added 61 blocked clauses in 292832 steps
c [phase-count-12] 376082 negative 98.9% of 380299 except 4217 1.1%
c [phase-count-12] 297233 positive 78.2% of 380299 except 83066 21.8%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 42968 enqueued variables after 36289 conflicts
c [score-dist-12] active 22995 (35%), one 19784 (30%), zero 23184 (35%)
c [score-dist-12] max exp 542, different 371 (68%)
c [score-dist-12] median active exp 507, avg 451.7
c [simplification-12] removed 1074 variables 1.6% (65963 remain 26%)
c [simplification-12] removed 9316 irredundant clauses 2.4% (380299 remain 34%)
c [simplification-12] maximum reduction of 2% = max (2%, 2%)
c [simplification-12] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-12] new conflict interval 19666
c [simplification-12] penalized conflict interval 19666 = 1 * 19666
c [simplification-12] hard conflict limit 65955 (soft 55955 + delta 10000)
c [simplification-12] new conflict limit 55955 (hard 65955)
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  103.8   65962   380299     37426   20949   2853 138913   46   145   59  31%     14   62   40   19  217%
c i  104.0   65961   380299     37495   21012   2853 138913   46   146   59  32%     13   64   50   19  266%
c i  104.7   65960   380299     37947   21410   2859 138925   46   144   60  32%      9   62   41   19  220%
c i  105.1   65959   380299     38177   21619   2861 138931   45   143   60  32%      7   60   44   19  233%
c i  106.3   65957   380299     38838   22235   2868 138936   44   136   60  32%      6   53   37   19  192%
c i  106.9   65956   380299     39226   22591   2872 138944   42   131   60  32%      4   47   28   19  147%
c i  110.2   65955   380299     41119   24346   2897 138974   37   117   60  32%     15   32   33   19  172%
c i  110.3   65954   380299     41196   24415   2899 138975   37   117   60  32%     14   32   35   19  182%
c i  110.4   65953   380299     41229   24443   2899 138975   37   116   60  32%     13   31   36   19  187%
c i  110.7   65952   380299     41390   24585   2901 138979   37   115   60  32%     11   30   36   19  184%
c i  111.8   65951   380299     42285   25450   2903 138981   33    99   60  33%      8   14   13   19   67%
c i  112.1   65950   380299     42613   25735   2910 138983   33    99   60  33%      6   13   27   19  139%
c i  112.6   65949   380299     42872   25986   2910 138983   32    96   60  34%      5   11   26   19  132%
c i  112.9   65948   380299     43046   26153   2911 138983   32    95   60  34%      4   10   23   19  118%
c i  113.0   65947   380299     43080   26185   2911 138983   32    95   60  34%      4    9   25   19  127%
c i  113.3   65946   380299     43251   26345   2911 138984   32    97   60  33%      3   11   32   20  162%
c i  113.6   65945   380299     43406   26491   2912 138984   33    97   60  34%      2   12   38   20  193%
c i  114.7   65941   380299     44026   27082   2917 138987   33    98   60  34%      3   12   33   20  170%
c i  117.7   65940   380299     45600   28534   2934 139002   36   107   60  33%     11   21   38   20  187%
c i  121.5   65938   380299     48230   30959   2959 139024   30    85   65  35%     24   -1   41   20  202%
c i  123.5   65937   380299     49353   32011   2966 139026   29    80   65  37%     13   -7   24   20  120%
c i  125.5   65936   380299     50804   33364   2973 139026   25    64   65  39%     11  -23   11   20   53%
c i  126.7   65935   380299     51595   34114   2978 139027   23    57   68  41%      7  -29   17   20   83%
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.5   65934   380299     52120   34617   2978 139027   22    54   68  41%      5  -32   15   20   74%
c i  128.9   65933   380299     53100   35501   2984 139034   22    51   68  43%      5  -35   21   20  105%
c i  129.9   65932   380299     53730   36072   2985 139036   21    47   68  45%      4  -37   19   20   94%
c i  130.5   65931   380299     54075   36390   2986 139039   22    50   68  43%      2  -34   25   20  123%
c i  135.2   65930   380299     57244   39364   2996 139046   20    44   72  47%     30  -39   13   20   67%
c i  140.8   65929   380299     61124   42891   3020 139056   20    43   72  46%     40  -38    9   20   46%
c 
c [simplification-13] limit 55955 conflicts (hard 65955) hit after 65958 conflicts
c [quatres-9] found 31233 quaternary clauses 43% in total
c [quatres-9-2] added 5 quaternary resolvents
c [ternres-9] limit 23131039 with penalty 0 = 0 + 0
c [ternres-9] all 65929 free variables schedulable
c [ternres-9] 631 ternary resolvents (3 bin, 628 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-8] limit 2313103 penalty 1 = 1 + 0
c [gauss-8] extracted 76 xors of average arity 2.9
c [gauss-8] connected 218 occurrences of 126 variables (average 1.7)
c [gauss-8] limit 2313103 penalty 1 = 1 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 11 variables
c [basicprobe-5] limit 115655196 penalty 0 = 0 + 0
c [basicprobe-5-0] 18707 probes remain 29% after last round
c [basicprobe-5-0] 426 units = 426 failed (100%) + 0 lifted (0%)
c [basicprobe-5-0] removed 551 variables, found 90362 hbrs
c [bate-3] eliminated 259 asymmetric tautologies during probing
c [unhide-13] limit 2313103 with penalty 1 = 0 + 1
c [unhide-13-13] 5 units, 17 failed, 2729 tauts, 0 hbrs, 389937 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 137 transitive binary clauses
c [bca-9] limit of 10000000 steps and 734948 added (scaled 2)
c [bca-9] 100919 out of 128600 literals actually usable 78%
c [bca-9] added 16 blocked clauses in 305657 steps
c [sweep-8] limit 3469655 penalty 1 = 1 + 0
c [sweep-8-1] 3259 pos 5.2% + 59098 neg 94.8% = 62357 sched 97.0% ret 1942
c [sweep-8-1] 3571169 steps 25 queries 9919.12 avg class size
c [sweep-8-1] 356 decisions 20 SAT calls 170.95 avg env size
c [sweep-8-1] 62214 variables remain 97% (2085 retained 3%)
c [decomp-37] removed 73 variables
c [sweep-8-1] removed 73 vars (0 failed, 3 eqs, 5 impls)
c [sweep-8] removed 73 vars in TOTAL (1 rounds, 24 queries)
c [phase-count-13] 362757 negative 98.9% of 366967 except 4210 1.1%
c [phase-count-13] 284795 positive 77.6% of 366967 except 82172 22.4%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 42170 enqueued variables after 65958 conflicts
c [score-dist-13] active 22056 (34%), one 20567 (32%), zero 21603 (34%)
c [score-dist-13] max exp 842, different 399 (47%)
c [score-dist-13] median active exp 809, avg 702.7
c [simplification-13] removed 1703 variables 2.6% (64226 remain 25%)
c [simplification-13] removed 13332 irredundant clauses 3.5% (366967 remain 33%)
c [simplification-13] maximum reduction of 4% = max (3%, 4%)
c [simplification-13] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-13] new conflict interval 23666
c [simplification-13] penalized conflict interval 23666 = 1 * 23666
c [simplification-13] hard conflict limit 101457 (soft 89624 + delta 11833)
c [simplification-13] new conflict limit 89624 (hard 101457)
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  155.7   64225   366967     66955   47950   3145 224863   17    33   90  53%     67  -44   20   20  102%
c i  155.8   64224   366967     67147   48117   3150 224865   18    34   91  52%     54  -43   26   20  132%
c i  159.2   64221   366967     69045   49852   3164 224875   18    34   91  52%     17  -41   12   20   59%
c i  160.4   64220   366967     69778   50527   3166 224876   17    33   91  53%      6  -42   15   20   78%
c i  163.0   64219   366967     71509   51878   3191 224880   15    28   91  54%      7  -46    5   20   27%
c i  167.4   63540   366967     74610   54655   3200 224886   14    27   91  51%     24  -45   19   19   96%
c i  168.4   63539   366967     75399   55303   3209 224893   13    27   91  50%      9  -44   12   19   64%
c i  168.7   63538   366967     75608   55499   3209 224895   14    28   91  50%      6  -43   19   19   97%
c -  171.4   63535   366967     77403   23766   3213 224896   15    30   50  48%      7  -39   24   19  124%
c i  174.2   63534   366967     79249   25506   3216 224902   17    35   58  48%     31  -34   22   19  117%
c i  175.9   63533   366967     80519   26585   3231 224909   16    33   58  48%      9  -36    8   19   43%
c i  176.3   63413   366967     80811   26851   3232 224912   17    34   58  48%      5  -34   23   19  120%
c i  186.7   63412   366967     87895   33063   3251 224928   13    23   61  59%     80  -41   15   18   83%
c i  193.1   63388   366967     92421   37026   3274 224940   14    25   65  56%     39  -36   12   18   68%
c i  194.0   63387   366967     93055   37506   3284 224942   13    24   65  56%     16  -37    9   18   52%
c i  196.7   63376   366967     94936   39048   3295 224945   13    22   65  57%      4  -38   14   18   79%
c i  206.7   63375   366967    101039   44334   3328 224961   17    33   66  50%     61  -24    8   18   46%
c 
c [simplification-14] limit 89624 conflicts (hard 101457) hit after 101459 conflicts
c [quatres-10] found 29876 quaternary clauses 44% in total
c [quatres-10-1] removed 1 duplicate quaternary clauses
c [quatres-10-2] added 16 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1 quaternary resolvents
c [ternres-10] limit 35705797 with penalty 0 = 0 + 0
c [ternres-10] all 63375 free variables schedulable
c [ternres-10] 107 ternary resolvents (0 bin, 107 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-38] removed 919 variables
c [simpleprobe-6] all 63307 free variables schedulable
c [simpleprobe-6] limit 142823188 penalty 0 = 0 + 0
c [decomp-39] removed 1389 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 1389 variables, found 47686 hbrs, 403 units
c [unhide-14] limit 3570579 with penalty 1 = 0 + 1
c [unhide-14-15] 2 units, 115 failed, 45816 tauts, 0 hbrs, 110469 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 213 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 223161232 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 803 (0%) of length 9
c [cce-4-1] eliminated 2 clauses out of 333 (1%) of length 8
c [cce-4-1] eliminated 10 clauses out of 598 (2%) of length 7
c [cce-4-1] eliminated 2130 clauses out of 3943 (54%) of length 6
c [cce-4-1] eliminated 14988 clauses out of 26801 (56%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 17131 large clauses in 223161232 steps
c [cce-4-1] allowing another 111580616 steps for small clauses
c [cce-4-1] scheduling 223642 clauses = 189886 binary + 33756 ternary
c [cce-4-1] tried to eliminate 4684 small clauses 2%
c [cce-4-1] eliminated 903 binary clauses 0%
c [cce-4-1] eliminated 285 ternary clauses 1%
c [cce-4-1] eliminated 1188 small clauses 1%
c [cce-4-1] eliminated 1740 small clauses in 223161233 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 18871 covered clauses in round 1
c [cce-4] eliminated 18871 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 60888 variables 100%
c [elim-11] limit of 357057972 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 12029 variables 20% in round 1 in 25604991 steps
c [elim-11-1] backward subsumption/strengthening limit 25604900
c [elim-11-1-1] backward checking 29503 touched variables 48%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 137 and strengthened 279 clauses in 5090620 steps
c [elim-11-1] rescheduled 995 variables 2% by backward subsumption
c [elim-11-2] eliminated 114 variables 0% in round 2 in 741804 steps
c [elim-11-2] backward subsumption/strengthening limit 741800
c [elim-11-2-1] backward checking 838 touched variables 1%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 22 and strengthened 20 clauses in 673446 steps
c [elim-11-2] rescheduled 115 variables 0% by backward subsumption
c [elim-11-3] eliminated 4 variables 0% in round 3 in 95778 steps
c [elim-11-3] backward subsumption/strengthening limit 95700
c [elim-11-3-1] backward checking 56 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 9 and strengthened 3 clauses in 95701 steps
c [elim-11] incomplete 13 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 12148 = 20% variables out of 60888 scheduled
c [bca-10] limit of 10000000 steps and 590468 added (scaled 2)
c [bca-10] 86804 out of 97482 literals actually usable 89%
c [bca-10] added 179 blocked clauses in 223327 steps
c [sweep-9] limit 10711739 penalty 0 = 0 + 0
c [sweep-9-1] 2873 pos 6.1% + 44420 neg 93.9% = 47293 sched 97.0% ret 1447
c [sweep-9-1] 10764204 steps 166 queries 2154.60 avg class size
c [sweep-9-1] 1754 decisions 136 SAT calls 73.88 avg env size
c [sweep-9-1] 44172 variables remain 91% (4536 retained 9%)
c [decomp-40] removed 101 variables
c [sweep-9-1] removed 101 vars (0 failed, 33 eqs, 42 impls)
c [sweep-9] removed 101 vars in TOTAL (1 rounds, 165 queries)
c [phase-count-14] 293350 negative 99.6% of 294411 except 1061 0.4%
c [phase-count-14] 215917 positive 73.3% of 294411 except 78494 26.7%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 31002 enqueued variables after 101459 conflicts
c [score-dist-14] active 17637 (36%), one 15865 (33%), zero 15137 (31%)
c [score-dist-14] max exp 692, different 374 (54%)
c [score-dist-14] median active exp 650, avg 574.5
c [simplification-14] removed 14736 variables 23.3% (48639 remain 19%)
c [simplification-14] removed 72556 irredundant clauses 19.8% (294411 remain 26%)
c [simplification-14] maximum reduction of 23% = max (23%, 20%)
c [simplification-14] large reduction 23% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 113459 (soft 103459 + delta 10000)
c [simplification-14] new conflict limit 103459 (hard 113459)
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  220.8   48638   294411    101983    7788   2494 186629   17    47   38  35%     17  -10   21   18  116%
c i  221.6   48637   294411    103162    8833   2504 186638   17    61   38  28%     -0    3   16   18   90%
c i  222.1   48634   294411    104035    9632   2509 186642   17    56   39  30%     -7   -1   19   18  108%
c 
c [simplification-15] limit 103459 conflicts (hard 113459) hit after 106023 conflicts
c [quatres-11] found 34613 quaternary clauses 65% in total
c [quatres-11-1] removed 3 duplicate quaternary clauses
c [quatres-11-2] added 14 single-self-subsuming ternary resolvents
c [quatres-11-2] added 7 quaternary resolvents
c [ternres-11] limit 36604376 with penalty 0 = 0 + 0
c [ternres-11] all 48634 free variables schedulable
c [ternres-11] 828 ternary resolvents (7 bin, 821 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1143886 penalty 4 = 4 + 0
c [card-5] found 3335 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1143886 for elimination
c [card-5] 3335 out of 3335 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-41] removed 5 variables
c [unhide-15] limit 7320875 with penalty 0 = 0 + 0
c [unhide-15-19] 0 units, 184 failed, 22642 tauts, 0 hbrs, 62305 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 158 transitive binary clauses
c [transred-11] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 47666 variables 100%
c [block-5] limit of 45755470 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 20 blocked clauses
c [block-5] 20 < 1/100 * 286805 = 2868 considered unsuccessful
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 47666 variables 100%
c [elim-12] limit of 732087520 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 790 variables 2% in round 1 in 22140907 steps
c [elim-12-1] backward subsumption/strengthening limit 22140900
c [elim-12-1-1] backward checking 3919 touched variables 8%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 35 and strengthened 10 clauses in 848749 steps
c [elim-12-1] rescheduled 121 variables 0% by backward subsumption
c [elim-12-2] eliminated 12 variables 0% in round 2 in 54787 steps
c [elim-12-2] backward subsumption/strengthening limit 54700
c [elim-12-2-1] backward checking 78 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 4 and strengthened 11 clauses in 54701 steps
c [elim-12-2] rescheduled 38 variables 0% by backward subsumption
c [elim-12-3] eliminated 1 variables 0% in round 3 in 23897 steps
c [elim-12-3] backward subsumption/strengthening limit 23800
c [elim-12-3-1] backward checking 10 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 2 and strengthened 0 clauses in 23801 steps
c [elim-12] incomplete 4 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 803 = 2% variables out of 47666 scheduled
c [bca-11] limit of 10000000 steps and 568038 added (scaled 2)
c [bca-11] 79799 out of 93728 literals actually usable 85%
c [bca-11] added 48 blocked clauses in 202243 steps
c [sweep-10] limit 10981312 penalty 0 = 0 + 0
c [sweep-10-1] 2831 pos 6.6% + 39865 neg 93.4% = 42696 sched 91.1% ret 4167
c [sweep-10-1] 10986448 steps 141 queries 2122.38 avg class size
c [sweep-10-1] 1393 decisions 118 SAT calls 60.40 avg env size
c [sweep-10-1] 40867 variables remain 87% (5971 retained 13%)
c [decomp-42] removed 118 variables
c [sweep-10-1] removed 118 vars (0 failed, 27 eqs, 34 impls)
c [sweep-10] removed 118 vars in TOTAL (1 rounds, 140 queries)
c [phase-count-15] 282158 negative 99.6% of 283217 except 1059 0.4%
c [phase-count-15] 206027 positive 72.7% of 283217 except 77190 27.3%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 27501 enqueued variables after 106023 conflicts
c [score-dist-15] active 19244 (41%), one 14260 (31%), zero 13241 (28%)
c [score-dist-15] max exp 925, different 455 (49%)
c [score-dist-15] median active exp 842, avg 740.6
c [simplification-15] removed 1889 variables 3.9% (46745 remain 19%)
c [simplification-15] removed 11194 irredundant clauses 3.8% (283217 remain 25%)
c [simplification-15] maximum reduction of 4% = max (4%, 4%)
c [simplification-15] geometric conflict interval increment 4733 = 23666 / 5
c [simplification-15] new conflict interval 28399
c [simplification-15] penalized conflict interval 28399 = 1 * 28399
c [simplification-15] hard conflict limit 148621 (soft 134422 + delta 14199)
c [simplification-15] new conflict limit 134422 (hard 148621)
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  228.6   46744   283217    106780   11069   2672 169892   24    70   40  35%     10   12   49   18  267%
c i  229.8   46743   283217    108600   12524   2712 169912   20    54   40  37%      1   -4    5   18   29%
c i  230.4   46448   283217    109329   13126   2720 169914   19    49   40  39%     -6   -8   19   18  102%
c i  231.7   46444   283217    111276   14937   2725 169920   17    38   40  44%     -0  -19   11   18   62%
c i  232.5   46443   283217    112150   15747   2725 169920   17    37   43  46%     -6  -20   18   18   98%
c i  233.0   46442   283217    112741   16255   2725 169921   17    36   43  47%    -10  -21   19   18  107%
c i  234.1   46441   283217    114371   17737   2731 169928   16    33   43  50%     -4  -24   18   18  100%
c i  239.9   46439   283217    121928   24224   2765 169953   13    22   49  60%     80  -32    7   17   38%
c i  240.1   45370   283217    122127   24355   2775 169958   13    21   49  60%     62  -32    6   17   33%
c i  241.1   45315   283217    123351   25387   2777 169961   14    22   49  62%     11  -31   15   17   87%
c i  241.2   45311   283217    123410   25430   2777 169961   13    22   49  62%      9  -31   14   17   81%
c i  245.0   45305   283217    128788   29705   2815 169975    9    14   50  65%     45  -35    5   17   30%
c i  245.7   42736   283217    129659   30369   2827 169981   11    18   50  60%     10  -32   13   17   79%
c i  245.8   41498   283217    129839   30508   2834 169984   11    17   50  61%      4  -32   11   17   67%
c i  245.8   39567   283217    129843   30505   2835 169985   10    17   50  61%      4  -32   11   17   66%
c i  245.8   39139   283217    129854   30503   2837 169987   10    17   50  61%      4  -32   11   17   64%
c i  245.9   38659   283217    129892   30520   2840 169991   10    17   50  61%      3  -32   10   17   58%
c i  245.9   36569   283217    129894   30520   2840 169992   10    17   50  61%      3  -32   10   17   58%
c i  245.9   35853   283217    129904   30523   2842 169994   10    17   50  61%      3  -32    9   17   56%
c i  245.9   33454   283217    129905   30523   2842 169994   10    17   50  61%      3  -32    9   17   56%
c i  245.9   32359   283217    129909   30524   2842 169996   10    17   50  61%      3  -32    9   17   55%
c i  245.9   30255   283217    129915   30527   2842 169997   10    17   50  61%      2  -32    9   17   54%
c i  245.9   29609   283217    129917   30527   2843 169997   10    17   50  61%      2  -32    9   17   54%
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  245.9   27049   283217    129918   30527   2843 169997   10    17   50  61%      2  -32    9   17   53%
c i  245.9   26165   283217    129919   30527   2843 169997   10    17   50  61%      2  -32    9   17   53%
c 0  245.9   25354   283217    129919   30527   2843 169997   10    17   50  61%      2  -32    9   17   53%
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: 344 basic ate = 330 trn 96% + 14 lrg 4% in 3 updates
c bcas: 11 count, 848 added (74 skipped), 3575458 steps
c bkwd: tried 365969 clauses, 731447 lits, 2.00 lits/clause
c bkwd: checked 8906998 occs, 24.34 occs/clause, 12.18 occs/lit
c bkwd: subsumed 20 binary, 369 ternary, 32 large
c bkwd: strengthened 1 binary, 3 ternary (100% self), 656 large (0% self)
c blkd: 5 bces, 10197 removed, 7218335 resolutions, 19703782 steps
c blkd: 10040 blocking literals 2%, 0 pure
c bump: 130019 bumped seen, 56799004 lits 436.9 on average
c card: 5 count, 0 units, 0 am1, 25537356 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 82861 subsumed
c card: 17356 at-most-one constraints found, average size 4.71
c card: 17356 at-most-one constraints used 100%, average size 4.71
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 4 cces, 18610 eliminated, 18610 ate 100%, 0 abce 0%
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: 3776495 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 110 gcs, 0 rescored clauses, 68 rescored vars
c dcps: 42 decompositions, 11910 equivalent 5%
c deco: 2918 decision-only clauses 2%, 62% reduction
c decs: 1681965 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 12 elims, 113056 eliminated 43%, 1 pure 0%
c elms: 28 rounds, 2.3 rounds/bve
c elms: 97009 small 86%, 16046 large 14%
c elms: 309764 tried small, 97009 succeeded 31%, 212755 failed 69%
c elms: 46133 subsumed, 68552 strengthened, 275 blocked
c elms: 15623811 copies, 15211007 resolutions, 12519836 ipos
c elms: 2321609 subchks, 1411766 strchks
c gaus: 8 extractions, 1533 extracted, 2.3 size, 3 max
c gaus: exported 1 units, 13 binary and 0 ternary equations
c gaus: 0 gc, 32626814 steps, 16313407 extr 50%, 37066 elim 0%
c glue: 24.3 orig avg, 24.3 real avg, 3.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 383168 = 146767 simple 38% + 226835 trn 59% + 9566 lrg 2%, 2297 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 130019 clauses, 130.6 length
c lrnd: 16985911 lits = 31199716 orig - 14213805 removed 46%
c lrnd: 55486 uips 43%, 64922 flips 50%
c mins: 122388 mins 95%, 1359 bin 1%, 2584 size 2%
c mins: 51813668 poisoned searches, 11379850 hits, 22% hit rate
c mins: 68099082 used twice searches, 1544641 hits, 2% hit rate
c move: moved 17635, 11000 bin 62%, 6635 trn 38%
c otfs: 256 driving 29%, 640 restarting 71%
c otfs: str 896, 856 red 96%, 40 irr 4%
c otfs: str 896, 0 bin 0%, 51 trn 6%, 845 lrg 94%
c otfs: sub 2, 2 red 100%, 0 irr 0%
c otfs: sub 2, 0 bin 0%, 0 trn 0%, 2 lrg 100%
c phas: 15 computed, 128317 set, 0 pos (0%), 128317 neg (100%)
c prbs: 5 basic, 5712 probed, 660 failed, 0 lifted
c prbs: 6 simple, 982194 probed, 1161 failed, 2564 eqs
c prbs: 5 treelook, 70 probed, 11 failed, 0 lifted
c prom: 4795 locked 2% out of 230962 tried
c prps: 774265057 props, 447 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 11 count, 143 quat, 80 self1, 0 self2, 825 dup
c queu: 15 sorted, 1681965 next (86529 steps 0.05)
c queu: 59469393 enq (62316968 steps 1.05), 56799004 deq 96%
c redc: 3203 clauses 18%, 17664 tried 14%, 59 sat 0%
c redc: 6205 lits 4%, 170854 tried 1%, 59 sat 0%
c redc: 365 times jump level reduced, 30.1 levels on average
c reds: 1 count, 129919.0 conflicts per reduce
c reds: 0 memlim 0%, 1 arith 100%
c reds: 25004 collected 75%, 8420 retired 25%
c rmbd: 42780 removed, 7767 red 18%
c rsts: 5488 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: 15 count, 13 confs 87%, 0 vars 0%
c simp: 1 its 7%, 1 bin 7%, 0 trns 0%
c subl: 130019 count (117366 tried 0.9), 11259 sub out of 125866 (8.9%)
c swps: 10 count, 10 rounds, 547 queries (54.7/round)
c swps: 453 sat calls, 25 unsat (0.8% success rate)
c swps: 5377 decisions 11.9, 356 conflicts 0.8
c swps; 5220.8 avg class size, 77.9 avg environment size
c swps: 0 failed, 151 impls, 109 equivs
c swp0: 179 type 0 queries, 49 unsat (27.4%), 165 sat (92.2%)
c swp1: 368 type 1 queries, 280 unsat (76.1%), 273 sat (74.2%)
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: 3624714 calls to obtain time
c tops: 111933 fixed 43%, 325 its, 399.75 confs/it
c trds: 11 transitive reductions, 1598 removed, 20 failed
c trds: 10815 nodes, 22673 edges, 21017489 steps
c trim: 486839 words, 1.9 MB
c trnr: 11 count, 33 bin, 6647 trn, 55967225 steps
c unhd: 15 count, 19 rounds, 54561113 steps
c unhd: 1469 non-trivial sccs of average size 2.2
c unhd: 84 units, 84 bin, 0 trn, 0 lrg
c unhd: 8238 failed, 8194 stamp, 0 lits, 15 bin, 20 trn, 0 lrg
c unhd: 165561 tauts, 3185 bin 2%, 13843 trn 8%, 5248 lrg 3%
c unhd: 165561 tauts, 143285 stamp 87%, 118675 red 72%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 852346 str, 84 bin 0%, 7383 trn 1%, 844879 lrg 99%, 813101 red 95%
c vars: 25354 remaining 10% and 236899 removed 90% out of 262253
c vars: 111933 fixed 43%, 113056 eliminated 43%, 11910 equivalent 5%
c vsts: 4312260563 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 5.5 search visits per propagation, 31917.1 per conflict
c wchs: 403827043 pushed, 47641938 enlarged, 167 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         126009         25004          8420       4710529        815047         56226
c 
c  0 0         14806  12       500   2         0   0   2695871  57    376908  46     19045  34     1.8
c  1 5          8703   7       870   3       327   4    438874   9<    97517  12      6753  12     1.3
c  2 6         30689  24      5830  23      1226  15    513581  11    133589  16<     9662  17     5.4
c  3 9         31006  25<     8672  35      1813  22    281696   6     68238   8      5100   9<    7.3
c  4 14         9990   8      3065  12<     1003  12    243655   5     33481   4      3152   6     3.5
c  5 21         5722   5      1224   5       691   8<   160532   3     23077   3      2385   4     2.2
c  6 30         5641   4      1040   4       574   7    128034   3     20913   3      2053   4     1.6
c  7 41         5065   4      1083   4       541   6     95012   2     21315   3      2281   4     1.9
c  8 54         3898   3       904   4       506   6     61487   1     13159   2      1641   3     1.6
c  9 69         2828   2       626   3       387   5     34567   1      9214   1      1280   2     1.1
c 10 86         3134   2       659   3       477   6     39451   1     10422   1      1601   3     1.3
c 11 126        2911   2       382   2       508   6     13574   0      5485   1       967   2     1.1
c 12 230        1524   1       148   1       354   4      4016   0      1667   0       297   1     0.9
c 13 534          92   0         1   0        13   0       179   0        62   0         9   0     0.1
c 
c avg                  3.5           3.8           5.4           1.5           1.8           2.7
c std                  2.8           2.4           3.2           2.3           2.5           3.0
c 
c   18.242   7% elim
c   11.824   5% probe
c   10.132   4% bump
c    9.939   4% unhide
c    9.525   4% cce
c    4.655   2% sweep
c    3.530   1% gauss
c    2.042   1% bca
c    2.002   1% block
c    1.194   0% transred
c 
c    2.833 < 1% rest (below)
c 
c    1.183   0% decide
c    0.529   0% ternres
c    0.519   0% quatres
c    0.355   0% card
c    0.245   0% rescore
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    5.327   2% preprocessing     7%
c   66.016  27% inprocessing     93%
c ==================================
c   71.343  29% simplifying
c  174.550  71% search
c ==================================
c  245.897 100% all
c 
c        129919 conflicts,         528.3 confs/sec
c          1915 ternaries,          67.8 confs/ternary
c          1773 binaries,           73.3 confs/binary
c           325 iterations,        399.8 confs/iteration
c 
c             1 reductions,          0.0 redus/sec, 129919.0 confs/reduction
c          5488 restarts,           22.3 rests/sec,     23.7 confs/restart
c       1681965 decisions,        6840.1 decis/sec,     12.9 decis/conflict
c     774265057 propagations,  3148732.9 props/sec,    460.3 props/decision
c 
c 245.9 seconds, 98.7 MB
c launch: done
