c launch: /data/cnf/sc2014/app/ACG-15-10p0.cnf.bz2
c host: atom24
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=6
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] AVG (--score=6)
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        45      40      4  5529    0    10   51   1%      0   10    2    0 23341%
c i    5.5  115445   680813        83      66     10  5531    0    11   51   3%      0   11    4    0 21664%
c i    5.7  115444   680813       185     141     20  5543    0    16   51   3%      0   16    5    0 17060%
c i    5.8  115071   680813       255     192     29  5552    1    17   51   3%      0   17    5    0 14456%
c i    6.2  114338   680813       424     308     55  5575    1    24   51   3%      0   24    7    0 12273%
c i    6.3  114006   680813       487     352     62  5585    1    26   51   4%      0   26    8    0 11714%
c i    6.6  113878   680813       606     446     70  5601    1    31   51   4%      0   31   10    0 11012%
c i    6.8  113090   680813       667     490     78  5609    1    35   51   4%      0   35    9    0 9810%
c i    7.3  113075   680813       851     643     92  5617    2    44   51   5%      1   44   14    0 9509%
c i    7.4  113059   680813       874     659     94  5619    2    46   51   5%      1   46   16    0 9910%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 3618 variables
c [simpleprobe-2] all 111903 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 111903 variables remain 100% (0 retained 0%)
c [simpleprobe-2] removed 0 variables, found 6849 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 58363 literals 26%
c [treelook-1] scheduling used 307694 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 407062 steps
c [treelook-1] 58359 literals remain 26%
c [treelook-1] 58117 variables remain to probed next time 52%
c [treelook-1] removed 0 variables, found 2764 hbrs
c [basicprobe-1] limit 5263232 based on 657904 irredundant clauses
c [basicprobe-1-0] 32241 probes remain 30% after last round
c [basicprobe-1-0] 16 units = 16 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3358 variables, found 14412 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 6 units, 1950 failed, 2540 tauts, 0 hbrs, 15375 literals
c [elim-2] 54602 variables 52% will be scheduled this time
c [elim-2] scheduled 54602 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 10567 not tried 10% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 1462 = 3% variables out of 54602 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 591093 negative 99.2% of 595889 except 4796 0.8%
c [phase-count-2] 473042 positive 79.4% of 595889 except 122847 20.6%
c [phase-count-2] less non-negative clauses 4796 than limit 59500 (10.0%)
c [phase-count-2] non-pos/non-neg = 122847/4796 = 25.61 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 3480 negative 100%
c [sort-queue-2] sorted 84127 enqueued variables after 874 conflicts
c [score-dist-2] active 19632 (19%), one 0 (0%), zero 84127 (81%)
c [score-dist-2] max exp 511, different 9 (2%)
c [score-dist-2] median active exp 510, avg 510.1
c [simplification-2] removed 8407 variables 7.5% (103759 remain 41%)
c [simplification-2] removed 84924 irredundant clauses 12.5% (595889 remain 53%)
c [simplification-2] maximum reduction of 12% = max (7%, 12%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1000 (hard 11000)
c [simplification-2] 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   11.1  103758   595889       937     688     95 23462    3    54   46   5%      1   53   19    0 10052%
c i   11.2  103748   595889       958     704     95 23465    3    56   46   5%      1   56   20    0 10176%
c i   11.3  103741   595889       997     737     96 23467    4    61   46   6%      1   61   26    0 11131%
c 
c [simplification-3] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4375 at-most-one constraints of average size 4.4
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4375 out of 4375 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 835 variables
c [unhide-3] limit 111283 with penalty 0 = 0 + 0
c [unhide-3-3] 10 units, 849 failed, 8148 tauts, 0 hbrs, 6198 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 101313 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 19759 not tried 20% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 3297 = 3% variables out of 101313 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 564084 negative 99.2% of 568841 except 4757 0.8%
c [phase-count-3] 449955 positive 79.1% of 568841 except 118886 20.9%
c [phase-count-3] less non-negative clauses 4757 than limit 56800 (10.0%)
c [phase-count-3] non-pos/non-neg = 118886/4757 = 24.99 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 2771 negative 100%
c [sort-queue-3] sorted 74377 enqueued variables after 1000 conflicts
c [score-dist-3] active 23639 (24%), one 0 (0%), zero 74377 (76%)
c [score-dist-3] max exp 511, different 9 (2%)
c [score-dist-3] median active exp 511, avg 510.3
c [simplification-3] removed 5689 variables 5.5% (98016 remain 39%)
c [simplification-3] removed 27048 irredundant clauses 4.5% (568841 remain 51%)
c [simplification-3] maximum reduction of 5% = max (5%, 5%)
c [simplification-3] large reduction 5% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-3] new conflict limit 3000 (hard 13000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   14.3   98015   568841      1010     724     92 19612    4    61   45   6%      1   61   26    0 10824%
c i   14.3   98005   568841      1011     724     92 19612    4    61   45   6%      1   61   26    0 10782%
c i   14.3   97997   568841      1018     729     92 19613    4    62   45   6%      1   61   26    0 10627%
c i   14.5   97988   568841      1090     783    100 19621    4    72   46   5%      1   71   23    0 8851%
c i   14.5   97973   568841      1097     787    100 19623    4    72   46   5%      1   72   23    0 8822%
c i   14.6   97841   568841      1142     825    103 19625    4    77   46   5%      1   76   22    0 8166%
c i   14.6   97808   568841      1144     825    104 19625    4    77   46   5%      1   76   22    0 8103%
c i   14.7   97459   568841      1153     833    104 19625    4    78   46   5%      1   77   25    0 8748%
c i   14.7   97452   568841      1158     836    104 19626    4    78   46   6%      1   77   26    0 8903%
c i   14.8   97031   568841      1206     880    104 19628    5    83   46   6%      1   82   29    0 8973%
c i   14.8   96718   568841      1212     885    104 19628    5    83   46   6%      1   82   29    0 8822%
c i   14.8   96712   568841      1223     895    104 19628    5    83   46   6%      0   83   28    0 8619%
c i   14.9   96699   568841      1224     895    104 19628    5    83   46   6%      0   83   28    0 8586%
c i   14.9   96695   568841      1255     922    106 19629    5    86   46   6%      0   85   29    0 8471%
c i   14.9   96694   568841      1259     925    106 19629    5    86   46   6%      0   85   30    0 8455%
c i   15.2   96534   568841      1372    1029    108 19634    6    99   46   6%      1   98   30    0 7536%
c i   15.2   96533   568841      1374    1030    108 19634    6    99   46   6%      1   99   30    0 7481%
c i   15.3   96489   568841      1448    1097    111 19634    7   103   46   6%      1  102   35    0 7591%
c i   15.6   96486   568841      1636    1249    123 19652    7   115   46   6%      1  114   30    1 5751%
c i   15.7   96479   568841      1670    1273    127 19656    7   117   46   6%      1  116   30    1 5505%
c i   15.8   96475   568841      1682    1284    127 19656    8   119   46   6%      1  117   32    1 5730%
c i   15.9   96470   568841      1765    1349    132 19660    8   128   46   6%      1  126   31    1 5224%
c i   16.3   96465   568841      1902    1476    135 19662    9   138   47   7%      1  136   33    1 4942%
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   16.3   96458   568841      1903    1476    135 19662    9   138   47   7%      1  136   33    1 4923%
c i   16.3   96451   568841      1904    1476    135 19662    9   138   47   7%      1  136   32    1 4904%
c i   16.3   96444   568841      1905    1476    135 19662    9   138   47   7%      1  136   32    1 4885%
c i   16.3   96437   568841      1906    1476    135 19662    9   138   47   7%      1  136   32    1 4866%
c i   16.4   96430   568841      1946    1507    139 19663    9   141   47   7%      1  139   31    1 4610%
c i   16.8   96429   568841      2125    1668    144 19666   12   159   47   8%      1  157   50    1 5674%
c i   16.8   96420   568841      2131    1673    144 19666   12   159   47   8%      1  157   49    1 5608%
c i   16.9   96419   568841      2162    1701    145 19667   13   168   47   8%      1  166   62    1 6485%
c i   16.9   96418   568841      2170    1708    145 19667   13   170   47   8%      1  167   62    1 6430%
c i   16.9   96409   568841      2186    1721    146 19667   13   173   47   8%      1  170   63    1 6393%
c i   17.0   96399   568841      2196    1730    146 19667   14   174   47   8%      1  171   66    1 6530%
c i   17.0   96392   568841      2201    1734    146 19667   14   174   47   8%      1  172   64    1 6420%
c i   17.2   96391   568841      2332    1851    151 19672   14   175   47   8%      1  172   46    1 4419%
c i   17.6   96378   568841      2483    1988    159 19674   15   180   47   8%      1  177   45    1 3970%
c i   17.6   96368   568841      2516    2017    159 19675   16   185   47   8%      1  181   50    1 4227%
c i   18.4   96365   568841      2930    2368    179 19698   17   203   48   8%      2  198   34    1 2472%
c 
c [simplification-4] limit 3083 conflicts (hard 13000) hit after 3083 conflicts
c [decomp-7] removed 1813 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 44031 literals 23%
c [treelook-2] scheduling used 197045 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 291784 steps
c [treelook-2] 44028 literals remain 23%
c [treelook-2] 28557 variables remain to probed next time 30%
c [treelook-2] removed 0 variables, found 1579 hbrs
c [unhide-4] limit 325116 with penalty 0 = 0 + 0
c [unhide-4-4] 10 units, 909 failed, 1471 tauts, 0 hbrs, 15847 literals
c [elim-4] 10403 variables 11% will be scheduled this time
c [elim-4] scheduled 10403 variables 11%
c [elim-4] boosting limit by 20
c [elim-4] limit of 650232100 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 3 variables 0% in round 1 in 19583180 steps
c [elim-4-1] backward subsumption/strengthening limit 19583100
c [elim-4-1-1] backward checking 5528 touched variables 6%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 215 and strengthened 76 clauses in 884003 steps
c [elim-4-1] rescheduled 744 variables 1% by backward subsumption
c [elim-4-2] eliminated 95 variables 0% in round 2 in 442434 steps
c [elim-4-2] backward subsumption/strengthening limit 442400
c [elim-4-2-1] backward checking 737 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 67 and strengthened 62 clauses in 284591 steps
c [elim-4-2] rescheduled 297 variables 0% by backward subsumption
c [elim-4-3] eliminated 12 variables 0% in round 3 in 238725 steps
c [elim-4-3] backward subsumption/strengthening limit 238700
c [elim-4-3-1] backward checking 112 touched variables 0%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 4 and strengthened 4 clauses in 131168 steps
c [elim-4] incomplete 20 not tried 0% in round 3
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 110 = 1% variables out of 10403 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 539130 negative 99.1% of 543887 except 4757 0.9%
c [phase-count-4] 428310 positive 78.7% of 543887 except 115577 21.3%
c [phase-count-4] less non-negative clauses 4757 than limit 54300 (10.0%)
c [phase-count-4] non-pos/non-neg = 115577/4757 = 24.30 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 714 negative 100%
c [sort-queue-4] sorted 61790 enqueued variables after 3083 conflicts
c [score-dist-4] active 32818 (35%), one 0 (0%), zero 61790 (65%)
c [score-dist-4] max exp 513, different 11 (2%)
c [score-dist-4] median active exp 513, avg 512.3
c [simplification-4] removed 1757 variables 1.8% (94608 remain 38%)
c [simplification-4] removed 24954 irredundant clauses 4.4% (543887 remain 49%)
c [simplification-4] maximum reduction of 4% = max (2%, 4%)
c [simplification-4] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-4] new conflict interval 4000
c [simplification-4] penalized conflict interval 4000 = 1 * 4000
c [simplification-4] hard conflict limit 17083 (soft 7083 + delta 10000)
c [simplification-4] new conflict limit 7083 (hard 17083)
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   21.3   94607   543887      3635    2979    195 19027   20   199   47  10%      4  193   31    2 1781%
c i   21.4   94606   543887      3710    3049    196 19029   21   200   47  10%      4  193   37    2 2080%
c i   21.7   94600   543887      3892    3212    198 19034   21   202   47  10%      3  194   35    2 1840%
c i   22.2   94589   543887      4137    3421    202 19049   23   213   47  11%      3  205   43    2 2072%
c i   22.2   94513   543887      4138    3421    202 19049   23   213   47  11%      3  205   43    2 2064%
c i   22.6   94213   543887      4359    3613    215 19060   24   218   47  11%      3  209   39    2 1761%
c i   22.6   94203   543887      4360    3613    215 19060   24   218   47  11%      3  209   39    2 1754%
c i   22.6   94197   543887      4361    3613    215 19060   24   218   47  11%      3  209   38    2 1747%
c i   22.6   94185   543887      4363    3614    215 19060   24   218   47  11%      3  209   38    2 1745%
c i   22.7   94170   543887      4413    3655    217 19063   24   218   47  11%      3  209   35    2 1571%
c i   22.8   94161   543887      4454    3694    217 19064   24   220   47  11%      2  211   36    2 1603%
c i   23.3   93920   543887      4683    3891    221 19071   25   231   47  11%      2  221   43    2 1783%
c i   23.4   93894   543887      4720    3925    221 19072   26   234   47  11%      2  224   51    2 2069%
c i   23.7   93596   543887      4871    4065    221 19074   27   240   48  11%      2  229   59    3 2261%
c i   23.8   93583   543887      4912    4104    222 19074   28   241   48  11%      2  230   56    3 2132%
c i   23.9   93582   543887      4979    4164    226 19074   28   242   48  12%      2  231   54    3 2018%
c i   24.0   93574   543887      5021    4203    226 19075   29   244   48  12%      2  232   65    3 2374%
c i   24.0   93565   543887      5022    4203    226 19075   29   244   48  12%      2  232   65    3 2365%
c i   24.1   93552   543887      5024    4203    226 19075   29   243   48  12%      2  232   65    3 2356%
c i   24.1   93536   543887      5025    4203    226 19075   29   243   48  12%      2  232   65    3 2347%
c i   24.1   93529   543887      5026    4203    226 19075   29   243   48  12%      2  232   64    3 2337%
c i   24.1   93523   543887      5050    4220    229 19078   29   243   48  12%      2  232   61    3 2216%
c i   24.1   93506   543887      5051    4220    229 19078   29   243   48  12%      2  232   61    3 2208%
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.1   93487   543887      5052    4220    229 19078   29   243   48  12%      2  231   61    3 2199%
c i   24.3   93238   543887      5195    4344    234 19083   30   242   48  12%      2  230   57    3 1983%
c i   25.3   93237   543887      5722    4805    252 19100   32   242   49  13%      3  228   50    3 1543%
c i   26.9   93236   543887      6499    5518    265 19110   34   242   50  14%      5  225   49    4 1333%
c 
c [simplification-5] limit of 295 binary hit after 295 binaries
c [quatres-1] found 32940 quaternary clauses 37% in total
c [quatres-1-2] added 15 single-self-subsuming ternary resolvents
c [quatres-1-2] added 5 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 93236 free variables schedulable
c [ternres-1] 1535 ternary resolvents (5 bin, 1530 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 638 xors of average arity 2.1
c [gauss-1] connected 1313 occurrences of 868 variables (average 1.5)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 663 variables
c [gauss-1] exported 0 unary, 10 binary and 0 ternary equations
c [basicprobe-2] limit 16342045 penalty 0 = 0 + 0
c [basicprobe-2-0] 28588 probes remain 31% after last round
c [basicprobe-2-0] 61 units = 61 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1507 variables, found 27496 hbrs
c [bate-1] eliminated 22 asymmetric tautologies during probing
c [unhide-5] limit 653681 with penalty 0 = 0 + 0
c [unhide-5-5] 10 units, 332 failed, 9047 tauts, 0 hbrs, 15721 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 120 transitive binary clauses
c [transred-1] found 9 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 90303 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 8876 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 13 clauses out of 330 (4%) of length 10
c [cce-1-1] eliminated 49 clauses out of 1799 (3%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 62 large clauses in 30000002 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 363962 clauses = 272181 binary + 91781 ternary
c [cce-1-1] tried to eliminate 327 small clauses 0%
c [cce-1-1] eliminated 59 binary clauses 0%
c [cce-1-1] eliminated 47 ternary clauses 0%
c [cce-1-1] eliminated 106 small clauses 0%
c [cce-1-1] eliminated 106 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 168 covered clauses in round 1
c [cce-1] eliminated 168 covered clauses in TOTAL during 1 rounds
c [cce-1] 168 < 1/100 * 503411 = 5034 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 90303 variables 100%
c [elim-5] limit of 65368182 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 2322 variables 3% in round 1 in 41010256 steps
c [elim-5-1] backward subsumption/strengthening limit 24357926
c [elim-5-1-1] backward checking 10406 touched variables 12%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 47 and strengthened 29 clauses in 2296226 steps
c [elim-5-1] rescheduled 215 variables 0% by backward subsumption
c [elim-5-2] eliminated 14 variables 0% in round 2 in 147545 steps
c [elim-5-2] backward subsumption/strengthening limit 147500
c [elim-5-2-1] backward checking 112 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 7 and strengthened 1 clauses in 137972 steps
c [elim-5-2] rescheduled 20 variables 0% by backward subsumption
c [elim-5-3] no variable eliminated in round 3 in 11282 steps
c [elim-5] fully completed in 3 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 2339 = 3% variables out of 90303 scheduled
c [bca-1] limit of 10000000 steps and 997820 added (scaled 2)
c [bca-1] 157669 out of 175930 literals actually usable 90%
c [bca-1] added 167 blocked clauses in 451829 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2753 pos 3.1% + 85211 neg 96.9% = 87964 sched 100.0% ret 0
c [sweep-1-1] 1101114 steps 13 queries 23243.31 avg class size
c [sweep-1-1] 115 decisions 11 SAT calls 58.45 avg env size
c [sweep-1-1] 87935 variables remain 100% (29 retained 0%)
c [decomp-11] removed 29 variables
c [sweep-1-1] removed 29 vars (0 failed, 1 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 29 vars in TOTAL (1 rounds, 12 queries)
c [phase-count-5] 493877 negative 99.1% of 498603 except 4726 0.9%
c [phase-count-5] 399335 positive 80.1% of 498603 except 99268 19.9%
c [phase-count-5] less non-negative clauses 4726 than limit 49800 (10.0%)
c [phase-count-5] non-pos/non-neg = 99268/4726 = 21.00 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 496 negative 100%
c [sort-queue-5] sorted 50825 enqueued variables after 6780 conflicts
c [score-dist-5] active 37110 (42%), one 0 (0%), zero 50825 (58%)
c [score-dist-5] max exp 514, different 12 (2%)
c [score-dist-5] median active exp 514, avg 513.3
c [simplification-5] removed 5301 variables 5.7% (87935 remain 35%)
c [simplification-5] removed 45284 irredundant clauses 8.3% (498603 remain 44%)
c [simplification-5] maximum reduction of 8% = max (6%, 8%)
c [simplification-5] forced so keeping old conflict interval 4000
c [simplification-5] conflict limit remains at 7173 (hard 17083)
c [simplification-5] new binary interval 1000
c 
c [simplification-6] limit 7173 conflicts (hard 17083) hit after 7177 conflicts
c [quatres-2] found 36334 quaternary clauses 41% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [quatres-2-2] added 10 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 87935 free variables schedulable
c [ternres-2] 362 ternary resolvents (0 bin, 362 trn)
c [ternres-2] 30191 variables remain 34% (57744 retained 66%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2579 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2579 out of 2579 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 43 xors of average arity 3.0
c [gauss-2] connected 129 occurrences of 75 variables (average 1.7)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-6] limit 685834 with penalty 0 = 0 + 0
c [unhide-6-6] 5 units, 691 failed, 4292 tauts, 0 hbrs, 12178 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 139 transitive binary clauses
c [transred-2] found 3 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 86802 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 400 blocked clauses
c [block-2] 400 < 1/100 * 497718 = 4977 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 86802 variables 100%
c [elim-6] limit of 68583412 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 1293 variables 1% in round 1 in 39700637 steps
c [elim-6-1] backward subsumption/strengthening limit 28882775
c [elim-6-1-1] backward checking 5692 touched variables 7%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 35 and strengthened 10 clauses in 1128458 steps
c [elim-6-1] rescheduled 131 variables 0% by backward subsumption
c [elim-6-2] eliminated 5 variables 0% in round 2 in 92398 steps
c [elim-6-2] backward subsumption/strengthening limit 92300
c [elim-6-2-1] backward checking 43 touched variables 0%
c [elim-6-2-1] incomplete backward checking 0 remain 0%
c [elim-6-2] subsumed 4 and strengthened 3 clauses in 92301 steps
c [elim-6-2] rescheduled 18 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 13482 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 1298 = 1% variables out of 86802 scheduled
c [bca-2] limit of 10000000 steps and 970161 added (scaled 2)
c [bca-2] 153016 out of 171010 literals actually usable 89%
c [bca-2] added 84 blocked clauses in 445262 steps
c [sweep-2] limit 1028751 penalty 0 = 0 + 0
c [sweep-2-1] 2450 pos 2.9% + 83031 neg 97.1% = 85481 sched 100.0% ret 23
c [sweep-2-1] 1062805 steps 13 queries 20861.69 avg class size
c [sweep-2-1] 277 decisions 12 SAT calls 62.58 avg env size
c [sweep-2-1] 85444 variables remain 100% (60 retained 0%)
c [decomp-13] removed 31 variables
c [sweep-2-1] removed 31 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 31 vars in TOTAL (1 rounds, 12 queries)
c [phase-count-6] 480012 negative 99.0% of 484727 except 4715 1.0%
c [phase-count-6] 385612 positive 79.6% of 484727 except 99115 20.4%
c [phase-count-6] less non-negative clauses 4715 than limit 48400 (10.0%)
c [phase-count-6] non-pos/non-neg = 99115/4715 = 21.02 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 494 negative 100%
c [sort-queue-6] sorted 48061 enqueued variables after 7177 conflicts
c [score-dist-6] active 37412 (44%), one 0 (0%), zero 48061 (56%)
c [score-dist-6] max exp 514, different 12 (2%)
c [score-dist-6] median active exp 514, avg 513.3
c [simplification-6] removed 2462 variables 2.8% (85473 remain 34%)
c [simplification-6] removed 13876 irredundant clauses 2.8% (484727 remain 43%)
c [simplification-6] maximum reduction of 3% = max (3%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 9000
c [simplification-6] penalized conflict interval 9000 = 1 * 9000
c [simplification-6] hard conflict limit 26177 (soft 16177 + delta 10000)
c [simplification-6] new conflict limit 16177 (hard 26177)
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.6   85472   484727      7224    5054   1325 47858   37   238   47  15%      5  219   44    4 1042%
c i   39.6   85467   484727      7756    5534   1336 47864   39   240   48  16%      5  219   65    5 1401%
c i   40.0   85466   484727      7986    5743   1343 47872   40   247   48  16%      4  226   64    5 1323%
c i   40.0   85465   484727      7987    5743   1343 47872   40   247   48  16%      4  226   63    5 1317%
c i   41.2   85464   484727      8740    6419   1351 47882   43   249   48  17%      5  226   68    5 1263%
c i   41.3   85463   484727      8769    6446   1351 47882   43   249   48  17%      5  225   65    5 1196%
c i   41.5   85462   484727      8887    6548   1354 47888   44   252   48  17%      5  227   68    6 1226%
c i   41.7   85460   484727      9042    6681   1360 47898   44   249   48  17%      4  224   52    6  929%
c i   41.7   85459   484727      9043    6681   1360 47898   43   249   48  17%      4  224   52    6  925%
c i   41.9   85458   484727      9178    6804   1361 47899   43   246   48  18%      4  221   49    6  852%
c i   42.1   85457   484727      9257    6875   1361 47901   43   246   48  18%      3  220   46    6  809%
c i   42.1   85454   484727      9258    6875   1361 47901   43   245   48  18%      3  220   46    6  806%
c i   42.7   85450   484727      9621    7193   1369 47913   45   248   48  18%      3  221   57    6  940%
c i   42.8   85444   484727      9633    7203   1369 47914   45   248   48  18%      3  221   55    6  918%
c i   42.8   85443   484727      9635    7204   1369 47914   45   248   48  18%      3  221   55    6  911%
c i   42.8   85442   484727      9636    7204   1369 47914   45   248   48  18%      3  221   55    6  908%
c i   42.8   85441   484727      9641    7208   1369 47914   45   247   48  18%      3  221   54    6  895%
c i   43.8   85440   484727     10364    7838   1383 47925   47   240   49  20%      4  210   64    7  966%
c i   44.0   85439   484727     10461    7925   1384 47926   48   241   49  20%      4  212   64    7  948%
c i   44.4   85438   484727     10603    8050   1385 47929   50   248   49  20%      4  218   91    7 1298%
c i   44.7   85434   484727     10758    8179   1387 47940   50   248   50  20%      3  217   73    7 1024%
c i   44.7   85433   484727     10783    8202   1387 47940   50   248   50  20%      3  218   71    7  999%
c i   44.8   85432   484727     10835    8251   1388 47941   51   249   50  20%      3  218   70    7  975%
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   46.1   85431   484727     11476    8838   1394 47955   53   247   53  22%      4  214   75    8  966%
c i   46.1   85381   484727     11477    8838   1394 47955   53   247   53  22%      4  214   74    8  963%
c i   46.8   85370   484727     11981    9281   1398 47962   56   247   53  23%      4  212   79    8  960%
c i   47.1   85369   484727     12115    9402   1398 47964   56   246   53  23%      3  211   73    8  873%
c i   47.4   85366   484727     12381    9631   1398 47966   56   240   53  23%      3  205   63    9  736%
c i   47.4   85365   484727     12382    9631   1398 47966   56   240   53  23%      3  205   63    9  733%
c i   47.8   85351   484727     12587    9816   1405 47972   56   243   53  23%      3  207   61    9  698%
c i   48.1   85346   484727     12758    9965   1409 47976   57   240   53  24%      2  203   63    9  707%
c i   48.2   85345   484727     12834   10029   1412 47978   57   243   53  24%      2  206   73    9  817%
c i   49.1   85338   484727     13238   10394   1420 47982   57   242   53  24%      2  203   54    9  587%
c i   49.5   85337   484727     13554   10669   1423 47989   56   237   54  24%      2  198   46    9  487%
c i   51.8   85336   484727     14831   11810   1444 48012   57   234   54  24%      9  191   51   10  492%
c i   51.8   85335   484727     14833   11811   1444 48012   57   234   54  24%      9  191   51   10  488%
c i   52.1   85334   484727     15009   11971   1448 48014   57   231   55  25%      7  188   50   10  473%
c i   54.3   85299   484727     16095   12936   1457 48037   61   244   55  25%      9  198   79   12  680%
c i   54.5   85298   484727     16160   12997   1459 48037   61   242   55  25%      8  195   66   12  570%
c i   54.6   85289   484727     16195   13023   1459 48037   61   241   55  25%      8  194   68   12  584%
c 
c [simplification-7] limit 16249 conflicts (hard 26177) hit after 16249 conflicts
c [quatres-3] found 35374 quaternary clauses 40% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [quatres-3-2] added 20 quaternary resolvents
c [ternres-3] limit 7115241 with penalty 0 = 0 + 0
c [ternres-3] 29255 schedulable variables 34%
c [ternres-3] 1228 ternary resolvents (2 bin, 1226 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-14] removed 235 variables
c [simpleprobe-3] all 85238 free variables schedulable
c [simpleprobe-3] limit 14230483 penalty 1 = 1 + 0
c [decomp-15] removed 1992 variables
c [simpleprobe-3] 18825 variables remain 23% (64421 retained 77%)
c [simpleprobe-3] removed 1992 variables, found 41710 hbrs, 363 units
c [unhide-7] limit 1423048 with penalty 0 = 0 + 0
c [unhide-7-7] 7 units, 93 failed, 6214 tauts, 0 hbrs, 52254 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 185 transitive binary clauses
c [transred-3] found 1 units
c [cce-2] limit of 17788103 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 8894058 steps for small clauses
c [cce-2-1] scheduling 298797 clauses = 252168 binary + 46629 ternary
c [cce-2-1] tried to eliminate 204 small clauses 0%
c [cce-2-1] eliminated 40 binary clauses 0%
c [cce-2-1] eliminated 4 ternary clauses 0%
c [cce-2-1] eliminated 44 small clauses 0%
c [cce-2-1] eliminated 1419 small clauses in 17788104 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1419 covered clauses in round 1
c [cce-2] eliminated 1419 covered clauses in TOTAL during 1 rounds
c [cce-2] 1419 < 1/100 * 465411 = 4654 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 83056 variables 100%
c [elim-7] limit of 142304830 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 1323 variables 2% in round 1 in 37984623 steps
c [elim-7-1] backward subsumption/strengthening limit 37984600
c [elim-7-1-1] backward checking 5674 touched variables 7%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 25 and strengthened 93 clauses in 1388434 steps
c [elim-7-1] rescheduled 286 variables 0% by backward subsumption
c [elim-7-2] eliminated 36 variables 0% in round 2 in 289394 steps
c [elim-7-2] backward subsumption/strengthening limit 289300
c [elim-7-2-1] backward checking 265 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 3 and strengthened 1 clauses in 184508 steps
c [elim-7-2] rescheduled 11 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 5442 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1359 = 2% variables out of 83056 scheduled
c [bca-3] limit of 10000000 steps and 922791 added (scaled 2)
c [bca-3] 142681 out of 163396 literals actually usable 87%
c [bca-3] added 50 blocked clauses in 414437 steps
c [sweep-3] limit 2134572 penalty 0 = 0 + 0
c [sweep-3-1] 2604 pos 3.2% + 79036 neg 96.8% = 81640 sched 99.9% ret 57
c [sweep-3-1] 2248351 steps 20 queries 9979.25 avg class size
c [sweep-3-1] 480 decisions 19 SAT calls 447.84 avg env size
c [sweep-3-1] 81515 variables remain 100% (182 retained 0%)
c [decomp-16] removed 6 variables
c [sweep-3-1] removed 6 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 6 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-7] 456364 negative 99.0% of 461072 except 4708 1.0%
c [phase-count-7] 364362 positive 79.0% of 461072 except 96710 21.0%
c [phase-count-7] less non-negative clauses 4708 than limit 46100 (10.0%)
c [phase-count-7] non-pos/non-neg = 96710/4708 = 20.54 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 439 negative 100%
c [sort-queue-7] sorted 40961 enqueued variables after 16249 conflicts
c [score-dist-7] active 40730 (50%), one 0 (0%), zero 40961 (50%)
c [score-dist-7] max exp 515, different 13 (3%)
c [score-dist-7] median active exp 515, avg 514.4
c [simplification-7] removed 3598 variables 4.2% (81691 remain 32%)
c [simplification-7] removed 23655 irredundant clauses 4.9% (461072 remain 41%)
c [simplification-7] maximum reduction of 5% = max (4%, 5%)
c [simplification-7] large reduction 5% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 28249 (soft 18249 + delta 10000)
c [simplification-7] new conflict limit 18249 (hard 28249)
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   60.5   81690   461072     16407    9997   1785 87405   62   249   54  25%      6  201   80   12  676%
c i   61.2   81680   461072     16898   10428   1792 87412   62   241   54  26%      5  192   59   12  485%
c i   62.0   81677   461072     17336   10804   1800 87417   63   238   54  27%      4  188   66   13  523%
c 
c [simplification-8] limit 18249 conflicts (hard 28249) hit after 18250 conflicts
c [quatres-4] found 33680 quaternary clauses 39% in total
c [quatres-4-2] added 6 single-self-subsuming ternary resolvents
c [quatres-4-2] added 10 quaternary resolvents
c [ternres-4] limit 7910480 with penalty 0 = 0 + 0
c [ternres-4] all 81606 free variables schedulable
c [ternres-4] 770 ternary resolvents (0 bin, 770 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 20 xors of average arity 2.9
c [gauss-3] connected 58 occurrences of 46 variables (average 1.3)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 4 variables
c [unhide-8] limit 1582096 with penalty 0 = 0 + 0
c [unhide-8-8] 5 units, 196 failed, 4830 tauts, 0 hbrs, 25005 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 150 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 81337 variables 100%
c [block-3] limit of 39552404 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 10 blocked clauses
c [block-3] 10 < 1/100 * 460338 = 4603 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 81337 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3164192340 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 646 variables 1% in round 1 in 37416191 steps
c [elim-8-1] backward subsumption/strengthening limit 37416100
c [elim-8-1-1] backward checking 2778 touched variables 3%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 10 and strengthened 10 clauses in 788470 steps
c [elim-8-1] rescheduled 56 variables 0% by backward subsumption
c [elim-8-2] eliminated 4 variables 0% in round 2 in 47147 steps
c [elim-8-2] backward subsumption/strengthening limit 47100
c [elim-8-2-1] backward checking 41 touched variables 0%
c [elim-8-2-1] incomplete backward checking 0 remain 0%
c [elim-8-2] subsumed 1 and strengthened 1 clauses in 47101 steps
c [elim-8-2] rescheduled 6 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 3561 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 650 = 1% variables out of 81337 scheduled
c [elim-8] 650 < 1/100 * 81337 = 813 considered unsuccessful
c [bca-4] limit of 10000000 steps and 913300 added (scaled 2)
c [bca-4] 140303 out of 161376 literals actually usable 87%
c [bca-4] added 64 blocked clauses in 407849 steps
c [sweep-4] limit 2373144 penalty 0 = 0 + 0
c [sweep-4-1] 3160 pos 3.9% + 77351 neg 96.1% = 80511 sched 99.8% ret 176
c [sweep-4-1] 2448513 steps 25 queries 14606.56 avg class size
c [sweep-4-1] 542 decisions 21 SAT calls 176.38 avg env size
c [sweep-4-1] 80401 variables remain 100% (286 retained 0%)
c [decomp-18] removed 23 variables
c [sweep-4-1] removed 23 vars (0 failed, 3 eqs, 7 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 23 vars in TOTAL (1 rounds, 24 queries)
c [phase-count-8] 451579 negative 99.0% of 456285 except 4706 1.0%
c [phase-count-8] 359905 positive 78.9% of 456285 except 96380 21.1%
c [phase-count-8] less non-negative clauses 4706 than limit 45600 (10.0%)
c [phase-count-8] non-pos/non-neg = 96380/4706 = 20.48 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 433 negative 100%
c [sort-queue-8] sorted 39676 enqueued variables after 18250 conflicts
c [score-dist-8] active 40988 (51%), one 0 (0%), zero 39676 (49%)
c [score-dist-8] max exp 516, different 14 (3%)
c [score-dist-8] median active exp 516, avg 515.0
c [simplification-8] removed 942 variables 1.2% (80664 remain 32%)
c [simplification-8] removed 4787 irredundant clauses 1.0% (456285 remain 41%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-8] new conflict interval 19000
c [simplification-8] penalized conflict interval 19000 = 1 * 19000
c [simplification-8] hard conflict limit 47250 (soft 37250 + delta 10000)
c [simplification-8] new conflict limit 37250 (hard 47250)
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   69.4   80663   456285     18971   11787   2144 82846   64   245   55  26%     13  190   63   14  453%
c i   70.3   80662   456285     19505   12261   2149 82856   64   241   55  27%      9  185   67   14  470%
c i   71.5   80661   456285     20277   12938   2152 82860   65   233   55  28%      7  174   76   15  507%
c i   71.6   80658   456285     20347   13005   2152 82861   65   233   55  28%      7  174   72   15  478%
c i   71.9   80654   456285     20465   13114   2154 82862   65   235   55  28%      6  175   75   15  496%
c i   72.4   80653   456285     20701   13330   2155 82864   64   229   55  28%      5  170   52   15  343%
c i   72.5   80649   456285     20777   13398   2155 82865   64   229   55  28%      4  169   56   15  369%
c i   73.1   80646   456285     21150   13740   2163 82867   64   232   55  28%      4  171   64   16  414%
c i   78.2   80645   456285     23825   16146   2195 82906   67   235   56  29%     26  168   78   18  439%
c i   80.3   80644   456285     24999   17208   2215 82934   67   230   59  29%     14  159   59   19  317%
c i   81.6   80643   456285     25708   17846   2220 82947   70   234   63  30%      9  161   93   19  481%
c i   82.7   80642   456285     26216   18291   2226 82959   71   234   63  30%      6  160   82   20  414%
c i   82.9   80636   456285     26305   18373   2231 82959   70   232   64  30%      6  158   65   20  329%
c i   83.4   80635   456285     26569   18600   2234 82962   70   231   64  30%      4  157   72   20  362%
c i   83.6   80634   456285     26629   18650   2234 82962   71   233   65  31%      4  158   89   20  445%
c i   87.3   80633   456285     28388   20211   2260 82983   71   224   67  32%     13  145   69   21  324%
c i   87.5   80629   456285     28499   20295   2262 82983   71   225   69  32%     12  146   75   22  349%
c i   88.1   80628   456285     28797   20569   2268 82992   70   222   69  31%      9  143   55   22  254%
c i   89.0   80627   456285     29292   21037   2269 82993   67   213   69  31%      6  133   47   22  213%
c i   89.2   80626   456285     29355   21097   2269 82994   67   214   69  31%      5  133   50   22  228%
c i   89.6   80620   456285     29549   21275   2270 82997   66   212   69  31%      4  130   49   22  222%
c i   90.3   80619   456285     29896   21595   2273 83000   66   208   69  32%      3  126   59   22  266%
c i   91.9   80579   456285     30601   22237   2278 83009   64   201   70  32%      3  118   51   23  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   93.6   80578   456285     31416   22954   2290 83023   69   211   70  33%      4  127  101   23  432%
c i   93.9   80574   456285     31552   23077   2290 83024   69   213   70  33%      3  128   93   23  394%
c i   96.3   80573   456285     32669   24107   2295 83030   69   206   70  33%      6  119   68   24  282%
c i  103.3   80571   456285     35915   27021   2346 83072   65   185   74  35%     32   93   54   26  209%
c i  103.4   80570   456285     35972   27073   2346 83074   65   186   74  35%     30   93   55   26  210%
c i  105.9   80569   456285     37119   28128   2356 83078   64   178   76  36%     14   84   50   27  189%
c 
c [simplification-9] limit 37250 conflicts (hard 47250) hit after 37250 conflicts
c [quatres-5] found 33388 quaternary clauses 39% in total
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [quatres-5-2] added 5 quaternary resolvents
c [ternres-5] limit 15994341 with penalty 0 = 0 + 0
c [ternres-5] all 80567 free variables schedulable
c [ternres-5] 613 ternary resolvents (3 bin, 610 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-19] removed 147 variables
c [unhide-9] limit 1599434 with penalty 1 = 0 + 1
c [unhide-9-9] 0 units, 53 failed, 3281 tauts, 0 hbrs, 137691 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 104 transitive binary clauses
c [transred-5] found 1 units
c [bca-5] limit of 10000000 steps and 904868 added (scaled 2)
c [bca-5] 136339 out of 160846 literals actually usable 85%
c [bca-5] added 35 blocked clauses in 407307 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 47983020 penalty 0 = 0 + 0
c [sweep-5-1] 2819 pos 3.5% + 77326 neg 96.5% = 80145 sched 99.7% ret 277
c [sweep-5-1] 48033739 steps 421 queries 814.04 avg class size
c [sweep-5-1] 4800 decisions 322 SAT calls 165.15 avg env size
c [sweep-5-1] 67739 variables remain 85% (12345 retained 15%)
c [decomp-20] removed 613 variables
c [sweep-5-1] removed 613 vars (0 failed, 112 eqs, 163 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 613 vars in TOTAL (1 rounds, 420 queries)
c [phase-count-9] 444860 negative 99.0% of 449568 except 4708 1.0%
c [phase-count-9] 354835 positive 78.9% of 449568 except 94733 21.1%
c [phase-count-9] less non-negative clauses 4708 than limit 44900 (10.0%)
c [phase-count-9] non-pos/non-neg = 94733/4708 = 20.12 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 218 negative 100%
c [sort-queue-9] sorted 34894 enqueued variables after 37250 conflicts
c [score-dist-9] active 44915 (56%), one 0 (0%), zero 34894 (44%)
c [score-dist-9] max exp 517, different 15 (3%)
c [score-dist-9] median active exp 517, avg 516.1
c [simplification-9] removed 758 variables 0.9% (79809 remain 32%)
c [simplification-9] removed 6717 irredundant clauses 1.5% (449568 remain 40%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-9] new conflict interval 29000
c [simplification-9] penalized conflict interval 29000 = 1 * 29000
c [simplification-9] hard conflict limit 80750 (soft 66250 + delta 14500)
c [simplification-9] new conflict limit 66250 (hard 80750)
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  113.3   79808   449568     37830   28695   2541 104734   67   182   89  37%      8   87   85   27  310%
c i  113.7   79807   449568     38006   28849   2541 104734   67   183   89  37%      7   88   78   27  283%
c i  115.0   79804   449568     38636   29427   2542 104739   67   186   89  36%      4   91   73   28  263%
c i  120.1   79801   449568     40907   31455   2564 104766   70   183   89  38%     18   85  102   29  347%
c i  120.4   79800   449568     41028   31565   2565 104766   71   185   89  38%     16   86  100   29  339%
c i  121.3   79796   449568     41401   31888   2571 104778   69   183   89  38%     10   84   71   30  239%
c i  122.7   79744   449568     41995   32414   2581 104780   70   188   89  37%      6   88   76   30  252%
c i  127.4   79743   449568     44164   34274   2608 104802   76   194   89  39%     16   91   52   32  164%
c i  127.9   79742   449568     44390   34468   2609 104805   75   192   89  39%     13   88   59   32  184%
c i  128.0   79741   449568     44431   34497   2609 104805   76   192   89  39%     12   89   74   32  233%
c i  128.1   79740   449568     44476   34537   2609 104806   76   193   89  39%     11   89   74   32  231%
c i  129.5   79739   449568     45067   35041   2611 104808   77   195   89  39%      6   91   78   32  240%
c i  129.6   79738   449568     45139   35103   2616 104810   76   195   89  39%      6   91   65   32  199%
c i  129.8   79737   449568     45214   35174   2616 104811   75   192   89  39%      5   87   51   32  157%
c i  131.7   79736   449568     46000   35867   2628 104816   75   190   89  39%      3   85   76   33  231%
c i  131.8   79734   449568     46051   35913   2628 104816   75   191   89  39%      3   85   74   33  225%
c i  133.0   79727   449568     46528   36337   2635 104823   74   193   89  38%      2   86   67   33  203%
c i  133.8   79726   449568     46860   36630   2639 104826   74   195   89  38%      1   88   79   33  235%
c i  134.2   79720   449568     47014   36758   2639 104831   76   196   89  39%      0   89   94   34  280%
c i  135.4   79717   449568     47547   37202   2641 104832   76   196   89  39%     -0   88   84   34  248%
c i  136.6   79714   449568     48016   37619   2648 104835   75   193   89  39%     -0   85   70   34  206%
c i  137.6   79704   449568     48428   37982   2651 104839   76   194   89  39%     -1   85   75   35  218%
c i  138.1   79702   449568     48644   38174   2653 104842   74   193   89  39%     -1   83   62   35  179%
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  138.5   79699   449568     48820   38334   2655 104845   74   193   89  38%     -1   83   64   35  184%
c i  138.7   79698   449568     48891   38398   2656 104845   74   194   89  38%     -2   84   66   35  189%
c i  141.6   79695   449568     50093   39525   2665 104849   70   184   92  38%      4   73   49   35  140%
c i  143.3   79694   449568     51012   40302   2673 104856   70   180   92  39%      4   68   70   36  196%
c i  143.6   79451   449568     51133   40385   2674 104861   69   178   92  39%      3   66   67   36  187%
c i  147.4   79450   449568     53181   42202   2682 104867   65   159   92  41%     14   45   85   36  234%
c i  148.2   79449   449568     53576   42565   2683 104868   65   162   92  40%      9   48   73   36  200%
c i  149.8   79448   449568     54366   43275   2696 104868   64   167   92  39%      5   52   57   37  155%
c i  151.4   79447   449568     55205   44001   2714 104874   65   169   92  39%      4   53   81   37  217%
c i  156.1   79445   449568     58680   47237   2730 104890   40    98  111  41%     33  -18   35   36   97%
c i  159.2   79444   449568     60646   49111   2736 104892   35    80  127  44%     16  -35   20   36   55%
c i  160.1   79437   449568     61299   49738   2742 104892   33    81  127  40%      8  -34   24   36   68%
c i  162.8   79436   449568     63134   51497   2746 104896   31    83  127  38%     11  -30   65   36  183%
c i  163.1   79435   449568     63294   51643   2746 104896   32    87  127  38%      9  -27   61   36  171%
c i  163.9   79434   449568     63668   51961   2747 104901   37    96  127  38%      5  -17   78   36  218%
c i  164.7   79431   449568     64029   52271   2749 104901   40   101  127  39%      2  -12   70   36  193%
c i  166.7   79430   449568     64963   53073   2751 104912   50   123  128  40%      2    9   88   37  239%
c i  167.0   79429   449568     65129   53209   2753 104922   51   126  128  40%      1   13   86   37  233%
c i  167.4   79428   449568     65303   53370   2753 104922   51   127  128  40%     -0   13   67   37  182%
c -  168.9   79428   449568     65984   17236   2757 104923   62   143   51  43%     -0   29  120   38  317%
c i  169.4   79427   449568     66238   17449   2759 104927   63   149   59  42%      1   35  101   38  265%
c 
c [simplification-10] limit 66250 conflicts (hard 80750) hit after 66250 conflicts
c [quatres-6] found 30797 quaternary clauses 37% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 3 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1 quaternary resolvents
c [ternres-6] limit 27257180 with penalty 0 = 0 + 0
c [ternres-6] all 79417 free variables schedulable
c [ternres-6] 217 ternary resolvents (4 bin, 213 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1703573 penalty 3 = 3 + 0
c [card-4] found 6027 at-most-one constraints of average size 4.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1703573 for elimination
c [card-4] 6027 out of 6027 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-21] removed 777 variables
c [treelook-3] limit 681429 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 92513 literals 59%
c [treelook-3] scheduling used 681513 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 681429 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 875084 steps
c [treelook-3] 92504 literals remain 59%
c [treelook-3] 20146 variables remain to probed next time 25%
c [decomp-22] removed 1 variables
c [treelook-3] removed 1 variables, found 5765 hbrs
c [unhide-10] limit 5451436 with penalty 0 = 0 + 0
c [unhide-10-11] 7 units, 353 failed, 10719 tauts, 0 hbrs, 121280 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 105 transitive binary clauses
c [transred-6] found 5 units
c [cce-3] limit of 34071475 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 15 clauses out of 1626 (1%) of length 9
c [cce-3-1] eliminated 25 clauses out of 372 (7%) of length 8
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 40 large clauses in 34071476 steps
c [cce-3-1] allowing another 17035738 steps for small clauses
c [cce-3-1] scheduling 312994 clauses = 238260 binary + 74734 ternary
c [cce-3-1] tried to eliminate 433 small clauses 0%
c [cce-3-1] eliminated 77 binary clauses 0%
c [cce-3-1] eliminated 44 ternary clauses 0%
c [cce-3-1] eliminated 121 small clauses 0%
c [cce-3-1] eliminated 3102 small clauses in 34071482 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 3142 covered clauses in round 1
c [cce-3] eliminated 3142 covered clauses in TOTAL during 1 rounds
c [cce-3] 3142 < 1/100 * 438330 = 4383 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 78181 variables 100%
c [elim-9] limit of 272571805 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1932 variables 2% in round 1 in 36309744 steps
c [elim-9-1] backward subsumption/strengthening limit 36309700
c [elim-9-1-1] backward checking 7577 touched variables 10%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 98 and strengthened 42 clauses in 1838580 steps
c [elim-9-1] rescheduled 391 variables 1% by backward subsumption
c [elim-9-2] eliminated 38 variables 0% in round 2 in 280050 steps
c [elim-9-2] backward subsumption/strengthening limit 280000
c [elim-9-2-1] backward checking 325 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 18 and strengthened 19 clauses in 192533 steps
c [elim-9-2] rescheduled 102 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 71348 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1970 = 3% variables out of 78181 scheduled
c [bca-6] limit of 10000000 steps and 862602 added (scaled 2)
c [bca-6] 131936 out of 152424 literals actually usable 87%
c [bca-6] added 299 blocked clauses in 387937 steps
c [sweep-6] limit 8177154 penalty 0 = 0 + 0
c [sweep-6-1] 2667 pos 4.1% + 62134 neg 95.9% = 64801 sched 85.0% ret 11410
c [sweep-6-1] 8331634 steps 76 queries 3593.16 avg class size
c [sweep-6-1] 1129 decisions 62 SAT calls 178.65 avg env size
c [sweep-6-1] 64054 variables remain 84% (12102 retained 16%)
c [decomp-23] removed 137 variables
c [sweep-6-1] removed 137 vars (0 failed, 14 eqs, 24 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 137 vars in TOTAL (1 rounds, 75 queries)
c [phase-count-10] 426076 negative 98.9% of 430640 except 4564 1.1%
c [phase-count-10] 337464 positive 78.4% of 430640 except 93176 21.6%
c [phase-count-10] less non-negative clauses 4564 than limit 43000 (10.0%)
c [phase-count-10] non-pos/non-neg = 93176/4564 = 20.42 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 168 negative 100%
c [sort-queue-10] sorted 29364 enqueued variables after 66250 conflicts
c [score-dist-10] active 46710 (61%), one 0 (0%), zero 29364 (39%)
c [score-dist-10] max exp 518, different 14 (3%)
c [score-dist-10] median active exp 517, avg 516.8
c [simplification-10] removed 3343 variables 4.2% (76074 remain 30%)
c [simplification-10] removed 18928 irredundant clauses 4.2% (430640 remain 38%)
c [simplification-10] maximum reduction of 4% = max (4%, 4%)
c [simplification-10] geometric conflict interval increment 5800 = 29000 / 5
c [simplification-10] new conflict interval 34800
c [simplification-10] penalized conflict interval 34800 = 1 * 34800
c [simplification-10] hard conflict limit 118450 (soft 101050 + delta 17400)
c [simplification-10] new conflict limit 101050 (hard 118450)
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  178.7   76073   430640     68251   15168   2109 105317   55   130   53  43%     12   16   28   38   72%
c i  179.3   76072   430640     68753   15604   2110 105320   54   125   55  43%      6   10   50   38  130%
c i  179.8   76070   430640     69004   15823   2111 105321   52   121   55  43%      4    6   37   38   98%
c i  180.0   76069   430640     69144   15954   2111 105321   52   119   55  44%      3    4   39   38  103%
c i  180.3   76066   430640     69363   16144   2113 105322   50   114   55  43%      1   -1   22   38   58%
c i  182.8   76062   430640     71589   18294   2121 105338   39    90   66  43%     14  -25   24   38   63%
c i  183.9   76061   430640     72327   18949   2124 105340   38    85   67  45%      7  -29   28   38   74%
c i  185.5   76060   430640     73578   20138   2131 105344   35    75   68  46%      5  -38   25   37   67%
c i  185.9   75359   430640     73918   20443   2143 105355   36    80   68  45%      2  -33   36   38   95%
c i  187.0   75358   430640     74764   21220   2147 105356   37    90   71  41%      1  -23   45   38  120%
c i  187.4   75152   430640     75092   21521   2148 105356   36    88   72  41%     -0  -25   29   38   77%
c i  189.4   75138   430640     76523   22824   2162 105371   34    80   74  42%      5  -32   24   37   64%
c i  189.5   75137   430640     76550   22847   2162 105372   34    80   74  42%      4  -32   26   37   69%
c i  190.2   75136   430640     76968   23240   2163 105372   32    75   74  43%      2  -37   20   37   54%
c i  193.5   75135   430640     79235   25260   2187 105398   41   102   75  40%     15   -9   57   38  152%
c i  193.7   75134   430640     79341   25355   2187 105398   42   104   75  40%     13   -8   57   38  152%
c i  195.4   75133   430640     80405   26351   2199 105400   40    99   79  40%      6  -12   21   38   55%
c i  197.8   75131   430640     81840   27595   2201 105406   51   123   80  41%      6   12   42   39  108%
c i  199.3   75100   430640     83048   28764   2204 105408   45   106   80  42%      4   -5   32   38   82%
c i  201.0   75099   430640     84089   29658   2211 105415   52   121   82  43%      3   10   71   39  181%
c i  203.3   75098   430640     85424   30793   2215 105421   59   134   82  44%      4   22  102   40  256%
c i  203.4   75097   430640     85476   30828   2217 105422   59   134   82  44%      4   23   96   40  241%
c i  205.2   75096   430640     86475   31670   2222 105431   64   142   87  45%      2   30   64   40  157%
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  205.5   75095   430640     86685   31839   2223 105432   64   141   87  45%      1   29   63   41  156%
c i  208.2   75094   430640     88384   33429   2228 105436   56   120   94  46%      7    8   22   41   54%
c i  209.7   75093   430640     89555   34551   2233 105442   49   107   95  45%      4   -5   26   40   64%
c i  211.3   75092   430640     90417   35291   2235 105443   53   119   96  45%      2    6   61   41  149%
c i  214.8   75091   430640     92486   37147   2244 105455   54   124  106  43%     12   10   28   41   68%
c i  214.8   75086   430640     92487   37147   2244 105455   54   124  106  43%     12   10   28   41   68%
c i  216.0   75081   430640     93218   37776   2251 105462   55   128  107  43%      5   15   56   42  135%
c i  216.1   75080   430640     93263   37814   2255 105463   55   127  107  43%      4   14   48   41  117%
c i  216.3   75073   430640     93346   37889   2255 105464   54   128  107  43%      3   14   48   41  115%
c i  222.1   75072   430640     97705   42040   2277 105480   39    85  109  46%     43  -28   46   41  113%
c i  225.2   75071   430640     99838   43922   2295 105517   42    92  119  46%     16  -20   27   41   67%
c i  225.3   75070   430640     99935   44004   2295 105517   43    92  119  46%     14  -20   35   41   85%
c i  225.9   75066   430640    100315   44355   2295 105518   42    90  119  46%      7  -22   31   41   76%
c i  227.4   75065   430640    101291   45263   2298 105521   37    79  119  47%      2  -33   24   41   59%
c i  228.1   75064   430640    101956   45854   2310 105539   41    88  119  46%     -1  -23   65   41  159%
c i  228.2   75049   430640    101997   45893   2310 105539   41    88  119  46%     -1  -24   60   41  147%
c i  229.3   75048   430640    102587   46391   2311 105540   46    98  119  47%     -3  -13   83   41  200%
c i  229.3   75047   430640    102600   46400   2311 105540   46    98  119  47%     -3  -13   81   41  195%
c i  229.3   75046   430640    102601   46400   2311 105540   46    98  119  47%     -3  -13   80   41  195%
c i  229.3   75045   430640    102602   46400   2311 105540   46    98  119  47%     -3  -13   80   41  194%
c i  229.6   75044   430640    102769   46546   2311 105540   47   100  119  47%     -4  -11   77   41  186%
c i  229.7   75040   430640    102815   46586   2311 105540   47   100  119  47%     -4  -11   74   41  180%
c 
c [simplification-11] limit 101080 conflicts (hard 118450) hit after 104053 conflicts
c [quatres-7] found 27678 quaternary clauses 36% in total
c [quatres-7-2] added 2 single-self-subsuming ternary resolvents
c [quatres-7-2] added 15 quaternary resolvents
c [ternres-7] limit 38874050 with penalty 0 = 0 + 0
c [ternres-7] all 75040 free variables schedulable
c [ternres-7] 890 ternary resolvents (1 bin, 889 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 1943702 penalty 2 = 2 + 0
c [gauss-4] extracted 96 xors of average arity 2.5
c [gauss-4] connected 240 occurrences of 172 variables (average 1.4)
c [gauss-4] limit 1943702 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [decomp-24] removed 67 variables
c [gauss-4] exported 0 unary, 1 binary and 0 ternary equations
c [basicprobe-3] limit 194370254 penalty 0 = 0 + 0
c [basicprobe-3-0] 22446 probes remain 31% after last round
c [basicprobe-3-0] 594 units = 588 failed (99%) + 6 lifted (1%)
c [basicprobe-3-0] removed 2341 variables, found 136979 hbrs
c [bate-2] eliminated 313 asymmetric tautologies during probing
c [unhide-11] limit 1943702 with penalty 2 = 0 + 2
c [unhide-11-12] 5 units, 43 failed, 3913 tauts, 0 hbrs, 1039122 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 144 transitive binary clauses
c [transred-7] found 4 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 72524 variables 100%
c [block-4] limit of 97185127 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 48 blocked clauses
c [block-4] 48 < 1/100 * 404433 = 4044 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 72523 variables 100%
c [elim-10] limit of 777481016 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 2832 variables 4% in round 1 in 34172211 steps
c [elim-10-1] backward subsumption/strengthening limit 34172200
c [elim-10-1-1] backward checking 9604 touched variables 13%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 57 and strengthened 203 clauses in 2519511 steps
c [elim-10-1] rescheduled 638 variables 1% by backward subsumption
c [elim-10-2] eliminated 80 variables 0% in round 2 in 568415 steps
c [elim-10-2] backward subsumption/strengthening limit 568400
c [elim-10-2-1] backward checking 586 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 8 and strengthened 13 clauses in 309831 steps
c [elim-10-2] rescheduled 56 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 37721 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 2913 = 4% variables out of 72523 scheduled
c [bca-7] limit of 10000000 steps and 793661 added (scaled 2)
c [bca-7] 120414 out of 139222 literals actually usable 86%
c [bca-7] added 55 blocked clauses in 363719 steps
c [sweep-7] limit 11662215 penalty 0 = 0 + 0
c [sweep-7-1] 2794 pos 4.8% + 56024 neg 95.2% = 58818 sched 84.5% ret 10792
c [sweep-7-1] 11731951 steps 117 queries 2234.03 avg class size
c [sweep-7-1] 1012 decisions 96 SAT calls 58.28 avg env size
c [sweep-7-1] 57460 variables remain 83% (12083 retained 17%)
c [decomp-26] removed 142 variables
c [sweep-7-1] removed 142 vars (0 failed, 25 eqs, 35 impls)
c [sweep-7] removed 142 vars in TOTAL (1 rounds, 116 queries)
c [phase-count-11] 391245 negative 98.9% of 395733 except 4488 1.1%
c [phase-count-11] 308318 positive 77.9% of 395733 except 87415 22.1%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 33 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 25720 enqueued variables after 104053 conflicts
c [score-dist-11] active 43748 (63%), one 0 (0%), zero 25720 (37%)
c [score-dist-11] max exp 518, different 14 (3%)
c [score-dist-11] median active exp 518, avg 517.3
c [simplification-11] removed 5572 variables 7.4% (69468 remain 28%)
c [simplification-11] removed 34907 irredundant clauses 8.1% (395733 remain 35%)
c [simplification-11] maximum reduction of 8% = max (7%, 8%)
c [simplification-11] large reduction 8% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 116053 (soft 106053 + delta 10000)
c [simplification-11] new conflict limit 106053 (hard 116053)
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  249.7   69467   395733    106469   26475   2481 220851   43    97   67  44%     31  -14   45   41  108%
c i  249.7   69466   395733    106496   26494   2481 220851   44    97   67  45%     30  -13   50   41  121%
c 
c [simplification-12] limit 106053 conflicts (hard 116053) hit after 107525 conflicts
c [quatres-8] found 27990 quaternary clauses 38% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 7 single-self-subsuming ternary resolvents
c [quatres-8-2] added 25 quaternary resolvents
c [ternres-8] limit 39813896 with penalty 0 = 0 + 0
c [ternres-8] all 69466 free variables schedulable
c [ternres-8] 803 ternary resolvents (4 bin, 799 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-27] removed 3 variables
c [simpleprobe-4] 15943 schedulable variables 23%
c [simpleprobe-4] limit 159255587 penalty 0 = 0 + 0
c [decomp-28] removed 2706 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 2706 variables, found 54931 hbrs, 596 units
c [unhide-12] limit 3981389 with penalty 1 = 0 + 1
c [unhide-12-14] 8 units, 327 failed, 37215 tauts, 0 hbrs, 109359 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 156 transitive binary clauses
c [transred-8] found 1 units
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 66409 variables 100%
c [elim-11] limit of 796277938 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 1435 variables 2% in round 1 in 31711954 steps
c [elim-11-1] backward subsumption/strengthening limit 31711900
c [elim-11-1-1] backward checking 6452 touched variables 10%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 75 and strengthened 18 clauses in 1663620 steps
c [elim-11-1] rescheduled 266 variables 0% by backward subsumption
c [elim-11-2] eliminated 16 variables 0% in round 2 in 155724 steps
c [elim-11-2] backward subsumption/strengthening limit 155700
c [elim-11-2-1] backward checking 123 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 9 and strengthened 8 clauses in 113866 steps
c [elim-11-2] rescheduled 46 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 30214 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 1451 = 2% variables out of 66409 scheduled
c [bca-8] limit of 10000000 steps and 740003 added (scaled 2)
c [bca-8] 110337 out of 129918 literals actually usable 85%
c [bca-8] added 123 blocked clauses in 332565 steps
c [sweep-8] limit 11944169 penalty 0 = 0 + 0
c [sweep-8-1] 2638 pos 4.9% + 51642 neg 95.1% = 54280 sched 83.6% ret 10678
c [sweep-8-1] 12050094 steps 133 queries 2309.22 avg class size
c [sweep-8-1] 1894 decisions 114 SAT calls 196.46 avg env size
c [sweep-8-1] 51893 variables remain 80% (12925 retained 20%)
c [decomp-29] removed 191 variables
c [sweep-8-1] removed 191 vars (0 failed, 25 eqs, 44 impls)
c [sweep-8] removed 191 vars in TOTAL (1 rounds, 132 queries)
c [phase-count-12] 364169 negative 98.8% of 368636 except 4467 1.2%
c [phase-count-12] 281907 positive 76.5% of 368636 except 86729 23.5%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 1 positive 20%, 4 negative 80%
c [sort-queue-12] sorted 21495 enqueued variables after 107525 conflicts
c [score-dist-12] active 43272 (67%), one 0 (0%), zero 21495 (33%)
c [score-dist-12] max exp 518, different 14 (3%)
c [score-dist-12] median active exp 518, avg 517.4
c [simplification-12] removed 4699 variables 6.8% (64767 remain 26%)
c [simplification-12] removed 27097 irredundant clauses 6.8% (368636 remain 33%)
c [simplification-12] maximum reduction of 7% = max (7%, 7%)
c [simplification-12] large reduction 7% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 119525 (soft 109525 + delta 10000)
c [simplification-12] new conflict limit 109525 (hard 119525)
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  259.3   64766   368636    108690   22038   1943 223311   44    95   62  46%     14  -15   45   42  108%
c i  262.6   64765   368636    111445   24615   1950 223327   40    84   63  48%     19  -25   49   41  119%
c i  263.9   64764   368636    112663   25769   1958 223333   36    74   65  48%      6  -35   25   41   62%
c i  264.0   64763   368636    112795   25887   1960 223334   36    74   65  48%      4  -35   32   41   77%
c i  264.3   64761   368636    113053   26142   1960 223334   35    71   65  49%      1  -38   20   41   49%
c i  264.4   64757   368636    113098   26177   1960 223336   35    73   65  48%      0  -36   34   41   82%
c i  269.9   64753   368636    118131   30918   1976 223350   35    72   77  48%     50  -34   29   40   72%
c 
c [simplification-13] limit 109525 conflicts (hard 119525) hit after 119526 conflicts
c [quatres-9] found 26613 quaternary clauses 36% in total
c [quatres-9-2] added 9 quaternary resolvents
c [ternres-9] limit 42563464 with penalty 0 = 0 + 0
c [ternres-9] all 64745 free variables schedulable
c [ternres-9] 612 ternary resolvents (1 bin, 611 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-5] limit 4256346 penalty 1 = 1 + 0
c [gauss-5] extracted 120 xors of average arity 3.0
c [gauss-5] connected 354 occurrences of 231 variables (average 1.5)
c [gauss-5] limit 4256346 penalty 1 = 1 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-30] removed 3 variables
c [unhide-13] limit 4256346 with penalty 1 = 0 + 1
c [unhide-13-16] 7 units, 98 failed, 15060 tauts, 0 hbrs, 1058439 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 171 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 64472 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 511 variables 1% in round 1 in 30970155 steps
c [elim-12-1] backward subsumption/strengthening limit 30970100
c [elim-12-1-1] backward checking 2914 touched variables 5%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 16 and strengthened 28 clauses in 738111 steps
c [elim-12-1] rescheduled 111 variables 0% by backward subsumption
c [elim-12-2] eliminated 8 variables 0% in round 2 in 93192 steps
c [elim-12-2] backward subsumption/strengthening limit 93100
c [elim-12-2-1] backward checking 56 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 0 and strengthened 1 clauses in 93101 steps
c [elim-12-2] rescheduled 4 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 2778 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 519 = 1% variables out of 64472 scheduled
c [elim-12] 519 < 1/100 * 64472 = 644 considered unsuccessful
c [bca-9] limit of 10000000 steps and 727392 added (scaled 2)
c [bca-9] 107011 out of 127908 literals actually usable 84%
c [bca-9] added 70 blocked clauses in 323572 steps
c [sweep-9] limit 12769039 penalty 0 = 0 + 0
c [sweep-9-1] 2516 pos 4.9% + 48878 neg 95.1% = 51394 sched 80.4% ret 12559
c [sweep-9-1] 12821328 steps 112 queries 1942.17 avg class size
c [sweep-9-1] 1415 decisions 99 SAT calls 132.25 avg env size
c [sweep-9-1] 49603 variables remain 78% (14033 retained 22%)
c [decomp-31] removed 370 variables
c [sweep-9-1] removed 370 vars (0 failed, 17 eqs, 31 impls)
c [sweep-9] removed 370 vars in TOTAL (1 rounds, 111 queries)
c [phase-count-13] 356761 negative 98.8% of 361151 except 4390 1.2%
c [phase-count-13] 275976 positive 76.4% of 361151 except 85175 23.6%
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 20329 enqueued variables after 119526 conflicts
c [score-dist-13] active 43254 (68%), one 0 (0%), zero 20329 (32%)
c [score-dist-13] max exp 518, different 14 (3%)
c [score-dist-13] median active exp 518, avg 517.5
c [simplification-13] removed 1162 variables 1.8% (63583 remain 25%)
c [simplification-13] removed 7485 irredundant clauses 2.0% (361151 remain 32%)
c [simplification-13] maximum reduction of 2% = max (2%, 2%)
c [simplification-13] geometric conflict interval increment 11600 = 34800 / 3
c [simplification-13] new conflict interval 46400
c [simplification-13] penalized conflict interval 46400 = 1 * 46400
c [simplification-13] hard conflict limit 189126 (soft 165926 + delta 23200)
c [simplification-13] new conflict limit 165926 (hard 189126)
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  280.6   63582   361151    120933   27654   2175 207007   32    76   69  42%     19  -29   26   40   65%
c i  286.5   63581   361151    126915   33448   2179 207018   25    49   83  51%     62  -52   17   38   45%
c i  287.7   63580   361151    127989   34438   2183 207021   25    50   83  50%     17  -50   21   38   55%
c i  292.4   63579   361151    132225   38336   2210 207043   24    53   86  46%     34  -45   14   37   37%
c i  293.2   63578   361151    132906   38941   2214 207048   26    56   86  47%     12  -41   50   37  135%
c i  293.5   63576   361151    133112   39117   2214 207053   28    60   86  47%      7  -37   53   38  143%
c i  293.6   63575   361151    133165   39168   2215 207053   28    60   86  47%      5  -37   49   38  132%
c i  293.9   63574   361151    133412   39389   2218 207060   28    62   86  45%      1  -34   36   37   95%
c i  297.4   63573   361151    136450   42338   2225 207069   20    40   86  49%     16  -54   12   36   33%
c i  297.9   63572   361151    136890   42729   2226 207071   22    43   86  50%      5  -51   22   36   61%
c i  298.1   63568   361151    137182   42984   2227 207071   24    49   86  49%      0  -45   52   36  142%
c i  298.1   63567   361151    137184   42985   2227 207071   24    49   86  49%      0  -45   51   36  141%
c i  303.3   63566   361151    141498   47060   2240 207084   28    59   91  48%     34  -33   37   36  103%
c i  304.2   63565   361151    142288   47825   2242 207087   30    59   96  50%      9  -32   36   36  101%
c i  304.2   63564   361151    142300   47833   2243 207087   30    59   96  50%      9  -32   37   36  102%
c i  308.4   63561   361151    145895   51196   2249 207089   33    57   97  58%     23  -32   38   36  105%
c -  313.2   63561   361151    150429   26496   2270 207108   20    33   52  60%     36  -53   12   35   36%
c i  315.2   63560   361151    152424   28414   2273 207118   19    33   64  58%     65  -52   16   34   48%
c i  316.0   63559   361151    153214   29155   2276 207119   20    34   64  58%     22  -50   14   34   42%
c i  322.0   63557   361151    158945   34692   2297 207134   17    30   76  56%     51  -50   13   33   41%
c i  326.9   63556   361151    163692   39211   2301 207146   18    31   82  58%     35  -45   22   32   70%
c i  330.2   63555   361151    166324   41690   2304 207160   17    30   82  56%      6  -45   13   31   42%
c i  330.8   63554   361151    166800   42121   2304 207160   20    36   82  54%     -4  -38   38   31  122%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  332.9   63548   361151    168575   43788   2308 207163   18    33   92  57%     -6  -41   21   31   69%
c i  333.8   63547   361151    169382   44563   2309 207166   18    31   92  58%    -12  -42   23   31   74%
c i  335.9   63546   361151    171418   46529   2311 207167   18    33   98  53%     -4  -39   46   30  153%
c i  347.9   63543   361151    180783   55071   2348 207185   18    32  109  55%    101  -35   21   29   74%
c -  350.9   63543   361151    183226   29734   2351 207185   16    26   53  60%      6  -40   11   28   40%
c i  351.7   63542   361151    183991   30416   2352 207185   15    24   65  62%     10  -41   10   28   36%
c i  352.9   63541   361151    184991   31335   2354 207185   17    27   66  62%     -9  -38   19   28   68%
c 
c [simplification-14] limit 165931 conflicts (hard 189126) hit after 189126 conflicts
c [quatres-10] found 26399 quaternary clauses 36% in total
c [quatres-10-2] added 3 single-self-subsuming ternary resolvents
c [quatres-10-2] added 4 quaternary resolvents
c [ternres-10] limit 59160907 with penalty 0 = 0 + 0
c [ternres-10] all 63541 free variables schedulable
c [ternres-10] 420 ternary resolvents (2 bin, 418 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-32] removed 48 variables
c [treelook-4] limit 2958045 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 93169 literals 73%
c [treelook-4] scheduling used 1233471 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 2958045 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 3032802 steps
c [treelook-4] 93109 literals remain 73%
c [treelook-4] 13860 variables remain to probed next time 22%
c [decomp-33] removed 1 variables
c [treelook-4] removed 4 variables, found 13258 hbrs
c [unhide-14] limit 5916090 with penalty 1 = 0 + 1
c [unhide-14-18] 3 units, 89 failed, 11204 tauts, 0 hbrs, 322330 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 158 transitive binary clauses
c [transred-10] found 4 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 369755670 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 423 (0%) of length 8
c [cce-4-1] eliminated 45 clauses out of 672 (7%) of length 7
c [cce-4-1] eliminated 2696 clauses out of 4201 (64%) of length 6
c [cce-4-1] eliminated 24233 clauses out of 35339 (69%) of length 5
c [cce-4-1] eliminated 349 clauses out of 25042 (1%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 27324 large clauses in 369755671 steps
c [cce-4-1] allowing another 184877835 steps for small clauses
c [cce-4-1] scheduling 232571 clauses = 198281 binary + 34290 ternary
c [cce-4-1] tried to eliminate 9380 small clauses 4%
c [cce-4-1] eliminated 1791 binary clauses 1%
c [cce-4-1] eliminated 575 ternary clauses 2%
c [cce-4-1] eliminated 2366 small clauses 1%
c [cce-4-1] eliminated 2698 small clauses in 369755671 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 30022 covered clauses in round 1
c [cce-4] eliminated 30022 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 657557 added (scaled 2)
c [bca-10] 105368 out of 126804 literals actually usable 83%
c [bca-10] added 74 blocked clauses in 285684 steps
c [sweep-10] limit 17748272 penalty 0 = 0 + 0
c [sweep-10-1] 2316 pos 4.7% + 47174 neg 95.3% = 49490 sched 78.1% ret 13911
c [sweep-10-1] 17858230 steps 167 queries 1709.01 avg class size
c [sweep-10-1] 1854 decisions 138 SAT calls 117.12 avg env size
c [sweep-10-1] 47100 variables remain 74% (16228 retained 26%)
c [decomp-34] removed 157 variables
c [sweep-10-1] removed 157 vars (0 failed, 31 eqs, 50 impls)
c [sweep-10] removed 157 vars in TOTAL (1 rounds, 166 queries)
c [phase-count-14] 327059 negative 99.8% of 327685 except 626 0.2%
c [phase-count-14] 244850 positive 74.7% of 327685 except 82835 25.3%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 1 positive 33%, 2 negative 67%
c [sort-queue-14] sorted 18567 enqueued variables after 189126 conflicts
c [score-dist-14] active 44677 (71%), one 0 (0%), zero 18567 (29%)
c [score-dist-14] max exp 519, different 15 (3%)
c [score-dist-14] median active exp 519, avg 518.4
c [simplification-14] removed 297 variables 0.5% (63244 remain 25%)
c [simplification-14] removed 33466 irredundant clauses 9.3% (327685 remain 29%)
c [simplification-14] maximum reduction of 9% = max (0%, 9%)
c [simplification-14] large reduction 9% >= 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 201126 (soft 191126 + delta 10000)
c [simplification-14] new conflict limit 191126 (hard 201126)
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  377.6   63243   327685    192481   38476   3063 220331   17    29   68  59%     69  -32   17   27   63%
c i  377.6   63242   327685    192494   38488   3063 220331   17    29   68  59%     68  -32   18   27   67%
c i  381.7   63241   327685    196322   42000   3080 220350   18    33   68  55%     14  -27   13   26   50%
c i  382.4   63240   327685    196948   42592   3081 220355   19    37   68  53%     -5  -22   27   26  103%
c i  383.9   63239   327685    198523   44123   3083 220355   19    33   68  56%    -15  -25   13   26   51%
c 
c [simplification-15] limit 191126 conflicts (hard 201126) hit after 201127 conflicts
c [quatres-11] found 25339 quaternary clauses 56% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-2] added 2 quaternary resolvents
c [ternres-11] limit 61810188 with penalty 0 = 0 + 0
c [ternres-11] all 63239 free variables schedulable
c [ternres-11] 108 ternary resolvents (1 bin, 107 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1931568 penalty 4 = 4 + 0
c [card-5] found 5856 at-most-one constraints of average size 3.9
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1931568 for elimination
c [card-5] 5856 out of 5856 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 5 variables
c [basicprobe-4] limit 309050944 penalty 0 = 0 + 0
c [basicprobe-4-0] 13541 probes remain 23% after last round
c [basicprobe-4-0] 1079 units = 1078 failed (100%) + 1 lifted (0%)
c [basicprobe-4-0] removed 3480 variables, found 354860 hbrs
c [bate-3] eliminated 644 asymmetric tautologies during probing
c [unhide-15] limit 6181018 with penalty 1 = 0 + 1
c [unhide-15-20] 18 units, 146 failed, 39227 tauts, 0 hbrs, 201043 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 93 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 59471 variables 100%
c [block-5] limit of 77262736 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 446 blocked clauses
c [block-5] 446 < 1/100 * 306382 = 3063 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 59444 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 14651 variables 25% in round 1 in 23122567 steps
c [elim-13-1] backward subsumption/strengthening limit 23122500
c [elim-13-1-1] backward checking 33854 touched variables 57%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 82 and strengthened 260 clauses in 5182749 steps
c [elim-13-1] rescheduled 707 variables 1% by backward subsumption
c [elim-13-2] eliminated 95 variables 0% in round 2 in 628339 steps
c [elim-13-2] backward subsumption/strengthening limit 628300
c [elim-13-2-1] backward checking 636 touched variables 1%
c [elim-13-2-1] incomplete backward checking 0 remain 0%
c [elim-13-2] subsumed 13 and strengthened 16 clauses in 628301 steps
c [elim-13-2] rescheduled 77 variables 0% by backward subsumption
c [elim-13-3] no variable eliminated in round 3 in 46809 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 14752 = 25% variables out of 59444 scheduled
c [bca-11] limit of 10000000 steps and 540548 added (scaled 2)
c [bca-11] 81239 out of 89386 literals actually usable 91%
c [bca-11] added 71 blocked clauses in 208754 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 185430560 penalty 0 = 0 + 0
c [sweep-11-1] 2268 pos 6.5% + 32631 neg 93.5% = 34899 sched 78.1% ret 9793
c [sweep-11-1] 185544608 steps 3207 queries 89.74 avg class size
c [sweep-11-1] 16206 decisions 2701 SAT calls 78.10 avg env size
c [sweep-11-1] 10872 variables remain 25% (33273 retained 75%)
c [decomp-36] removed 1881 variables
c [sweep-11-1] removed 1881 vars (4 failed, 559 eqs, 932 impls)
c [sweep-11] removed 1881 vars in TOTAL (1 rounds, 3206 queries)
c [phase-count-15] 264369 negative 99.8% of 264968 except 599 0.2%
c [phase-count-15] 187012 positive 70.6% of 264968 except 77956 29.4%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 1 positive 33%, 2 negative 67%
c [sort-queue-15] sorted 11014 enqueued variables after 201127 conflicts
c [score-dist-15] active 31797 (74%), one 0 (0%), zero 11014 (26%)
c [score-dist-15] max exp 519, different 14 (3%)
c [score-dist-15] median active exp 519, avg 518.8
c [simplification-15] removed 20428 variables 32.3% (42811 remain 17%)
c [simplification-15] removed 62717 irredundant clauses 19.1% (264968 remain 24%)
c [simplification-15] maximum reduction of 32% = max (32%, 19%)
c [simplification-15] large reduction 32% >= 5% limit
c [simplification-15] next conflict interval 2011 = min (201127/100, 46400)
c [simplification-15] penalized conflict interval 2011 = 1 * 2011
c [simplification-15] hard conflict limit 213138 (soft 203138 + delta 10000)
c [simplification-15] new conflict limit 203138 (hard 213138)
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  410.5   42810   264968    201555   15564   2765 540453   19    68   46  28%      1   11   18   26   69%
c i  412.0   42807   264968    203855   17705   2775 540460   18    57   47  31%     -6   -1   11   26   44%
c 
c [simplification-16] limit 203138 conflicts (hard 213138) hit after 206702 conflicts
c [quatres-12] found 27324 quaternary clauses 62% in total
c [quatres-12-1] removed 3 duplicate quaternary clauses
c [quatres-12-2] added 7 single-self-subsuming ternary resolvents
c [quatres-12-2] added 12 quaternary resolvents
c [ternres-12] limit 62690463 with penalty 0 = 0 + 0
c [ternres-12] all 42807 free variables schedulable
c [ternres-12] 1256 ternary resolvents (6 bin, 1250 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-6] limit 3134523 penalty 2 = 2 + 0
c [gauss-6] extracted 92 xors of average arity 2.8
c [gauss-6] connected 259 occurrences of 211 variables (average 1.2)
c [gauss-6] limit 3134523 penalty 2 = 2 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-37] removed 2 variables
c [simpleprobe-5] all 42805 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-38] removed 1301 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1301 variables, found 165611 hbrs, 448 units
c [unhide-16] limit 12538092 with penalty 0 = 0 + 0
c [unhide-16-25] 17 units, 361 failed, 177365 tauts, 0 hbrs, 71267 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 159 transitive binary clauses
c [transred-12] found 1 units
c [cce-5] limit of 78363079 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 9
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 8
c [cce-5-1] eliminated 3 clauses out of 30 (10%) of length 7
c [cce-5-1] eliminated 92 clauses out of 2908 (3%) of length 6
c [cce-5-1] eliminated 7 clauses out of 10093 (0%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 105 large clauses in 78363079 steps
c [cce-5-1] allowing another 39181539 steps for small clauses
c [cce-5-1] scheduling 183668 clauses = 137375 binary + 46293 ternary
c [cce-5-1] tried to eliminate 3054 small clauses 2%
c [cce-5-1] eliminated 596 binary clauses 0%
c [cce-5-1] eliminated 326 ternary clauses 1%
c [cce-5-1] eliminated 922 small clauses 1%
c [cce-5-1] eliminated 1090 small clauses in 78363084 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1195 covered clauses in round 1
c [cce-5] eliminated 1195 covered clauses in TOTAL during 1 rounds
c [cce-5] 1195 < 1/100 * 249841 = 2498 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 41252 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 1682 variables 4% in round 1 in 22487575 steps
c [elim-14-1] backward subsumption/strengthening limit 22487500
c [elim-14-1-1] backward checking 7291 touched variables 18%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 39 and strengthened 6 clauses in 1854299 steps
c [elim-14-1] rescheduled 119 variables 0% by backward subsumption
c [elim-14-2] eliminated 4 variables 0% in round 2 in 66942 steps
c [elim-14-2] backward subsumption/strengthening limit 66900
c [elim-14-2-1] backward checking 39 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 6 and strengthened 4 clauses in 66901 steps
c [elim-14-2] rescheduled 24 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 140270 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 1686 = 4% variables out of 41252 scheduled
c [bca-12] limit of 10000000 steps and 488696 added (scaled 2)
c [bca-12] 66128 out of 79134 literals actually usable 84%
c [bca-12] added 51 blocked clauses in 173748 steps
c [sweep-12] limit 18807138 penalty 0 = 0 + 0
c [sweep-12-1] 765 pos 8.0% + 8840 neg 92.0% = 9605 sched 24.3% ret 29961
c [sweep-12-1] 18807667 steps 447 queries 220.91 avg class size
c [sweep-12-1] 2717 decisions 378 SAT calls 75.01 avg env size
c [sweep-12-1] 8158 variables remain 21% (31396 retained 79%)
c [decomp-39] removed 236 variables
c [sweep-12-1] removed 236 vars (0 failed, 72 eqs, 136 impls)
c [sweep-12] removed 236 vars in TOTAL (1 rounds, 446 queries)
c [phase-count-16] 242921 negative 99.8% of 243455 except 534 0.2%
c [phase-count-16] 167309 positive 68.7% of 243455 except 76146 31.3%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-16] sorted 8395 enqueued variables after 206702 conflicts
c [score-dist-16] active 30935 (79%), one 0 (0%), zero 8395 (21%)
c [score-dist-16] max exp 519, different 14 (3%)
c [score-dist-16] median active exp 519, avg 518.8
c [simplification-16] removed 3477 variables 8.1% (39330 remain 16%)
c [simplification-16] removed 21513 irredundant clauses 8.1% (243455 remain 22%)
c [simplification-16] maximum reduction of 8% = max (8%, 8%)
c [simplification-16] large reduction 8% >= 5% limit
c [simplification-16] next conflict interval 2067 = min (206702/100, 46400)
c [simplification-16] penalized conflict interval 2067 = 1 * 2067
c [simplification-16] hard conflict limit 218769 (soft 208769 + delta 10000)
c [simplification-16] new conflict limit 208769 (hard 218769)
c 
c [simplification-17] limit 208769 conflicts (hard 218769) hit after 208769 conflicts
c [quatres-13] found 25996 quaternary clauses 60% in total
c [quatres-13-2] added 4 single-self-subsuming ternary resolvents
c [quatres-13-2] added 14 quaternary resolvents
c [ternres-13] limit 62977109 with penalty 0 = 0 + 0
c [ternres-13] all 39330 free variables schedulable
c [ternres-13] 650 ternary resolvents (4 bin, 646 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-40] removed 1 variables
c [treelook-5] limit 6297710 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 51085 literals 65%
c [treelook-5] scheduling used 991650 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 6297710 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 6312944 steps
c [treelook-5] 50909 literals remain 65%
c [treelook-5] 6032 variables remain to probed next time 15%
c [decomp-41] removed 2 variables
c [treelook-5] removed 25 variables, found 42332 hbrs
c [unhide-17] limit 12595421 with penalty 0 = 0 + 0
c [unhide-17-31] 9 units, 44 failed, 62514 tauts, 0 hbrs, 25762 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 168 transitive binary clauses
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 39212 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 285 variables 1% in round 1 in 22752329 steps
c [elim-15-1] backward subsumption/strengthening limit 22752300
c [elim-15-1-1] backward checking 1859 touched variables 5%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 5 and strengthened 5 clauses in 435895 steps
c [elim-15-1] rescheduled 27 variables 0% by backward subsumption
c [elim-15-2] eliminated 1 variables 0% in round 2 in 14236 steps
c [elim-15-2] backward subsumption/strengthening limit 14200
c [elim-15-2-1] backward checking 10 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 14201 steps
c [elim-15-2] fully rescheduled 38926 variables 99%
c [elim-15-3] eliminated 11 variables 0% in round 3 in 22688084 steps
c [elim-15-3] backward subsumption/strengthening limit 22688000
c [elim-15-3-1] backward checking 117 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 0 and strengthened 0 clauses in 76696 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 297 = 1% variables out of 39212 scheduled
c [elim-15] 297 < 1/100 * 39212 = 392 considered unsuccessful
c [bca-13] limit of 10000000 steps and 479615 added (scaled 2)
c [bca-13] 64022 out of 77832 literals actually usable 82%
c [bca-13] added 41 blocked clauses in 169349 steps
c [sweep-13] limit 18893132 penalty 0 = 0 + 0
c [sweep-13-1] 606 pos 7.6% + 7325 neg 92.4% = 7931 sched 20.4% ret 30984
c [sweep-13-1] 18894049 steps 504 queries 182.65 avg class size
c [sweep-13-1] 3118 decisions 419 SAT calls 82.85 avg env size
c [sweep-13-1] 6554 variables remain 17% (32359 retained 83%)
c [decomp-42] removed 144 variables
c [sweep-13-1] removed 144 vars (0 failed, 88 eqs, 152 impls)
c [sweep-13] removed 144 vars in TOTAL (1 rounds, 503 queries)
c [phase-count-17] 238560 negative 99.8% of 239074 except 514 0.2%
c [phase-count-17] 164359 positive 68.7% of 239074 except 74715 31.3%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-17] sorted 7986 enqueued variables after 208769 conflicts
c [score-dist-17] active 30785 (79%), one 0 (0%), zero 7986 (21%)
c [score-dist-17] max exp 519, different 14 (3%)
c [score-dist-17] median active exp 519, avg 518.9
c [simplification-17] removed 559 variables 1.4% (38771 remain 15%)
c [simplification-17] removed 4381 irredundant clauses 1.8% (239074 remain 21%)
c [simplification-17] maximum reduction of 2% = max (1%, 2%)
c [simplification-17] geometric conflict interval increment 15466 = 46400 / 3
c [simplification-17] new conflict interval 61866
c [simplification-17] penalized conflict interval 61866 = 1 * 61866
c [simplification-17] hard conflict limit 301568 (soft 270635 + delta 30933)
c [simplification-17] new conflict limit 270635 (hard 301568)
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  432.4   38770   239074    212739   25226   3465 477369   18    45   47  39%     88  -13   16   25   65%
c i  434.1   38769   239074    215390   27712   3470 477373   16    36   49  45%      0  -22   15   24   60%
c i  435.3   38763   239074    217962   30218   3475 477379   18    43   52  41%     -7  -14   13   24   55%
c i  451.9   38762   239074    244756   55127   3516 477416   12    21   63  57%    309  -27    9   21   43%
c -  454.4   38762   239074    248740   30220   3516 477422   17    27   47  62%    -40  -20   21   21  103%
c -  474.6   38762   239074    282538   32486   3556 477455   11    16   48  69%    383  -20   21   17  119%
c 
c [simplification-18] limit 270635 conflicts (hard 301568) hit after 301568 conflicts
c [quatres-14] found 26000 quaternary clauses 56% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 2 single-self-subsuming ternary resolvents
c [quatres-14-2] added 6 quaternary resolvents
c [ternres-14] limit 78317331 with penalty 0 = 0 + 0
c [ternres-14] all 38762 free variables schedulable
c [ternres-14] 418 ternary resolvents (5 bin, 413 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-43] removed 12 variables
c [basicprobe-5] limit 391586658 penalty 0 = 0 + 0
c [basicprobe-5-0] 10791 sched 29%, 878 failed, 18 lifted, 347701 hbrs
c [decomp-44] removed 2288 variables
c [basicprobe-5-1] 10155 probes remain 28% after last round
c [basicprobe-5-1] 956 units = 938 failed (98%) + 18 lifted (2%)
c [basicprobe-5-1] removed 2391 variables, found 387250 hbrs
c [bate-4] eliminated 1102 asymmetric tautologies during probing
c [unhide-18] limit 15663466 with penalty 0 = 0 + 0
c [unhide-18-36] 1 units, 36 failed, 116087 tauts, 0 hbrs, 127228 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 145 transitive binary clauses
c [bca-14] limit of 10000000 steps and 437418 added (scaled 2)
c [bca-14] 57979 out of 72688 literals actually usable 80%
c [bca-14] added 8 blocked clauses in 179111 steps
c [sweep-14] limit 23495199 penalty 0 = 0 + 0
c [sweep-14-1] 400 pos 6.8% + 5452 neg 93.2% = 5852 sched 16.1% ret 30491
c [sweep-14-1] 23524523 steps 393 queries 88.61 avg class size
c [sweep-14-1] 2867 decisions 334 SAT calls 109.52 avg env size
c [sweep-14-1] 4791 variables remain 13% (31392 retained 87%)
c [decomp-45] removed 435 variables
c [sweep-14-1] removed 435 vars (0 failed, 59 eqs, 107 impls)
c [sweep-14] removed 435 vars in TOTAL (1 rounds, 392 queries)
c [phase-count-18] 216114 negative 99.8% of 216638 except 524 0.2%
c [phase-count-18] 147492 positive 68.1% of 216638 except 69146 31.9%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 6613 enqueued variables after 301568 conflicts
c [score-dist-18] active 29295 (82%), one 0 (0%), zero 6613 (18%)
c [score-dist-18] max exp 520, different 15 (3%)
c [score-dist-18] median active exp 520, avg 519.4
c [simplification-18] removed 2854 variables 7.4% (35908 remain 14%)
c [simplification-18] removed 22436 irredundant clauses 9.4% (216638 remain 19%)
c [simplification-18] maximum reduction of 9% = max (7%, 9%)
c [simplification-18] large reduction 9% >= 5% limit
c [simplification-18] next conflict interval 3015 = min (301568/100, 61866)
c [simplification-18] penalized conflict interval 3015 = 1 * 3015
c [simplification-18] hard conflict limit 314583 (soft 304583 + delta 10000)
c [simplification-18] new conflict limit 304583 (hard 314583)
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  502.6   35907   216638    303145   51471   3569 664399   13    22   66  62%    556   -9   14   16   86%
c 
c [simplification-19] limit 304583 conflicts (hard 314583) hit after 314586 conflicts
c [quatres-15] found 21136 quaternary clauses 53% in total
c [quatres-15-2] added 11 single-self-subsuming ternary resolvents
c [ternres-15] limit 80729773 with penalty 0 = 0 + 0
c [ternres-15] all 35905 free variables schedulable
c [ternres-15] 220 ternary resolvents (0 bin, 220 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-46] removed 3 variables
c [simpleprobe-6] all 35905 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-47] removed 187 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 187 variables, found 166415 hbrs, 38 units
c [unhide-19] limit 16145954 with penalty 0 = 0 + 0
c [unhide-19-42] 1 units, 21 failed, 218564 tauts, 0 hbrs, 73851 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 228 transitive binary clauses
c [transred-15] found 3 units
c [cce-6] limit of 50456108 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 96
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 95
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 94
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 92
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 90
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 89
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 88
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 87
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 86
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 85
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 84
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 83
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 82
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 81
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 80
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 79
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 78
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 77
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 76
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 74
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 73
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 72
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 71
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 70
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 69
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 68
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 65
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 64
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 63
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 62
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 61
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 60
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 59
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 58
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 57
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 56
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 55
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 54
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 53
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 52
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 50
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 49
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 47
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 46
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 45
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 44
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 43
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 42
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 41
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 39
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 38
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 37
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 36
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 35
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 34
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 33
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 32
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 31
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 30
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 29
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 28
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 27
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 26
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 25
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 24
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 23
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 22
c [cce-6-1] eliminated 6 clauses out of 7 (86%) of length 21
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 20
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 19
c [cce-6-1] eliminated 8 clauses out of 8 (100%) of length 18
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 17
c [cce-6-1] eliminated 6 clauses out of 7 (86%) of length 16
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 15
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 14
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 13
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 12
c [cce-6-1] eliminated 7 clauses out of 9 (78%) of length 11
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 10
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 9
c [cce-6-1] eliminated 5 clauses out of 16 (31%) of length 8
c [cce-6-1] eliminated 7 clauses out of 38 (18%) of length 7
c [cce-6-1] eliminated 14 clauses out of 2740 (1%) of length 6
c [cce-6-1] eliminated 28 clauses out of 8669 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 257 large clauses in 50456111 steps
c [cce-6-1] allowing another 25228055 steps for small clauses
c [cce-6-1] scheduling 145215 clauses = 124778 binary + 20437 ternary
c [cce-6-1] tried to eliminate 2249 small clauses 2%
c [cce-6-1] eliminated 385 binary clauses 0%
c [cce-6-1] eliminated 86 ternary clauses 0%
c [cce-6-1] eliminated 471 small clauses 0%
c [cce-6-1] eliminated 528 small clauses in 50456111 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 785 covered clauses in round 1
c [cce-6] eliminated 785 covered clauses in TOTAL during 1 rounds
c [cce-6] 785 < 1/100 * 212706 = 2127 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 35674 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 1446 variables 4% in round 1 in 20285200 steps
c [elim-16-1] backward subsumption/strengthening limit 20285200
c [elim-16-1-1] backward checking 6548 touched variables 18%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 31 and strengthened 3 clauses in 1480872 steps
c [elim-16-1] rescheduled 96 variables 0% by backward subsumption
c [elim-16-2] eliminated 12 variables 0% in round 2 in 119975 steps
c [elim-16-2] backward subsumption/strengthening limit 119900
c [elim-16-2-1] backward checking 86 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 5 and strengthened 16 clauses in 84878 steps
c [elim-16-2] rescheduled 41 variables 0% by backward subsumption
c [elim-16-3] no variable eliminated in round 3 in 28072 steps
c [elim-16] fully completed in 3 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 1458 = 4% variables out of 35674 scheduled
c [bca-15] limit of 10000000 steps and 420564 added (scaled 2)
c [bca-15] 54272 out of 68434 literals actually usable 79%
c [bca-15] added 22 blocked clauses in 168597 steps
c [sweep-15] limit 24218931 penalty 0 = 0 + 0
c [sweep-15-1] 420 pos 9.6% + 3967 neg 90.4% = 4387 sched 12.8% ret 29829
c [sweep-15-1] 24336667 steps 620 queries 94.82 avg class size
c [sweep-15-1] 4001 decisions 530 SAT calls 77.98 avg env size
c [sweep-15-1] 2962 variables remain 9% (31235 retained 91%)
c [decomp-48] removed 251 variables
c [sweep-15-1] removed 251 vars (0 failed, 89 eqs, 176 impls)
c [sweep-15] removed 251 vars in TOTAL (1 rounds, 619 queries)
c [phase-count-19] 208863 negative 99.8% of 209368 except 505 0.2%
c [phase-count-19] 142059 positive 67.9% of 209368 except 67309 32.1%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-19] sorted 5786 enqueued variables after 314586 conflicts
c [score-dist-19] active 28179 (83%), one 0 (0%), zero 5786 (17%)
c [score-dist-19] max exp 520, different 14 (3%)
c [score-dist-19] median active exp 520, avg 519.5
c [simplification-19] removed 1940 variables 5.4% (33965 remain 13%)
c [simplification-19] removed 7270 irredundant clauses 3.4% (209368 remain 19%)
c [simplification-19] maximum reduction of 5% = max (5%, 3%)
c [simplification-19] large reduction 5% >= 5% limit
c [simplification-19] next conflict interval 3145 = min (314586/100, 61866)
c [simplification-19] penalized conflict interval 3145 = 1 * 3145
c [simplification-19] hard conflict limit 327731 (soft 317731 + delta 10000)
c [simplification-19] new conflict limit 317731 (hard 327731)
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  528.7   33964   209368    325379   57813   3421 510390   11    19   58  60%     31   -8   18   14  128%
c 
c [simplification-20] limit 317731 conflicts (hard 327731) hit after 327732 conflicts
c [quatres-16] found 21427 quaternary clauses 52% in total
c [quatres-16-1] removed 2 duplicate quaternary clauses
c [quatres-16-2] added 4 single-self-subsuming ternary resolvents
c [quatres-16-2] added 8 quaternary resolvents
c [ternres-16] limit 83073577 with penalty 0 = 0 + 0
c [ternres-16] all 33955 free variables schedulable
c [ternres-16] 400 ternary resolvents (4 bin, 396 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-7] limit 2076839 penalty 3 = 3 + 0
c [gauss-7] extracted 51 xors of average arity 3.0
c [gauss-7] connected 152 occurrences of 125 variables (average 1.2)
c [gauss-7] limit 2076839 penalty 3 = 3 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-6] limit 8307357 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 43520 literals 64%
c [treelook-6] scheduling used 1017251 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 8307357 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 8313756 steps
c [treelook-6] 43286 literals remain 64%
c [treelook-6] 4959 variables remain to probed next time 15%
c [treelook-6] removed 18 variables, found 44624 hbrs
c [unhide-20] limit 16614715 with penalty 0 = 0 + 0
c [unhide-20-49] 0 units, 25 failed, 95890 tauts, 0 hbrs, 89305 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 191 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 33900 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 28 blocked clauses
c [block-6] 28 < 1/100 * 206641 = 2066 considered unsuccessful
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 33899 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 375 variables 1% in round 1 in 32784549 steps
c [elim-17-1] backward subsumption/strengthening limit 32784500
c [elim-17-1-1] backward checking 2158 touched variables 6%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 3 and strengthened 6 clauses in 611181 steps
c [elim-17-1] rescheduled 29 variables 0% by backward subsumption
c [elim-17-2] eliminated 3 variables 0% in round 2 in 10950 steps
c [elim-17-2] backward subsumption/strengthening limit 10900
c [elim-17-2-1] backward checking 23 touched variables 0%
c [elim-17-2-1] incomplete backward checking 0 remain 0%
c [elim-17-2] subsumed 0 and strengthened 0 clauses in 10901 steps
c [elim-17-2] fully rescheduled 33521 variables 99%
c [elim-17-3] eliminated 14 variables 0% in round 3 in 35952812 steps
c [elim-17-3] backward subsumption/strengthening limit 35952800
c [elim-17-3-1] backward checking 125 touched variables 0%
c [elim-17-3-1] fully completed backward checking in 1 rounds
c [elim-17-3] subsumed 0 and strengthened 1 clauses in 84751 steps
c [elim-17] incomplete 4 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 392 = 1% variables out of 33899 scheduled
c [bca-16] limit of 10000000 steps and 413157 added (scaled 2)
c [bca-16] 52536 out of 67016 literals actually usable 78%
c [bca-16] added 8 blocked clauses in 173415 steps
c [sweep-16] limit 24922073 penalty 0 = 0 + 0
c [sweep-16-1] 222 pos 8.0% + 2541 neg 92.0% = 2763 sched 8.2% ret 30744
c [sweep-16-1] 24925849 steps 895 queries 34.97 avg class size
c [sweep-16-1] 4370 decisions 757 SAT calls 62.43 avg env size
c [sweep-16-1] 1304 variables remain 4% (32201 retained 96%)
c [decomp-51] removed 277 variables
c [sweep-16-1] removed 277 vars (0 failed, 138 eqs, 253 impls)
c [sweep-16] removed 277 vars in TOTAL (1 rounds, 894 queries)
c [phase-count-20] 205236 negative 99.8% of 205731 except 495 0.2%
c [phase-count-20] 140103 positive 68.1% of 205731 except 65628 31.9%
c [phase-count-20] skipping relative phase luck test
c [phase-20] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-20] sorted 5503 enqueued variables after 327732 conflicts
c [score-dist-20] active 27727 (83%), one 0 (0%), zero 5503 (17%)
c [score-dist-20] max exp 520, different 14 (3%)
c [score-dist-20] median active exp 520, avg 519.6
c [simplification-20] removed 725 variables 2.1% (33230 remain 13%)
c [simplification-20] removed 3637 irredundant clauses 1.7% (205731 remain 18%)
c [simplification-20] maximum reduction of 2% = max (2%, 2%)
c [simplification-20] geometric conflict interval increment 20622 = 61866 / 3
c [simplification-20] new conflict interval 82488
c [simplification-20] penalized conflict interval 82488 = 1 * 82488
c [simplification-20] hard conflict limit 451464 (soft 410220 + delta 41244)
c [simplification-20] new conflict limit 410220 (hard 451464)
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  543.1   33229   205731    331436   61139   3513 454963   11    18   60  61%   -202   -8   10   14   69%
c -  544.3   33229   205731    333683   33507   3515 454963   10    16   46  67%   -244  -10   10   14   72%
c i  558.5   33228   205731    359118   55562   3573 454991    9    12   55  74%    156  -11    9   12   70%
c i  564.2   33140   205731    369197   64271   3606 455005    8    10   60  75%    -97  -11    6   12   47%
c i  566.1   33112   205731    372146   66737   3627 455012    7    10   60  77%   -191  -11    6   12   49%
c -  566.3   31758   205731    372484   36667   3627 455013    8    11   47  73%   -200  -10   11   12   97%
c i  567.5   31757   205731    374486   38297   3647 455021    8    11   53  72%   -197   -9    7   12   61%
c i  568.8   31738   205731    376772   40221   3675 455034    9    14   53  63%   -192   -6    7   12   62%
c i  568.9   30679   205731    376965   40345   3684 455037    9    14   53  64%   -195   -6    6   12   53%
c i  569.0   30077   205731    377028   40374   3690 455043    9    14   53  64%   -196   -6    6   12   49%
c i  569.2   30047   205731    377419   40645   3702 455052    8    13   53  65%   -200   -7    5   11   46%
c i  569.3   29564   205731    377471   40656   3707 455057    8    13   53  65%   -200   -7    5   11   43%
c i  569.3   29002   205731    377504   40666   3711 455063    8    13   53  65%   -201   -7    5   11   41%
c i  569.3   27591   205731    377510   40667   3712 455063    8    13   53  65%   -201   -7    5   11   41%
c i  569.3   26926   205731    377513   40666   3712 455065    8    13   53  65%   -201   -7    5   11   40%
c 0  569.3   26528   205731    377513   40666   3712 455065    8    13   53  65%   -201   -7    5   11   40%
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: 2081 basic ate = 2020 trn 97% + 61 lrg 3% in 4 updates
c bcas: 16 count, 1222 added (1448 skipped), 4893135 steps
c bkwd: tried 720910 clauses, 1440759 lits, 2.00 lits/clause
c bkwd: checked 16440661 occs, 22.81 occs/clause, 11.41 occs/lit
c bkwd: subsumed 49 binary, 783 ternary, 51 large
c bkwd: strengthened 1 binary, 0 ternary (0% self), 938 large (0% self)
c blkd: 6 bces, 9808 removed, 8085440 resolutions, 22110902 steps
c blkd: 9929 blocking literals 2%, 29 pure
c bump: 380168 bumped seen, 175285596 lits 461.1 on average
c card: 5 count, 0 units, 0 am1, 203757450 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 101997 subsumed
c card: 23901 at-most-one constraints found, average size 4.45
c card: 23901 at-most-one constraints used 100%, average size 4.45
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: 6 cces, 31818 eliminated, 31787 ate 100%, 31 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: 162 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 51 decompositions, 13739 equivalent 5%
c deco: 10906 decision-only clauses 3%, 69% reduction
c decs: 2614099 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 17 elims, 121162 eliminated 46%, 7 pure 0%
c elms: 48 rounds, 2.8 rounds/bve
c elms: 104096 small 86%, 17030 large 14%
c elms: 432368 tried small, 104096 succeeded 24%, 328272 failed 76%
c elms: 50194 subsumed, 74955 strengthened, 599 blocked
c elms: 25513544 copies, 24583368 resolutions, 18046285 ipos
c elms: 6196920 subchks, 4628390 strchks
c gaus: 7 extractions, 1060 extracted, 2.4 size, 3 max
c gaus: exported 0 units, 11 binary and 0 ternary equations
c gaus: 0 gc, 32823762 steps, 16411881 extr 50%, 35608 elim 0%
c glue: 26.6 orig avg, 26.6 real avg, 3.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1717993 = 446701 simple 26% + 1223210 trn 71% + 48082 lrg 3%, 3898 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 380168 clauses, 184.0 length
c lrnd: 69960251 lits = 121081962 orig - 51121711 removed 42%
c lrnd: 138168 uips 36%, 218131 flips 57%
c mins: 361601 mins 96%, 1618 bin 0%, 3452 size 1%
c mins: 176992512 poisoned searches, 38408276 hits, 22% hit rate
c mins: 232348579 used twice searches, 4318563 hits, 2% hit rate
c move: moved 23638, 12426 bin 53%, 11212 trn 47%
c otfs: 601 driving 23%, 2027 restarting 77%
c otfs: str 2628, 2548 red 97%, 80 irr 3%
c otfs: str 2628, 0 bin 0%, 72 trn 3%, 2556 lrg 97%
c otfs: sub 8, 8 red 100%, 0 irr 0%
c otfs: sub 8, 0 bin 0%, 0 trn 0%, 8 lrg 100%
c phas: 20 computed, 124778 set, 36 pos (0%), 124742 neg (100%)
c prbs: 5 basic, 42499 probed, 2681 failed, 25 lifted
c prbs: 6 simple, 1020780 probed, 1465 failed, 4519 eqs
c prbs: 6 treelook, 444 probed, 23 failed, 0 lifted
c prom: 52474 locked 7% out of 763135 tried
c prps: 1633724910 props, 582 props/dec
c prps: 93% srch, 7% simp, 0% lkhd
c quat: 16 count, 146 quat, 67 self1, 0 self2, 2346 dup
c queu: 20 sorted, 2614099 next (7266 steps 0.00)
c queu: 176258853 enq (1869257304 steps 10.61), 175285596 deq 99%
c redc: 4498 clauses 15%, 30831 tried 8%, 38 sat 0%
c redc: 7284 lits 2%, 323916 tried 0%, 38 sat 0%
c redc: 348 times jump level reduced, 31.8 levels on average
c reds: 7 count, 53930.4 conflicts per reduce
c reds: 0 memlim 0%, 7 arith 100%
c reds: 185525 collected 88%, 25066 retired 12%
c rmbd: 58723 removed, 24392 red 42%
c rsts: 6601 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 20 count, 18 confs 90%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 380168 count (300563 tried 0.8), 29494 sub out of 375385 (7.9%)
c swps: 16 count, 16 rounds, 7147 queries (446.7/round)
c swps: 6013 sat calls, 124 unsat (0.5% success rate)
c swps: 46797 decisions 7.8, 3256 conflicts 0.5
c swps; 479.8 avg class size, 88.9 avg environment size
c swps: 4 failed, 2114 impls, 1233 equivs
c swp0: 2378 type 0 queries, 1461 unsat (61.4%), 2016 sat (84.8%)
c swp1: 4769 type 1 queries, 3350 unsat (70.2%), 3898 sat (81.7%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 5989225 calls to obtain time
c tops: 100824 fixed 38%, 302 its, 1250.04 confs/it
c trds: 16 transitive reductions, 2416 removed, 32 failed
c trds: 15810 nodes, 45276 edges, 32028620 steps
c trim: 941255 words, 3.6 MB
c trnr: 16 count, 42 bin, 10460 trn, 101034141 steps
c unhd: 20 count, 49 rounds, 144218576 steps
c unhd: 2778 non-trivial sccs of average size 2.1
c unhd: 135 units, 135 bin, 0 trn, 0 lrg
c unhd: 8535 failed, 8463 stamp, 0 lits, 35 bin, 17 trn, 0 lrg
c unhd: 842159 tauts, 8465 bin 1%, 19665 trn 2%, 7464 lrg 1%
c unhd: 842159 tauts, 806565 stamp 96%, 781710 red 93%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 3525254 str, 135 bin 0%, 9047 trn 0%, 3516072 lrg 100%, 3484372 red 99%
c vars: 26528 remaining 10% and 235725 removed 90% out of 262253
c vars: 100824 fixed 38%, 121162 eliminated 46%, 13739 equivalent 5%
c vsts: 10080190382 visits, 91% srch, 9% simp, 0% lkhd
c vsts: 6.0 search visits per propagation, 24197.4 per conflict
c wchs: 1094613446 pushed, 57800793 enlarged, 233 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         375531        185525         25066      12850024       2685877        172189
c 
c  0 0         21026   6      1519   1         0   0   6814551  53   1005855  37     47534  28     1.4
c  1 5         16199   4      3730   2       793   3   1319060  10<   350496  13     23625  14     1.3
c  2 6         72450  19     30892  17      3631  14   1764368  14    550801  21<    39742  23<    6.6
c  3 9        117671  31     73677  40      5608  22    980635   8    319627  12     21367  12    14.1
c  4 14        54235  14<    35155  19<     3178  13    679185   5    149924   6     10543   6     9.4
c  5 21        22279   6     12096   7      1843   7<   407338   3     82918   3      6866   4     6.9
c  6 30        16017   4      7684   4      1555   6    315136   2     63807   2      5394   3    10.5
c  7 41        15308   4      8091   4      1508   6    228996   2     58326   2      4844   3     6.7
c  8 54         9999   3      4392   2      1293   5    126752   1     38207   1      4017   2     4.4
c  9 69         8926   2      3944   2      1240   5     87126   1     25107   1      2922   2     5.6
c 10 86         7705   2      2554   1      1303   5     68954   1     20715   1      2632   2     4.2
c 11 126        7464   2      1155   1      1492   6     43297   0     14024   1      2053   1     3.0
c 12 230        5920   2       598   0      1515   6     14250   0      5882   0       634   0     4.0
c 13 534         332   0        38   0       107   0       376   0       188   0        16   0     0.5
c 
c avg                  3.8           3.8           5.5           1.5           1.9           2.5
c std                  2.6           2.0           3.3           2.2           2.3           2.6
c 
c   59.687  10% bump
c   39.357   7% probe
c   37.827   7% unhide
c   29.078   5% elim
c   21.190   4% sweep
c   19.954   4% cce
c    3.040   1% bca
c    2.800   0% gauss
c 
c    8.118 < 1% rest (below)
c 
c    2.749   0% block
c    1.736   0% transred
c    1.614   0% decide
c    0.805   0% ternres
c    0.770   0% quatres
c    0.445   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.349   1% preprocessing     3%
c  164.818  29% inprocessing     97%
c ==================================
c  170.167  30% simplifying
c  399.106  70% search
c ==================================
c  569.278 100% all
c 
c        377513 conflicts,         663.1 confs/sec
c          1827 ternaries,         206.6 confs/ternary
c          1754 binaries,          215.2 confs/binary
c           302 iterations,       1250.0 confs/iteration
c 
c             7 reductions,          0.0 redus/sec,  53930.4 confs/reduction
c          6601 restarts,           11.6 rests/sec,     57.2 confs/restart
c       2614099 decisions,        4592.0 decis/sec,      6.9 decis/conflict
c    1633724910 propagations,  2869821.1 props/sec,    625.0 props/decision
c 
c 569.3 seconds, 134.7 MB
c launch: done
