c launch: /data/cnf/sc2014/app/SAT_dat.k75-24_1_rule_3.cnf.bz2
c host: atom02
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/SAT_dat.k75-24_1_rule_3.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k75-24_1_rule_3.cnf.bz2
c no embedded options
c found 'p cnf 1213331 4754042' header
c read 1213331 variables, 4754042 clauses, 11933943 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=3
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 1175373 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] SUM (--score=3)
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 1175373  4715950         0       0      0     0    0     0  262   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1178987 based on 4715950 irredundant clauses
c [card-1] found 1036 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1178987 for elimination
c [card-1] 1036 out of 1036 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 282979 variables
c [simpleprobe-1] all 930352 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 7560640 based on 3780320 irredundant clauses
c [decomp-2] removed 1369 variables
c [simpleprobe-1] 884321 variables remain 95% (44662 retained 5%)
c [simpleprobe-1] removed 1369 variables, found 19289 hbrs, 189 units
c [unhide-1] limit 235868 based on 3773892 irredundant clauses
c [unhide-1-1] 1471 units, 1081 failed, 8287 tauts, 0 hbrs, 47688 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 923592 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 843189 not tried 91% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 81033 = 9% variables out of 923592 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3333359 negative 95.2% of 3501363 except 168004 4.8%
c [phase-count-1] 3278109 positive 93.6% of 3501363 except 223254 6.4%
c [phase-1] phase bias: 391175 positive 46%, 451384 negative 54%
c [sort-queue-1] sorted 842559 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 842559 (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 164714 variables 16.4% (842559 remain 72%)
c [simplification-1] removed 1214587 irredundant clauses 25.8% (3501363 remain 74%)
c [simplification-1] maximum reduction of 26% = max (16%, 26%)
c [simplification-1] large reduction 26% >= 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   14.3  842558  3501363         7       5      9 15562    0     1  219   1%      0    1    0    0 25233%
c i   14.4  842425  3501363         9       6      9 15562    0     1  219   1%      0    1    0    0 25086%
c i   14.4  842424  3501363        14       7      9 15565    0     1  219   1%      0    1    0    0 24778%
c i   14.4  842423  3501363        29      13     14 15568    0     1  219   1%      0    1    0    0 24124%
c i   14.4  842422  3501363        32      15     14 15568    0     1  219   2%      0    1    0    0 24089%
c i   14.7  842218  3501363       180     115     33 15593    0     2  220   6%      0    2    1    0 18712%
c i   14.7  842217  3501363       183     116     34 15593    0     2  220   6%      0    2    1    0 18552%
c i   15.1  842201  3501363       284     191     43 15603    0     3  220   7%      0    3    2    0 15900%
c i   15.5  842200  3501363       370     256     55 15608    0     5  220   5%      0    5    3    0 14538%
c i   16.8  842199  3501363       851     652     98 15632    1     9  221  13%      2    9    8    0 10235%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 3475 variables
c [simpleprobe-2] 798743 schedulable variables 95%
c [simpleprobe-2] limit 6984098 based on 3492049 irredundant clauses
c [decomp-4] removed 1709 variables
c [simpleprobe-2] 700226 variables remain 84% (137149 retained 16%)
c [simpleprobe-2] removed 1709 variables, found 21769 hbrs, 421 units
c [treelook-1] limit 871106 based on 3484427 irredundant clauses
c [treelook-1] scheduled 173227 literals 10%
c [treelook-1] scheduling used 871527 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 871106 based on 3484427 irredundant clauses
c [treelook-1] used 871469 steps
c [treelook-1] 172845 literals remain 10%
c [treelook-1] 170639 variables remain to probed next time 20%
c [decomp-5] removed 125 variables
c [treelook-1] removed 181 variables, found 3703 hbrs
c [basicprobe-1] limit 27869968 based on 3483746 irredundant clauses
c [basicprobe-1-0] 757438 probes remain 91% after last round
c [basicprobe-1-0] 4262 units = 2125 failed (50%) + 2137 lifted (50%)
c [basicprobe-1-0] removed 9081 variables, found 178248 hbrs
c [unhide-2] limit 217734 based on 3483746 irredundant clauses
c [unhide-2-2] 792 units, 927 failed, 11365 tauts, 0 hbrs, 30821 literals
c [elim-2] 825941 variables 100% will be scheduled this time
c [elim-2] scheduled 825941 variables 100%
c [elim-2] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 742823 not tried 90% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 83127 = 10% variables out of 825941 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 3081435 negative 95.1% of 3240392 except 158957 4.9%
c [phase-count-2] 3025669 positive 93.4% of 3240392 except 214723 6.6%
c [phase-2] phase bias: 843 positive 29%, 2066 negative 71%
c [sort-queue-2] sorted 730378 enqueued variables after 851 conflicts
c [score-dist-2] active 12436 (2%), one 0 (0%), zero 730378 (98%)
c [score-dist-2] max exp 518, different 18 (3%)
c [score-dist-2] median active exp 512, avg 511.8
c [simplification-2] removed 99385 variables 11.8% (742814 remain 63%)
c [simplification-2] removed 260971 irredundant clauses 7.5% (3240392 remain 69%)
c [simplification-2] maximum reduction of 12% = max (12%, 7%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1014 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c [simplification-3] limit 1014 conflicts (hard 11000) hit after 1015 conflicts
c [card-2] limit 810098 based on 3240392 irredundant clauses
c [card-2] found 719 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 810098 for elimination
c [card-2] 719 out of 719 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 4934 variables
c [treelook-2] limit 808060 based on 3232243 irredundant clauses
c [treelook-2] scheduled 152872 literals 10%
c [treelook-2] scheduling used 808216 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 808060 based on 3232243 irredundant clauses
c [treelook-2] used 815589 steps
c [treelook-2] 152742 literals remain 10%
c [treelook-2] 92102 variables remain to probed next time 12%
c [decomp-7] removed 142 variables
c [treelook-2] removed 151 variables, found 2306 hbrs
c [unhide-3] limit 201983 based on 3231742 irredundant clauses
c [unhide-3-3] 286 units, 576 failed, 15510 tauts, 0 hbrs, 17701 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 736779 variables 100%
c [elim-3] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 656538 not tried 89% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 80241 = 11% variables out of 736779 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 2884011 negative 95.0% of 3036913 except 152902 5.0%
c [phase-count-3] 2827352 positive 93.1% of 3036913 except 209561 6.9%
c [phase-3] phase bias: 617 positive 31%, 1379 negative 69%
c [sort-queue-3] sorted 644822 enqueued variables after 1015 conflicts
c [score-dist-3] active 11716 (2%), one 0 (0%), zero 644822 (98%)
c [score-dist-3] max exp 518, different 18 (3%)
c [score-dist-3] median active exp 512, avg 512.1
c [simplification-3] removed 86276 variables 11.6% (656538 remain 56%)
c [simplification-3] removed 203479 irredundant clauses 6.3% (3036913 remain 64%)
c [simplification-3] maximum reduction of 12% = max (12%, 6%)
c [simplification-3] large reduction 12% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13015 (soft 3015 + delta 10000)
c [simplification-3] new conflict limit 3015 (hard 13015)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   52.7  656537  3036913      1908    1090    115 124008    5    15  206  36%      7   15   23    0 5820%
c i   53.0  656413  3036913      2030    1204    117 124008    6    15  206  38%      6   15   21    0 4968%
c i   53.0  656412  3036913      2034    1206    118 124008    6    15  206  38%      6   15   21    0 4897%
c i   53.0  656411  3036913      2035    1206    118 124008    6    15  206  38%      6   15   21    0 4878%
c i   53.2  656410  3036913      2106    1254    133 124014    6    17  206  35%      6   16   16    0 3829%
c i   53.7  656376  3036913      2239    1356    154 124018    6    20  207  28%      5   20   12    0 2685%
c i   53.7  656375  3036913      2240    1356    154 124018    6    20  207  28%      5   20   12    0 2674%
c i   53.9  656374  3036913      2267    1377    156 124020    6    21  207  27%      5   21   11    0 2479%
c i   54.4  656373  3036913      2336    1433    163 124025    6    24  207  24%      5   23    9    0 2082%
c i   54.4  656372  3036913      2339    1435    163 124025    6    24  207  24%      5   23    9    0 2063%
c i   54.5  656371  3036913      2340    1435    163 124025    6    24  207  24%      5   23    9    0 2055%
c i   54.5  656370  3036913      2341    1435    163 124025    6    24  207  24%      5   23    9    0 2047%
c i   54.7  656369  3036913      2365    1455    164 124026    6    25  207  23%      5   24    9    0 1951%
c i   54.7  656368  3036913      2366    1455    164 124026    6    25  207  23%      5   24    9    0 1943%
c i   54.8  656367  3036913      2382    1468    165 124027    6    25  207  23%      4   25    9    0 1906%
c i   54.8  656366  3036913      2383    1468    165 124027    6    25  207  23%      4   25    8    0 1899%
c i   55.4  656365  3036913      2580    1625    183 124038    6    29  207  21%      4   28   10    0 2164%
c i   55.6  656364  3036913      2626    1665    186 124038    6    29  207  21%      4   28   10    0 2153%
c i   56.1  656363  3036913      2720    1737    199 124045    6    32  207  18%      3   32    9    0 1772%
c i   56.8  656362  3036913      2803    1805    204 124054    6    35  207  17%      3   34    7    0 1446%
c i   56.9  656361  3036913      2807    1807    204 124054    6    35  207  17%      3   34    7    0 1434%
c 
c [simplification-4] limit 3082 conflicts (hard 13015) hit after 3082 conflicts
c [decomp-8] removed 1180 variables
c [basicprobe-2] limit 24263576 based on 3032947 irredundant clauses
c [basicprobe-2-0] 505839 probes remain 78% after last round
c [basicprobe-2-0] 2228 units = 1537 failed (69%) + 691 lifted (31%)
c [basicprobe-2-0] removed 4610 variables, found 118318 hbrs
c [unhide-4] limit 189559 based on 3032947 irredundant clauses
c [unhide-4-4] 348 units, 455 failed, 12425 tauts, 0 hbrs, 32693 literals
c [elim-4] 649888 variables 100% will be scheduled this time
c [elim-4] scheduled 649888 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 378741630 steps penalty 1 = 0 + 1
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 2889 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 358287 = 55% variables out of 649888 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 1941722 negative 95.6% of 2030789 except 89067 4.4%
c [phase-count-4] 1902816 positive 93.7% of 2030789 except 127973 6.3%
c [phase-4] phase bias: 2582 positive 44%, 3340 negative 56%
c [sort-queue-4] sorted 279676 enqueued variables after 3082 conflicts
c [score-dist-4] active 11925 (4%), one 0 (0%), zero 279676 (96%)
c [score-dist-4] max exp 522, different 22 (4%)
c [score-dist-4] median active exp 514, avg 514.5
c [simplification-4] removed 364760 variables 55.6% (291601 remain 25%)
c [simplification-4] removed 1006124 irredundant clauses 33.1% (2030789 remain 43%)
c [simplification-4] maximum reduction of 56% = max (56%, 33%)
c [simplification-4] large reduction 56% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 15082 (soft 5082 + delta 10000)
c [simplification-4] new conflict limit 5082 (hard 15082)
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   86.6  291600  2030789      3635     815    170 60315    6    65  181   9%      5   63    6    1 1091%
c i   86.6  291599  2030789      3636     815    170 60315    6    65  181   9%      5   63    6    1 1087%
c i   86.6  291598  2030789      3640     818    170 60315    6    65  181   9%      5   63    6    1 1075%
c i   86.7  291597  2030789      3658     833    171 60315    6    66  181   9%      5   64    6    1 1071%
c i   87.3  291596  2030789      3745     908    175 60319    6    71  181   8%      5   70    6    1  988%
c i   87.6  291595  2030789      3808     957    178 60327    6    74  181   8%      5   73    5    1  923%
c i   88.2  291594  2030789      3906    1043    179 60333    6    77  181   8%      4   75    7    1 1152%
c i   88.4  291593  2030789      3964    1097    181 60334    6    78  181   8%      4   76    8    1 1313%
c i   90.8  291592  2030789      4799    1840    197 60344    9    83  182  10%      6   80   15    1 1785%
c i   91.1  291591  2030789      4864    1897    200 60346    9    84  182  10%      5   82   13    1 1545%
c i   91.1  291590  2030789      4865    1897    200 60346    9    84  182  10%      5   82   13    1 1539%
c i   91.9  291589  2030789      4997    2006    213 60349    8    91  182   9%      5   88   10    1 1204%
c 
c [simplification-5] limit 5104 conflicts (hard 15082) hit after 5104 conflicts
c [quatres-1] found 253601 quaternary clauses 40% in total
c [quatres-1-1] removed 9 duplicate quaternary clauses
c [quatres-1-1] added 94 double-self-subsuming ternary resolvents
c [quatres-1-2] added 1897 single-self-subsuming ternary resolvents
c [quatres-1-2] added 8517 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 10000000 with penalty 1 = 0 + 1
c [ternres-1] all 291589 free variables schedulable
c [ternres-1] 49353 ternary resolvents (175 bin, 49178 trn)
c [ternres-1] 174826 variables remain 60% (116763 retained 40%)
c [gauss-1] limit 1015337 based on 2030675 irredundant clauses
c [gauss-1] extracted 4828 xors of average arity 3.0
c [gauss-1] connected 14276 occurrences of 5859 variables (average 2.4)
c [gauss-1] limit 1015305 based on 2030611 irredundant clauses
c [decomp-9] removed 1789 variables
c [gauss-1] exported 0 unary, 1 binary and 0 ternary equations
c [decomp-10] removed 2 variables
c [simpleprobe-3] 243230 schedulable variables 84%
c [simpleprobe-3] limit 6845577 penalty 1 = 0 + 1
c [decomp-11] removed 329 variables
c [simpleprobe-3] 245350 variables remain 85% (44119 retained 15%)
c [simpleprobe-3] removed 329 variables, found 19716 hbrs, 67 units
c [unhide-5] limit 126536 based on 2024587 irredundant clauses
c [unhide-5-5] 206 units, 312 failed, 40783 tauts, 0 hbrs, 58845 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 797 transitive binary clauses
c [transred-1] found 12 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 288862 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 23521 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 28
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 25
c [cce-1-1] eliminated 4 clauses out of 8 (50%) of length 24
c [cce-1-1] eliminated 6 clauses out of 7 (86%) of length 23
c [cce-1-1] eliminated 9 clauses out of 12 (75%) of length 22
c [cce-1-1] eliminated 12 clauses out of 16 (75%) of length 21
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 20
c [cce-1-1] eliminated 16 clauses out of 20 (80%) of length 19
c [cce-1-1] eliminated 51 clauses out of 690 (7%) of length 18
c [cce-1-1] eliminated 314 clauses out of 852 (37%) of length 17
c [cce-1-1] eliminated 257 clauses out of 697 (37%) of length 16
c [cce-1-1] eliminated 229 clauses out of 1646 (14%) of length 15
c [cce-1-1] eliminated 630 clauses out of 2186 (29%) of length 14
c [cce-1-1] eliminated 258 clauses out of 3971 (6%) of length 13
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1794 large clauses in 30000107 steps
c [cce-1-1] allowing another 15000053 steps for small clauses
c [cce-1-1] scheduling 1103874 clauses = 882766 binary + 221108 ternary
c [cce-1-1] tried to eliminate 7179 small clauses 1%
c [cce-1-1] eliminated 1262 binary clauses 0%
c [cce-1-1] eliminated 296 ternary clauses 0%
c [cce-1-1] eliminated 1558 small clauses 0%
c [cce-1-1] eliminated 1558 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3352 covered clauses in round 1
c [cce-1] eliminated 3352 covered clauses in TOTAL during 1 rounds
c [cce-1] 3352 < 1/100 * 1957863 = 19578 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 288273 variables 100%
c [elim-5] limit of 68455773 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 67636 not tried 23% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 16573 = 6% variables out of 288273 scheduled
c [bca-1] limit of 10000000 steps and 3825052 added (scaled 2)
c [bca-1] 519159 out of 543402 literals actually usable 96%
c [bca-1] added 7020 blocked clauses in 1638684 steps
c [sweep-1] limit 3824552 based on 1912276 irredundant clauses
c [sweep-1-1] 95426 pos 35.1% + 176274 neg 64.9% = 271700 sched 100.0% ret 0
c [sweep-1-1] 3840779 steps 96 queries 77452.96 avg class size
c [sweep-1-1] 1184 decisions 86 SAT calls 35.23 avg env size
c [sweep-1-1] 271250 variables remain 100% (443 retained 0%)
c [decomp-12] removed 501 variables
c [sweep-1-1] removed 501 vars (0 failed, 19 eqs, 29 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 501 vars in TOTAL (1 rounds, 95 queries)
c [phase-count-5] 1826440 negative 95.6% of 1911228 except 84788 4.4%
c [phase-count-5] 1805899 positive 94.5% of 1911228 except 105329 5.5%
c [phase-5] phase bias: 648 positive 49%, 666 negative 51%
c [sort-queue-5] sorted 247025 enqueued variables after 5104 conflicts
c [score-dist-5] active 24174 (9%), one 0 (0%), zero 247025 (91%)
c [score-dist-5] max exp 522, different 21 (4%)
c [score-dist-5] median active exp 515, avg 515.5
c [simplification-5] removed 20390 variables 7.0% (271199 remain 23%)
c [simplification-5] removed 119561 irredundant clauses 5.9% (1911228 remain 41%)
c [simplification-5] maximum reduction of 7% = max (7%, 6%)
c [simplification-5] large reduction 7% >= 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 17104 (soft 7104 + delta 10000)
c [simplification-5] new conflict limit 7104 (hard 17104)
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  120.6  271198  1911226      6616    9722  39395 78299   14   122  182  12%     13  117   29    1 1937%
c 
c [simplification-6] limit 7104 conflicts (hard 17104) hit after 7104 conflicts
c [quatres-2] found 257956 quaternary clauses 41% in total
c [quatres-2-1] removed 12 duplicate quaternary clauses
c [quatres-2-1] added 18 double-self-subsuming ternary resolvents
c [quatres-2-2] added 1499 single-self-subsuming ternary resolvents
c [quatres-2-2] added 6397 quaternary resolvents
c [ternres-2] limit 7644636 based on 1911159 irredundant clauses
c [ternres-2] 162489 schedulable variables 60%
c [ternres-2] 34219 ternary resolvents (900 bin, 33319 trn)
c [ternres-2] 94576 variables remain 35% (176622 retained 65%)
c [card-3] limit 614762 penalty 2 = 2 + 0
c [card-3] found 346 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 614762 for elimination
c [card-3] 346 out of 346 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 8979 xors of average arity 3.0
c [gauss-2] connected 26866 occurrences of 9706 variables (average 2.8)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 290 variables
c [treelook-3] limit 491809 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 59267 literals 11%
c [treelook-3] scheduling used 491811 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 491809 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 496259 steps
c [treelook-3] 59217 literals remain 11%
c [treelook-3] 33761 variables remain to probed next time 12%
c [decomp-14] removed 8 variables
c [treelook-3] removed 15 variables, found 518 hbrs
c [unhide-6] limit 122952 with penalty 3 = 0 + 3
c [unhide-6-6] 209 units, 458 failed, 4988 tauts, 0 hbrs, 37893 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 904 transitive binary clauses
c [transred-2] found 21 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 270230 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 25632 blocked clauses
c [elim-6] 2798 variables 1% will be scheduled this time
c [elim-6] scheduled 2798 variables 1%
c [elim-6] limit of 98361922 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 1423 not tried 1% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 75 = 3% variables out of 2798 scheduled
c [elim-6] 75 < 1/100 * 2798 = 27 considered unsuccessful
c [bca-2] limit of 10000000 steps and 3745904 added (scaled 2)
c [bca-2] 502413 out of 539658 literals actually usable 93%
c [bca-2] added 1703 blocked clauses in 1573537 steps
c [sweep-2] limit 3741894 based on 1870947 irredundant clauses
c [sweep-2-1] 94682 pos 35.1% + 174726 neg 64.9% = 269408 sched 99.8% ret 420
c [sweep-2-1] 3755811 steps 98 queries 81553.64 avg class size
c [sweep-2-1] 1279 decisions 97 SAT calls 31.15 avg env size
c [sweep-2-1] 268851 variables remain 100% (974 retained 0%)
c [decomp-15] removed 479 variables
c [sweep-2-1] removed 479 vars (0 failed, 13 eqs, 16 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 479 vars in TOTAL (1 rounds, 97 queries)
c [phase-count-6] 1787600 negative 95.6% of 1869925 except 82325 4.4%
c [phase-count-6] 1765050 positive 94.4% of 1869925 except 104875 5.6%
c [phase-6] phase bias: 231 positive 47%, 265 negative 53%
c [sort-queue-6] sorted 239945 enqueued variables after 7104 conflicts
c [score-dist-6] active 29404 (11%), one 0 (0%), zero 239945 (89%)
c [score-dist-6] max exp 523, different 22 (4%)
c [score-dist-6] median active exp 517, avg 516.6
c [simplification-6] removed 1849 variables 0.7% (269349 remain 23%)
c [simplification-6] removed 41300 irredundant clauses 2.2% (1869925 remain 40%)
c [simplification-6] maximum reduction of 2% = max (1%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 6666
c [simplification-6] penalized conflict interval 6666 = 1 * 6666
c [simplification-6] hard conflict limit 23770 (soft 13770 + delta 10000)
c [simplification-6] new conflict limit 13770 (hard 23770)
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  150.3  269348  1869925     10205   18567  69461 86847   14   166  184   8%     39  154    9    2  424%
c i  150.7  269347  1869925     10295   18652  69463 86848   14   167  184   8%     36  154    9    2  408%
c 
c [simplification-7] limit of 341 binary hit after 341 binaries
c [quatres-3] found 261508 quaternary clauses 43% in total
c [quatres-3-1] removed 13 duplicate quaternary clauses
c [quatres-3-1] added 23 double-self-subsuming ternary resolvents
c [quatres-3-2] added 678 single-self-subsuming ternary resolvents
c [quatres-3-2] added 2612 quaternary resolvents
c [ternres-3] limit 7479364 based on 1869841 irredundant clauses
c [ternres-3] 93803 schedulable variables 35%
c [ternres-3] 38940 ternary resolvents (1418 bin, 37522 trn)
c [ternres-3] 54201 variables remain 20% (215146 retained 80%)
c [decomp-16] removed 431 variables
c [basicprobe-3] limit 36543949 penalty 0 = 0 + 0
c [basicprobe-3-0] 151180 probes remain 57% after last round
c [basicprobe-3-0] 2908 units = 2703 failed (93%) + 205 lifted (7%)
c [basicprobe-3-0] removed 3755 variables, found 154352 hbrs
c [bate-1] eliminated 3232 asymmetric tautologies during probing
c [unhide-7] limit 182719 with penalty 3 = 0 + 3
c [unhide-7-7] 93 units, 184 failed, 25078 tauts, 0 hbrs, 21457 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 1462 transitive binary clauses
c [transred-3] found 5 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 264850 variables 100%
c [block-3] limit of 73087899 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 3008 blocked clauses
c [block-3] 3008 < 1/100 * 1798978 = 17989 considered unsuccessful
c [cce-2] limit of 18271974 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 10 clauses out of 13 (77%) of length 22
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 21
c [cce-2-1] eliminated 2 clauses out of 11 (18%) of length 19
c [cce-2-1] eliminated 2 clauses out of 603 (0%) of length 18
c [cce-2-1] eliminated 12 clauses out of 530 (2%) of length 17
c [cce-2-1] eliminated 13 clauses out of 405 (3%) of length 16
c [cce-2-1] eliminated 19 clauses out of 1070 (2%) of length 15
c [cce-2-1] eliminated 378 clauses out of 1719 (22%) of length 14
c [cce-2-1] eliminated 65 clauses out of 3565 (2%) of length 13
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 502 large clauses in 18271974 steps
c [cce-2-1] allowing another 9135987 steps for small clauses
c [cce-2-1] scheduling 1009200 clauses = 774015 binary + 235185 ternary
c [cce-2-1] tried to eliminate 4233 small clauses 0%
c [cce-2-1] eliminated 633 binary clauses 0%
c [cce-2-1] eliminated 152 ternary clauses 0%
c [cce-2-1] eliminated 785 small clauses 0%
c [cce-2-1] eliminated 785 small clauses in 18271977 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1287 covered clauses in round 1
c [cce-2] eliminated 1287 covered clauses in TOTAL during 1 rounds
c [cce-2] 1287 < 1/100 * 1793282 = 17932 considered unsuccessful
c [bca-3] limit of 10000000 steps and 3588851 added (scaled 2)
c [bca-3] 486413 out of 529376 literals actually usable 92%
c [bca-3] added 412 blocked clauses in 1476293 steps
c [sweep-3] limit 3583990 based on 1791995 irredundant clauses
c [sweep-3-1] 97218 pos 36.9% + 166516 neg 63.1% = 263734 sched 99.6% ret 953
c [sweep-3-1] 3603414 steps 97 queries 86552.14 avg class size
c [sweep-3-1] 1024 decisions 96 SAT calls 31.32 avg env size
c [sweep-3-1] 263176 variables remain 99% (1508 retained 1%)
c [decomp-17] removed 3675 variables
c [sweep-3-1] removed 3675 vars (0 failed, 16 eqs, 16 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 3675 vars in TOTAL (1 rounds, 96 queries)
c [phase-count-7] 1703080 negative 95.3% of 1786541 except 83461 4.7%
c [phase-count-7] 1685532 positive 94.3% of 1786541 except 101009 5.7%
c [phase-7] phase bias: 371 positive 58%, 274 negative 42%
c [sort-queue-7] sorted 224389 enqueued variables after 10363 conflicts
c [score-dist-7] active 36623 (14%), one 0 (0%), zero 224389 (86%)
c [score-dist-7] max exp 524, different 22 (4%)
c [score-dist-7] median active exp 517, avg 517.0
c [simplification-7] removed 8335 variables 3.1% (261012 remain 22%)
c [simplification-7] removed 83384 irredundant clauses 4.5% (1786541 remain 38%)
c [simplification-7] maximum reduction of 4% = max (3%, 4%)
c [simplification-7] forced so keeping old conflict interval 6666
c [simplification-7] conflict limit remains at 13770 (hard 23770)
c [simplification-7] 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  180.5  261011  1786541     12639   22676  90676 180444   27   162  185  17%     24  144   67    4 1877%
c 
c [simplification-8] limit 13770 conflicts (hard 23770) hit after 13770 conflicts
c [quatres-4] found 255978 quaternary clauses 43% in total
c [quatres-4-1] removed 19 duplicate quaternary clauses
c [quatres-4-1] added 34 double-self-subsuming ternary resolvents
c [quatres-4-2] added 640 single-self-subsuming ternary resolvents
c [quatres-4-2] added 2308 quaternary resolvents
c [ternres-4] limit 12268880 with penalty 0 = 0 + 0
c [ternres-4] 52416 schedulable variables 20%
c [ternres-4] 53468 ternary resolvents (2387 bin, 51081 trn)
c [ternres-4] 3121 variables remain 1% (257890 retained 99%)
c [gauss-3] limit 1226888 penalty 1 = 1 + 0
c [gauss-3] extracted 4467 xors of average arity 3.0
c [gauss-3] connected 13266 occurrences of 5085 variables (average 2.6)
c [gauss-3] limit 1226888 penalty 1 = 1 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 754 variables
c [simpleprobe-4] 220380 schedulable variables 85%
c [simpleprobe-4] limit 49075523 penalty 0 = 0 + 0
c [decomp-19] removed 3134 variables
c [simpleprobe-4] 127500 variables remain 50% (129623 retained 50%)
c [simpleprobe-4] removed 3134 variables, found 90681 hbrs, 568 units
c [unhide-8] limit 306722 with penalty 3 = 0 + 3
c [unhide-8-8] 154 units, 301 failed, 27435 tauts, 0 hbrs, 34334 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1356 transitive binary clauses
c [transred-4] found 10 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 256639 variables 100%
c [elim-7] limit of 122688807 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 11102 not tried 4% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 14226 = 6% variables out of 256639 scheduled
c [bca-4] limit of 10000000 steps and 3410691 added (scaled 2)
c [bca-4] 442312 out of 484828 literals actually usable 91%
c [bca-4] added 1397 blocked clauses in 1378839 steps
c [sweep-4] limit 3680664 penalty 0 = 0 + 0
c [sweep-4-1] 87547 pos 36.3% + 153484 neg 63.7% = 241031 sched 99.4% ret 1382
c [sweep-4-1] 3705205 steps 98 queries 65790.39 avg class size
c [sweep-4-1] 1414 decisions 93 SAT calls 34.08 avg env size
c [sweep-4-1] 240521 variables remain 99% (1889 retained 1%)
c [decomp-20] removed 604 variables
c [sweep-4-1] removed 604 vars (0 failed, 11 eqs, 15 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 604 vars in TOTAL (1 rounds, 97 queries)
c [phase-count-8] 1620031 negative 95.2% of 1701238 except 81207 4.8%
c [phase-count-8] 1601776 positive 94.2% of 1701238 except 99462 5.8%
c [phase-8] phase bias: 386 positive 50%, 386 negative 50%
c [sort-queue-8] sorted 202990 enqueued variables after 13770 conflicts
c [score-dist-8] active 38819 (16%), one 0 (0%), zero 202990 (84%)
c [score-dist-8] max exp 526, different 24 (5%)
c [score-dist-8] median active exp 518, avg 518.6
c [simplification-8] removed 19202 variables 7.4% (241809 remain 21%)
c [simplification-8] removed 85303 irredundant clauses 4.8% (1701238 remain 36%)
c [simplification-8] maximum reduction of 7% = max (7%, 5%)
c [simplification-8] large reduction 7% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 25770 (soft 15770 + delta 10000)
c [simplification-8] new conflict limit 15770 (hard 25770)
c 
c [simplification-9] limit 15770 conflicts (hard 25770) hit after 15770 conflicts
c [quatres-5] found 254998 quaternary clauses 44% in total
c [quatres-5-1] removed 166 duplicate quaternary clauses
c [quatres-5-1] added 30 double-self-subsuming ternary resolvents
c [quatres-5-2] added 1035 single-self-subsuming ternary resolvents
c [quatres-5-2] added 3857 quaternary resolvents
c [ternres-5] limit 14832966 with penalty 0 = 0 + 0
c [ternres-5] 2823 schedulable variables 1%
c [ternres-5] 59795 ternary resolvents (2102 bin, 57693 trn)
c [ternres-5] 380 variables remain 0% (241429 retained 100%)
c [decomp-21] removed 394 variables
c [treelook-4] limit 1483296 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 113728 literals 24%
c [treelook-4] scheduling used 1483528 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1483296 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1500157 steps
c [treelook-4] 113341 literals remain 23%
c [treelook-4] 28771 variables remain to probed next time 12%
c [decomp-22] removed 21 variables
c [treelook-4] removed 34 variables, found 1874 hbrs
c [unhide-9] limit 370824 with penalty 3 = 0 + 3
c [unhide-9-9] 39 units, 127 failed, 15249 tauts, 0 hbrs, 15764 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1392 transitive binary clauses
c [transred-5] found 19 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 241181 variables 100%
c [block-4] limit of 74164832 steps penalty 1 = 1 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 6244 blocked clauses
c [block-4] 6244 < 1/100 * 1687513 = 16875 considered unsuccessful
c [elim-8] 1415 variables 1% will be scheduled this time
c [elim-8] scheduled 1415 variables 1%
c [elim-8] boosting limit by 20
c [elim-8] limit of 5933186580 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 289008020 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 5 = 0% variables out of 1415 scheduled
c [elim-8] 5 < 1/100 * 1415 = 14 considered unsuccessful
c [bca-5] limit of 10000000 steps and 3353062 added (scaled 2)
c [bca-5] 433096 out of 481836 literals actually usable 90%
c [bca-5] added 419 blocked clauses in 1351729 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 44498890 penalty 0 = 0 + 0
c [sweep-5-1] 88562 pos 37.0% + 150484 neg 63.0% = 239046 sched 99.2% ret 1871
c [sweep-5-1] 44545711 steps 1139 queries 37045.03 avg class size
c [sweep-5-1] 15330 decisions 1092 SAT calls 33.80 avg env size
c [sweep-5-1] 227952 variables remain 95% (12862 retained 5%)
c [decomp-23] removed 923 variables
c [sweep-5-1] removed 923 vars (0 failed, 191 eqs, 251 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 923 vars in TOTAL (1 rounds, 1138 queries)
c [phase-count-9] 1589104 negative 95.1% of 1670237 except 81133 4.9%
c [phase-count-9] 1571956 positive 94.1% of 1670237 except 98281 5.9%
c [phase-9] phase bias: 80 positive 38%, 128 negative 62%
c [sort-queue-9] sorted 194580 enqueued variables after 15770 conflicts
c [score-dist-9] active 45414 (19%), one 0 (0%), zero 194580 (81%)
c [score-dist-9] max exp 526, different 24 (5%)
c [score-dist-9] median active exp 518, avg 518.8
c [simplification-9] removed 1815 variables 0.8% (239994 remain 20%)
c [simplification-9] removed 31001 irredundant clauses 1.8% (1670237 remain 35%)
c [simplification-9] maximum reduction of 2% = max (1%, 2%)
c [simplification-9] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-9] new conflict interval 13332
c [simplification-9] penalized conflict interval 13332 = 1 * 13332
c [simplification-9] hard conflict limit 39102 (soft 29102 + delta 10000)
c [simplification-9] new conflict limit 29102 (hard 39102)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  245.3  239993  1670237     15918   27002 141573 208532   30   166  184  18%     34  142   14    5  271%
c i  254.5  239992  1670237     16848   27408 141581 208536   53   175  185  30%     16  148  159    7 2247%
c i  310.5  239991  1670237     24667   33173 141775 208643   51   185  191  28%     97  140   21   12  169%
c i  314.3  239989  1670237     25418   33821 141813 208660   47   183  191  26%     45  136   31   13  242%
c 
c [simplification-10] limit 29102 conflicts (hard 39102) hit after 29102 conflicts
c [quatres-6] found 255260 quaternary clauses 45% in total
c [quatres-6-1] removed 38 duplicate quaternary clauses
c [quatres-6-1] added 22 double-self-subsuming ternary resolvents
c [quatres-6-2] added 433 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1662 quaternary resolvents
c [ternres-6] limit 40007517 with penalty 0 = 0 + 0
c [ternres-6] 353 schedulable variables 0%
c [ternres-6] 102509 ternary resolvents (2029 bin, 100480 trn)
c [ternres-6] 8 variables remain 0% (239981 retained 100%)
c [card-4] limit 2500469 penalty 3 = 3 + 0
c [card-4] found 1367 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2500469 for elimination
c [card-4] 1367 out of 1367 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-24] removed 534 variables
c [basicprobe-4] limit 200037587 penalty 0 = 0 + 0
c [basicprobe-4-0] 127521 sched 56%, 7595 failed, 475 lifted, 261521 hbrs
c [decomp-25] removed 19343 variables
c [basicprobe-4-1] 82278 probes remain 38% after last round
c [basicprobe-4-1] 9341 units = 8784 failed (94%) + 557 lifted (6%)
c [basicprobe-4-1] removed 25684 variables, found 300172 hbrs
c [bate-2] eliminated 7701 asymmetric tautologies during probing
c [unhide-10] limit 1000187 with penalty 3 = 0 + 3
c [unhide-10-10] 66 units, 76 failed, 45775 tauts, 0 hbrs, 109935 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 2215 transitive binary clauses
c [transred-6] found 4 units
c [cce-3] limit of 50009396 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 2 clauses out of 3 (67%) of length 22
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 21
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 20
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 19
c [cce-3-1] eliminated 12 clauses out of 581 (2%) of length 18
c [cce-3-1] eliminated 23 clauses out of 714 (3%) of length 17
c [cce-3-1] eliminated 12 clauses out of 353 (3%) of length 16
c [cce-3-1] eliminated 15 clauses out of 1061 (1%) of length 15
c [cce-3-1] eliminated 49 clauses out of 1130 (4%) of length 14
c [cce-3-1] eliminated 826 clauses out of 2814 (29%) of length 13
c [cce-3-1] eliminated 2328 clauses out of 5463 (43%) of length 12
c [cce-3-1] eliminated 315 clauses out of 6729 (5%) of length 11
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 3590 large clauses in 50009449 steps
c [cce-3-1] allowing another 25004724 steps for small clauses
c [cce-3-1] scheduling 774539 clauses = 610002 binary + 164537 ternary
c [cce-3-1] tried to eliminate 9531 small clauses 1%
c [cce-3-1] eliminated 1961 binary clauses 0%
c [cce-3-1] eliminated 486 ternary clauses 0%
c [cce-3-1] eliminated 2447 small clauses 0%
c [cce-3-1] eliminated 3643 small clauses in 50009463 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 7233 covered clauses in round 1
c [cce-3] eliminated 7233 covered clauses in TOTAL during 1 rounds
c [cce-3] 7233 < 1/100 * 1456209 = 14562 considered unsuccessful
c [bca-6] limit of 10000000 steps and 2903927 added (scaled 2)
c [bca-6] 377596 out of 427256 literals actually usable 88%
c [bca-6] added 958 blocked clauses in 1140955 steps
c [sweep-6] limit 12002255 penalty 0 = 0 + 0
c [sweep-6-1] 72960 pos 36.0% + 129632 neg 64.0% = 202592 sched 94.8% ret 11035
c [sweep-6-1] 12028691 steps 382 queries 45763.49 avg class size
c [sweep-6-1] 4875 decisions 351 SAT calls 32.64 avg env size
c [sweep-6-1] 199458 variables remain 93% (14148 retained 7%)
c [decomp-26] removed 3728 variables
c [sweep-6-1] removed 3728 vars (0 failed, 36 eqs, 63 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 3728 vars in TOTAL (1 rounds, 381 queries)
c [phase-count-10] 1364030 negative 94.8% of 1439451 except 75421 5.2%
c [phase-count-10] 1344384 positive 93.4% of 1439451 except 95067 6.6%
c [phase-10] phase bias: 324 positive 56%, 254 negative 44%
c [sort-queue-10] sorted 159900 enqueued variables after 29102 conflicts
c [score-dist-10] active 49999 (24%), one 0 (0%), zero 159900 (76%)
c [score-dist-10] max exp 529, different 27 (5%)
c [score-dist-10] median active exp 521, avg 521.4
c [simplification-10] removed 30090 variables 12.5% (209899 remain 18%)
c [simplification-10] removed 230786 irredundant clauses 13.8% (1439451 remain 31%)
c [simplification-10] maximum reduction of 14% = max (13%, 14%)
c [simplification-10] large reduction 14% >= 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 41102 (soft 31102 + delta 10000)
c [simplification-10] new conflict limit 31102 (hard 41102)
c 
c [simplification-11] limit 31102 conflicts (hard 41102) hit after 31102 conflicts
c [quatres-7] found 227709 quaternary clauses 46% in total
c [quatres-7-1] removed 179 duplicate quaternary clauses
c [quatres-7-1] added 140 double-self-subsuming ternary resolvents
c [quatres-7-2] added 1425 single-self-subsuming ternary resolvents
c [quatres-7-2] added 3004 quaternary resolvents
c [ternres-7] limit 44778448 with penalty 0 = 0 + 0
c [ternres-7] 8 schedulable variables 0%
c [ternres-7] 30660 ternary resolvents (663 bin, 29997 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 2238922 penalty 2 = 2 + 0
c [gauss-4] extracted 6000 xors of average arity 3.0
c [gauss-4] connected 17908 occurrences of 6121 variables (average 2.9)
c [gauss-4] limit 2238922 penalty 2 = 2 + 0
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-27] removed 168 variables
c [simpleprobe-5] 101152 schedulable variables 48%
c [simpleprobe-5] limit 179113792 penalty 0 = 0 + 0
c [decomp-28] removed 6611 variables
c [simpleprobe-5] 45333 variables remain 22% (157787 retained 78%)
c [simpleprobe-5] removed 6611 variables, found 226031 hbrs, 421 units
c [unhide-11] limit 2238922 with penalty 2 = 0 + 2
c [unhide-11-11] 19 units, 20 failed, 21064 tauts, 0 hbrs, 29753 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 2880 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 202995 variables 100%
c [elim-9] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 277 not tried 0% in round 1
c [gc-83] reconnected 456641 binary clauses (produced 0 empty 1 units)
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 18363 = 9% variables out of 202995 scheduled
c [bca-7] limit of 10000000 steps and 2613424 added (scaled 2)
c [bca-7] 323440 out of 369266 literals actually usable 88%
c [bca-7] added 1828 blocked clauses in 1022842 steps
c [sweep-7] limit 13433534 penalty 0 = 0 + 0
c [sweep-7-1] 61134 pos 35.5% + 110920 neg 64.5% = 172054 sched 93.2% ret 12578
c [sweep-7-1] 13450930 steps 422 queries 30308.05 avg class size
c [sweep-7-1] 5855 decisions 408 SAT calls 39.65 avg env size
c [sweep-7-1] 167886 variables remain 91% (16663 retained 9%)
c [decomp-29] removed 544 variables
c [sweep-7-1] removed 544 vars (0 failed, 60 eqs, 67 impls)
c [sweep-7] removed 544 vars in TOTAL (1 rounds, 421 queries)
c [phase-count-11] 1233017 negative 94.8% of 1301248 except 68231 5.2%
c [phase-count-11] 1213509 positive 93.3% of 1301248 except 87739 6.7%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 258 positive 40%, 387 negative 60%
c [sort-queue-11] sorted 137740 enqueued variables after 31102 conflicts
c [score-dist-11] active 46348 (25%), one 0 (0%), zero 137740 (75%)
c [score-dist-11] max exp 529, different 26 (5%)
c [score-dist-11] median active exp 522, avg 521.6
c [simplification-11] removed 25811 variables 12.3% (184088 remain 16%)
c [simplification-11] removed 138203 irredundant clauses 9.6% (1301248 remain 28%)
c [simplification-11] maximum reduction of 12% = max (12%, 10%)
c [simplification-11] large reduction 12% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 43102 (soft 33102 + delta 10000)
c [simplification-11] new conflict limit 33102 (hard 43102)
c 
c [simplification-12] limit 33102 conflicts (hard 43102) hit after 33102 conflicts
c [quatres-8] found 217650 quaternary clauses 46% in total
c [quatres-8-1] removed 1391 duplicate quaternary clauses
c [quatres-8-1] added 20 double-self-subsuming ternary resolvents
c [quatres-8-2] added 323 single-self-subsuming ternary resolvents
c [quatres-8-2] added 3875 quaternary resolvents
c [ternres-8] limit 47954415 with penalty 0 = 0 + 0
c [ternres-8] all 184088 free variables schedulable
c [ternres-8] 40331 ternary resolvents (1549 bin, 38782 trn)
c [ternres-8] 684 variables remain 0% (183404 retained 100%)
c [decomp-30] removed 293 variables
c [treelook-5] limit 4795441 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 148000 literals 40%
c [treelook-5] scheduling used 3307160 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 4795441 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 4799817 steps
c [treelook-5] 146916 literals remain 40%
c [treelook-5] 20578 variables remain to probed next time 11%
c [decomp-31] removed 119 variables
c [treelook-5] removed 158 variables, found 3943 hbrs
c [unhide-12] limit 2397720 with penalty 2 = 0 + 2
c [unhide-12-12] 28 units, 221 failed, 61797 tauts, 0 hbrs, 28453 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2285 transitive binary clauses
c [transred-8] found 2 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 183517 variables 100%
c [block-5] limit of 119886039 steps penalty 2 = 2 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 3545 blocked clauses
c [block-5] 3545 < 1/100 * 1298455 = 12984 considered unsuccessful
c [elim-10] 277 variables 0% will be scheduled this time
c [elim-10] scheduled 277 variables 0%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] no variable eliminated in round 1 in 59097865 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 10 = 4% variables out of 277 scheduled
c [elim-10] 10 < 1/100 * 277 = 2 considered unsuccessful
c [bca-8] limit of 10000000 steps and 2594482 added (scaled 2)
c [bca-8] 316534 out of 366774 literals actually usable 86%
c [bca-8] added 796 blocked clauses in 992439 steps
c [sweep-8] limit 14386324 penalty 0 = 0 + 0
c [sweep-8-1] 59505 pos 35.7% + 107316 neg 64.3% = 166821 sched 91.0% ret 16565
c [sweep-8-1] 14415882 steps 510 queries 35738.18 avg class size
c [sweep-8-1] 6936 decisions 489 SAT calls 36.78 avg env size
c [sweep-8-1] 162763 variables remain 89% (20614 retained 11%)
c [decomp-32] removed 400 variables
c [sweep-8-1] removed 400 vars (0 failed, 85 eqs, 90 impls)
c [sweep-8] removed 400 vars in TOTAL (1 rounds, 509 queries)
c [phase-count-12] 1223263 negative 94.6% of 1292423 except 69160 5.4%
c [phase-count-12] 1204247 positive 93.2% of 1292423 except 88176 6.8%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 104 positive 44%, 133 negative 56%
c [sort-queue-12] sorted 135184 enqueued variables after 33102 conflicts
c [score-dist-12] active 47802 (26%), one 0 (0%), zero 135184 (74%)
c [score-dist-12] max exp 529, different 26 (5%)
c [score-dist-12] median active exp 522, avg 521.7
c [simplification-12] removed 1102 variables 0.6% (182986 remain 16%)
c [simplification-12] removed 8825 irredundant clauses 0.7% (1292423 remain 27%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-12] new conflict interval 23332
c [simplification-12] penalized conflict interval 23332 = 1 * 23332
c [simplification-12] hard conflict limit 68100 (soft 56434 + delta 11666)
c [simplification-12] new conflict limit 56434 (hard 68100)
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  588.0  182985  1292423     49188   37534 129615 337555   52   152  177  34%    293   77   16   36   45%
c 
c [simplification-13] limit 56434 conflicts (hard 68100) hit after 56434 conflicts
c [quatres-9] found 217820 quaternary clauses 46% in total
c [quatres-9-1] removed 25 duplicate quaternary clauses
c [quatres-9-1] added 21 double-self-subsuming ternary resolvents
c [quatres-9-2] added 530 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1233 quaternary resolvents
c [ternres-9] limit 78788893 with penalty 0 = 0 + 0
c [ternres-9] 672 schedulable variables 0%
c [ternres-9] 32295 ternary resolvents (1187 bin, 31108 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-5] limit 7878889 penalty 1 = 1 + 0
c [gauss-5] extracted 17068 xors of average arity 3.0
c [gauss-5] connected 50959 occurrences of 12972 variables (average 3.9)
c [gauss-5] limit 7878889 penalty 1 = 1 + 0
c [gauss-5] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-33] removed 251 variables
c [basicprobe-5] limit 393944469 penalty 0 = 0 + 0
c [basicprobe-5-0] 68049 sched 38%, 1584 failed, 183 lifted, 46188 hbrs
c [decomp-34] removed 6022 variables
c [basicprobe-5-1] 115032 sched 66%, 1385 failed, 123 lifted, 32178 hbrs
c [decomp-35] removed 4115 variables
c [basicprobe-5-2] 110990 sched 65%, 277 failed, 13 lifted, 7615 hbrs
c [decomp-36] removed 994 variables
c [basicprobe-5-3] 8055 probes remain 5% after last round
c [basicprobe-5-3] 3636 units = 3309 failed (91%) + 327 lifted (9%)
c [basicprobe-5-3] removed 11202 variables, found 88200 hbrs
c [bate-3] eliminated 7569 asymmetric tautologies during probing
c [unhide-13] limit 3939444 with penalty 2 = 0 + 2
c [unhide-13-13] 0 units, 1 failed, 13188 tauts, 0 hbrs, 48825 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 2713 transitive binary clauses
c [bca-9] limit of 10000000 steps and 2387702 added (scaled 2)
c [bca-9] 289212 out of 343064 literals actually usable 84%
c [bca-9] added 196 blocked clauses in 912776 steps
c [sweep-9] limit 23636668 penalty 0 = 0 + 0
c [sweep-9-1] 56000 pos 36.7% + 96574 neg 63.3% = 152574 sched 88.9% ret 18957
c [sweep-9-1] 23669333 steps 824 queries 22337.01 avg class size
c [sweep-9-1] 11545 decisions 762 SAT calls 41.72 avg env size
c [sweep-9-1] 144041 variables remain 84% (27489 retained 16%)
c [decomp-37] removed 432 variables
c [sweep-9-1] removed 432 vars (0 failed, 123 eqs, 135 impls)
c [sweep-9] removed 432 vars in TOTAL (1 rounds, 823 queries)
c [phase-count-13] 1123844 negative 94.5% of 1188982 except 65138 5.5%
c [phase-count-13] 1103203 positive 92.8% of 1188982 except 85779 7.2%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 64 positive 42%, 88 negative 58%
c [sort-queue-13] sorted 116511 enqueued variables after 56434 conflicts
c [score-dist-13] active 54588 (32%), one 0 (0%), zero 116511 (68%)
c [score-dist-13] max exp 531, different 27 (5%)
c [score-dist-13] median active exp 523, avg 522.5
c [simplification-13] removed 11886 variables 6.5% (171099 remain 15%)
c [simplification-13] removed 103441 irredundant clauses 8.0% (1188982 remain 25%)
c [simplification-13] maximum reduction of 8% = max (6%, 8%)
c [simplification-13] large reduction 8% >= 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 68434 (soft 58434 + delta 10000)
c [simplification-13] new conflict limit 58434 (hard 68434)
c 
c [simplification-14] limit 58434 conflicts (hard 68434) hit after 58434 conflicts
c [quatres-10] found 198437 quaternary clauses 46% in total
c [quatres-10-1] removed 137 duplicate quaternary clauses
c [quatres-10-1] added 21 double-self-subsuming ternary resolvents
c [quatres-10-2] added 675 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1160 quaternary resolvents
c [ternres-10] limit 82563745 with penalty 0 = 0 + 0
c [ternres-10] all 171099 free variables schedulable
c [ternres-10] 20020 ternary resolvents (605 bin, 19415 trn)
c [ternres-10] 3 variables remain 0% (171096 retained 100%)
c [gauss-6] limit 16512749 penalty 0 = 0 + 0
c [gauss-6] extracted 35056 xors of average arity 3.0
c [gauss-6] connected 104793 occurrences of 16278 variables (average 6.4)
c [gauss-6] limit 16512749 penalty 0 = 0 + 0
c [decomp-38] removed 102 variables
c [gauss-6] exported 0 unary, 3 binary and 1 ternary equations
c [simpleprobe-6] 36529 schedulable variables 21%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-40] removed 2818 variables
c [simpleprobe-6] 18665 variables remain 11% (149514 retained 89%)
c [simpleprobe-6] removed 2818 variables, found 122794 hbrs, 29 units
c [unhide-14] limit 4128187 with penalty 2 = 0 + 2
c [unhide-14-14] 4 units, 14 failed, 79190 tauts, 0 hbrs, 93407 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2308 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 516023407 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 23
c [cce-4-1] eliminated 3 clauses out of 1119 (0%) of length 15
c [cce-4-1] eliminated 21 clauses out of 1114 (2%) of length 14
c [cce-4-1] eliminated 15 clauses out of 1826 (1%) of length 13
c [cce-4-1] eliminated 41 clauses out of 3153 (1%) of length 12
c [cce-4-1] eliminated 284 clauses out of 4682 (6%) of length 11
c [cce-4-1] eliminated 3257 clauses out of 9860 (33%) of length 10
c [cce-4-1] eliminated 3148 clauses out of 11424 (28%) of length 9
c [cce-4-1] eliminated 3944 clauses out of 19343 (20%) of length 8
c [cce-4-1] eliminated 4121 clauses out of 24872 (17%) of length 7
c [cce-4-1] eliminated 6571 clauses out of 45580 (14%) of length 6
c [cce-4-1] eliminated 18648 clauses out of 95819 (19%) of length 5
c [cce-4-1] eliminated 23668 clauses out of 175896 (13%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 63722 large clauses in 516023441 steps
c [cce-4-1] allowing another 258011720 steps for small clauses
c [cce-4-1] scheduling 635686 clauses = 477420 binary + 158266 ternary
c [cce-4-1] tried to eliminate 150756 small clauses 24%
c [cce-4-1] eliminated 15986 binary clauses 3%
c [cce-4-1] eliminated 5729 ternary clauses 4%
c [cce-4-1] eliminated 21715 small clauses 3%
c [cce-4-1] eliminated 21969 small clauses in 516023407 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 85691 covered clauses in round 1
c [cce-4] eliminated 85691 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 168166 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 21578 variables 13% in round 1 in 311889017 steps
c [elim-11-1] backward subsumption/strengthening limit 88110983
c [elim-11-1-1] backward checking 78010 touched variables 46%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 828 and strengthened 1191 clauses in 48784394 steps
c [elim-11-1] rescheduled 5778 variables 3% by backward subsumption
c [elim-11-2] eliminated 273 variables 0% in round 2 in 37846603 steps
c [elim-11-2] backward subsumption/strengthening limit 1479986
c [elim-11-2-1] backward checking 2200 touched variables 1%
c [elim-11-2-1] incomplete backward checking 1753 remain 80%
c [elim-11-2] subsumed 29 and strengthened 69 clauses in 1480036 steps
c [elim-11] incomplete 212 not tried 0% in round 2
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 21862 = 13% variables out of 168166 scheduled
c [bca-10] limit of 10000000 steps and 2028012 added (scaled 2)
c [bca-10] 247772 out of 292610 literals actually usable 85%
c [bca-10] added 3787 blocked clauses in 778485 steps
c [sweep-10] limit 24769123 penalty 0 = 0 + 0
c [sweep-10-1] 44368 pos 36.2% + 78312 neg 63.8% = 122680 sched 83.9% ret 23624
c [sweep-10-1] 24795410 steps 942 queries 13389.40 avg class size
c [sweep-10-1] 14047 decisions 911 SAT calls 36.69 avg env size
c [sweep-10-1] 112593 variables remain 77% (33673 retained 23%)
c [decomp-41] removed 434 variables
c [sweep-10-1] removed 434 vars (0 failed, 129 eqs, 124 impls)
c [sweep-10] removed 434 vars in TOTAL (1 rounds, 941 queries)
c [phase-count-14] 949436 negative 94.1% of 1008537 except 59101 5.9%
c [phase-count-14] 935341 positive 92.7% of 1008537 except 73196 7.3%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 101 positive 47%, 115 negative 53%
c [sort-queue-14] sorted 94822 enqueued variables after 58434 conflicts
c [score-dist-14] active 51048 (35%), one 0 (0%), zero 94822 (65%)
c [score-dist-14] max exp 531, different 27 (5%)
c [score-dist-14] median active exp 523, avg 522.6
c [simplification-14] removed 25229 variables 14.7% (145870 remain 12%)
c [simplification-14] removed 180445 irredundant clauses 15.2% (1008537 remain 21%)
c [simplification-14] maximum reduction of 15% = max (15%, 15%)
c [simplification-14] large reduction 15% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 70434 (soft 60434 + delta 10000)
c [simplification-14] new conflict limit 60434 (hard 70434)
c 
c [simplification-15] limit 60434 conflicts (hard 70434) hit after 60435 conflicts
c [quatres-11] found 168190 quaternary clauses 47% in total
c [quatres-11-1] removed 217 duplicate quaternary clauses
c [quatres-11-1] added 150 double-self-subsuming ternary resolvents
c [quatres-11-2] added 883 single-self-subsuming ternary resolvents
c [quatres-11-2] added 4352 quaternary resolvents
c [ternres-11] limit 83710312 with penalty 0 = 0 + 0
c [ternres-11] 3 schedulable variables 0%
c [ternres-11] 426 ternary resolvents (7 bin, 419 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 2615947 penalty 4 = 4 + 0
c [card-5] found 1773 at-most-one constraints of average size 3.3
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2615947 for elimination
c [card-5] 1773 out of 1773 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-7] limit 16742062 penalty 0 = 0 + 0
c [gauss-7] extracted 34434 xors of average arity 3.0
c [gauss-7] connected 103270 occurrences of 14804 variables (average 7.0)
c [gauss-7] limit 16742062 penalty 0 = 0 + 0
c [decomp-42] removed 8 variables
c [gauss-7] exported 0 unary, 4 binary and 0 ternary equations
c [decomp-43] removed 1 variables
c [treelook-6] limit 8371031 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 121420 literals 42%
c [treelook-6] scheduling used 2657094 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 8371031 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 8393390 steps
c [treelook-6] 121005 literals remain 41%
c [treelook-6] 16789 variables remain to probed next time 12%
c [decomp-44] removed 34 variables
c [treelook-6] removed 42 variables, found 29225 hbrs
c [unhide-15] limit 4185515 with penalty 2 = 0 + 2
c [unhide-15-15] 4 units, 4 failed, 5916 tauts, 0 hbrs, 6587 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 2630 transitive binary clauses
c [transred-11] found 2 units
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 145810 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 2472 variables 2% in round 1 in 293417498 steps
c [elim-12-1] backward subsumption/strengthening limit 293417400
c [elim-12-1-1] backward checking 17204 touched variables 12%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 99 and strengthened 117 clauses in 23419546 steps
c [elim-12-1] rescheduled 642 variables 0% by backward subsumption
c [elim-12-2] eliminated 39 variables 0% in round 2 in 4293790 steps
c [elim-12-2] backward subsumption/strengthening limit 4293700
c [elim-12-2-1] backward checking 298 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 22 and strengthened 29 clauses in 706440 steps
c [elim-12-2] rescheduled 117 variables 0% by backward subsumption
c [elim-12-3] eliminated 8 variables 0% in round 3 in 575899 steps
c [elim-12-3] backward subsumption/strengthening limit 575800
c [elim-12-3-1] backward checking 48 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 2 and strengthened 4 clauses in 463201 steps
c [elim-12] incomplete 27 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 2519 = 2% variables out of 145810 scheduled
c [bca-11] limit of 10000000 steps and 1995922 added (scaled 2)
c [bca-11] 236512 out of 286584 literals actually usable 83%
c [bca-11] added 521 blocked clauses in 750083 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 251130930 penalty 0 = 0 + 0
c [sweep-11-1] 39477 pos 35.8% + 70880 neg 64.2% = 110357 sched 77.0% ret 32934
c [sweep-11-1] 251147530 steps 11111 queries 1895.09 avg class size
c [sweep-11-1] 113679 decisions 10347 SAT calls 28.11 avg env size
c [sweep-11-1] 25015 variables remain 18% (117794 retained 82%)
c [decomp-45] removed 3592 variables
c [sweep-11-1] removed 3592 vars (0 failed, 2625 eqs, 2386 impls)
c [sweep-11] removed 3592 vars in TOTAL (1 rounds, 11110 queries)
c [phase-count-15] 920309 negative 93.8% of 981344 except 61035 6.2%
c [phase-count-15] 905471 positive 92.3% of 981344 except 75873 7.7%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 11 positive 19%, 46 negative 81%
c [sort-queue-15] sorted 73560 enqueued variables after 60435 conflicts
c [score-dist-15] active 66139 (47%), one 0 (0%), zero 73560 (53%)
c [score-dist-15] max exp 531, different 26 (5%)
c [score-dist-15] median active exp 520, avg 521.9
c [simplification-15] removed 6171 variables 4.2% (139699 remain 12%)
c [simplification-15] removed 27193 irredundant clauses 2.7% (981344 remain 21%)
c [simplification-15] maximum reduction of 4% = max (4%, 3%)
c [simplification-15] geometric conflict interval increment 4666 = 23332 / 5
c [simplification-15] new conflict interval 27998
c [simplification-15] penalized conflict interval 27998 = 1 * 27998
c [simplification-15] hard conflict limit 102432 (soft 88433 + delta 13999)
c [simplification-15] new conflict limit 88433 (hard 102432)
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  793.3  139698   981344     66905   43644 109595 310631   57   131  158  44%    178   32   13   40   33%
c 
c [simplification-16] limit 88433 conflicts (hard 102432) hit after 88434 conflicts
c [quatres-12] found 168171 quaternary clauses 47% in total
c [quatres-12-1] removed 191 duplicate quaternary clauses
c [quatres-12-1] added 54 double-self-subsuming ternary resolvents
c [quatres-12-2] added 651 single-self-subsuming ternary resolvents
c [quatres-12-2] added 1954 quaternary resolvents
c [ternres-12] limit 109202784 with penalty 0 = 0 + 0
c [ternres-12] all 139698 free variables schedulable
c [ternres-12] 26398 ternary resolvents (1167 bin, 25231 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-8] limit 21840556 penalty 0 = 0 + 0
c [gauss-8] extracted 42345 xors of average arity 3.0
c [gauss-8] connected 126435 occurrences of 14704 variables (average 8.6)
c [gauss-8] limit 21840556 penalty 0 = 0 + 0
c [decomp-46] removed 99 variables
c [gauss-8] exported 0 unary, 1 binary and 3 ternary equations
c [decomp-47] removed 8 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 12145 sched 9%, 162 failed, 14 lifted, 5275 hbrs
c [decomp-48] removed 556 variables
c [basicprobe-6-1] 87807 sched 64%, 932 failed, 22 lifted, 26770 hbrs
c [decomp-49] removed 2882 variables
c [basicprobe-6-2] 86047 sched 63%, 224 failed, 13 lifted, 5177 hbrs
c [decomp-50] removed 451 variables
c [basicprobe-6-3] 41930 probes remain 31% after last round
c [basicprobe-6-3] 1404 units = 1348 failed (96%) + 56 lifted (4%)
c [basicprobe-6-3] removed 3930 variables, found 38395 hbrs
c [bate-4] eliminated 2735 asymmetric tautologies during probing
c [unhide-16] limit 5000000 with penalty 2 = 0 + 2
c [unhide-16-16] 0 units, 7 failed, 43571 tauts, 0 hbrs, 228986 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 2327 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 135656 variables 100%
c [block-6] limit of 100000000 steps penalty 3 = 3 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 3851 blocked clauses
c [block-6] 3851 < 1/100 * 937624 = 9376 considered unsuccessful
c [cce-5] limit of 136503481 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 20
c [cce-5-1] eliminated 1 clauses out of 81 (1%) of length 19
c [cce-5-1] eliminated 3 clauses out of 463 (1%) of length 18
c [cce-5-1] eliminated 1 clauses out of 481 (0%) of length 16
c [cce-5-1] eliminated 83 clauses out of 912 (9%) of length 15
c [cce-5-1] eliminated 102 clauses out of 881 (12%) of length 14
c [cce-5-1] eliminated 221 clauses out of 1506 (15%) of length 13
c [cce-5-1] eliminated 293 clauses out of 2155 (14%) of length 12
c [cce-5-1] eliminated 342 clauses out of 2395 (14%) of length 11
c [cce-5-1] eliminated 1010 clauses out of 5175 (20%) of length 10
c [cce-5-1] eliminated 1115 clauses out of 10203 (11%) of length 9
c [cce-5-1] eliminated 1965 clauses out of 16425 (12%) of length 8
c [cce-5-1] eliminated 3536 clauses out of 20754 (17%) of length 7
c [cce-5-1] eliminated 51 clauses out of 39383 (0%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 8726 large clauses in 136503566 steps
c [cce-5-1] allowing another 68251783 steps for small clauses
c [cce-5-1] scheduling 494747 clauses = 358829 binary + 135918 ternary
c [cce-5-1] tried to eliminate 39853 small clauses 8%
c [cce-5-1] eliminated 6346 binary clauses 2%
c [cce-5-1] eliminated 1970 ternary clauses 1%
c [cce-5-1] eliminated 8316 small clauses 2%
c [cce-5-1] eliminated 8316 small clauses in 136503565 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 17042 covered clauses in round 1
c [cce-5] eliminated 17042 covered clauses in TOTAL during 1 rounds
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 135481 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 5554 variables 4% in round 1 in 257111155 steps
c [elim-13-1] backward subsumption/strengthening limit 257111100
c [elim-13-1-1] backward checking 37321 touched variables 28%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 395 and strengthened 543 clauses in 32566851 steps
c [elim-13-1] rescheduled 2239 variables 2% by backward subsumption
c [elim-13-2] eliminated 61 variables 0% in round 2 in 15456177 steps
c [elim-13-2] backward subsumption/strengthening limit 15456100
c [elim-13-2-1] backward checking 621 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 32 and strengthened 37 clauses in 1751932 steps
c [elim-13-2] rescheduled 170 variables 0% by backward subsumption
c [elim-13-3] eliminated 4 variables 0% in round 3 in 1824275 steps
c [elim-13-3] backward subsumption/strengthening limit 1824200
c [elim-13-3-1] backward checking 55 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 1 and strengthened 3 clauses in 596399 steps
c [elim-13] incomplete 9 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 5619 = 4% variables out of 135481 scheduled
c [bca-12] limit of 10000000 steps and 1795538 added (scaled 2)
c [bca-12] 204850 out of 259726 literals actually usable 79%
c [bca-12] added 1941 blocked clauses in 657546 steps
c [sweep-12] limit 32760835 penalty 0 = 0 + 0
c [sweep-12-1] 8329 pos 38.1% + 13508 neg 61.9% = 21837 sched 16.8% ret 108025
c [sweep-12-1] 32761457 steps 4216 queries 836.46 avg class size
c [sweep-12-1] 32497 decisions 3674 SAT calls 25.11 avg env size
c [sweep-12-1] 10861 variables remain 8% (118904 retained 92%)
c [decomp-51] removed 1579 variables
c [sweep-12-1] removed 1579 vars (0 failed, 1166 eqs, 1079 impls)
c [sweep-12] removed 1579 vars in TOTAL (1 rounds, 4215 queries)
c [phase-count-16] 834368 negative 93.8% of 889616 except 55248 6.2%
c [phase-count-16] 816568 positive 91.8% of 889616 except 73048 8.2%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 14 positive 58%, 10 negative 42%
c [sort-queue-16] sorted 63337 enqueued variables after 88434 conflicts
c [score-dist-16] active 64946 (51%), one 0 (0%), zero 63337 (49%)
c [score-dist-16] max exp 532, different 25 (5%)
c [score-dist-16] median active exp 521, avg 522.6
c [simplification-16] removed 11415 variables 8.2% (128283 remain 11%)
c [simplification-16] removed 91728 irredundant clauses 9.3% (889616 remain 19%)
c [simplification-16] maximum reduction of 9% = max (8%, 9%)
c [simplification-16] large reduction 9% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 100434 (soft 90434 + delta 10000)
c [simplification-16] new conflict limit 90434 (hard 100434)
c 
c [simplification-17] limit 90434 conflicts (hard 100434) hit after 90434 conflicts
c [quatres-13] found 158451 quaternary clauses 48% in total
c [quatres-13-1] removed 97 duplicate quaternary clauses
c [quatres-13-1] added 23 double-self-subsuming ternary resolvents
c [quatres-13-2] added 622 single-self-subsuming ternary resolvents
c [quatres-13-2] added 1911 quaternary resolvents
c [ternres-13] limit 109977862 with penalty 0 = 0 + 0
c [ternres-13] all 128283 free variables schedulable
c [ternres-13] 19010 ternary resolvents (661 bin, 18349 trn)
c [ternres-13] fully completed ternary resolution
c [gauss-9] limit 21995572 penalty 0 = 0 + 0
c [gauss-9] extracted 42444 xors of average arity 3.0
c [gauss-9] connected 126830 occurrences of 13117 variables (average 9.7)
c [gauss-9] limit 21995572 penalty 0 = 0 + 0
c [decomp-52] removed 57 variables
c [gauss-9] exported 0 unary, 1 binary and 5 ternary equations
c [simpleprobe-7] 13015 schedulable variables 10%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-54] removed 1925 variables
c [simpleprobe-7] 9150 variables remain 7% (117151 retained 93%)
c [simpleprobe-7] removed 1925 variables, found 109057 hbrs, 82 units
c [unhide-17] limit 5000000 with penalty 2 = 0 + 2
c [unhide-17-17] 2 units, 1 failed, 7533 tauts, 0 hbrs, 27856 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 2895 transitive binary clauses
c [transred-13] found 3 units
c [cce-6] limit of 274944655 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 2 clauses out of 563 (0%) of length 16
c [cce-6-1] eliminated 30 clauses out of 836 (4%) of length 15
c [cce-6-1] eliminated 27 clauses out of 689 (4%) of length 14
c [cce-6-1] eliminated 49 clauses out of 1307 (4%) of length 13
c [cce-6-1] eliminated 66 clauses out of 2031 (3%) of length 12
c [cce-6-1] eliminated 54 clauses out of 2078 (3%) of length 11
c [cce-6-1] eliminated 92 clauses out of 4218 (2%) of length 10
c [cce-6-1] eliminated 152 clauses out of 9020 (2%) of length 9
c [cce-6-1] eliminated 200 clauses out of 13963 (1%) of length 8
c [cce-6-1] eliminated 493 clauses out of 17274 (3%) of length 7
c [cce-6-1] eliminated 3500 clauses out of 38597 (9%) of length 6
c [cce-6-1] eliminated 6487 clauses out of 71266 (9%) of length 5
c [cce-6-1] eliminated 334 clauses out of 134661 (0%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 11486 large clauses in 274944658 steps
c [cce-6-1] allowing another 137472329 steps for small clauses
c [cce-6-1] scheduling 453405 clauses = 322925 binary + 130480 ternary
c [cce-6-1] tried to eliminate 90995 small clauses 20%
c [cce-6-1] eliminated 6184 binary clauses 2%
c [cce-6-1] eliminated 3132 ternary clauses 2%
c [cce-6-1] eliminated 9316 small clauses 2%
c [cce-6-1] eliminated 9392 small clauses in 274944655 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 20878 covered clauses in round 1
c [cce-6] eliminated 20878 covered clauses in TOTAL during 1 rounds
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 126295 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 3644 variables 3% in round 1 in 234326742 steps
c [elim-14-1] backward subsumption/strengthening limit 234326700
c [elim-14-1-1] backward checking 27091 touched variables 21%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 590 and strengthened 522 clauses in 27465907 steps
c [elim-14-1] rescheduled 2690 variables 2% by backward subsumption
c [elim-14-2] eliminated 75 variables 0% in round 2 in 29012853 steps
c [elim-14-2] backward subsumption/strengthening limit 29012800
c [elim-14-2-1] backward checking 709 touched variables 1%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 51 and strengthened 69 clauses in 1666322 steps
c [elim-14-2] rescheduled 272 variables 0% by backward subsumption
c [elim-14-3] eliminated 6 variables 0% in round 3 in 2205622 steps
c [elim-14-3] backward subsumption/strengthening limit 2205600
c [elim-14-3-1] backward checking 142 touched variables 0%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 11 and strengthened 5 clauses in 613121 steps
c [elim-14] incomplete 35 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 3725 = 3% variables out of 126295 scheduled
c [bca-13] limit of 10000000 steps and 1680775 added (scaled 2)
c [bca-13] 190079 out of 245142 literals actually usable 78%
c [bca-13] added 669 blocked clauses in 610974 steps
c [sweep-13] limit 32993358 penalty 0 = 0 + 0
c [sweep-13-1] 3884 pos 39.4% + 5970 neg 60.6% = 9854 sched 8.0% ret 112716
c [sweep-13-1] 26846509 steps 5483 queries 334.87 avg class size
c [sweep-13-1] 40437 decisions 4885 SAT calls 22.80 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-55] removed 1778 variables
c [sweep-13-1] removed 1778 vars (0 failed, 1552 eqs, 1185 impls)
c [sweep-13-2] 44285 pos 36.7% + 76507 neg 63.3% = 120792 sched 100.0% ret 0
c [sweep-13-2] 6159022 steps 221 queries 26070.00 avg class size
c [sweep-13-2] 3270 decisions 228 SAT calls 41.75 avg env size
c [sweep-13-2] 118150 variables remain 98% (2642 retained 2%)
c [decomp-56] removed 24 variables
c [sweep-13-2] removed 24 vars (0 failed, 17 eqs, 13 impls)
c [sweep-13] removed 1802 vars in TOTAL (2 rounds, 5702 queries)
c [phase-count-17] 777858 negative 93.6% of 831168 except 53310 6.4%
c [phase-count-17] 760545 positive 91.5% of 831168 except 70623 8.5%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 3 positive 33%, 6 negative 67%
c [sort-queue-17] sorted 56930 enqueued variables after 90434 conflicts
c [score-dist-17] active 63838 (53%), one 0 (0%), zero 56930 (47%)
c [score-dist-17] max exp 532, different 25 (5%)
c [score-dist-17] median active exp 521, avg 522.6
c [simplification-17] removed 7515 variables 5.9% (120768 remain 10%)
c [simplification-17] removed 58448 irredundant clauses 6.6% (831168 remain 18%)
c [simplification-17] maximum reduction of 7% = max (6%, 7%)
c [simplification-17] large reduction 7% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 102434 (soft 92434 + delta 10000)
c [simplification-17] new conflict limit 92434 (hard 102434)
c 
c [simplification-18] limit 92434 conflicts (hard 102434) hit after 92434 conflicts
c [quatres-14] found 154754 quaternary clauses 49% in total
c [quatres-14-1] removed 149 duplicate quaternary clauses
c [quatres-14-1] added 43 double-self-subsuming ternary resolvents
c [quatres-14-2] added 589 single-self-subsuming ternary resolvents
c [quatres-14-2] added 1438 quaternary resolvents
c [ternres-14] limit 111550935 with penalty 0 = 0 + 0
c [ternres-14] all 120768 free variables schedulable
c [ternres-14] 10518 ternary resolvents (268 bin, 10250 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-10] limit 22310187 penalty 0 = 0 + 0
c [gauss-10] extracted 40602 xors of average arity 3.0
c [gauss-10] connected 121429 occurrences of 12786 variables (average 9.5)
c [gauss-10] limit 22310187 penalty 0 = 0 + 0
c [gauss-10] exported 0 unary, 0 binary and 5 ternary equations
c [decomp-57] removed 29 variables
c [treelook-7] limit 11155093 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 109002 literals 45%
c [treelook-7] scheduling used 2402077 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 11155093 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 11159758 steps
c [treelook-7] 108231 literals remain 45%
c [treelook-7] 14132 variables remain to probed next time 12%
c [decomp-58] removed 40 variables
c [treelook-7] removed 50 variables, found 24247 hbrs
c [unhide-18] limit 5000000 with penalty 2 = 0 + 2
c [unhide-18-18] 9 units, 162 failed, 65943 tauts, 0 hbrs, 72613 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 2029 transitive binary clauses
c [cce-7] limit of 557754676 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 426 (0%) of length 18
c [cce-7-1] eliminated 1 clauses out of 767 (0%) of length 15
c [cce-7-1] eliminated 6 clauses out of 605 (1%) of length 14
c [cce-7-1] eliminated 28 clauses out of 1163 (2%) of length 13
c [cce-7-1] eliminated 32 clauses out of 1932 (2%) of length 12
c [cce-7-1] eliminated 76 clauses out of 1692 (4%) of length 11
c [cce-7-1] eliminated 119 clauses out of 2915 (4%) of length 10
c [cce-7-1] eliminated 108 clauses out of 8301 (1%) of length 9
c [cce-7-1] eliminated 163 clauses out of 15248 (1%) of length 8
c [cce-7-1] eliminated 588 clauses out of 17204 (3%) of length 7
c [cce-7-1] eliminated 1844 clauses out of 34441 (5%) of length 6
c [cce-7-1] eliminated 4976 clauses out of 63339 (8%) of length 5
c [cce-7-1] eliminated 20797 clauses out of 131018 (16%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 28739 large clauses in 377611295 steps
c [cce-7-1] allowing another 188805647 steps for small clauses
c [cce-7-1] scheduling 430081 clauses = 305308 binary + 124773 ternary
c [cce-7-1] tried to eliminate 258461 small clauses 60%
c [cce-7-1] eliminated 33931 binary clauses 11%
c [cce-7-1] eliminated 10909 ternary clauses 9%
c [cce-7-1] eliminated 44840 small clauses 10%
c [cce-7-1] eliminated 45380 small clauses in 557754701 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 74119 covered clauses in round 1
c [cce-7] eliminated 74119 covered clauses in TOTAL during 1 rounds
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 120629 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 8548 variables 7% in round 1 in 204047786 steps
c [elim-15-1] backward subsumption/strengthening limit 204047700
c [elim-15-1-1] backward checking 38755 touched variables 32%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 304 and strengthened 818 clauses in 27213811 steps
c [elim-15-1] rescheduled 2925 variables 2% by backward subsumption
c [elim-15-2] eliminated 79 variables 0% in round 2 in 24340924 steps
c [elim-15-2] backward subsumption/strengthening limit 24340900
c [elim-15-2-1] backward checking 686 touched variables 1%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 18 and strengthened 52 clauses in 1449987 steps
c [elim-15-2] rescheduled 193 variables 0% by backward subsumption
c [elim-15-3] eliminated 8 variables 0% in round 3 in 1489351 steps
c [elim-15-3] backward subsumption/strengthening limit 1489300
c [elim-15-3-1] backward checking 86 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 5 and strengthened 4 clauses in 653119 steps
c [elim-15] incomplete 28 not tried 0% in round 3
c [gc-144] reconnected 319534 binary clauses (produced 0 empty 6 units)
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 8645 = 7% variables out of 120629 scheduled
c [bca-14] limit of 10000000 steps and 1480527 added (scaled 2)
c [bca-14] 172083 out of 223970 literals actually usable 77%
c [bca-14] added 2750 blocked clauses in 556788 steps
c [sweep-14] limit 33465280 penalty 0 = 0 + 0
c [sweep-14-1] 40273 pos 36.8% + 69288 neg 63.2% = 109561 sched 97.8% ret 2423
c [sweep-14-1] 33468613 steps 1219 queries 8892.42 avg class size
c [sweep-14-1] 19260 decisions 1205 SAT calls 40.21 avg env size
c [sweep-14-1] 88199 variables remain 79% (23760 retained 21%)
c [decomp-59] removed 229 variables
c [sweep-14-1] removed 229 vars (0 failed, 109 eqs, 105 impls)
c [sweep-14] removed 229 vars in TOTAL (1 rounds, 1218 queries)
c [phase-count-18] 688754 negative 93.9% of 733802 except 45048 6.1%
c [phase-count-18] 671555 positive 91.5% of 733802 except 62247 8.5%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 8 positive 47%, 9 negative 53%
c [sort-queue-18] sorted 51073 enqueued variables after 92434 conflicts
c [score-dist-18] active 60682 (54%), one 0 (0%), zero 51073 (46%)
c [score-dist-18] max exp 533, different 26 (5%)
c [score-dist-18] median active exp 521, avg 522.7
c [simplification-18] removed 9013 variables 7.5% (111755 remain 10%)
c [simplification-18] removed 97366 irredundant clauses 11.7% (733802 remain 16%)
c [simplification-18] maximum reduction of 12% = max (7%, 12%)
c [simplification-18] large reduction 12% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 104434 (soft 94434 + delta 10000)
c [simplification-18] new conflict limit 94434 (hard 104434)
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 21237 basic ate = 15687 trn 74% + 5550 lrg 26% in 4 updates
c bcas: 14 count, 24397 added (17784 skipped), 14841970 steps
c bkwd: tried 1909385 clauses, 3815537 lits, 2.00 lits/clause
c bkwd: checked 115752759 occs, 60.62 occs/clause, 30.34 occs/lit
c bkwd: subsumed 31 binary, 1042 ternary, 1314 large
c bkwd: strengthened 6 binary, 1 ternary (100% self), 3456 large (0% self)
c blkd: 6 bces, 65801 removed, 45615516 resolutions, 119926609 steps
c blkd: 61954 blocking literals 3%, 1634 pure
c bump: 119096 bumped seen, 148668029 lits 1248.3 on average
c card: 5 count, 0 units, 0 am1, 97917430 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 14953 subsumed
c card: 5241 at-most-one constraints found, average size 3.13
c card: 5241 at-most-one constraints used 100%, average size 3.13
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: 7 cces, 207536 eliminated, 173435 ate 84%, 34101 abce 16%
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: 16687985 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 147 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 59 decompositions, 135657 equivalent 11%
c deco: 30785 decision-only clauses 26%, 85% reduction
c decs: 1332941 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 694857 eliminated 57%, 11717 pure 2%
c elms: 29 rounds, 1.9 rounds/bve
c elms: 596543 small 86%, 84963 large 12%
c elms: 762031 tried small, 596543 succeeded 78%, 165488 failed 22%
c elms: 325477 subsumed, 446435 strengthened, 22130 blocked
c elms: 49795529 copies, 61768661 resolutions, 14730506 ipos
c elms: 37817640 subchks, 68390376 strchks
c gaus: 10 extractions, 236223 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 10 binary and 16 ternary equations
c gaus: 0 gc, 227530624 steps, 113765312 extr 50%, 114044573 elim 50%
c glue: 45.1 orig avg, 45.1 real avg, 4.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1587263 = 609337 simple 38% + 962487 trn 61% + 15439 lrg 1%, 45551 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 119095 clauses, 110.1 length
c lrnd: 13106874 lits = 38634786 orig - 25527912 removed 66%
c lrnd: 28316 uips 24%, 62061 flips 52%
c mins: 77734 mins 65%, 3688 bin 3%, 6877 size 6%
c mins: 36358014 poisoned searches, 5271022 hits, 14% hit rate
c mins: 42479866 used twice searches, 774089 hits, 2% hit rate
c move: moved 171190, 96798 bin 57%, 74392 trn 43%
c otfs: 2780 driving 54%, 2349 restarting 46%
c otfs: str 5129, 3948 red 77%, 1181 irr 23%
c otfs: str 5129, 0 bin 0%, 2456 trn 48%, 2673 lrg 52%
c otfs: sub 172, 159 red 92%, 13 irr 8%
c otfs: sub 172, 0 bin 0%, 105 trn 61%, 67 lrg 39%
c phas: 18 computed, 858756 set, 397820 pos (46%), 460936 neg (54%)
c prbs: 6 basic, 1853089 probed, 19806 failed, 3973 lifted
c prbs: 7 simple, 2039434 probed, 1777 failed, 22859 eqs
c prbs: 7 treelook, 3117 probed, 86 failed, 0 lifted
c prom: 0 locked 0% out of 694797 tried
c prps: 1789409570 props, 1257 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 14 count, 44280 quat, 11880 self1, 693 self2, 5540 dup
c queu: 18 sorted, 1332941 next (62529 steps 0.05)
c queu: 154376781 enq (447911625 steps 2.90), 148668029 deq 96%
c redc: 3821 clauses 14%, 27777 tried 30%, 172 sat 1%
c redc: 6588 lits 4%, 177317 tried 0%, 174 sat 0%
c redc: 611 times jump level reduced, 26.6 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 348585 removed, 243931 red 70%
c rsts: 5143 restarts 98%, 94 skipped 2%
c rsts: 94 saturating 100%, 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: 18 count, 16 confs 89%, 0 vars 0%
c simp: 1 its 6%, 1 bin 6%, 0 trns 0%
c subl: 119095 count (240673 tried 2.0), 32453 sub out of 103138 (31.5%)
c swps: 14 count, 15 rounds, 26843 queries (1789.5/round)
c swps: 24724 sat calls, 4117 unsat (1.1% success rate)
c swps: 272632 decisions 11.0, 27793 conflicts 1.1
c swps; 7264.5 avg class size, 28.8 avg environment size
c swps: 0 failed, 5574 impls, 6152 equivs
c swp0: 8943 type 0 queries, 2827 unsat (31.6%), 7942 sat (88.8%)
c swp1: 17900 type 1 queries, 12680 unsat (70.8%), 12749 sat (71.2%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 2904486 calls to obtain time
c tops: 271062 fixed 22%, 53 its, 1775.15 confs/it
c trds: 14 transitive reductions, 28193 removed, 79 failed
c trds: 333218 nodes, 570487 edges, 28011235 steps
c trim: 852265 words, 3.3 MB
c trnr: 14 count, 15118 bin, 502824 trn, 582900526 steps
c unhd: 18 count, 18 rounds, 198195885 steps
c unhd: 26931 non-trivial sccs of average size 2.5
c unhd: 3730 units, 3713 bin, 17 trn, 0 lrg
c unhd: 4927 failed, 4268 stamp, 0 lits, 30 bin, 539 trn, 0 lrg
c unhd: 505097 tauts, 10071 bin 2%, 91762 trn 18%, 18143 lrg 4%
c unhd: 505097 tauts, 385121 stamp 76%, 390091 red 77%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 943611 str, 3713 bin 0%, 64814 trn 7%, 875084 lrg 93%, 561893 red 60%
c vars: 111755 remaining 9% and 1101576 removed 91% out of 1213331
c vars: 271062 fixed 22%, 694857 eliminated 57%, 135657 equivalent 11%
c vsts: 12433602601 visits, 92% srch, 8% simp, 0% lkhd
c vsts: 6.8 search visits per propagation, 121485.9 per conflict
c wchs: 1454525901 pushed, 195859965 enlarged, 224 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         147418             0             0      14655222       5514861         35997
c 
c  0 0         63147  43         0   0<        0   0< 11521118  79   3748861  68     12372  34     0.8
c  1 5          2771   2         0   0         0   0    671547   5<   370303   7<     2737   8     0.2
c  2 6          7493   5         0   0         0   0    825604   6    454534   8      5273  15     0.9
c  3 9         12875   9         0   0         0   0    620818   4    364222   7      4653  13<    3.9
c  4 14        10574   7<        0   0         0   0    366750   3    213211   4      2813   8     3.7
c  5 21         6895   5         0   0         0   0    187208   1    118104   2      1473   4     3.4
c  6 30         4067   3         0   0         0   0    100184   1     58771   1      1349   4     2.5
c  7 41         1944   1         0   0         0   0    113433   1     45509   1      1003   3     0.7
c  8 54         3314   2         0   0         0   0    121072   1     56322   1      1231   3     1.6
c  9 69         1639   1         0   0         0   0     43799   0     29889   1      1474   4     0.7
c 10 86        17334  12         0   0         0   0     59148   0     40925   1      1560   4     4.4
c 11 126       15356  10         0   0         0   0     24521   0     14205   0        59   0     3.1
c 12 230           9   0         0   0         0   0        20   0         5   0         0   0     0.0
c 
c avg                  3.8           0.0           0.0           0.7           1.0           2.8
c std                  4.2           0.0           0.0           1.7           2.0           3.0
c 
c   99.184  10% probe
c   85.519   9% elim
c   79.210   8% sweep
c   50.227   5% cce
c   44.288   4% bump
c   29.494   3% unhide
c   22.001   2% gauss
c   16.356   2% block
c   12.875   1% bca
c   10.070   1% quatres
c 
c   10.989 < 1% rest (below)
c 
c    6.443   1% ternres
c    2.103   0% decide
c    1.802   0% transred
c    0.641   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   14.176   1% preprocessing     3%
c  440.346  44% inprocessing     97%
c ==================================
c  454.521  46% simplifying
c  542.314  54% search
c ==================================
c  996.858 100% all
c 
c         94083 conflicts,          94.4 confs/sec
c          1375 ternaries,          68.4 confs/ternary
c           652 binaries,          144.3 confs/binary
c            53 iterations,       1775.2 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          5143 restarts,            5.2 rests/sec,     18.3 confs/restart
c       1332941 decisions,        1337.1 decis/sec,     14.2 decis/conflict
c    1789409570 propagations,  1795050.3 props/sec,   1342.5 props/decision
c 
c 996.9 seconds, 466.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
