c launch: /data/cnf/sc2014/app/UR-15-10p1.cnf.bz2
c host: atom18
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/UR-15-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UR-15-10p1.cnf.bz2
c no embedded options
c found 'p cnf 199996 1019200' header
c read 199996 variables, 1019200 clauses, 2430990 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=4
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 189747 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  189747  1008281         0       0      0     0    0     0   53   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 6083 at-most-one constraints of average size 5.7
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6083 out of 6083 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 54081 variables
c [simpleprobe-1] all 145915 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 53 variables
c [simpleprobe-1] 237 variables remain 0% (145625 retained 100%)
c [simpleprobe-1] removed 53 variables, found 13804 hbrs, 1 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 4 units, 592 failed, 7212 tauts, 0 hbrs, 8802 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 145473 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 32892 not tried 23% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 55795 = 38% variables out of 145473 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 615269 negative 99.2% of 620148 except 4879 0.8%
c [phase-count-1] 489917 positive 79.0% of 620148 except 130231 21.0%
c [phase-count-1] less non-negative clauses 4879 than limit 62000 (10.0%)
c [phase-count-1] non-pos/non-neg = 130231/4879 = 26.69 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 89678 negative 100%
c [sort-queue-1] sorted 89678 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 89678 (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 62173 variables 40.9% (89678 remain 47%)
c [simplification-1] removed 388133 irredundant clauses 38.5% (620148 remain 62%)
c [simplification-1] maximum reduction of 41% = max (41%, 38%)
c [simplification-1] large reduction 41% >= 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    3.9   89677   620148         8       7      0  9660    0     5   43   0%      0    5    0    0 25223%
c i    4.0   89622   620148        45      39      1  9661    0     7   44   3%      0    7    3    0 24078%
c i    4.2   89606   620148       156     125     14  9669    0    19   44   2%      0   19    4    0 18434%
c i    4.5   89596   620148       274     222     23  9678    1    27   44   4%      0   27   12    0 19308%
c i    4.5   89516   620148       275     222     23  9678    1    27   44   4%      0   27   12    0 19232%
c i    4.8   89515   620148       424     346     36  9684    2    47   44   5%      0   47   23    0 15938%
c i    5.0   89220   620148       555     463     45  9687    4    75   44   6%      0   75   39    0 14121%
c i    5.0   88760   620148       556     463     45  9687    4    75   44   6%      0   75   39    0 14066%
c i    5.1   88644   620148       577     473     49  9692    4    79   44   5%      0   78   38    0 13316%
c i    5.6   88642   620148       744     606     53  9714    6   104   45   6%      1  104   49    0 11374%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 1065 variables
c [simpleprobe-2] 234 schedulable variables 0%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] fully completed simple probing
c [simpleprobe-2] removed 0 variables, found 412 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 58467 literals 33%
c [treelook-1] scheduling used 300047 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 326277 steps
c [treelook-1] 58463 literals remain 33%
c [treelook-1] 56211 variables remain to probed next time 63%
c [treelook-1] removed 0 variables, found 2520 hbrs
c [basicprobe-1] limit 4911808 based on 613976 irredundant clauses
c [basicprobe-1-0] 32567 probes remain 38% after last round
c [basicprobe-1-0] 23 units = 23 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3988 variables, found 23556 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 5 units, 1290 failed, 6635 tauts, 0 hbrs, 2083 literals
c [elim-2] 31512 variables 38% will be scheduled this time
c [elim-2] scheduled 31512 variables 38%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 9705 not tried 12% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 7 = 0% variables out of 31512 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 558010 negative 99.1% of 562889 except 4879 0.9%
c [phase-count-2] 443164 positive 78.7% of 562889 except 119725 21.3%
c [phase-count-2] less non-negative clauses 4879 than limit 56200 (10.0%)
c [phase-count-2] non-pos/non-neg = 119725/4879 = 24.54 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 1084 negative 100%
c [sort-queue-2] sorted 63111 enqueued variables after 744 conflicts
c [score-dist-2] active 19878 (24%), one 0 (0%), zero 63111 (76%)
c [score-dist-2] max exp 507, different 9 (2%)
c [score-dist-2] median active exp 503, avg 502.6
c [simplification-2] removed 5643 variables 6.4% (82989 remain 44%)
c [simplification-2] removed 57259 irredundant clauses 9.2% (562889 remain 56%)
c [simplification-2] maximum reduction of 9% = max (6%, 9%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1021 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c [simplification-3] limit 1021 conflicts (hard 11000) hit after 1021 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4377 at-most-one constraints of average size 4.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4377 out of 4377 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 137 variables
c [unhide-3] limit 122094 with penalty 0 = 0 + 0
c [unhide-3-3] 2 units, 554 failed, 8486 tauts, 0 hbrs, 9641 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 82382 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 17211 not tried 21% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1763 = 2% variables out of 82382 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 544178 negative 99.1% of 549009 except 4831 0.9%
c [phase-count-3] 432606 positive 78.8% of 549009 except 116403 21.2%
c [phase-count-3] less non-negative clauses 4831 than limit 54900 (10.0%)
c [phase-count-3] non-pos/non-neg = 116403/4831 = 24.10 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1067 negative 100%
c [sort-queue-3] sorted 60709 enqueued variables after 1021 conflicts
c [score-dist-3] active 19910 (25%), one 0 (0%), zero 60709 (75%)
c [score-dist-3] max exp 509, different 12 (2%)
c [score-dist-3] median active exp 502, avg 502.1
c [simplification-3] removed 2370 variables 2.9% (80619 remain 42%)
c [simplification-3] removed 13880 irredundant clauses 2.5% (549009 remain 54%)
c [simplification-3] maximum reduction of 3% = max (3%, 2%)
c [simplification-3] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-3] new conflict interval 5000
c [simplification-3] penalized conflict interval 5000 = 1 * 5000
c [simplification-3] hard conflict limit 16021 (soft 6021 + delta 10000)
c [simplification-3] new conflict limit 6021 (hard 16021)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   10.3   80618   549009      1202     936     59 23890   20   141   41  14%      2  140  108    1 7823%
c i   10.3   80608   549009      1208     940     60 23890   20   141   41  14%      2  140  109    1 7779%
c i   10.4   80596   549009      1219     946     60 23890   21   142   41  15%      2  140  114    1 7939%
c i   10.4   80582   549009      1231     953     60 23890   22   142   41  15%      2  141  118    1 8027%
c i   10.4   80312   549009      1237     958     60 23890   22   143   41  15%      2  141  117    1 7908%
c i   11.5   80171   549009      1899    1489     67 23898   47   201   42  23%      4  198  226    3 6749%
c i   11.5   80159   549009      1900    1489     67 23898   47   201   42  23%      4  198  225    3 6723%
c i   11.6   80146   549009      1945    1530     67 23898   47   207   42  23%      3  204  198    3 5861%
c i   12.1   80139   549009      2247    1794     70 23900   65   245   42  27%      3  241  292    5 6126%
c i   12.2   80126   549009      2248    1794     70 23900   65   245   42  27%      3  241  291    5 6102%
c i   12.2   80116   549009      2253    1798     70 23900   66   245   42  27%      3  241  295    5 6135%
c i   12.2   80115   549009      2254    1798     70 23900   66   245   42  27%      3  241  294    5 6111%
c i   12.2   80114   549009      2255    1798     70 23900   66   245   42  27%      3  241  292    5 6087%
c i   12.2   80113   549009      2256    1798     70 23900   66   245   42  27%      3  241  291    5 6064%
c i   12.2   80112   549009      2276    1816     70 23900   67   247   43  27%      3  243  288    5 5899%
c i   12.2   80100   549009      2279    1816     70 23900   67   247   43  27%      3  243  289    5 5910%
c i   12.2   80086   549009      2281    1817     70 23900   67   247   43  27%      3  243  288    5 5877%
c i   12.3   80076   549009      2283    1818     70 23900   67   247   43  27%      3  243  287    5 5845%
c i   12.3   80063   549009      2284    1818     70 23900   67   247   43  27%      3  243  285    5 5822%
c i   12.3   80050   549009      2285    1818     70 23900   67   247   43  27%      3  243  284    5 5800%
c i   12.3   80038   549009      2286    1818     70 23900   67   247   43  27%      3  242  283    5 5777%
c i   12.3   80024   549009      2287    1818     70 23900   67   247   43  27%      3  242  282    5 5755%
c i   12.5   80011   549009      2380    1902     70 23900   70   251   43  28%      3  246  257    5 4956%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   13.4   79998   549009      2843    2277     80 23913   79   276   43  29%      3  269  129    6 2064%
c i   13.5   79992   549009      2846    2278     80 23913   79   276   43  29%      3  269  131    6 2093%
c i   13.5   79982   549009      2881    2299     82 23914   81   277   43  29%      3  271  156    6 2427%
c i   13.5   79975   549009      2882    2299     82 23914   81   277   43  29%      3  271  155    6 2418%
c i   13.6   79965   549009      2883    2299     82 23914   81   277   43  29%      3  271  155    6 2408%
c i   13.6   79957   549009      2884    2299     82 23914   81   277   43  29%      3  270  154    6 2399%
c i   13.6   79947   549009      2885    2299     82 23914   81   277   43  29%      3  270  153    6 2389%
c i   13.7   79941   549009      2947    2331     82 23916   84   280   43  30%      3  273  181    7 2705%
c i   13.7   79931   549009      2949    2332     82 23916   84   280   43  30%      3  273  179    7 2687%
c i   13.7   79919   549009      2950    2332     82 23916   84   280   43  30%      3  273  179    7 2677%
c i   13.7   79907   549009      2951    2332     82 23916   84   280   43  30%      3  273  178    7 2666%
c i   13.8   79895   549009      2953    2333     82 23916   84   280   43  30%      3  273  177    7 2652%
c i   13.8   79888   549009      2954    2333     82 23916   84   279   43  30%      3  272  176    7 2642%
c i   13.8   79884   549009      2955    2333     82 23916   84   279   43  30%      3  272  176    7 2631%
c i   13.8   79874   549009      2956    2333     82 23916   84   279   43  30%      3  272  175    7 2621%
c i   13.8   79865   549009      2957    2333     82 23916   84   279   43  30%      3  272  174    7 2611%
c i   13.8   79858   549009      2958    2333     82 23916   84   279   43  30%      3  272  174    7 2601%
c i   13.8   79848   549009      2959    2333     82 23916   84   279   43  30%      3  272  173    7 2591%
c i   13.8   79838   549009      2960    2333     82 23916   84   279   43  30%      3  272  172    7 2581%
c i   13.9   79828   549009      2962    2334     82 23916   84   279   43  30%      3  272  171    7 2561%
c i   13.9   79821   549009      2964    2335     82 23916   84   279   43  30%      3  272  170    7 2547%
c i   13.9   79812   549009      2965    2335     82 23916   84   279   43  30%      3  272  169    7 2537%
c i   13.9   79805   549009      2967    2336     82 23916   84   279   43  30%      3  272  168    7 2523%
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.4   79796   549009      3279    2606     89 23919   89   299   45  30%      3  291  157    7 2125%
c i   14.9   79761   549009      3534    2790     93 23920  101   319   45  32%      3  309  249    9 2928%
c i   15.5   79760   549009      3829    3012     94 23922  126   346   47  36%      2  335  397   11 3778%
c i   15.9   79752   549009      4077    3190    109 23930  131   371   48  35%      2  359  278   11 2466%
c i   16.3   79745   549009      4280    3369    110 23940  137   399   49  34%      2  385  268   12 2231%
c i   16.5   79735   549009      4403    3479    113 23942  141   421   49  34%      2  407  278   13 2221%
c i   16.5   79723   549009      4409    3484    113 23942  142   422   49  34%      2  408  282   13 2247%
c i   16.5   79710   549009      4411    3485    113 23942  142   422   49  34%      2  408  284   13 2261%
c i   16.5   79709   549009      4415    3485    113 23942  142   422   49  34%      2  408  283   13 2252%
c i   16.5   79708   549009      4416    3485    113 23942  142   422   49  34%      2  408  282   13 2243%
c i   16.6   79707   549009      4417    3485    113 23942  142   422   49  34%      2  408  281   13 2234%
c i   16.6   79706   549009      4437    3499    116 23944  143   425   49  34%      2  411  286   13 2259%
c i   16.6   79705   549009      4456    3511    116 23944  145   428   49  34%      2  413  311   13 2420%
c i   16.7   79704   549009      4457    3511    116 23944  145   428   49  34%      2  413  310   13 2411%
c i   16.7   79703   549009      4458    3511    116 23944  145   428   49  34%      2  413  309   13 2401%
c i   16.7   79702   549009      4459    3511    116 23944  145   428   49  34%      2  413  308   13 2392%
c i   16.7   79701   549009      4460    3511    116 23944  145   427   49  34%      2  413  306   13 2383%
c i   16.7   79700   549009      4461    3511    116 23944  145   427   49  34%      2  413  305   13 2374%
c i   16.7   79699   549009      4462    3511    116 23944  145   427   49  34%      2  413  304   13 2364%
c i   16.7   79698   549009      4463    3511    116 23944  145   427   49  34%      2  413  303   13 2355%
c i   16.7   79697   549009      4464    3511    116 23944  145   427   49  34%      2  413  302   13 2346%
c i   16.7   79696   549009      4465    3511    116 23944  145   427   49  34%      2  412  300   13 2337%
c i   16.7   79695   549009      4466    3511    116 23944  145   427   49  34%      2  412  299   13 2328%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   16.7   79694   549009      4467    3511    116 23944  145   427   49  34%      2  412  298   13 2319%
c i   16.8   79693   549009      4468    3511    116 23944  145   427   49  34%      2  412  297   13 2310%
c i   16.8   79692   549009      4469    3511    116 23944  145   427   49  34%      2  412  296   13 2301%
c i   16.8   79691   549009      4480    3515    116 23944  147   428   49  34%      2  414  317   13 2442%
c i   16.9   79690   549009      4545    3569    116 23944  149   436   49  34%      2  421  317   13 2389%
c i   17.0   79689   549009      4598    3610    118 23944  151   440   49  34%      2  425  311   13 2302%
c i   17.5   79678   549009      4816    3766    126 23965  156   459   49  34%      2  442  280   14 1961%
c i   18.1   79677   549009      5103    3977    149 23970  164   487   49  34%      2  468  319   15 2072%
c i   18.4   79664   549009      5255    4097    152 23978  171   522   49  33%      2  502  311   16 1922%
c i   18.5   79650   549009      5332    4166    154 23978  170   542   49  31%      2  521  258   16 1586%
c i   19.4   79637   549009      5632    4432    154 23981  179   575   50  31%      2  552  293   18 1667%
c 
c [simplification-4] limit of 165 binary hit after 165 binaries
c [decomp-7] removed 1021 variables
c [treelook-2] limit 165207 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 32190 literals 20%
c [treelook-2] scheduling used 231661 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 165207 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 209426 steps
c [treelook-2] 32027 literals remain 20%
c [treelook-2] 24347 variables remain to probed next time 31%
c [decomp-8] removed 31 variables
c [treelook-2] removed 167 variables, found 1565 hbrs
c [unhide-4] limit 660831 with penalty 0 = 0 + 0
c [unhide-4-4] 1 units, 827 failed, 3174 tauts, 0 hbrs, 104027 literals
c [elim-4] 9624 variables 12% will be scheduled this time
c [elim-4] scheduled 9624 variables 12%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1321663200 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 19635741 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 9624 scheduled
c [phase-count-4] 527412 negative 99.1% of 532243 except 4831 0.9%
c [phase-count-4] 418295 positive 78.6% of 532243 except 113948 21.4%
c [phase-count-4] less non-negative clauses 4831 than limit 53200 (10.0%)
c [phase-count-4] non-pos/non-neg = 113948/4831 = 23.59 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 206 negative 100%
c [sort-queue-4] sorted 41577 enqueued variables after 5861 conflicts
c [score-dist-4] active 37052 (47%), one 0 (0%), zero 41577 (53%)
c [score-dist-4] max exp 509, different 31 (6%)
c [score-dist-4] median active exp 501, avg 497.8
c [simplification-4] removed 1003 variables 1.3% (78629 remain 41%)
c [simplification-4] removed 16766 irredundant clauses 3.1% (532243 remain 53%)
c [simplification-4] maximum reduction of 3% = max (1%, 3%)
c [simplification-4] forced so keeping old conflict interval 5000
c [simplification-4] conflict limit remains at 6454 (hard 16021)
c [simplification-4] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   21.9   78628   532243      5864    4557    148 20066  184   583   45  32%      2  558  285   18 1540%
c i   21.9   78625   532243      5878    4564    148 20066  185   583   49  32%      2  558  295   19 1586%
c i   21.9   78615   532243      5879    4564    148 20066  185   583   49  32%      2  558  293   19 1579%
c i   21.9   78607   532243      5880    4564    148 20066  185   583   49  32%      2  558  292   19 1573%
c i   21.9   78596   532243      5881    4564    148 20066  185   583   49  32%      2  558  291   19 1567%
c i   21.9   78585   532243      5882    4564    148 20066  185   583   49  32%      2  557  290   19 1561%
c i   22.1   78577   532243      5939    4611    148 20071  185   582   50  32%      2  556  270   19 1445%
c i   22.1   78571   532243      5958    4627    148 20072  185   581   50  32%      2  555  260   19 1385%
c i   22.1   78562   532243      5959    4627    148 20072  185   581   50  32%      2  555  259   19 1379%
c i   22.6   78551   532243      6293    4837    149 20072  187   563   51  33%      2  534  239   20 1210%
c 
c [simplification-5] limit 6504 conflicts (hard 16021) hit after 6504 conflicts
c [quatres-1] found 25720 quaternary clauses 30% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 78544 free variables schedulable
c [ternres-1] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 61 xors of average arity 2.9
c [gauss-1] connected 177 occurrences of 122 variables (average 1.5)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 6 variables
c [basicprobe-2] limit 18170524 penalty 0 = 0 + 0
c [basicprobe-2-0] 28260 probes remain 38% after last round
c [basicprobe-2-0] 73 units = 73 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 3449 variables, found 46019 hbrs
c [bate-1] eliminated 44 asymmetric tautologies during probing
c [unhide-5] limit 726820 with penalty 0 = 0 + 0
c [unhide-5-5] 6 units, 304 failed, 10742 tauts, 0 hbrs, 11407 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 162 transitive binary clauses
c [transred-1] found 8 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 74689 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 8935 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 9 clauses out of 308 (3%) of length 10
c [cce-1-1] eliminated 53 clauses out of 1550 (3%) of length 9
c [cce-1-1] eliminated 25 clauses out of 465 (5%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 87 large clauses in 30000010 steps
c [cce-1-1] allowing another 15000005 steps for small clauses
c [cce-1-1] scheduling 264137 clauses = 247795 binary + 16342 ternary
c [cce-1-1] tried to eliminate 396 small clauses 0%
c [cce-1-1] eliminated 124 binary clauses 0%
c [cce-1-1] eliminated 7 ternary clauses 0%
c [cce-1-1] eliminated 131 small clauses 0%
c [cce-1-1] eliminated 131 small clauses in 30000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 218 covered clauses in round 1
c [cce-1] eliminated 218 covered clauses in TOTAL during 1 rounds
c [cce-1] 218 < 1/100 * 486066 = 4860 considered unsuccessful
c [bca-1] limit of 10000000 steps and 972196 added (scaled 2)
c [bca-1] 132012 out of 149380 literals actually usable 88%
c [bca-1] added 162 blocked clauses in 394047 steps
c [sweep-1] limit 1090231 penalty 0 = 0 + 0
c [sweep-1-1] 3870 pos 5.2% + 70819 neg 94.8% = 74689 sched 100.0% ret 0
c [sweep-1-1] 2363905 steps 14 queries 22569.14 avg class size
c [sweep-1-1] 192 decisions 11 SAT calls 87.36 avg env size
c [sweep-1-1] 74631 variables remain 100% (28 retained 0%)
c [decomp-10] removed 151 variables
c [sweep-1-1] removed 151 vars (0 failed, 2 eqs, 6 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 151 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-5] 480557 negative 99.0% of 485368 except 4811 1.0%
c [phase-count-5] 388894 positive 80.1% of 485368 except 96474 19.9%
c [phase-count-5] less non-negative clauses 4811 than limit 48500 (10.0%)
c [phase-count-5] non-pos/non-neg = 96474/4811 = 20.05 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 206 negative 100%
c [sort-queue-5] sorted 38608 enqueued variables after 6504 conflicts
c [score-dist-5] active 35930 (48%), one 0 (0%), zero 38608 (52%)
c [score-dist-5] max exp 509, different 34 (7%)
c [score-dist-5] median active exp 498, avg 495.5
c [simplification-5] removed 4006 variables 5.1% (74538 remain 39%)
c [simplification-5] removed 46875 irredundant clauses 8.8% (485368 remain 48%)
c [simplification-5] maximum reduction of 9% = max (5%, 9%)
c [simplification-5] large reduction 9% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 18504 (soft 8504 + delta 10000)
c [simplification-5] new conflict limit 8504 (hard 18504)
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   28.2   74537   485368      6968    5157    178 70416  202   535   49  38%      4  501  255   22 1136%
c i   28.2   74532   485368      6970    5157    178 70416  202   535   49  38%      4  501  254   22 1133%
c i   28.2   74531   485368      6971    5157    178 70416  202   534   49  38%      4  501  253   22 1129%
c i   28.2   74530   485368      6974    5159    178 70416  201   534   49  38%      4  500  250   22 1116%
c i   28.2   74529   485368      6977    5161    178 70416  201   534   49  38%      4  500  247   22 1104%
c i   28.2   74528   485368      6978    5161    178 70416  201   534   49  38%      4  500  247   22 1099%
c i   28.2   74527   485368      6979    5161    178 70416  201   534   49  38%      4  500  246   22 1095%
c i   29.4   74526   485368      7589    5696    185 70425  204   566   50  36%      4  528  244   24 1008%
c i   30.2   74525   485368      7999    6028    189 70435  247   636   50  39%      4  594  626   28 2225%
c i   30.7   74524   485368      8328    6301    192 70442  250   685   53  37%      3  640  395   29 1345%
c 
c [simplification-6] limit 8545 conflicts (hard 18504) hit after 8545 conflicts
c [ternres-2] limit 4571513 with penalty 0 = 0 + 0
c [ternres-2] all 74455 free variables schedulable
c [ternres-2] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-2] 35653 variables remain 48% (38802 retained 52%)
c [card-3] limit 571439 penalty 2 = 2 + 0
c [card-3] found 2388 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 571439 for elimination
c [card-3] 2388 out of 2388 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 83 variables
c [unhide-6] limit 914302 with penalty 0 = 0 + 0
c [unhide-6-6] 10 units, 839 failed, 5668 tauts, 0 hbrs, 71842 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 193 transitive binary clauses
c [transred-2] found 8 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 73862 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 553 blocked clauses
c [block-2] 553 < 1/100 * 484916 = 4849 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 73862 variables 100%
c [elim-5] limit of 45715132 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 1304 variables 2% in round 1 in 43039192 steps
c [elim-5-1] backward subsumption/strengthening limit 2675940
c [elim-5-1-1] backward checking 5511 touched variables 7%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 70 clauses in 2286678 steps
c [elim-5-1] rescheduled 143 variables 0% by backward subsumption
c [elim-5-2] eliminated 20 variables 0% in round 2 in 193220 steps
c [elim-5-2] backward subsumption/strengthening limit 193200
c [elim-5-2-1] backward checking 143 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 155276 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 1324 = 2% variables out of 73862 scheduled
c [bca-2] limit of 10000000 steps and 953317 added (scaled 2)
c [bca-2] 128140 out of 145078 literals actually usable 88%
c [bca-2] added 107 blocked clauses in 384194 steps
c [sweep-2] limit 1371453 penalty 0 = 0 + 0
c [sweep-2-1] 3762 pos 5.2% + 68753 neg 94.8% = 72515 sched 100.0% ret 23
c [sweep-2-1] 1450156 steps 11 queries 13334.64 avg class size
c [sweep-2-1] 40 decisions 8 SAT calls 67.12 avg env size
c [sweep-2-1] 72496 variables remain 100% (42 retained 0%)
c [decomp-12] removed 3 variables
c [sweep-2-1] removed 3 vars (0 failed, 2 eqs, 4 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 3 vars in TOTAL (1 rounds, 10 queries)
c [phase-count-6] 471704 negative 99.0% of 476365 except 4661 1.0%
c [phase-count-6] 380277 positive 79.8% of 476365 except 96088 20.2%
c [phase-count-6] less non-negative clauses 4661 than limit 47600 (10.0%)
c [phase-count-6] non-pos/non-neg = 96088/4661 = 20.62 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 164 negative 100%
c [sort-queue-6] sorted 34120 enqueued variables after 8545 conflicts
c [score-dist-6] active 38415 (53%), one 0 (0%), zero 34120 (47%)
c [score-dist-6] max exp 509, different 41 (8%)
c [score-dist-6] median active exp 499, avg 495.1
c [simplification-6] removed 1920 variables 2.6% (72535 remain 38%)
c [simplification-6] removed 9003 irredundant clauses 1.9% (476365 remain 47%)
c [simplification-6] maximum reduction of 3% = max (3%, 2%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 10000
c [simplification-6] penalized conflict interval 10000 = 1 * 10000
c [simplification-6] hard conflict limit 28545 (soft 18545 + delta 10000)
c [simplification-6] new conflict limit 18545 (hard 28545)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   36.1   72534   476365      9360    4811    191 65831  273   801   46  34%      7  745  401   34 1165%
c i   37.5   72533   476365     10160    5465    217 65864  284   848   46  34%      7  783  388   38 1022%
c i   38.2   72532   476365     10531    5741    230 65870  309   886   49  35%      5  817  579   41 1415%
c i   39.4   72531   476365     11055    6026    240 65898  357   914   52  39%      5  838  673   46 1457%
c i   39.5   72523   476365     11059    6028    240 65898  357   914   52  39%      5  838  671   46 1453%
c i   39.5   72521   476365     11060    6028    240 65898  357   914   52  39%      5  838  669   46 1447%
c i   39.6   72515   476365     11121    6049    240 65898  365   914   52  40%      5  837  725   47 1541%
c i   39.7   72511   476365     11122    6049    240 65898  365   914   52  40%      5  837  722   47 1535%
c i   39.7   72503   476365     11126    6052    240 65898  365   914   52  40%      5  837  715   47 1520%
c i   39.7   72501   476365     11127    6052    240 65898  365   913   52  40%      4  837  712   47 1514%
c i   39.7   72499   476365     11128    6052    240 65898  365   913   52  40%      4  836  709   47 1508%
c i   39.7   72495   476365     11129    6052    240 65898  365   913   52  40%      4  836  707   47 1502%
c i   39.7   72491   476365     11130    6052    240 65898  365   913   52  40%      4  836  704   47 1497%
c i   39.7   72484   476365     11131    6052    240 65898  365   912   52  40%      4  836  701   47 1491%
c i   39.7   72480   476365     11132    6052    240 65898  364   912   52  40%      4  835  698   47 1485%
c i   39.7   72473   476365     11133    6052    240 65898  364   912   52  40%      4  835  696   47 1479%
c i   39.7   72466   476365     11134    6052    240 65898  364   912   52  40%      4  835  693   47 1473%
c i   39.8   72461   476365     11135    6052    240 65898  364   912   52  40%      4  835  690   47 1468%
c i   39.8   72454   476365     11136    6052    240 65898  364   911   52  40%      4  834  688   47 1462%
c i   41.3   72449   476365     11990    6686    258 65912  368   899   52  41%      6  811  319   51  621%
c i   42.5   72448   476365     12583    7112    264 65943  358   871   59  41%      5  776  330   54  617%
c i   42.8   72447   476365     12794    7266    266 65947  352   855   59  41%      4  758  289   54  533%
c i   42.9   72446   476365     12843    7301    266 65949  352   851   59  41%      4  753  303   54  557%
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   42.9   72445   476365     12847    7302    266 65951  352   851   59  41%      4  753  300   54  551%
c i   42.9   72357   476365     12855    7309    266 65951  352   850   59  41%      4  752  301   54  553%
c i   43.0   72356   476365     12856    7309    266 65951  352   850   59  41%      4  752  300   54  551%
c i   43.0   72355   476365     12857    7309    266 65951  352   849   59  41%      4  752  299   54  549%
c i   43.0   72354   476365     12858    7309    266 65951  352   849   59  41%      4  751  297   54  546%
c i   43.0   72353   476365     12863    7313    266 65951  352   849   59  41%      4  751  300   54  550%
c i   43.3   72352   476365     13002    7395    267 65954  354   839   59  42%      4  740  356   55  644%
c i   43.3   72351   476365     13003    7395    267 65954  354   839   59  42%      4  739  354   55  641%
c i   43.3   72350   476365     13008    7396    267 65954  354   838   59  42%      4  739  355   55  642%
c i   43.3   72349   476365     13020    7402    267 65955  354   837   59  42%      4  738  357   55  646%
c i   43.4   72348   476365     13087    7456    267 65956  353   833   59  42%      3  733  342   56  615%
c i   43.4   72347   476365     13092    7459    267 65956  353   833   59  42%      3  732  337   56  606%
c i   44.8   72346   476365     13815    7905    286 66014  341   806   59  42%      4  698  334   58  577%
c i   44.8   72339   476365     13816    7905    286 66014  341   806   59  42%      4  698  333   58  575%
c i   45.4   72287   476365     14165    8183    287 66028  343   818   59  42%      4  706  380   60  638%
c i   45.4   72281   476365     14168    8185    287 66028  343   818   59  42%      4  706  379   60  636%
c i   45.4   72277   476365     14169    8185    287 66028  343   818   59  42%      4  706  378   60  634%
c i   45.4   72273   476365     14170    8185    287 66028  343   817   59  42%      4  706  376   60  631%
c i   45.4   72269   476365     14171    8185    287 66028  343   817   59  42%      4  705  375   60  629%
c i   47.0   72264   476365     14777    8497    291 66034  362   798   60  45%      4  679  434   63  684%
c i   47.1   72263   476365     14812    8528    291 66034  360   796   60  45%      4  678  404   63  637%
c i   48.6   72262   476365     15478    8923    295 66039  362   772   60  47%      4  646  318   67  478%
c i   50.7   72261   476365     16659    9793    315 66068  333   730   66  46%      8  594  235   70  337%
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   54.5   72252   476365     18511   10754    330 66097  285   583   67  49%     16  433  194   73  264%
c i   54.7   72251   476365     18580   10767    330 66098  284   577   67  49%     15  426  194   74  264%
c 
c [simplification-7] limit 18761 conflicts (hard 28545) hit after 18763 conflicts
c [quatres-2] found 29779 quaternary clauses 37% in total
c [quatres-2-2] added 4 quaternary resolvents
c [ternres-3] limit 9697629 with penalty 0 = 0 + 0
c [ternres-3] 34578 schedulable variables 48%
c [ternres-3] 24 ternary resolvents (0 bin, 24 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 19 xors of average arity 2.8
c [gauss-2] connected 54 occurrences of 54 variables (average 1.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 14 variables
c [simpleprobe-3] all 72237 free variables schedulable
c [simpleprobe-3] limit 19395258 penalty 1 = 1 + 0
c [decomp-14] removed 705 variables
c [simpleprobe-3] 15463 variables remain 22% (56069 retained 78%)
c [simpleprobe-3] removed 705 variables, found 49306 hbrs, 471 units
c [unhide-7] limit 969762 with penalty 1 = 0 + 1
c [unhide-7-7] 2 units, 121 failed, 7882 tauts, 0 hbrs, 226108 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 222 transitive binary clauses
c [transred-3] found 2 units
c [cce-2] limit of 24244072 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 12122051 steps for small clauses
c [cce-2-1] scheduling 364080 clauses = 234653 binary + 129427 ternary
c [cce-2-1] tried to eliminate 293 small clauses 0%
c [cce-2-1] eliminated 51 binary clauses 0%
c [cce-2-1] eliminated 18 ternary clauses 0%
c [cce-2-1] eliminated 69 small clauses 0%
c [cce-2-1] eliminated 1280 small clauses in 24244075 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1280 covered clauses in round 1
c [cce-2] eliminated 1280 covered clauses in TOTAL during 1 rounds
c [cce-2] 1280 < 1/100 * 461314 = 4613 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 71395 variables 100%
c [elim-6] limit of 193952580 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 257 variables 0% in round 1 in 41144432 steps
c [elim-6-1] backward subsumption/strengthening limit 41144400
c [elim-6-1-1] backward checking 1392 touched variables 2%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 21 clauses in 620421 steps
c [elim-6-1] rescheduled 52 variables 0% by backward subsumption
c [elim-6-2] eliminated 9 variables 0% in round 2 in 60512 steps
c [elim-6-2] backward subsumption/strengthening limit 60500
c [elim-6-2-1] backward checking 58 touched variables 0%
c [elim-6-2-1] incomplete backward checking 0 remain 0%
c [elim-6-2] subsumed 0 and strengthened 0 clauses in 60501 steps
c [elim-6-2] fully rescheduled 71129 variables 100%
c [elim-6-3] eliminated 6 variables 0% in round 3 in 41090862 steps
c [elim-6-3] backward subsumption/strengthening limit 41090800
c [elim-6-3-1] backward checking 52 touched variables 0%
c [elim-6-3-1] fully completed backward checking in 1 rounds
c [elim-6-3] subsumed 0 and strengthened 0 clauses in 104989 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 272 = 0% variables out of 71395 scheduled
c [elim-6] 272 < 1/100 * 71395 = 713 considered unsuccessful
c [bca-3] limit of 10000000 steps and 919786 added (scaled 2)
c [bca-3] 119934 out of 142248 literals actually usable 84%
c [bca-3] added 45 blocked clauses in 356792 steps
c [sweep-3] limit 2909288 penalty 0 = 0 + 0
c [sweep-3-1] 3149 pos 4.4% + 67933 neg 95.6% = 71082 sched 99.9% ret 41
c [sweep-3-1] 2965368 steps 38 queries 13351.63 avg class size
c [sweep-3-1] 481 decisions 33 SAT calls 115.48 avg env size
c [sweep-3-1] 70734 variables remain 99% (379 retained 1%)
c [decomp-15] removed 16 variables
c [sweep-3-1] removed 16 vars (0 failed, 6 eqs, 11 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 16 vars in TOTAL (1 rounds, 37 queries)
c [phase-count-7] 454796 negative 99.0% of 459459 except 4663 1.0%
c [phase-count-7] 365645 positive 79.6% of 459459 except 93814 20.4%
c [phase-count-7] less non-negative clauses 4663 than limit 45900 (10.0%)
c [phase-count-7] non-pos/non-neg = 93814/4663 = 20.12 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 96 negative 100%
c [sort-queue-7] sorted 27166 enqueued variables after 18763 conflicts
c [score-dist-7] active 43941 (62%), one 0 (0%), zero 27166 (38%)
c [score-dist-7] max exp 509, different 81 (16%)
c [score-dist-7] median active exp 493, avg 486.3
c [simplification-7] removed 1144 variables 1.6% (71107 remain 37%)
c [simplification-7] removed 16906 irredundant clauses 3.5% (459459 remain 46%)
c [simplification-7] maximum reduction of 4% = max (2%, 4%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 14000
c [simplification-7] penalized conflict interval 14000 = 1 * 14000
c [simplification-7] hard conflict limit 42763 (soft 32763 + delta 10000)
c [simplification-7] new conflict limit 32763 (hard 42763)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   62.0   71106   459459     18820   10611    359 113677  276   560   59  49%     12  408  165   74  224%
c i   62.0   71105   459459     18825   10611    359 113677  276   560   59  49%     12  407  165   74  224%
c i   62.3   71104   459459     19020   10759    359 113677  270   544   61  50%     10  390  160   74  216%
c i   63.4   71103   459459     19683   11204    361 113687  250   496   61  50%      7  338  173   75  233%
c i   63.9   71102   459459     19948   11282    361 113689  244   476   61  51%      6  318  155   75  207%
c i   64.0   71093   459459     20004   11324    362 113689  242   473   61  51%      5  314  145   75  193%
c i   64.3   71018   459459     20222   11443    363 113694  236   460   61  51%      4  300  144   75  192%
c i   66.9   71017   459459     22027   12582    395 113716  188   367   63  51%     14  200  102   76  134%
c i   68.4   71001   459459     22860   13043    401 113725  176   334   63  53%     10  165  119   76  156%
c i   70.0   71000   459459     23933   13738    402 113732  158   298   65  53%      9  127   86   77  112%
c i   70.3   70996   459459     24131   13894    402 113734  154   294   66  53%      7  122   82   77  107%
c i   71.4   70989   459459     24901   14359    411 113738  159   296   74  54%      6  123  215   78  275%
c i   73.0   70985   459459     25848   14960    421 113771  158   296   74  53%      6  121  118   79  149%
c i   80.5   70984   459459     30972   18214    432 113791  114   195   81  58%     60   14   72   81   88%
c i   80.8   70983   459459     31294   18406    432 113791  113   189   81  60%     43    8   91   81  112%
c i   87.3   70978   459459     35231   21952    438 113802   86   133  107  65%     41  -47   70   80   87%
c i   89.8   70975   459459     36926   23437    443 113805   76   114  113  66%     16  -64   46   80   57%
c i   96.5   70974   459459     40937   27353    448 113813   52    77  139  68%     40  -96   33   77   43%
c i   97.5   70909   459459     41577   27979    448 113814   50    74  143  67%     20  -98   31   77   40%
c i   97.6   70906   459459     41697   28094    448 113814   50    74  143  67%     17  -98   39   77   51%
c 
c [simplification-8] limit 32765 conflicts (hard 42763) hit after 42763 conflicts
c [quatres-3] found 30215 quaternary clauses 38% in total
c [quatres-3-2] added 1 quaternary resolvents
c [ternres-4] limit 18432488 with penalty 0 = 0 + 0
c [ternres-4] all 70903 free variables schedulable
c [ternres-4] 34 ternary resolvents (0 bin, 34 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-16] removed 217 variables
c [treelook-3] limit 1843248 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 115449 literals 81%
c [treelook-3] scheduling used 1474272 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1843248 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 1931519 steps
c [treelook-3] 115421 literals remain 81%
c [treelook-3] 20456 variables remain to probed next time 29%
c [decomp-17] removed 1 variables
c [treelook-3] removed 6 variables, found 8841 hbrs
c [unhide-8] limit 460812 with penalty 3 = 0 + 3
c [unhide-8-8] 2 units, 236 failed, 10991 tauts, 0 hbrs, 4695825 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 172 transitive binary clauses
c [transred-4] found 6 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 70658 variables 100%
c [block-3] limit of 92162444 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1 blocked clauses
c [block-3] 1 < 1/100 * 458064 = 4580 considered unsuccessful
c [bca-4] limit of 10000000 steps and 913023 added (scaled 2)
c [bca-4] 115374 out of 141318 literals actually usable 82%
c [bca-4] added 62 blocked clauses in 351758 steps
c [sweep-4] limit 5529746 penalty 0 = 0 + 0
c [sweep-4-1] 3731 pos 5.3% + 66561 neg 94.7% = 70292 sched 99.5% ret 366
c [sweep-4-1] 5580121 steps 56 queries 5211.84 avg class size
c [sweep-4-1] 942 decisions 48 SAT calls 486.23 avg env size
c [sweep-4-1] 69309 variables remain 98% (1226 retained 2%)
c [decomp-18] removed 130 variables
c [sweep-4-1] removed 130 vars (0 failed, 8 eqs, 16 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 130 vars in TOTAL (1 rounds, 55 queries)
c [phase-count-8] 450459 negative 99.0% of 455122 except 4663 1.0%
c [phase-count-8] 361646 positive 79.5% of 455122 except 93476 20.5%
c [phase-count-8] less non-negative clauses 4663 than limit 45500 (10.0%)
c [phase-count-8] non-pos/non-neg = 93476/4663 = 20.05 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 82 negative 100%
c [sort-queue-8] sorted 25165 enqueued variables after 42763 conflicts
c [score-dist-8] active 45363 (64%), one 0 (0%), zero 25165 (36%)
c [score-dist-8] max exp 509, different 175 (34%)
c [score-dist-8] median active exp 496, avg 459.3
c [simplification-8] removed 375 variables 0.5% (70528 remain 37%)
c [simplification-8] removed 4337 irredundant clauses 0.9% (455122 remain 45%)
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 24000
c [simplification-8] penalized conflict interval 24000 = 1 * 24000
c [simplification-8] hard conflict limit 78763 (soft 66763 + delta 12000)
c [simplification-8] new conflict limit 66763 (hard 78763)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  114.9   70527   455122     47066   32721    501 114386   53    77  164  69%     58  -88   49   75   65%
c i  115.3   70526   455122     47275   32900    503 114389   53    77  164  69%     46  -88   50   75   66%
c i  115.4   70525   455122     47316   32940    503 114389   53    77  164  69%     44  -88   50   75   66%
c i  121.6   70461   455122     50967   35707    531 114411   91   143  174  64%     32  -19   58   77   75%
c i  121.8   70460   455122     51276   35912    540 114423   89   143  174  63%     21  -19   67   77   86%
c i  121.8   70459   455122     51290   35923    540 114423   89   143  174  63%     21  -19   66   77   86%
c i  121.8   70458   455122     51298   35925    540 114423   89   142  174  63%     20  -19   67   77   87%
c i  121.8   70457   455122     51299   35925    540 114423   89   142  174  63%     20  -19   67   77   87%
c i  121.8   70456   455122     51300   35925    540 114423   89   142  174  63%     20  -19   67   77   86%
c i  121.9   70455   455122     51301   35925    540 114423   89   142  174  63%     20  -19   67   77   86%
c i  122.1   70454   455122     51589   36103    540 114423   89   141  174  63%     13  -20   74   77   96%
c i  122.4   70397   455122     51855   36307    542 114429  102   170  174  60%      8    9  245   78  313%
c i  122.5   70396   455122     51904   36339    542 114429  106   177  174  60%      7   16  291   79  370%
c i  124.7   70395   455122     53368   37581    553 114452  163   374  174  43%      4  210  218   83  261%
c i  125.2   70384   455122     53697   37829    553 114455  175   405  174  43%      0  239  324   85  383%
c i  126.3   70383   455122     54395   38415    557 114472  205   522  174  39%     -3  353  404   88  462%
c i  126.5   70382   455122     54540   38548    557 114474  205   536  174  38%     -4  367  315   88  359%
c i  127.0   70379   455122     54815   38776    560 114478  205   555  174  37%     -5  384  247   88  280%
c i  127.1   70378   455122     54881   38836    561 114480  207   565  174  37%     -5  394  258   88  292%
c i  127.2   70377   455122     54974   38920    563 114481  214   574  174  37%     -6  402  342   89  384%
c i  128.8   70362   455122     55943   39738    571 114502  244   669  183  36%     -4  491  356   93  383%
c i  129.6   70361   455122     56475   40195    574 114534  247   689  183  36%     -5  507  284   94  300%
c i  129.6   70360   455122     56476   40195    574 114534  247   689  183  36%     -5  507  283   94  299%
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  130.3   70359   455122     56808   40453    574 114541  258   694  183  37%     -6  509  339   96  353%
c i  130.8   70358   455122     57002   40570    575 114557  265   692  183  38%     -7  506  384   97  396%
c i  131.9   70357   455122     57624   41050    576 114569  279   715  183  39%     -6  523  393   99  396%
c i  132.1   70356   455122     57728   41123    578 114577  281   718  183  39%     -7  525  368  100  369%
c i  132.1   70355   455122     57730   41124    578 114577  281   717  183  39%     -7  525  367  100  368%
c i  132.7   70354   455122     58115   41427    577 114582  300   745  183  40%     -7  549  496  102  486%
c i  134.2   70353   455122     59079   42221    584 114609  323   810  183  40%     -4  606  290  107  272%
c i  134.2   70352   455122     59081   42221    584 114610  323   809  183  40%     -4  606  288  107  270%
c i  134.3   70351   455122     59086   42224    584 114611  323   809  183  40%     -4  606  283  107  265%
c i  134.3   70350   455122     59087   42224    584 114611  323   809  183  40%     -4  605  282  107  264%
c i  134.3   70349   455122     59094   42230    584 114611  322   809  183  40%     -4  605  276  107  259%
c i  134.3   70348   455122     59115   42246    584 114615  321   809  183  40%     -4  606  269  107  253%
c i  134.3   70347   455122     59116   42246    584 114615  321   809  183  40%     -4  605  268  107  252%
c i  135.0   70346   455122     59583   42636    584 114626  336   839  183  40%     -5  631  440  109  403%
c i  135.9   70343   455122     60140   43013    602 114648  339   852  197  40%     -6  639  289  111  260%
c i  135.9   70342   455122     60141   43013    602 114648  339   852  197  40%     -6  639  288  111  259%
c i  136.9   70341   455122     60657   43391    612 114667  358   891  197  40%     -6  672  511  114  447%
c i  136.9   70340   455122     60681   43411    612 114667  361   893  197  40%     -6  674  541  115  472%
c i  137.1   70336   455122     60764   43468    612 114668  367   899  197  41%     -6  680  574  115  498%
c i  138.7   70335   455122     61692   44166    617 114680  368   899  197  41%     -4  670  304  119  256%
c i  139.2   70334   455122     62068   44489    618 114688  351   880  197  40%     -5  647  202  119  169%
c i  139.7   70319   455122     62330   44715    619 114691  348   874  197  40%     -6  638  272  120  227%
c i  140.3   70315   455122     62656   44988    623 114693  355   874  197  41%     -7  635  396  121  326%
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  141.6   70311   455122     63315   45466    627 114712  348   832  197  42%     -6  588  331  123  269%
c i  141.6   70310   455122     63317   45467    627 114712  348   832  197  42%     -6  587  331  123  268%
c i  141.6   70309   455122     63318   45467    627 114712  347   832  197  42%     -6  587  330  123  267%
c i  141.6   70308   455122     63319   45467    627 114712  347   832  197  42%     -6  587  328  123  266%
c i  141.7   70307   455122     63346   45477    628 114713  348   829  197  42%     -6  584  337  123  273%
c i  141.9   70306   455122     63435   45515    629 114714  347   822  197  42%     -6  577  331  124  267%
c i  142.4   70305   455122     63857   45805    629 114716  351   807  197  44%     -7  557  396  125  316%
c i  142.9   70304   455122     64209   46072    632 114718  345   791  216  44%     -7  539  299  126  237%
c i  142.9   70303   455122     64222   46080    632 114718  345   790  216  44%     -7  538  302  126  239%
c i  142.9   70302   455122     64225   46082    632 114718  345   790  216  44%     -7  538  298  126  236%
c i  142.9   70301   455122     64226   46082    632 114718  345   790  216  44%     -7  537  297  126  235%
c i  143.0   70300   455122     64246   46093    632 114718  345   789  216  44%     -7  537  300  126  238%
c i  143.0   70299   455122     64247   46093    632 114718  345   789  216  44%     -7  536  299  126  237%
c i  143.0   70298   455122     64248   46093    632 114718  345   789  216  44%     -7  536  298  126  236%
c i  143.0   70297   455122     64249   46093    632 114718  345   788  216  44%     -7  536  296  126  235%
c i  143.1   70296   455122     64293   46122    632 114719  344   786  216  44%     -7  534  292  126  231%
c i  143.2   70294   455122     64423   46233    633 114720  338   780  216  43%     -7  526  238  126  188%
c i  143.3   70293   455122     64466   46269    633 114721  337   779  216  43%     -7  525  238  126  188%
c i  146.3   70292   455122     65972   47147    648 114733  338   724  216  47%      1  459  243  131  185%
c i  146.8   70291   455122     66153   47218    648 114734  341   717  216  48%     -0  450  331  132  250%
c i  146.8   70290   455122     66154   47218    648 114734  341   717  216  48%     -0  450  329  132  249%
c i  147.5   70289   455122     66376   47366    651 114735  344   711  216  48%     -2  443  364  133  274%
c 
c [simplification-9] limit 66925 conflicts (hard 78763) hit after 67583 conflicts
c [quatres-4] found 30140 quaternary clauses 38% in total
c [ternres-5] limit 27614767 with penalty 0 = 0 + 0
c [ternres-5] all 70289 free variables schedulable
c [ternres-5] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-19] removed 245 variables
c [basicprobe-3] limit 138073837 penalty 0 = 0 + 0
c [basicprobe-3-0] 24254 probes remain 35% after last round
c [basicprobe-3-0] 475 units = 471 failed (99%) + 4 lifted (1%)
c [basicprobe-3-0] removed 1434 variables, found 229771 hbrs
c [bate-2] eliminated 267 asymmetric tautologies during probing
c [unhide-9] limit 345184 with penalty 4 = 0 + 4
c [unhide-9-9] 4 units, 87 failed, 6816 tauts, 0 hbrs, 2039454 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 169 transitive binary clauses
c [transred-5] found 1 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 68745 variables 100%
c [elim-7] limit of 276147675 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 1568 variables 2% in round 1 in 38971981 steps
c [elim-7-1] backward subsumption/strengthening limit 38971900
c [elim-7-1-1] backward checking 5454 touched variables 8%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 5 and strengthened 362 clauses in 2041455 steps
c [elim-7-1] rescheduled 702 variables 1% by backward subsumption
c [elim-7-2] eliminated 109 variables 0% in round 2 in 837976 steps
c [elim-7-2] backward subsumption/strengthening limit 837900
c [elim-7-2-1] backward checking 717 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 2 and strengthened 1 clauses in 392979 steps
c [elim-7-2] rescheduled 7 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 3542 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1677 = 2% variables out of 68745 scheduled
c [bca-5] limit of 10000000 steps and 870404 added (scaled 2)
c [bca-5] 109382 out of 134138 literals actually usable 82%
c [bca-5] added 53 blocked clauses in 328483 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 82844300 penalty 0 = 0 + 0
c [sweep-5-1] 3239 pos 4.9% + 62737 neg 95.1% = 65976 sched 98.4% ret 1092
c [sweep-5-1] 82990704 steps 1118 queries 391.18 avg class size
c [sweep-5-1] 13550 decisions 979 SAT calls 132.92 avg env size
c [sweep-5-1] 35204 variables remain 53% (31502 retained 47%)
c [decomp-20] removed 865 variables
c [sweep-5-1] removed 865 vars (0 failed, 151 eqs, 276 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 865 vars in TOTAL (1 rounds, 1117 queries)
c [phase-count-9] 426630 negative 98.9% of 431239 except 4609 1.1%
c [phase-count-9] 341812 positive 79.3% of 431239 except 89427 20.7%
c [phase-count-9] less non-negative clauses 4609 than limit 43100 (10.0%)
c [phase-count-9] non-pos/non-neg = 89427/4609 = 19.40 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 25 negative 100%
c [sort-queue-9] sorted 19168 enqueued variables after 67583 conflicts
c [score-dist-9] active 47035 (71%), one 0 (0%), zero 19168 (29%)
c [score-dist-9] max exp 510, different 244 (48%)
c [score-dist-9] median active exp 501, avg 468.2
c [simplification-9] removed 4086 variables 5.8% (66203 remain 35%)
c [simplification-9] removed 23883 irredundant clauses 5.2% (431239 remain 43%)
c [simplification-9] maximum reduction of 6% = max (6%, 5%)
c [simplification-9] large reduction 6% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 79583 (soft 69583 + delta 10000)
c [simplification-9] new conflict limit 69583 (hard 79583)
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  173.3   66202   431239     68199   22136    784 390788  304   626   85  48%      6  347  166  136  122%
c i  173.8   66201   431239     68809   22565    786 390796  276   580   85  48%      1  298   98  136   72%
c i  173.9   66200   431239     68855   22593    786 390803  274   577   85  48%      1  294  101  136   75%
c 
c [simplification-10] limit 69583 conflicts (hard 79583) hit after 69961 conflicts
c [ternres-6] limit 28292766 with penalty 0 = 0 + 0
c [ternres-6] all 66200 free variables schedulable
c [ternres-6] 58 ternary resolvents (0 bin, 58 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1768297 penalty 3 = 3 + 0
c [card-4] found 2716 at-most-one constraints of average size 3.9
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1768297 for elimination
c [card-4] 2716 out of 2716 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1414638 penalty 2 = 2 + 0
c [gauss-3] extracted 20 xors of average arity 2.9
c [gauss-3] connected 58 occurrences of 55 variables (average 1.1)
c [gauss-3] limit 1414638 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-21] removed 4 variables
c [simpleprobe-4] 14735 schedulable variables 22%
c [simpleprobe-4] limit 113171064 penalty 0 = 0 + 0
c [decomp-22] removed 767 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 767 variables, found 57878 hbrs, 375 units
c [unhide-10] limit 2829276 with penalty 1 = 0 + 1
c [unhide-10-10] 8 units, 281 failed, 45325 tauts, 0 hbrs, 107426 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 132 transitive binary clauses
c [transred-6] found 1 units
c [cce-3] limit of 35365957 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1139 (0%) of length 9
c [cce-3-1] eliminated 2 clauses out of 472 (0%) of length 8
c [cce-3-1] eliminated 27 clauses out of 744 (4%) of length 7
c [cce-3-1] eliminated 2795 clauses out of 4438 (63%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2825 large clauses in 35365961 steps
c [cce-3-1] allowing another 17682980 steps for small clauses
c [cce-3-1] scheduling 333869 clauses = 216138 binary + 117731 ternary
c [cce-3-1] tried to eliminate 488 small clauses 0%
c [cce-3-1] eliminated 88 binary clauses 0%
c [cce-3-1] eliminated 48 ternary clauses 0%
c [cce-3-1] eliminated 136 small clauses 0%
c [cce-3-1] eliminated 1788 small clauses in 35365957 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 4613 covered clauses in round 1
c [cce-3] eliminated 4613 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 65240 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 11317106420 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1946 variables 3% in round 1 in 41695590 steps
c [elim-8-1] backward subsumption/strengthening limit 41695500
c [elim-8-1-1] backward checking 6158 touched variables 9%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 31 and strengthened 388 clauses in 6903004 steps
c [elim-8-1] rescheduled 883 variables 1% by backward subsumption
c [elim-8-2] eliminated 129 variables 0% in round 2 in 3935586 steps
c [elim-8-2] backward subsumption/strengthening limit 3935500
c [elim-8-2-1] backward checking 947 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 1 and strengthened 2 clauses in 669027 steps
c [elim-8-2] rescheduled 8 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 4974 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 2075 = 3% variables out of 65240 scheduled
c [bca-6] limit of 10000000 steps and 828338 added (scaled 2)
c [bca-6] 106255 out of 126332 literals actually usable 84%
c [bca-6] added 176 blocked clauses in 310255 steps
c [sweep-6] limit 8487829 penalty 0 = 0 + 0
c [sweep-6-1] 2505 pos 7.4% + 31448 neg 92.6% = 33953 sched 53.8% ret 29212
c [sweep-6-1] 8506358 steps 147 queries 1554.21 avg class size
c [sweep-6-1] 1501 decisions 135 SAT calls 95.36 avg env size
c [sweep-6-1] 32836 variables remain 52% (30265 retained 48%)
c [decomp-23] removed 115 variables
c [sweep-6-1] removed 115 vars (0 failed, 11 eqs, 29 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 115 vars in TOTAL (1 rounds, 146 queries)
c [phase-count-10] 411796 negative 99.6% of 413427 except 1631 0.4%
c [phase-count-10] 325038 positive 78.6% of 413427 except 88389 21.4%
c [phase-count-10] less non-negative clauses 1631 than limit 41300 (10.0%)
c [phase-count-10] non-pos/non-neg = 88389/1631 = 54.19 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 25 negative 100%
c [sort-queue-10] sorted 16298 enqueued variables after 69961 conflicts
c [score-dist-10] active 46752 (74%), one 0 (0%), zero 16298 (26%)
c [score-dist-10] max exp 509, different 249 (49%)
c [score-dist-10] median active exp 495, avg 470.2
c [simplification-10] removed 3150 variables 4.8% (63050 remain 33%)
c [simplification-10] removed 17812 irredundant clauses 4.1% (413427 remain 41%)
c [simplification-10] maximum reduction of 5% = max (5%, 4%)
c [simplification-10] large reduction 5% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 81961 (soft 71961 + delta 10000)
c [simplification-10] new conflict limit 71961 (hard 81961)
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  183.7   63049   413427     70562   11279    829 387218  227   472   53  48%      5  184  144  136  107%
c i  183.7   63048   413427     70568   11283    829 387218  227   472   53  48%      5  183  147  136  108%
c i  183.7   63047   413427     70571   11285    829 387218  227   472   53  48%      5  183  147  136  108%
c i  183.7   63046   413427     70579   11291    829 387218  227   471   53  48%      5  183  151  136  111%
c i  183.9   63045   413427     70753   11404    830 387218  228   470   53  49%      3  181  197  136  145%
c i  184.0   63044   413427     70828   11466    830 387218  228   472   53  48%      2  183  194  136  143%
c i  184.1   63043   413427     70880   11504    831 387218  227   474   53  48%      1  184  185  136  136%
c i  185.2   63042   413427     71808   12309    838 387227  239   555   54  43%     -1  263  353  138  256%
c i  185.3   63041   413427     71922   12377    869 387230  241   558   54  43%     -2  265  342  138  247%
c i  185.4   63038   413427     71995   12419    870 387233  244   558   54  44%     -2  265  352  139  254%
c i  185.4   63037   413427     72005   12427    870 387233  244   558   54  44%     -2  265  357  139  258%
c i  185.4   63036   413427     72006   12427    870 387233  244   558   54  44%     -2  265  356  139  257%
c i  185.9   63035   413427     72327   12672    884 387269  234   564   54  42%     -4  269  207  138  150%
c i  186.2   63034   413427     72551   12840    884 387273  246   589   54  42%     -5  293  338  140  242%
c i  187.3   63033   413427     73259   13413    886 387280  267   636   59  42%     -4  337  370  142  260%
c i  187.3   63032   413427     73278   13429    886 387281  266   636   59  42%     -5  337  346  142  243%
c i  187.3   63031   413427     73279   13429    886 387281  266   635   59  42%     -5  336  344  142  242%
c i  187.3   63030   413427     73282   13431    886 387281  266   635   59  42%     -5  336  340  142  239%
c i  187.3   63029   413427     73287   13435    886 387281  265   635   59  42%     -5  336  334  142  235%
c i  187.3   63028   413427     73291   13438    886 387281  265   635   59  42%     -5  336  329  142  232%
c i  187.3   63027   413427     73297   13443    886 387281  265   635   59  42%     -5  336  322  142  226%
c i  187.4   63026   413427     73367   13489    888 387284  265   632   59  42%     -5  333  314  142  221%
c i  187.4   63025   413427     73369   13490    888 387284  265   632   59  42%     -5  333  312  142  220%
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  187.7   63024   413427     73551   13622    888 387286  265   624   59  42%     -6  324  277  143  195%
c i  187.7   63023   413427     73623   13676    889 387286  263   619   59  42%     -6  318  247  143  174%
c i  187.7   63022   413427     73625   13677    889 387286  263   619   59  42%     -6  318  246  143  172%
c i  187.8   63021   413427     73633   13679    889 387287  262   618   59  42%     -6  317  244  143  171%
c i  187.8   63020   413427     73648   13686    889 387288  262   617   59  43%     -6  316  240  143  168%
c i  188.0   63019   413427     73722   13716    889 387289  261   610   59  43%     -6  309  227  143  159%
c 
c [simplification-11] limit 72006 conflicts (hard 81961) hit after 75052 conflicts
c [quatres-5] found 29692 quaternary clauses 42% in total
c [quatres-5-2] added 8 quaternary resolvents
c [ternres-7] limit 30094394 with penalty 0 = 0 + 0
c [ternres-7] all 63019 free variables schedulable
c [ternres-7] 156 ternary resolvents (0 bin, 156 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-24] removed 32 variables
c [treelook-4] limit 3009439 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 101964 literals 81%
c [treelook-4] scheduling used 1716257 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 3009439 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 3090260 steps
c [treelook-4] 101833 literals remain 81%
c [treelook-4] 17333 variables remain to probed next time 28%
c [treelook-4] removed 16 variables, found 15119 hbrs
c [unhide-11] limit 3009439 with penalty 1 = 0 + 1
c [unhide-11-12] 12 units, 269 failed, 26140 tauts, 0 hbrs, 145665 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 145 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 62590 variables 100%
c [block-4] limit of 75235986 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 114 blocked clauses
c [block-4] 114 < 1/100 * 409258 = 4092 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 62588 variables 100%
c [elim-9] limit of 601887894 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 806 variables 1% in round 1 in 38897641 steps
c [elim-9-1] backward subsumption/strengthening limit 38897600
c [elim-9-1-1] backward checking 2976 touched variables 5%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 4 and strengthened 167 clauses in 1175686 steps
c [elim-9-1] rescheduled 354 variables 1% by backward subsumption
c [elim-9-2] eliminated 55 variables 0% in round 2 in 481779 steps
c [elim-9-2] backward subsumption/strengthening limit 481700
c [elim-9-2-1] backward checking 385 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 2 clauses in 231288 steps
c [elim-9-2] rescheduled 8 variables 0% by backward subsumption
c [elim-9-3] eliminated 1 variables 0% in round 3 in 9623 steps
c [elim-9-3] backward subsumption/strengthening limit 9600
c [elim-9-3-1] backward checking 10 touched variables 0%
c [elim-9-3-1] incomplete backward checking 1 remain 10%
c [elim-9-3] subsumed 0 and strengthened 2 clauses in 9610 steps
c [elim-9] incomplete 8 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 867 = 1% variables out of 62588 scheduled
c [bca-7] limit of 10000000 steps and 809040 added (scaled 2)
c [bca-7] 101043 out of 123444 literals actually usable 82%
c [bca-7] added 55 blocked clauses in 287542 steps
c [sweep-7] limit 9028318 penalty 0 = 0 + 0
c [sweep-7-1] 2248 pos 7.0% + 30068 neg 93.0% = 32316 sched 52.4% ret 29405
c [sweep-7-1] 9081859 steps 120 queries 1670.92 avg class size
c [sweep-7-1] 1565 decisions 108 SAT calls 98.37 avg env size
c [sweep-7-1] 31515 variables remain 51% (30102 retained 49%)
c [decomp-26] removed 170 variables
c [sweep-7-1] removed 170 vars (0 failed, 12 eqs, 25 impls)
c [sweep-7] removed 170 vars in TOTAL (1 rounds, 119 queries)
c [phase-count-11] 401792 negative 99.6% of 403364 except 1572 0.4%
c [phase-count-11] 317327 positive 78.7% of 403364 except 86037 21.3%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 6 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 15303 enqueued variables after 75052 conflicts
c [score-dist-11] active 46248 (75%), one 0 (0%), zero 15303 (25%)
c [score-dist-11] max exp 509, different 262 (51%)
c [score-dist-11] median active exp 496, avg 470.6
c [simplification-11] removed 1468 variables 2.3% (61551 remain 32%)
c [simplification-11] removed 10063 irredundant clauses 2.4% (403364 remain 40%)
c [simplification-11] maximum reduction of 2% = max (2%, 2%)
c [simplification-11] geometric conflict interval increment 8000 = 24000 / 3
c [simplification-11] new conflict interval 32000
c [simplification-11] penalized conflict interval 32000 = 1 * 32000
c [simplification-11] hard conflict limit 123052 (soft 107052 + delta 16000)
c [simplification-11] new conflict limit 107052 (hard 123052)
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  202.4   61550   403364     81517   18971    971 377293   92   194   72  47%     91 -112   54  134   40%
c i  202.5   61549   403364     81537   18987    971 377293   92   195   72  47%     89 -111   59  134   44%
c i  203.4   61548   403364     82580   19743    976 377304  110   237   72  47%     28  -68  204  135  151%
c i  203.7   61547   403364     82793   19889    977 377305  115   249   72  46%     20  -56  213  135  157%
c i  205.4   61546   403364     83960   20619    981 377316  151   302   76  50%      3   -3  215  137  156%
c i  206.3   61542   403364     84755   21093    983 377323  146   289   79  51%     -3  -15  133  137   97%
c i  206.4   61541   403364     84866   21187    983 377323  144   287   79  50%     -4  -17  111  137   81%
c i  206.4   61540   403364     84910   21222    983 377324  144   287   79  50%     -5  -17  116  137   85%
c i  206.5   61539   403364     84987   21272    983 377324  144   287   79  50%     -6  -17  131  137   96%
c i  206.6   61538   403364     85100   21340    984 377324  144   286   79  50%     -7  -18  135  137   98%
c i  206.6   61537   403364     85165   21380    996 377327  143   285   79  50%     -7  -19  118  137   86%
c i  206.6   61536   403364     85166   21380    996 377327  143   285   79  50%     -7  -19  117  137   86%
c i  206.6   61535   403364     85167   21380    996 377327  143   285   79  50%     -7  -19  117  137   85%
c i  206.7   61534   403364     85172   21384    996 377327  143   285   79  50%     -7  -19  117  137   86%
c i  206.7   61533   403364     85177   21387    996 377327  143   285   79  50%     -7  -19  117  137   85%
c i  206.7   61532   403364     85199   21399    996 377327  143   284   79  50%     -7  -20  118  137   86%
c i  206.8   61531   403364     85250   21427    996 377327  143   283   79  50%     -8  -21  123  137   90%
c i  207.2   61530   403364     85596   21622   1004 377335  142   278   79  51%     -9  -26  136  137   99%
c i  207.2   61529   403364     85597   21622   1004 377335  142   278   79  51%     -9  -26  135  137   99%
c i  207.3   61528   403364     85685   21685   1004 377335  142   277   79  51%    -10  -27  139  137  102%
c i  207.6   61527   403364     85944   21837   1004 377336  143   275   79  52%    -10  -29  150  137  109%
c i  208.2   61526   403364     86521   22161   1007 377337  139   263   79  53%    -10  -40  123  137   90%
c i  208.2   61525   403364     86523   22162   1007 377337  139   263   79  53%    -10  -41  122  137   89%
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  208.4   61524   403364     86625   22219   1007 377337  139   261   79  53%    -11  -43  124  137   90%
c i  208.4   61523   403364     86629   22220   1007 377337  139   261   79  53%    -11  -43  124  137   90%
c i  209.8   61522   403364     87833   22922   1012 377343  130   233   79  56%     -6  -69   94  136   69%
c i  212.3   61521   403364     90107   24282   1031 377357  113   189   79  60%      7 -110   90  135   67%
c i  212.4   61520   403364     90138   24298   1031 377357  112   188   79  60%      6 -111   90  135   67%
c i  213.0   61519   403364     90633   24641   1033 377358  110   187   83  59%     -0 -112   98  134   73%
c i  213.0   61518   403364     90634   24641   1033 377358  110   187   83  59%     -0 -112   98  134   73%
c i  213.0   61517   403364     90636   24642   1033 377358  110   187   83  59%     -0 -112   98  134   73%
c i  213.0   61516   403364     90638   24643   1033 377358  110   187   83  59%     -0 -112   98  134   73%
c i  213.1   61515   403364     90651   24650   1032 377359  111   187   83  59%     -1 -111  103  134   77%
c i  213.1   61514   403364     90654   24651   1033 377359  111   187   83  59%     -1 -111  103  134   77%
c i  213.2   61513   403364     90781   24730   1033 377359  111   189   83  59%     -2 -109  112  134   83%
c i  213.4   61512   403364     90940   24852   1033 377360  111   193   83  57%     -4 -105  106  134   79%
c i  213.7   61511   403364     91206   25057   1034 377362  110   196   83  56%     -6 -101  108  134   80%
c i  213.7   61510   403364     91218   25065   1036 377363  110   197   83  56%     -6 -101  104  134   77%
c i  213.7   61509   403364     91231   25076   1036 377363  110   197   83  56%     -6 -100  105  134   79%
c i  214.6   61508   403364     92000   25576   1036 377365  113   203   83  55%     -7  -93  128  134   95%
c i  214.7   61507   403364     92028   25590   1036 377366  113   203   83  56%     -7  -93  129  134   96%
c i  215.6   61506   403364     92732   25979   1036 377373  117   207   83  57%     -8  -88  146  134  109%
c i  217.2   61505   403364     93631   26357   1036 377374  121   202   83  60%     -7  -92  127  134   95%
c i  217.3   61504   403364     93735   26410   1036 377374  121   201   83  60%     -8  -93  124  134   92%
c i  218.5   61503   403364     94510   26779   1040 377387  126   204   83  62%     -8  -88  155  134  115%
c i  218.9   61502   403364     94845   26976   1041 377394  129   212   87  61%     -9  -80  167  134  124%
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  221.4   61499   403364     96798   28639   1044 377401  110   182   98  60%      3 -107   53  133   40%
c i  221.8   61498   403364     97264   29049   1044 377401  103   175   98  59%     -2 -114   50  132   38%
c i  224.4   61497   403364     99743   30903   1050 377406   94   148  107  63%     11 -136   73  130   56%
c i  224.8   61496   403364    100129   31143   1050 377406   94   148  107  64%      4 -135   88  130   68%
c i  230.0   61492   403364    104571   34767   1057 377421   89   150  119  60%     39 -124  165  127  130%
c i  230.0   61491   403364    104572   34767   1057 377421   89   150  119  60%     38 -124  165  127  129%
c i  232.2   61490   403364    105766   35261   1062 377426  119   179  119  67%      9  -93  204  129  158%
c i  235.8   61489   403364    107531   36130   1068 377428  130   192  119  68%      3  -78  131  129  101%
c i  235.8   61488   403364    107551   36135   1068 377428  130   192  119  68%      3  -78  134  129  104%
c i  236.4   61469   403364    107876   36306   1068 377429  131   194  119  68%     -2  -76  142  129  110%
c i  241.0   61468   403364    110430   37511   1080 377438  162   235  121  69%     11  -32  231  132  176%
c i  241.2   61467   403364    110501   37550   1080 377438  161   234  121  69%      9  -33  211  132  160%
c i  242.3   61466   403364    111339   38130   1082 377443  148   221  121  67%     -1  -46   90  131   69%
c i  242.6   61465   403364    111514   38172   1082 377443  150   222  121  68%     -3  -45  149  131  114%
c i  243.3   61464   403364    111917   38447   1086 377443  150   227  121  66%     -6  -39  158  131  120%
c i  249.7   61463   403364    115851   40601   1088 377447  118   181  122  65%     30  -82   75  130   58%
c i  250.3   61462   403364    116328   41053   1090 377449  110   169  122  65%     14  -93   44  129   34%
c i  253.4   61461   403364    118404   42869   1090 377456   88   136  127  65%      6 -123   58  127   46%
c i  258.7   61459   403364    121618   45338   1097 377462   86   139  134  62%     19 -113  107  124   86%
c i  259.1   61458   403364    121921   45567   1098 377465   99   176  134  56%     11  -76  234  125  187%
c i  259.7   61455   403364    122281   45757   1098 377470  117   200  136  59%      3  -52  290  126  230%
c i  259.7   61454   403364    122285   45760   1098 377470  117   200  136  59%      3  -52  289  126  229%
c i  259.8   61453   403364    122343   45776   1098 377471  120   202  136  59%      2  -49  287  126  227%
c 
c [simplification-12] limit 107128 conflicts (hard 123052) hit after 123055 conflicts
c [quatres-6] found 29869 quaternary clauses 43% in total
c [quatres-6-2] added 2 single-self-subsuming ternary resolvents
c [quatres-6-2] added 7 quaternary resolvents
c [ternres-8] limit 46074148 with penalty 0 = 0 + 0
c [ternres-8] all 61453 free variables schedulable
c [ternres-8] 158 ternary resolvents (0 bin, 158 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-27] removed 102 variables
c [basicprobe-4] limit 230370742 penalty 0 = 0 + 0
c [basicprobe-4-0] 16219 probes remain 27% after last round
c [basicprobe-4-0] 794 units = 780 failed (98%) + 14 lifted (2%)
c [basicprobe-4-0] removed 1241 variables, found 361505 hbrs
c [bate-3] eliminated 541 asymmetric tautologies during probing
c [unhide-12] limit 1151853 with penalty 3 = 0 + 3
c [unhide-12-13] 6 units, 215 failed, 47151 tauts, 0 hbrs, 1082282 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 115 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 1151853710 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 8 clauses out of 652 (1%) of length 7
c [cce-4-1] eliminated 52 clauses out of 1827 (3%) of length 6
c [cce-4-1] eliminated 20822 clauses out of 30118 (69%) of length 5
c [cce-4-1] eliminated 17666 clauses out of 29669 (60%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 38548 large clauses in 614948780 steps
c [cce-4-1] allowing another 307474390 steps for small clauses
c [cce-4-1] scheduling 217947 clauses = 200872 binary + 17075 ternary
c [cce-4-1] tried to eliminate 49818 small clauses 23%
c [cce-4-1] eliminated 11115 binary clauses 6%
c [cce-4-1] eliminated 1787 ternary clauses 10%
c [cce-4-1] eliminated 12902 small clauses 6%
c [cce-4-1] eliminated 14629 small clauses in 1151853717 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 53177 covered clauses in round 1
c [cce-4] eliminated 53177 covered clauses in TOTAL during 1 rounds
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 60039 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 15956 variables 27% in round 1 in 28939304 steps
c [elim-10-1] backward subsumption/strengthening limit 28939300
c [elim-10-1-1] backward checking 33683 touched variables 56%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 18 and strengthened 37 clauses in 4649858 steps
c [elim-10-1] rescheduled 117 variables 0% by backward subsumption
c [elim-10-2] eliminated 5 variables 0% in round 2 in 83413 steps
c [elim-10-2] backward subsumption/strengthening limit 83400
c [elim-10-2-1] backward checking 46 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 0 and strengthened 4 clauses in 83401 steps
c [elim-10-2] rescheduled 13 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 12199 steps
c [elim-10-3] backward subsumption/strengthening limit 12100
c [elim-10-3-1] backward checking 10 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 0 and strengthened 2 clauses in 12101 steps
c [elim-10] incomplete 8 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 15963 = 27% variables out of 60039 scheduled
c [bca-8] limit of 10000000 steps and 615364 added (scaled 2)
c [bca-8] 80852 out of 88154 literals actually usable 92%
c [bca-8] added 206 blocked clauses in 192945 steps
c [sweep-8] limit 13822244 penalty 0 = 0 + 0
c [sweep-8-1] 2385 pos 9.0% + 24082 neg 91.0% = 26467 sched 60.0% ret 17609
c [sweep-8-1] 13832763 steps 266 queries 996.36 avg class size
c [sweep-8-1] 3586 decisions 248 SAT calls 104.50 avg env size
c [sweep-8-1] 24323 variables remain 55% (19687 retained 45%)
c [decomp-28] removed 214 variables
c [sweep-8-1] removed 214 vars (0 failed, 21 eqs, 51 impls)
c [sweep-8] removed 214 vars in TOTAL (1 rounds, 265 queries)
c [phase-count-12] 306024 negative 99.8% of 306570 except 546 0.2%
c [phase-count-12] 230559 positive 75.2% of 306570 except 76011 24.8%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-12] sorted 10547 enqueued variables after 123055 conflicts
c [score-dist-12] active 33315 (76%), one 0 (0%), zero 10547 (24%)
c [score-dist-12] max exp 510, different 410 (80%)
c [score-dist-12] median active exp 502, avg 459.0
c [simplification-12] removed 17591 variables 28.6% (43862 remain 23%)
c [simplification-12] removed 96794 irredundant clauses 24.0% (306570 remain 30%)
c [simplification-12] maximum reduction of 29% = max (29%, 24%)
c [simplification-12] large reduction 29% >= 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 135055 (soft 125055 + delta 10000)
c [simplification-12] new conflict limit 125055 (hard 135055)
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  310.4   43861   306570    123101    3164   2873 560596  148   232   40  64%     -4  -19  245  128  191%
c 
c [simplification-13] limit 125055 conflicts (hard 135055) hit after 125055 conflicts
c [quatres-7] found 21095 quaternary clauses 55% in total
c [quatres-7-2] added 13 quaternary resolvents
c [ternres-9] limit 46571532 with penalty 0 = 0 + 0
c [ternres-9] all 43858 free variables schedulable
c [ternres-9] 439 ternary resolvents (0 bin, 439 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-29] removed 4 variables
c [simpleprobe-5] all 43858 free variables schedulable
c [simpleprobe-5] limit 186286128 penalty 0 = 0 + 0
c [decomp-30] removed 310 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 310 variables, found 105506 hbrs, 188 units
c [unhide-13] limit 9314306 with penalty 0 = 0 + 0
c [unhide-13-18] 3 units, 205 failed, 66704 tauts, 0 hbrs, 20260 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 128 transitive binary clauses
c [cce-5] limit of 232857661 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 4 clauses out of 86 (5%) of length 7
c [cce-5-1] eliminated 194 clauses out of 2957 (7%) of length 6
c [cce-5-1] eliminated 1968 clauses out of 12449 (16%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 2166 large clauses in 232857672 steps
c [cce-5-1] allowing another 116428836 steps for small clauses
c [cce-5-1] scheduling 246139 clauses = 139379 binary + 106760 ternary
c [cce-5-1] tried to eliminate 4952 small clauses 2%
c [cce-5-1] eliminated 764 binary clauses 1%
c [cce-5-1] eliminated 269 ternary clauses 0%
c [cce-5-1] eliminated 1033 small clauses 0%
c [cce-5-1] eliminated 1037 small clauses in 232857668 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 3203 covered clauses in round 1
c [cce-5] eliminated 3203 covered clauses in TOTAL during 1 rounds
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 43370 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 432 variables 1% in round 1 in 24671317 steps
c [elim-11-1] backward subsumption/strengthening limit 24671300
c [elim-11-1-1] backward checking 2760 touched variables 6%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 4 and strengthened 3 clauses in 729415 steps
c [elim-11-1] rescheduled 23 variables 0% by backward subsumption
c [elim-11-2] eliminated 2 variables 0% in round 2 in 11600 steps
c [elim-11-2] backward subsumption/strengthening limit 11600
c [elim-11-2-1] backward checking 26 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 2 and strengthened 0 clauses in 11601 steps
c [elim-11-2] rescheduled 6 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 5441 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 434 = 1% variables out of 43370 scheduled
c [bca-9] limit of 10000000 steps and 588871 added (scaled 2)
c [bca-9] 75615 out of 85874 literals actually usable 88%
c [bca-9] added 323 blocked clauses in 179652 steps
c [sweep-9] limit 13971459 penalty 0 = 0 + 0
c [sweep-9-1] 2323 pos 9.8% + 21444 neg 90.2% = 23767 sched 55.4% ret 19169
c [sweep-9-1] 13975257 steps 353 queries 790.37 avg class size
c [sweep-9-1] 3971 decisions 320 SAT calls 91.46 avg env size
c [sweep-9-1] 21399 variables remain 50% (21291 retained 50%)
c [decomp-31] removed 383 variables
c [sweep-9-1] removed 383 vars (0 failed, 36 eqs, 60 impls)
c [sweep-9] removed 383 vars in TOTAL (1 rounds, 352 queries)
c [phase-count-13] 292024 negative 99.8% of 292547 except 523 0.2%
c [phase-count-13] 220160 positive 75.3% of 292547 except 72387 24.7%
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 9699 enqueued variables after 125055 conflicts
c [score-dist-13] active 32854 (77%), one 0 (0%), zero 9699 (23%)
c [score-dist-13] max exp 509, different 407 (80%)
c [score-dist-13] median active exp 499, avg 468.8
c [simplification-13] removed 1305 variables 3.0% (42553 remain 22%)
c [simplification-13] removed 14023 irredundant clauses 4.6% (292547 remain 29%)
c [simplification-13] maximum reduction of 5% = max (3%, 5%)
c [simplification-13] large reduction 5% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 137055 (soft 127055 + delta 10000)
c [simplification-13] new conflict limit 127055 (hard 137055)
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  326.0   42552   292547    126826    5459   3107 591037  142   249   45  57%     26   -2  111  129   87%
c 
c [simplification-14] limit 127055 conflicts (hard 137055) hit after 127545 conflicts
c [quatres-8] found 20162 quaternary clauses 58% in total
c [quatres-8-2] added 2 single-self-subsuming ternary resolvents
c [quatres-8-2] added 6 quaternary resolvents
c [ternres-10] limit 47182354 with penalty 0 = 0 + 0
c [ternres-10] all 42552 free variables schedulable
c [ternres-10] 564 ternary resolvents (0 bin, 564 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1179558 penalty 3 = 3 + 0
c [gauss-4] extracted 11 xors of average arity 3.0
c [gauss-4] connected 33 occurrences of 33 variables (average 1.0)
c [gauss-4] limit 1179558 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-5] limit 4718235 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 61790 literals 73%
c [treelook-5] scheduling used 1454015 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 4718235 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 4749083 steps
c [treelook-5] 61625 literals remain 72%
c [treelook-5] 8413 variables remain to probed next time 20%
c [decomp-33] removed 1 variables
c [treelook-5] removed 5 variables, found 22961 hbrs
c [unhide-14] limit 9436470 with penalty 0 = 0 + 0
c [unhide-14-23] 7 units, 104 failed, 31750 tauts, 0 hbrs, 19401 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 94 transitive binary clauses
c [cce-6] limit of 235911772 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 2 clauses out of 84 (2%) of length 7
c [cce-6-1] eliminated 3 clauses out of 2763 (0%) of length 6
c [cce-6-1] eliminated 16 clauses out of 10313 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 21 large clauses in 235911774 steps
c [cce-6-1] allowing another 117955887 steps for small clauses
c [cce-6-1] scheduling 152674 clauses = 136386 binary + 16288 ternary
c [cce-6-1] tried to eliminate 7760 small clauses 5%
c [cce-6-1] eliminated 1390 binary clauses 1%
c [cce-6-1] eliminated 193 ternary clauses 1%
c [cce-6-1] eliminated 1583 small clauses 1%
c [cce-6-1] eliminated 1620 small clauses in 235911782 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1641 covered clauses in round 1
c [cce-6] eliminated 1641 covered clauses in TOTAL during 1 rounds
c [cce-6] 1641 < 1/100 * 290634 = 2906 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 42457 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 302 variables 1% in round 1 in 25013503 steps
c [elim-12-1] backward subsumption/strengthening limit 25013500
c [elim-12-1-1] backward checking 1908 touched variables 4%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 11 and strengthened 4 clauses in 572714 steps
c [elim-12-1] rescheduled 25 variables 0% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 151218 steps
c [elim-12-2] backward subsumption/strengthening limit 151200
c [elim-12-2-1] backward checking 3 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 0 clauses in 37583 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 303 = 1% variables out of 42457 scheduled
c [elim-12] 303 < 1/100 * 42457 = 424 considered unsuccessful
c [bca-10] limit of 10000000 steps and 577546 added (scaled 2)
c [bca-10] 72909 out of 84310 literals actually usable 86%
c [bca-10] added 86 blocked clauses in 173834 steps
c [sweep-10] limit 14154706 penalty 0 = 0 + 0
c [sweep-10-1] 1941 pos 9.2% + 19127 neg 90.8% = 21068 sched 50.0% ret 21086
c [sweep-10-1] 14211549 steps 339 queries 765.74 avg class size
c [sweep-10-1] 3604 decisions 314 SAT calls 90.23 avg env size
c [sweep-10-1] 19388 variables remain 46% (22747 retained 54%)
c [decomp-34] removed 145 variables
c [sweep-10-1] removed 145 vars (0 failed, 29 eqs, 52 impls)
c [sweep-10] removed 145 vars in TOTAL (1 rounds, 338 queries)
c [phase-count-14] 287489 negative 99.8% of 287966 except 477 0.2%
c [phase-count-14] 217150 positive 75.4% of 287966 except 70816 24.6%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 9407 enqueued variables after 127545 conflicts
c [score-dist-14] active 32602 (78%), one 0 (0%), zero 9407 (22%)
c [score-dist-14] max exp 509, different 412 (81%)
c [score-dist-14] median active exp 499, avg 470.3
c [simplification-14] removed 543 variables 1.3% (42009 remain 22%)
c [simplification-14] removed 4581 irredundant clauses 1.6% (287966 remain 29%)
c [simplification-14] maximum reduction of 2% = max (1%, 2%)
c [simplification-14] geometric conflict interval increment 10666 = 32000 / 3
c [simplification-14] new conflict interval 42666
c [simplification-14] penalized conflict interval 42666 = 1 * 42666
c [simplification-14] hard conflict limit 191544 (soft 170211 + delta 21333)
c [simplification-14] new conflict limit 170211 (hard 191544)
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  337.9   42008   287966    127600    6056   3559 585558  135   252   44  53%      7    1   98  128   76%
c i  339.3   42007   287966    129524    7552   3574 585574  148   326   46  45%      3   74  185  129  143%
c i  370.4   42006   287966    170615   39781   3784 585750   61   103  101  59%    459 -113  169  107  158%
c i  374.8   41986   287966    175558   42844   3843 585793  124   222  114  56%   -100    9  111  110  100%
c 
c [simplification-15] limit 170211 conflicts (hard 191544) hit after 186346 conflicts
c [quatres-9] found 20282 quaternary clauses 55% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [ternres-11] limit 61198111 with penalty 0 = 0 + 0
c [ternres-11] all 41929 free variables schedulable
c [ternres-11] 182 ternary resolvents (0 bin, 182 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1912440 penalty 4 = 4 + 0
c [card-5] found 1573 at-most-one constraints of average size 3.9
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1912440 for elimination
c [card-5] 1573 out of 1573 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 80 variables
c [basicprobe-5] limit 305990559 penalty 0 = 0 + 0
c [basicprobe-5-0] 1589 probes remain 4% after last round
c [basicprobe-5-0] 917 units = 863 failed (94%) + 54 lifted (6%)
c [basicprobe-5-0] removed 1132 variables, found 532884 hbrs
c [bate-4] eliminated 1787 asymmetric tautologies during probing
c [unhide-15] limit 3059905 with penalty 2 = 0 + 2
c [unhide-15-25] 1 units, 8 failed, 78263 tauts, 0 hbrs, 671534 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 140 transitive binary clauses
c [transred-11] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 40782 variables 100%
c [block-5] limit of 76497639 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 305 blocked clauses
c [block-5] 305 < 1/100 * 273408 = 2734 considered unsuccessful
c [bca-11] limit of 10000000 steps and 547197 added (scaled 2)
c [bca-11] 62619 out of 81566 literals actually usable 77%
c [bca-11] added 35 blocked clauses in 190225 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 183594330 penalty 0 = 0 + 0
c [sweep-11-1] 1732 pos 9.2% + 17153 neg 90.8% = 18885 sched 46.3% ret 21897
c [sweep-11-1] 183647810 steps 4255 queries 69.65 avg class size
c [sweep-11-1] 33554 decisions 3755 SAT calls 101.82 avg env size
c [sweep-11-1] 2281 variables remain 6% (37619 retained 94%)
c [decomp-36] removed 1874 variables
c [sweep-11-1] removed 1874 vars (0 failed, 514 eqs, 945 impls)
c [sweep-11] removed 1874 vars in TOTAL (1 rounds, 4254 queries)
c [phase-count-15] 265835 negative 99.8% of 266311 except 476 0.2%
c [phase-count-15] 200210 positive 75.2% of 266311 except 66101 24.8%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 8222 enqueued variables after 186346 conflicts
c [score-dist-15] active 30686 (79%), one 343 (1%), zero 7879 (20%)
c [score-dist-15] max exp 510, different 417 (82%)
c [score-dist-15] median active exp 503, avg 473.9
c [simplification-15] removed 3021 variables 7.2% (38908 remain 21%)
c [simplification-15] removed 21655 irredundant clauses 7.5% (266311 remain 26%)
c [simplification-15] maximum reduction of 8% = max (7%, 8%)
c [simplification-15] large reduction 8% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 198346 (soft 188346 + delta 10000)
c [simplification-15] new conflict limit 188346 (hard 198346)
c 
c [simplification-16] limit 188346 conflicts (hard 198346) hit after 188346 conflicts
c [ternres-12] limit 61809540 with penalty 0 = 0 + 0
c [ternres-12] all 38908 free variables schedulable
c [ternres-12] 1267 ternary resolvents (0 bin, 1267 trn)
c [ternres-12] fully completed ternary resolution
c [simpleprobe-6] all 38908 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-38] removed 155 variables
c [simpleprobe-6] 3414 variables remain 9% (35339 retained 91%)
c [simpleprobe-6] removed 155 variables, found 176893 hbrs, 87 units
c [unhide-16] limit 3090477 with penalty 2 = 0 + 2
c [unhide-16-26] 2 units, 11 failed, 135419 tauts, 0 hbrs, 143268 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 319 transitive binary clauses
c [cce-7] limit of 154523852 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 17
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 16
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 15
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 14
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 13
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 12
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 11
c [cce-7-1] eliminated 8 clauses out of 11 (73%) of length 10
c [cce-7-1] eliminated 10 clauses out of 15 (67%) of length 9
c [cce-7-1] eliminated 8 clauses out of 16 (50%) of length 8
c [cce-7-1] eliminated 12 clauses out of 97 (12%) of length 7
c [cce-7-1] eliminated 15 clauses out of 2719 (1%) of length 6
c [cce-7-1] eliminated 40 clauses out of 8404 (0%) of length 5
c [cce-7-1] eliminated 6 clauses out of 16354 (0%) of length 4
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 119 large clauses in 154523853 steps
c [cce-7-1] allowing another 77261926 steps for small clauses
c [cce-7-1] scheduling 221681 clauses = 130998 binary + 90683 ternary
c [cce-7-1] tried to eliminate 3958 small clauses 2%
c [cce-7-1] eliminated 605 binary clauses 0%
c [cce-7-1] eliminated 117 ternary clauses 0%
c [cce-7-1] eliminated 722 small clauses 0%
c [cce-7-1] eliminated 918 small clauses in 154523854 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1037 covered clauses in round 1
c [cce-7] eliminated 1037 covered clauses in TOTAL during 1 rounds
c [cce-7] 1037 < 1/100 * 264941 = 2649 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 38734 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 629 variables 2% in round 1 in 23149041 steps
c [elim-13-1] backward subsumption/strengthening limit 23149000
c [elim-13-1-1] backward checking 3601 touched variables 9%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 5 and strengthened 14 clauses in 938591 steps
c [elim-13-1] rescheduled 50 variables 0% by backward subsumption
c [elim-13-2] eliminated 4 variables 0% in round 2 in 26054 steps
c [elim-13-2] backward subsumption/strengthening limit 26000
c [elim-13-2-1] backward checking 40 touched variables 0%
c [elim-13-2-1] incomplete backward checking 0 remain 0%
c [elim-13-2] subsumed 5 and strengthened 0 clauses in 26001 steps
c [elim-13-2] rescheduled 7 variables 0% by backward subsumption
c [elim-13-3] eliminated 3 variables 0% in round 3 in 6014 steps
c [elim-13-3] backward subsumption/strengthening limit 6000
c [elim-13-3-1] backward checking 18 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 4 and strengthened 0 clauses in 6001 steps
c [elim-13] incomplete 6 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 636 = 2% variables out of 38734 scheduled
c [bca-12] limit of 10000000 steps and 525579 added (scaled 2)
c [bca-12] 56029 out of 76198 literals actually usable 74%
c [bca-12] added 48 blocked clauses in 164579 steps
c [sweep-12] limit 18542862 penalty 0 = 0 + 0
c [sweep-12-1] 93 pos 5.5% + 1601 neg 94.5% = 1694 sched 4.4% ret 36404
c [sweep-12-1] 18595601 steps 704 queries 35.99 avg class size
c [sweep-12-1] 4741 decisions 588 SAT calls 63.70 avg env size
c [sweep-12-1] 626 variables remain 2% (37423 retained 98%)
c [decomp-39] removed 295 variables
c [sweep-12-1] removed 295 vars (0 failed, 121 eqs, 212 impls)
c [sweep-12] removed 295 vars in TOTAL (1 rounds, 703 queries)
c [phase-count-16] 260758 negative 99.8% of 261212 except 454 0.2%
c [phase-count-16] 196383 positive 75.2% of 261212 except 64829 24.8%
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 7951 enqueued variables after 188346 conflicts
c [score-dist-16] active 29852 (79%), one 341 (1%), zero 7610 (20%)
c [score-dist-16] max exp 510, different 414 (81%)
c [score-dist-16] median active exp 496, avg 473.2
c [simplification-16] removed 1105 variables 2.8% (37803 remain 20%)
c [simplification-16] removed 5099 irredundant clauses 1.9% (261212 remain 26%)
c [simplification-16] maximum reduction of 3% = max (3%, 2%)
c [simplification-16] geometric conflict interval increment 10666 = 42666 / 4
c [simplification-16] new conflict interval 53332
c [simplification-16] penalized conflict interval 53332 = 1 * 53332
c [simplification-16] hard conflict limit 268344 (soft 241678 + delta 26666)
c [simplification-16] new conflict limit 241678 (hard 268344)
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  429.4   37802   261212    191110   43986   5197 936851  145   240  112  61%     72    5   98  126   78%
c i  434.6   37801   261212    196986   48376   5218 936902  215   418  117  51%    -71  177  172  134  129%
c i  434.9   37789   261212    197443   48711   5221 936903  205   402  117  51%    -97  161  101  133   76%
c i  438.1   37785   261212    201046   51355   5229 936916  231   434  127  53%    -99  184  263  139  189%
c i  442.8   37783   261212    205539   54205   5250 936927  283   520  127  54%    -79  258  278  149  186%
c i  442.8   37779   261212    205540   54205   5250 936927  283   520  127  54%    -79  258  277  149  186%
c -  444.3   37779   261212    207114   25565   5257 936931  235   455   59  52%   -108  186  106  149   71%
c i  447.0   37778   261212    210157   27790   5261 936936  157   295   72  53%    -70   22   96  146   66%
c 
c [simplification-17] limit 241688 conflicts (hard 268344) hit after 241688 conflicts
c [quatres-10] found 17158 quaternary clauses 51% in total
c [quatres-10-1] removed 4 duplicate quaternary clauses
c [quatres-10-2] added 2 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1 quaternary resolvents
c [ternres-13] limit 77001232 with penalty 0 = 0 + 0
c [ternres-13] all 37776 free variables schedulable
c [ternres-13] 441 ternary resolvents (0 bin, 441 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-40] removed 27 variables
c [treelook-6] limit 7700123 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 55697 literals 74%
c [treelook-6] scheduling used 1770066 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 7700123 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 7780096 steps
c [treelook-6] 55553 literals remain 74%
c [treelook-6] 7248 variables remain to probed next time 19%
c [decomp-41] removed 2 variables
c [treelook-6] removed 6 variables, found 43703 hbrs
c [unhide-17] limit 3850061 with penalty 2 = 0 + 2
c [unhide-17-28] 1 units, 14 failed, 60590 tauts, 0 hbrs, 1448783 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 270 transitive binary clauses
c [transred-13] found 1 units
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 37758 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 306 variables 1% in round 1 in 25193307 steps
c [elim-14-1] backward subsumption/strengthening limit 25193300
c [elim-14-1-1] backward checking 1420 touched variables 4%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 3 clauses in 503174 steps
c [elim-14-1] rescheduled 11 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 3197 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 306 = 1% variables out of 37758 scheduled
c [elim-14] 306 < 1/100 * 37758 = 377 considered unsuccessful
c [bca-13] limit of 10000000 steps and 519117 added (scaled 2)
c [bca-13] 54462 out of 74906 literals actually usable 73%
c [bca-13] added 29 blocked clauses in 161980 steps
c [sweep-13] limit 23100369 penalty 0 = 0 + 0
c [sweep-13-1] 28 pos 5.9% + 444 neg 94.1% = 472 sched 1.3% ret 36980
c [sweep-13-1] 9271269 steps 377 queries 14.49 avg class size
c [sweep-13-1] 2883 decisions 314 SAT calls 65.92 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-42] removed 67 variables
c [sweep-13-1] removed 67 vars (0 failed, 62 eqs, 122 impls)
c [sweep-13-2] 3091 pos 8.3% + 34294 neg 91.7% = 37385 sched 100.0% ret 0
c [sweep-13-2] 14058217 steps 218 queries 1270.86 avg class size
c [sweep-13-2] 6083 decisions 208 SAT calls 260.22 avg env size
c [sweep-13-2] 30422 variables remain 82% (6788 retained 18%)
c [decomp-43] removed 187 variables
c [sweep-13-2] removed 187 vars (0 failed, 12 eqs, 27 impls)
c [sweep-13] removed 254 vars in TOTAL (2 rounds, 593 queries)
c [phase-count-17] 255859 negative 99.8% of 256285 except 426 0.2%
c [phase-count-17] 191100 positive 74.6% of 256285 except 65185 25.4%
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 7839 enqueued variables after 241688 conflicts
c [score-dist-17] active 29359 (79%), one 617 (2%), zero 7222 (19%)
c [score-dist-17] max exp 509, different 438 (86%)
c [score-dist-17] median active exp 494, avg 441.4
c [simplification-17] removed 578 variables 1.5% (37198 remain 20%)
c [simplification-17] removed 4927 irredundant clauses 1.9% (256285 remain 25%)
c [simplification-17] maximum reduction of 2% = max (2%, 2%)
c [simplification-17] geometric conflict interval increment 17777 = 53332 / 3
c [simplification-17] new conflict interval 71109
c [simplification-17] penalized conflict interval 71109 = 1 * 71109
c [simplification-17] hard conflict limit 348351 (soft 312797 + delta 35554)
c [simplification-17] new conflict limit 312797 (hard 348351)
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  500.6   37197   256285    253282   50498   5401 824051  117   187  105  63%    419  -57   92  137   67%
c i  508.6   37196   256285    262025   56540   5407 824105  114   192  116  59%   -104  -43  135  133  101%
c -  510.3   37196   256285    263558   29214   5412 824109  141   226   57  62%   -183   -8  187  134  139%
c i  529.8   37195   256285    282823   42136   5463 824168   99   161   93  62%    101  -88   62  142   44%
c i  534.4   37190   256285    287648   45024   5472 824188  116   194   97  60%   -137  -50  141  140  101%
c i  535.9   37188   256285    288967   45644   5477 824194  116   185   97  63%   -170  -58  104  140   74%
c -  557.3   37186   256285    311062   30881   5567 824330   99   144   58  69%    141  -95   77  135   57%
c 
c [simplification-18] limit 312797 conflicts (hard 348351) hit after 348351 conflicts
c [quatres-11] found 17175 quaternary clauses 47% in total
c [quatres-11-2] added 1 quaternary resolvents
c [ternres-14] limit 112945949 with penalty 0 = 0 + 0
c [ternres-14] all 37186 free variables schedulable
c [ternres-14] 99 ternary resolvents (0 bin, 99 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-44] removed 13 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 2378 sched 6%, 336 failed, 3 lifted, 65830 hbrs
c [decomp-45] removed 494 variables
c [basicprobe-6-1] 2261 probes remain 6% after last round
c [basicprobe-6-1] 578 units = 568 failed (98%) + 10 lifted (2%)
c [basicprobe-6-1] removed 854 variables, found 234127 hbrs
c [bate-5] eliminated 290 asymmetric tautologies during probing
c [unhide-18] limit 5000000 with penalty 2 = 0 + 2
c [unhide-18-30] 0 units, 6 failed, 78798 tauts, 0 hbrs, 1037947 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 222 transitive binary clauses
c [bca-14] limit of 10000000 steps and 490367 added (scaled 2)
c [bca-14] 51633 out of 72656 literals actually usable 71%
c [bca-14] added 13 blocked clauses in 171441 steps
c [sweep-14] limit 33883784 penalty 0 = 0 + 0
c [sweep-14-1] 2966 pos 9.9% + 27080 neg 90.1% = 30046 sched 82.7% ret 6281
c [sweep-14-1] 33886687 steps 614 queries 377.48 avg class size
c [sweep-14-1] 14252 decisions 596 SAT calls 220.61 avg env size
c [sweep-14-1] 19866 variables remain 55% (16407 retained 45%)
c [decomp-46] removed 78 variables
c [sweep-14-1] removed 78 vars (0 failed, 19 eqs, 55 impls)
c [sweep-14] removed 78 vars in TOTAL (1 rounds, 613 queries)
c [phase-count-18] 243754 negative 99.8% of 244180 except 426 0.2%
c [phase-count-18] 180637 positive 74.0% of 244180 except 63543 26.0%
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 9579 enqueued variables after 348351 conflicts
c [score-dist-18] active 26670 (74%), one 3177 (9%), zero 6402 (18%)
c [score-dist-18] max exp 510, different 474 (93%)
c [score-dist-18] median active exp 502, avg 444.7
c [simplification-18] removed 937 variables 2.5% (36249 remain 19%)
c [simplification-18] removed 12105 irredundant clauses 4.7% (244180 remain 24%)
c [simplification-18] maximum reduction of 5% = max (3%, 5%)
c [simplification-18] large reduction 5% >= 5% limit
c [simplification-18] next conflict interval 3483 = min (348351/100, 71109)
c [simplification-18] penalized conflict interval 3483 = 1 * 3483
c [simplification-18] hard conflict limit 361834 (soft 351834 + delta 10000)
c [simplification-18] new conflict limit 351834 (hard 361834)
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 -  626.8   36249   244180    349838   32072   5294 923713   72    99   59  73%    535  -79   68  105   65%
c 
c [simplification-19] limit 351834 conflicts (hard 361834) hit after 361834 conflicts
c [quatres-12] found 16714 quaternary clauses 46% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [quatres-12-2] added 2 single-self-subsuming ternary resolvents
c [quatres-12-2] added 3 quaternary resolvents
c [ternres-15] limit 117821766 with penalty 0 = 0 + 0
c [ternres-15] all 36249 free variables schedulable
c [ternres-15] 68 ternary resolvents (0 bin, 68 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 1472772 penalty 4 = 4 + 0
c [gauss-5] extracted 20 xors of average arity 3.0
c [gauss-5] connected 60 occurrences of 60 variables (average 1.0)
c [gauss-5] limit 1472772 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-7] 2879 schedulable variables 8%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-48] removed 36 variables
c [simpleprobe-7] 185 variables remain 1% (36028 retained 99%)
c [simpleprobe-7] removed 36 variables, found 79847 hbrs, 14 units
c [unhide-19] limit 10000000 with penalty 1 = 0 + 1
c [unhide-19-34] 0 units, 6 failed, 120173 tauts, 0 hbrs, 661179 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 213 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 1472772077 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 211
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 210
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 209
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 208
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 207
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 206
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 205
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 204
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 203
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 202
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 201
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 200
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 199
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 198
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 197
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 196
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 195
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 194
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 193
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 192
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 191
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 190
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 189
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 188
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 187
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 186
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 185
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 184
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 183
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 182
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 181
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 180
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 179
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 178
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 177
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 176
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 175
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 174
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 173
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 172
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 171
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 170
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 169
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 168
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 167
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 166
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 165
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 164
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 163
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 162
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 161
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 160
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 159
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 158
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 157
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 156
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 155
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 154
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 153
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 152
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 151
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 150
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 149
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 148
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 147
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 146
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 145
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 144
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 143
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 142
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 141
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 140
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 139
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 138
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 137
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 136
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 135
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 134
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 133
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 132
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 131
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 130
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 129
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 128
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 127
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 126
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 125
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 124
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 123
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 122
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 121
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 120
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 119
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 118
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 117
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 116
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 115
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 114
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 113
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 112
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 111
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 110
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 109
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 108
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 107
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 106
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 105
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 104
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 103
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 102
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 101
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 100
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 99
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 98
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 97
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 96
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 95
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 94
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 92
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 90
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 89
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 88
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 87
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 86
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 85
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 83
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 81
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 79
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 77
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 74
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 73
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 71
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 70
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 69
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 67
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 66
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 65
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 64
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 63
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 62
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 61
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 60
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 59
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 58
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 57
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 56
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 55
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 54
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 53
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 52
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 51
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 50
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 49
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 47
c [cce-8-1] eliminated 3 clauses out of 3 (100%) of length 46
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 45
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 44
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 43
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 42
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 41
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 39
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 38
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 37
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 36
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 35
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 34
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 33
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 32
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 31
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 30
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 29
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 28
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 27
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 26
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 25
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 24
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 23
c [cce-8-1] eliminated 3 clauses out of 9 (33%) of length 22
c [cce-8-1] eliminated 8 clauses out of 9 (89%) of length 21
c [cce-8-1] eliminated 6 clauses out of 10 (60%) of length 20
c [cce-8-1] eliminated 7 clauses out of 12 (58%) of length 19
c [cce-8-1] eliminated 8 clauses out of 12 (67%) of length 18
c [cce-8-1] eliminated 8 clauses out of 12 (67%) of length 17
c [cce-8-1] eliminated 10 clauses out of 14 (71%) of length 16
c [cce-8-1] eliminated 7 clauses out of 11 (64%) of length 15
c [cce-8-1] eliminated 10 clauses out of 17 (59%) of length 14
c [cce-8-1] eliminated 10 clauses out of 16 (62%) of length 13
c [cce-8-1] eliminated 11 clauses out of 24 (46%) of length 12
c [cce-8-1] eliminated 14 clauses out of 25 (56%) of length 11
c [cce-8-1] eliminated 13 clauses out of 27 (48%) of length 10
c [cce-8-1] eliminated 22 clauses out of 32 (69%) of length 9
c [cce-8-1] eliminated 23 clauses out of 44 (52%) of length 8
c [cce-8-1] eliminated 26 clauses out of 129 (20%) of length 7
c [cce-8-1] eliminated 26 clauses out of 2730 (1%) of length 6
c [cce-8-1] eliminated 110 clauses out of 8301 (1%) of length 5
c [cce-8-1] eliminated 1192 clauses out of 15759 (8%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 1738 large clauses in 498152194 steps
c [cce-8-1] allowing another 249076097 steps for small clauses
c [cce-8-1] scheduling 202390 clauses = 127317 binary + 75073 ternary
c [cce-8-1] tried to eliminate 62143 small clauses 31%
c [cce-8-1] eliminated 6436 binary clauses 5%
c [cce-8-1] eliminated 1778 ternary clauses 2%
c [cce-8-1] eliminated 8214 small clauses 4%
c [cce-8-1] eliminated 8230 small clauses in 1472772077 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 9968 covered clauses in round 1
c [cce-8] eliminated 9968 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 36207 variables 100%
c [elim-15] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 780 variables 2% in round 1 in 23362611 steps
c [elim-15-1] backward subsumption/strengthening limit 23362600
c [elim-15-1-1] backward checking 4659 touched variables 13%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 9 and strengthened 31 clauses in 1014547 steps
c [elim-15-1] rescheduled 93 variables 0% by backward subsumption
c [elim-15-2] eliminated 2 variables 0% in round 2 in 65228 steps
c [elim-15-2] backward subsumption/strengthening limit 65200
c [elim-15-2-1] backward checking 29 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 51802 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 782 = 2% variables out of 36207 scheduled
c [bca-15] limit of 10000000 steps and 463078 added (scaled 2)
c [bca-15] 51264 out of 70852 literals actually usable 72%
c [bca-15] added 42 blocked clauses in 149089 steps
c [sweep-15] limit 35346529 penalty 0 = 0 + 0
c [sweep-15-1] 2354 pos 12.2% + 16974 neg 87.8% = 19328 sched 54.6% ret 16097
c [sweep-15-1] 35351516 steps 875 queries 156.11 avg class size
c [sweep-15-1] 13719 decisions 853 SAT calls 113.02 avg env size
c [sweep-15-1] 12399 variables remain 35% (23018 retained 65%)
c [decomp-49] removed 30 variables
c [sweep-15-1] removed 30 vars (0 failed, 22 eqs, 74 impls)
c [sweep-15] 30 < 1/1000 * 35425 = 35 considered unsuccessful
c [sweep-15] removed 30 vars in TOTAL (1 rounds, 874 queries)
c [sort-queue-19] sorted 9001 enqueued variables after 361834 conflicts
c [score-dist-19] active 26394 (75%), one 2753 (8%), zero 6248 (18%)
c [score-dist-19] max exp 510, different 469 (92%)
c [score-dist-19] median active exp 502, avg 449.0
c [simplification-19] removed 854 variables 2.4% (35395 remain 19%)
c [simplification-19] removed 13323 irredundant clauses 5.5% (230857 remain 23%)
c [simplification-19] maximum reduction of 5% = max (2%, 5%)
c [simplification-19] large reduction 5% >= 5% limit
c [simplification-19] next conflict interval 3618 = min (361834/100, 71109)
c [simplification-19] penalized conflict interval 3618 = 1 * 3618
c [simplification-19] hard conflict limit 375452 (soft 365452 + delta 10000)
c [simplification-19] new conflict limit 365452 (hard 375452)
c 
c [simplification-20] limit 365452 conflicts (hard 375452) hit after 372530 conflicts
c [quatres-13] found 15816 quaternary clauses 45% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 5 quaternary resolvents
c [ternres-16] limit 121109308 with penalty 0 = 0 + 0
c [ternres-16] all 35395 free variables schedulable
c [ternres-16] 237 ternary resolvents (0 bin, 237 trn)
c [ternres-16] fully completed ternary resolution
c [treelook-7] limit 12110930 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 51335 literals 73%
c [treelook-7] scheduling used 1395822 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 12110930 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 12308842 steps
c [treelook-7] 51217 literals remain 72%
c [treelook-7] 6471 variables remain to probed next time 18%
c [treelook-7] removed 2 variables, found 56653 hbrs
c [unhide-20] limit 10000000 with penalty 1 = 0 + 1
c [unhide-20-38] 0 units, 0 failed, 59420 tauts, 0 hbrs, 295655 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 165 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 35393 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 21 blocked clauses
c [block-6] 21 < 1/100 * 230032 = 2300 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 35393 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 36 variables 0% in round 1 in 26030140 steps
c [elim-16-1] backward subsumption/strengthening limit 26030100
c [elim-16-1-1] backward checking 285 touched variables 1%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 0 and strengthened 1 clauses in 92059 steps
c [elim-16-1] rescheduled 4 variables 0% by backward subsumption
c [elim-16-2] no variable eliminated in round 2 in 1173 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 36 = 0% variables out of 35393 scheduled
c [elim-16] 36 < 1/100 * 35393 = 353 considered unsuccessful
c [bca-16] limit of 10000000 steps and 461157 added (scaled 2)
c [bca-16] 50357 out of 70716 literals actually usable 71%
c [bca-16] added 21 blocked clauses in 154136 steps
c [sort-queue-20] sorted 9014 enqueued variables after 372530 conflicts
c [score-dist-20] active 26343 (75%), one 2819 (8%), zero 6195 (18%)
c [score-dist-20] max exp 510, different 453 (89%)
c [score-dist-20] median active exp 498, avg 458.6
c [simplification-20] removed 38 variables 0.1% (35357 remain 19%)
c [simplification-20] removed 889 irredundant clauses 0.4% (229968 remain 23%)
c [simplification-20] maximum reduction of 0% = max (0%, 0%)
c [simplification-20] full geometric conflict interval increment 71109
c [simplification-20] new conflict interval 142218
c [simplification-20] penalized conflict interval 142218 = 1 * 142218
c [simplification-20] hard conflict limit 585857 (soft 514748 + delta 71109)
c [simplification-20] new conflict limit 514748 (hard 585857)
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 -  744.9   35357   229968    410292   32495   6708 778474  137   186   55  74%    830   32  155  108  143%
c -  801.6   35357   229968    462271   33232   6788 778559  208   284   55  73%    936  106  295  131  225%
c i  852.2   35356   229968    513936   60082   6856 778625  106   174  113  61%    984  -31  105  145   73%
c i  860.3   35354   229968    522522   65582   6879 778642   99   180  139  55%  -2143  -22  123  140   88%
c -  861.5   35348   229968    523616   34461   6881 778642   92   172   55  53%  -2178  -30   77  138   56%
c -  920.0   35348   229968    580834   35317   6997 778751  107   144   55  75%   -333  -52  111  132   84%
c 
c [simplification-21] limit 514748 conflicts (hard 585857) hit after 585858 conflicts
c [quatres-14] found 16164 quaternary clauses 44% in total
c [quatres-14-2] added 12 single-self-subsuming ternary resolvents
c [quatres-14-2] added 10 quaternary resolvents
c [ternres-17] limit 185828182 with penalty 0 = 0 + 0
c [ternres-17] all 35348 free variables schedulable
c [ternres-17] 87 ternary resolvents (0 bin, 87 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 5807130 penalty 4 = 4 + 0
c [card-6] found 3742 at-most-one constraints of average size 3.9
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 5807130 for elimination
c [card-6] 3742 out of 3742 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-52] removed 9 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 2684 sched 8%, 132 failed, 5 lifted, 35183 hbrs
c [decomp-53] removed 157 variables
c [basicprobe-7-1] 11778 sched 34%, 90 failed, 3 lifted, 58471 hbrs
c [decomp-54] removed 288 variables
c [basicprobe-7-2] 10026 probes remain 29% after last round
c [basicprobe-7-2] 238 units = 229 failed (96%) + 9 lifted (4%)
c [basicprobe-7-2] removed 454 variables, found 96293 hbrs
c [bate-6] eliminated 164 asymmetric tautologies during probing
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 192 transitive binary clauses
c [cce-9] limit of 464570455 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 135
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 134
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 133
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 132
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 131
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 130
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 129
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 128
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 127
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 126
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 125
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 124
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 123
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 122
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 121
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 120
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 119
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 118
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 117
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 116
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 115
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 114
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 113
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 112
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 111
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 110
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 109
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 108
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 107
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 106
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 105
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 104
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 103
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 102
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 101
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 100
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 99
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 98
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 97
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 96
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 95
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 94
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 93
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 92
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 90
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 89
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 88
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 87
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 86
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 85
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 84
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 83
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 82
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 81
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 80
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 79
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 78
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 77
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 76
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 75
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 74
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 73
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 71
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 70
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 69
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 67
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 66
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 65
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 64
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 63
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 62
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 61
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 60
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 59
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 58
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 57
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 56
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 55
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 54
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 53
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 52
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 51
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 50
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 49
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 47
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 46
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 45
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 44
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 43
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 42
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 41
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 39
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 38
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 37
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 36
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 35
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 34
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 33
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 32
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 31
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 30
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 29
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 28
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 27
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 26
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 25
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 24
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 23
c [cce-9-1] eliminated 4 clauses out of 11 (36%) of length 22
c [cce-9-1] eliminated 2 clauses out of 7 (29%) of length 21
c [cce-9-1] eliminated 3 clauses out of 9 (33%) of length 20
c [cce-9-1] eliminated 7 clauses out of 14 (50%) of length 19
c [cce-9-1] eliminated 4 clauses out of 12 (33%) of length 18
c [cce-9-1] eliminated 7 clauses out of 14 (50%) of length 17
c [cce-9-1] eliminated 5 clauses out of 14 (36%) of length 16
c [cce-9-1] eliminated 9 clauses out of 18 (50%) of length 15
c [cce-9-1] eliminated 8 clauses out of 22 (36%) of length 14
c [cce-9-1] eliminated 9 clauses out of 22 (41%) of length 13
c [cce-9-1] eliminated 8 clauses out of 29 (28%) of length 12
c [cce-9-1] eliminated 17 clauses out of 31 (55%) of length 11
c [cce-9-1] eliminated 15 clauses out of 39 (38%) of length 10
c [cce-9-1] eliminated 18 clauses out of 37 (49%) of length 9
c [cce-9-1] eliminated 20 clauses out of 53 (38%) of length 8
c [cce-9-1] eliminated 29 clauses out of 146 (20%) of length 7
c [cce-9-1] eliminated 35 clauses out of 2808 (1%) of length 6
c [cce-9-1] eliminated 68 clauses out of 8221 (1%) of length 5
c [cce-9-1] eliminated 52 clauses out of 14708 (0%) of length 4
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 460 large clauses in 464570465 steps
c [cce-9-1] allowing another 232285232 steps for small clauses
c [cce-9-1] scheduling 188930 clauses = 119580 binary + 69350 ternary
c [cce-9-1] tried to eliminate 11453 small clauses 6%
c [cce-9-1] eliminated 1230 binary clauses 1%
c [cce-9-1] eliminated 323 ternary clauses 0%
c [cce-9-1] eliminated 1553 small clauses 1%
c [cce-9-1] eliminated 1661 small clauses in 464570458 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 2121 covered clauses in round 1
c [cce-9] eliminated 2121 covered clauses in TOTAL during 1 rounds
c [cce-9] 2121 < 1/100 * 226920 = 2269 considered unsuccessful
c [bca-17] limit of 10000000 steps and 450829 added (scaled 2)
c [bca-17] 49010 out of 69790 literals actually usable 70%
c [bca-17] added 6 blocked clauses in 142756 steps
c [sweep-16] limit 27874227 penalty 1 = 1 + 0
c [sweep-16-1] 1400 pos 11.5% + 10797 neg 88.5% = 12197 sched 35.0% ret 22697
c [sweep-16-1] 27876765 steps 766 queries 225.64 avg class size
c [sweep-16-1] 10804 decisions 737 SAT calls 93.89 avg env size
c [sweep-16-1] 8583 variables remain 25% (26306 retained 75%)
c [decomp-55] removed 37 variables
c [sweep-16-1] removed 37 vars (0 failed, 32 eqs, 76 impls)
c [sweep-16] removed 37 vars in TOTAL (1 rounds, 765 queries)
c [sort-queue-21] sorted 9766 enqueued variables after 585858 conflicts
c [score-dist-21] active 25091 (72%), one 3887 (11%), zero 5879 (17%)
c [score-dist-21] max exp 510, different 414 (81%)
c [score-dist-21] median active exp 502, avg 465.6
c [simplification-21] removed 491 variables 1.4% (34857 remain 18%)
c [simplification-21] removed 5230 irredundant clauses 2.3% (224738 remain 22%)
c [simplification-21] maximum reduction of 2% = max (1%, 2%)
c [simplification-21] geometric conflict interval increment 47406 = 142218 / 3
c [simplification-21] new conflict interval 189624
c [simplification-21] penalized conflict interval 189624 = 1 * 189624
c [simplification-21] hard conflict limit 870294 (soft 775482 + delta 94812)
c [simplification-21] new conflict limit 775482 (hard 870294)
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 3093 basic ate = 2929 trn 95% + 164 lrg 5% in 6 updates
c bcas: 17 count, 1469 added (529 skipped), 4093708 steps
c bkwd: tried 415480 clauses, 830807 lits, 2.00 lits/clause
c bkwd: checked 16414951 occs, 39.51 occs/clause, 19.76 occs/lit
c bkwd: subsumed 11 binary, 68 ternary, 22 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1114 large (0% self)
c blkd: 6 bces, 9929 removed, 7835482 resolutions, 21778305 steps
c blkd: 12828 blocking literals 3%, 2 pure
c bump: 631452 bumped seen, 515774015 lits 816.8 on average
c card: 6 count, 0 units, 0 am1, 386416593 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 76326 subsumed
c card: 20879 at-most-one constraints found, average size 4.61
c card: 20879 at-most-one constraints used 100%, average size 4.61
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: 9 cces, 72307 eliminated, 71562 ate 99%, 745 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 3450190 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 162 gcs, 0 rescored clauses, 2455 rescored vars
c dcps: 55 decompositions, 8938 equivalent 4%
c deco: 218706 decision-only clauses 35%, 69% reduction
c decs: 8657036 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 82236 eliminated 41%, 133 pure 0%
c elms: 42 rounds, 2.6 rounds/bve
c elms: 63736 small 78%, 18365 large 22%
c elms: 180220 tried small, 63736 succeeded 35%, 116484 failed 65%
c elms: 37267 subsumed, 55960 strengthened, 1295 blocked
c elms: 20921011 copies, 20725850 resolutions, 4724224 ipos
c elms: 5911014 subchks, 4273768 strchks
c gaus: 5 extractions, 131 extracted, 2.9 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 14140592 steps, 7070296 extr 50%, 1024 elim 0%
c glue: 137.8 orig avg, 137.8 real avg, 8.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2406363 = 483646 simple 20% + 1863222 trn 77% + 59495 lrg 2%, 4001 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 631451 clauses, 308.7 length
c lrnd: 194932225 lits = 341849223 orig - 146916998 removed 43%
c lrnd: 308476 uips 49%, 278284 flips 44%
c mins: 365140 mins 62%, 2465 bin 0%, 5620 size 1%
c mins: 277201843 poisoned searches, 55741327 hits, 20% hit rate
c mins: 336549015 used twice searches, 18514642 hits, 6% hit rate
c move: moved 42609, 31316 bin 73%, 11293 trn 27%
c otfs: 4698 driving 38%, 7755 restarting 62%
c otfs: str 12453, 12296 red 99%, 157 irr 1%
c otfs: str 12453, 0 bin 0%, 103 trn 1%, 12350 lrg 99%
c otfs: sub 112, 112 red 100%, 0 irr 0%
c otfs: sub 112, 0 bin 0%, 0 trn 0%, 112 lrg 100%
c phas: 18 computed, 92640 set, 6 pos (0%), 92634 neg (100%)
c prbs: 7 basic, 92730 probed, 3007 failed, 91 lifted
c prbs: 7 simple, 831492 probed, 1136 failed, 387 eqs
c prbs: 7 treelook, 578 probed, 30 failed, 0 lifted
c prom: 44145 locked 2% out of 1845910 tried
c prps: 2496826238 props, 272 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 14 count, 59 quat, 20 self1, 0 self2, 476 dup
c queu: 21 sorted, 8657036 next (72212 steps 0.01)
c queu: 591954789 enq (1022773029 steps 1.73), 515774015 deq 87%
c redc: 3463 clauses 23%, 14923 tried 2%, 55 sat 0%
c redc: 8787 lits 6%, 157419 tried 0%, 55 sat 0%
c redc: 382 times jump level reduced, 71.8 levels on average
c reds: 8 count, 79045.9 conflicts per reduce
c reds: 0 memlim 0%, 8 arith 100%
c reds: 214051 collected 88%, 28516 retired 12%
c rmbd: 68860 removed, 38633 red 56%
c rsts: 11628 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: 21 count, 19 confs 90%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 631451 count (809177 tried 1.3), 211911 sub out of 625159 (33.9%)
c swps: 16 count, 17 rounds, 10254 queries (603.2/round)
c swps: 9255 sat calls, 120 unsat (0.4% success rate)
c swps: 115468 decisions 12.5, 3783 conflicts 0.4
c swps; 397.6 avg class size, 114.3 avg environment size
c swps: 0 failed, 2041 impls, 1060 equivs
c swp0: 3412 type 0 queries, 1761 unsat (51.6%), 3040 sat (89.1%)
c swp1: 6842 type 1 queries, 3774 unsat (55.2%), 6154 sat (89.9%)
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: 18582653 calls to obtain time
c tops: 73965 fixed 37%, 367 its, 1723.07 confs/it
c trds: 17 transitive reductions, 3053 removed, 28 failed
c trds: 14749 nodes, 52180 edges, 34039413 steps
c trim: 4152594 words, 15.8 MB
c trnr: 17 count, 0 bin, 3839 trn, 194868608 steps
c unhd: 20 count, 38 rounds, 110938072 steps
c unhd: 616 non-trivial sccs of average size 2.1
c unhd: 76 units, 75 bin, 1 trn, 0 lrg
c unhd: 5969 failed, 5939 stamp, 0 lits, 13 bin, 7 trn, 0 lrg
c unhd: 817339 tauts, 17748 bin 2%, 8381 trn 1%, 346 lrg 0%
c unhd: 817339 tauts, 790864 stamp 97%, 770096 red 94%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 12802589 str, 75 bin 0%, 2485 trn 0%, 12800029 lrg 100%, 12787201 red 100%
c vars: 34857 remaining 17% and 165139 removed 83% out of 199996
c vars: 73965 fixed 37%, 82236 eliminated 41%, 8938 equivalent 4%
c vsts: 21459895260 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 8.5 search visits per propagation, 31680.5 per conflict
c wchs: 1528417818 pushed, 57265570 enlarged, 238 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         625218        214051         28516      51321811       9232983        328498
c 
c  0 0         17362   3      1778   1         0   0  22064269  43   2694342  29     45208  14     1.4
c  1 5          6486   1      1538   1       745   3   3453116   7    603483   7     15681   5     0.6
c  2 6         16711   3      6006   3      1391   5   5247166  10    960779  10     31810  10     1.7
c  3 9         22119   4      9629   4      1342   5   4605653   9<   879471  10     29182   9     2.1
c  4 14        23031   4     10485   5      1454   5   3392573   7    672193   7<    26270   8     2.2
c  5 21        25332   4     12068   6      1654   6   2816336   5    611932   7     24730   8<    3.1
c  6 30        29136   5     14999   7      1709   6   2157565   4    522514   6     22667   7     4.7
c  7 41        36224   6     17834   8      1862   7   1559909   3    415659   5     21480   7    22.0
c  8 54        50257   8     27626  13<     2369   8<  2212955   4    543715   6     22622   7    21.6
c  9 69        55868   9<    32058  15      2713  10   1122425   2    376498   4     20347   6    20.2
c 10 86        83622  13     37283  17      3667  13   1323514   3    438804   5     25735   8    14.6
c 11 126      149381  24     24686  12      5158  18    904566   2    336194   4     23137   7    18.9
c 12 230       95563  15     16471   8      4111  14    408510   1    156229   2     16552   5    14.8
c 13 534       14122   2      1590   1       341   1     53248   0     21170   0      3077   1    20.9
c 14 1526          4   0         0   0         0   0         6   0         0   0         0   0     0.0
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                  8.7           8.1           8.3           2.6           3.8           5.5
c std                  3.2           2.8           3.3           3.2           3.6           3.8
c 
c  104.222  10% bump
c   88.490   9% cce
c   72.036   7% probe
c   57.195   6% unhide
c   26.789   3% sweep
c   18.923   2% elim
c    9.808   1% rescore
c    5.157   1% decide
c 
c   12.326 < 1% rest (below)
c 
c    3.774   0% bca
c    2.970   0% block
c    1.903   0% transred
c    1.381   0% gauss
c    1.231   0% ternres
c    0.628   0% quatres
c    0.437   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    3.904   0% preprocessing     1%
c  286.444  29% inprocessing     99%
c ==================================
c  290.348  29% simplifying
c  709.079  71% search
c ==================================
c  999.430 100% all
c 
c        632367 conflicts,         632.7 confs/sec
c          2177 ternaries,         290.5 confs/ternary
c          2667 binaries,          237.1 confs/binary
c           367 iterations,       1723.1 confs/iteration
c 
c             8 reductions,          0.0 redus/sec,  79045.9 confs/reduction
c         11628 restarts,           11.6 rests/sec,     54.4 confs/restart
c       8657036 decisions,        8662.0 decis/sec,     13.7 decis/conflict
c    2496826238 propagations,  2498249.1 props/sec,    288.4 props/decision
c 
c 999.4 seconds, 232.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
