c launch: /data/cnf/sc2014/app/SAT_dat.k95-24_1_rule_3.cnf.bz2
c host: atom19
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.k95-24_1_rule_3.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k95-24_1_rule_3.cnf.bz2
c no embedded options
c found 'p cnf 1540071 6036162' header
c read 1540071 variables, 6036162 clauses, 15152823 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 1492293 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 1492293  5988250         0       0      0     0    0     0  291   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1497062 based on 5988250 irredundant clauses
c [card-1] found 1425 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1497062 for elimination
c [card-1] 1425 out of 1425 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 311739 variables
c [simpleprobe-1] all 1228332 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 9996520 based on 4998260 irredundant clauses
c [decomp-2] removed 4188 variables
c [simpleprobe-1] 1088492 variables remain 89% (135652 retained 11%)
c [simpleprobe-1] removed 4188 variables, found 18917 hbrs, 622 units
c [unhide-1] limit 311069 based on 4977109 irredundant clauses
c [unhide-1-1] 1735 units, 1346 failed, 10715 tauts, 0 hbrs, 61346 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1218766 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 1138161 not tried 93% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 80609 = 7% variables out of 1218766 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 4459232 negative 95.2% of 4684257 except 225025 4.8%
c [phase-count-1] 4387527 positive 93.7% of 4684257 except 296730 6.3%
c [phase-1] phase bias: 529121 positive 46%, 609036 negative 54%
c [sort-queue-1] sorted 1138157 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1138157 (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 184696 variables 14.0% (1138157 remain 76%)
c [simplification-1] removed 1303993 irredundant clauses 21.8% (4684257 remain 78%)
c [simplification-1] maximum reduction of 22% = max (14%, 22%)
c [simplification-1] large reduction 22% >= 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   19.1 1138156  4684257         2       1     27 14429    0     0  281   1%      0    0    0    0 25500%
c i   19.2 1137893  4684257         4       1     28 14429    0     0  281   1%      0    0    0    0 25352%
c i   19.2 1137892  4684257         9       1     29 14432    0     0  281   1%      0    0    0    0 25107%
c i   19.2 1137740  4684257        11       1     29 14433    0     0  281   1%      0    0    0    0 24977%
c i   19.2 1137710  4684257        14       1     30 14434    0     0  281   1%      0    0    0    0 24874%
c i   19.3 1137673  4684257        69      39     36 14441    0     1  281  16%      0    1    1    0 23887%
c i   19.4 1137672  4684257       122      73     45 14445    0     1  282  22%      0    1    2    0 21273%
c i   19.4 1137657  4684257       123      73     45 14445    0     1  282  22%      0    1    2    0 21191%
c i   19.5 1137349  4684257       177     104     57 14455    0     1  282  15%      0    1    2    0 18252%
c i   19.9 1137319  4684257       269     159     78 14468    0     2  282  13%      0    2    2    0 14732%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 4457 variables
c [simpleprobe-2] 1008204 schedulable variables 89%
c [simpleprobe-2] limit 9344416 based on 4672208 irredundant clauses
c [decomp-4] removed 1277 variables
c [simpleprobe-2] 953881 variables remain 84% (178542 retained 16%)
c [simpleprobe-2] removed 1277 variables, found 31685 hbrs, 291 units
c [treelook-1] limit 1166709 based on 4666836 irredundant clauses
c [treelook-1] scheduled 232867 literals 10%
c [treelook-1] scheduling used 1166724 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1166709 based on 4666836 irredundant clauses
c [treelook-1] used 1167019 steps
c [treelook-1] 232667 literals remain 10%
c [treelook-1] 229956 variables remain to probed next time 20%
c [decomp-5] removed 131 variables
c [treelook-1] removed 149 variables, found 2825 hbrs
c [basicprobe-1] limit 37330152 based on 4666269 irredundant clauses
c [basicprobe-1-0] 1025918 probes remain 92% after last round
c [basicprobe-1-0] 4755 units = 2369 failed (50%) + 2386 lifted (50%)
c [basicprobe-1-0] removed 11912 variables, found 247195 hbrs
c [unhide-2] limit 291641 based on 4666269 irredundant clauses
c [unhide-2-2] 932 units, 1329 failed, 14348 tauts, 0 hbrs, 42808 literals
c [elim-2] 1117819 variables 100% will be scheduled this time
c [elim-2] scheduled 1117819 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 1036365 not tried 93% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 81457 = 7% variables out of 1117819 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 4194383 negative 95.1% of 4409543 except 215160 4.9%
c [phase-count-2] 4121729 positive 93.5% of 4409543 except 287814 6.5%
c [phase-2] phase bias: 1941 positive 31%, 4417 negative 69%
c [sort-queue-2] sorted 1032248 enqueued variables after 269 conflicts
c [score-dist-2] active 4114 (0%), one 0 (0%), zero 1032248 (100%)
c [score-dist-2] max exp 513, different 13 (3%)
c [score-dist-2] median active exp 509, avg 509.5
c [simplification-2] removed 100957 variables 8.9% (1036362 remain 69%)
c [simplification-2] removed 274714 irredundant clauses 5.9% (4409543 remain 74%)
c [simplification-2] maximum reduction of 9% = max (9%, 6%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1030 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   47.4 1036361  4409543       352     164     56 217772    0     4  275   7%      0    4    2    0 12556%
c i   47.7 1036360  4409543       395     192     65 217775    0     5  275   6%      0    5    3    0 11852%
c i   48.3 1036359  4409543       565     306     92 217793    0     7  275   7%      0    7    3    0 9316%
c i   48.3 1036358  4409543       566     306     92 217793    0     7  275   7%      0    7    3    0 9280%
c i   48.4 1036357  4409543       567     306     92 217793    0     7  275   7%      0    7    3    0 9244%
c i   49.0 1036356  4409543       680     388    108 217804    1    10  275   5%      0   10    3    0 9406%
c i   49.5 1036355  4409543       831     512    123 217809    1    12  275   6%      1   12    5    0 9065%
c 
c [simplification-3] limit 1050 conflicts (hard 11000) hit after 1052 conflicts
c [card-2] limit 1102385 based on 4409543 irredundant clauses
c [card-2] found 1059 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1102385 for elimination
c [card-2] 1059 out of 1059 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 6050 variables
c [treelook-2] limit 1099919 based on 4399678 irredundant clauses
c [treelook-2] scheduled 211395 literals 10%
c [treelook-2] scheduling used 1099987 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1099919 based on 4399678 irredundant clauses
c [treelook-2] used 1100660 steps
c [treelook-2] 211194 literals remain 10%
c [treelook-2] 129781 variables remain to probed next time 13%
c [decomp-7] removed 132 variables
c [treelook-2] removed 140 variables, found 3570 hbrs
c [unhide-3] limit 274956 based on 4399300 irredundant clauses
c [unhide-3-3] 386 units, 723 failed, 22683 tauts, 0 hbrs, 20312 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1028969 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 952850 not tried 93% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 76119 = 7% variables out of 1028969 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 3994707 negative 95.0% of 4203748 except 209041 5.0%
c [phase-count-3] 3923697 positive 93.3% of 4203748 except 280051 6.7%
c [phase-3] phase bias: 854 positive 32%, 1831 negative 68%
c [sort-queue-3] sorted 940067 enqueued variables after 1052 conflicts
c [score-dist-3] active 12783 (1%), one 0 (0%), zero 940067 (99%)
c [score-dist-3] max exp 518, different 18 (3%)
c [score-dist-3] median active exp 512, avg 511.9
c [simplification-3] removed 83505 variables 8.1% (952850 remain 64%)
c [simplification-3] removed 205795 irredundant clauses 4.7% (4203748 remain 70%)
c [simplification-3] maximum reduction of 8% = max (8%, 5%)
c [simplification-3] large reduction 8% >= 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 13052 (soft 3052 + delta 10000)
c [simplification-3] new conflict limit 3052 (hard 13052)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   70.2  952849  4203748      1475     852    145 187396    2    15  268  16%      3   15   12    0 6740%
c i   70.2  952690  4203748      1485     855    147 187400    2    15  268  16%      3   15   11    0 6517%
c i   70.2  952658  4203748      1487     855    147 187400    2    15  268  16%      3   15   11    0 6491%
c i   70.2  952657  4203748      1565     914    151 187401    2    15  268  16%      3   15    9    0 5299%
c i   71.3  952604  4203748      1701    1013    169 187410    3    18  270  14%      2   18    7    0 3958%
c i   71.3  952603  4203748      1704    1015    169 187410    3    18  270  14%      2   18    7    0 3921%
c i   71.5  952602  4203748      1734    1039    172 187412    3    19  270  14%      2   18    7    0 3662%
c i   71.8  952601  4203748      1789    1082    180 187414    3    20  270  13%      2   19    7    0 3425%
c i   72.6  952600  4203748      1914    1170    199 187427    3    22  270  13%      2   22    8    0 3651%
c i   76.2  952599  4203748      2380    1542    244 187463    3    39  270   8%      3   38    5    0 2119%
c i   76.3  952571  4203748      2381    1542    244 187463    3    39  270   8%      3   38    5    0 2111%
c i   76.4  952500  4203748      2382    1542    244 187463    3    39  270   8%      3   38    5    0 2103%
c i   78.0  952497  4203748      2521    1636    266 187484    3    50  270   6%      3   50    5    0 1929%
c i   78.1  952496  4203748      2523    1637    266 187484    3    50  270   6%      3   50    5    0 1918%
c 
c [simplification-4] limit of 201 binary hit after 201 binaries
c [decomp-8] removed 1358 variables
c [basicprobe-2] limit 33597464 based on 4199683 irredundant clauses
c [basicprobe-2-0] 728682 probes remain 77% after last round
c [basicprobe-2-0] 1573 units = 1465 failed (93%) + 108 lifted (7%)
c [basicprobe-2-0] removed 3766 variables, found 161532 hbrs
c [unhide-4] limit 262480 based on 4199683 irredundant clauses
c [unhide-4-4] 287 units, 697 failed, 15491 tauts, 0 hbrs, 34696 literals
c [elim-4] 946686 variables 100% will be scheduled this time
c [elim-4] scheduled 946686 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 245458290 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 55619 not tried 6% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 553638 = 58% variables out of 946686 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 2704573 negative 95.7% of 2826341 except 121768 4.3%
c [phase-count-4] 2657345 positive 94.0% of 2826341 except 168996 6.0%
c [phase-4] phase bias: 3388 positive 37%, 5682 negative 63%
c [sort-queue-4] sorted 378319 enqueued variables after 2610 conflicts
c [score-dist-4] active 14729 (4%), one 0 (0%), zero 378319 (96%)
c [score-dist-4] max exp 520, different 19 (4%)
c [score-dist-4] median active exp 514, avg 513.8
c [simplification-4] removed 559448 variables 58.7% (393048 remain 26%)
c [simplification-4] removed 1377407 irredundant clauses 32.8% (2826341 remain 47%)
c [simplification-4] maximum reduction of 59% = max (59%, 33%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3086 (hard 13052)
c [simplification-4] new binary interval 1000
c 
c [simplification-5] limit 3086 conflicts (hard 13052) hit after 3086 conflicts
c [quatres-1] found 343098 quaternary clauses 37% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-1] added 106 double-self-subsuming ternary resolvents
c [quatres-1-2] added 5411 single-self-subsuming ternary resolvents
c [quatres-1-2] added 11096 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 11301484 based on 2825371 irredundant clauses
c [ternres-1] all 393048 free variables schedulable
c [ternres-1] 46778 ternary resolvents (92 bin, 46686 trn)
c [ternres-1] 278396 variables remain 71% (114652 retained 29%)
c [gauss-1] limit 1412685 based on 2825371 irredundant clauses
c [gauss-1] extracted 6710 xors of average arity 3.0
c [gauss-1] connected 19943 occurrences of 7833 variables (average 2.5)
c [gauss-1] limit 1412685 based on 2825371 irredundant clauses
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 1795 variables
c [simpleprobe-3] 331061 schedulable variables 85%
c [simpleprobe-3] limit 5679018 penalty 1 = 0 + 1
c [decomp-10] removed 252 variables
c [simpleprobe-3] 326342 variables remain 83% (64659 retained 17%)
c [simpleprobe-3] removed 252 variables, found 12753 hbrs, 53 units
c [unhide-5] limit 176254 based on 2820077 irredundant clauses
c [unhide-5-5] 130 units, 232 failed, 95294 tauts, 0 hbrs, 134230 literals
c [transred-1] limit 2742768 based on 2742768 irredundant clauses
c [transred-1] removed 1125 transitive binary clauses
c [transred-1] found 21 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 390640 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 250000000 steps penalty 1 = 0 + 1
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 27870 blocked clauses
c [cce-1] limit of 15000000 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 26
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 25
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 24
c [cce-1-1] eliminated 5 clauses out of 6 (83%) of length 22
c [cce-1-1] eliminated 10 clauses out of 16 (62%) of length 21
c [cce-1-1] eliminated 14 clauses out of 22 (64%) of length 20
c [cce-1-1] eliminated 32 clauses out of 62 (52%) of length 19
c [cce-1-1] eliminated 386 clauses out of 1470 (26%) of length 18
c [cce-1-1] eliminated 208 clauses out of 1545 (13%) of length 17
c [cce-1-1] eliminated 245 clauses out of 875 (28%) of length 16
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 905 large clauses in 15000031 steps
c [cce-1-1] allowing another 7500015 steps for small clauses
c [cce-1-1] scheduling 1554890 clauses = 1203851 binary + 351039 ternary
c [cce-1-1] tried to eliminate 3182 small clauses 0%
c [cce-1-1] eliminated 507 binary clauses 0%
c [cce-1-1] eliminated 138 ternary clauses 0%
c [cce-1-1] eliminated 645 small clauses 0%
c [cce-1-1] eliminated 645 small clauses in 15000262 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1550 covered clauses in round 1
c [cce-1] eliminated 1550 covered clauses in TOTAL during 1 rounds
c [cce-1] 1550 < 1/100 * 2710061 = 27100 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 390068 variables 100%
c [elim-5] limit of 28395091 steps penalty 1 = 0 + 1
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 249811 not tried 64% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 15126 = 4% variables out of 390068 scheduled
c [bca-1] limit of 10000000 steps and 5360968 added (scaled 2)
c [bca-1] 721984 out of 749886 literals actually usable 96%
c [bca-1] added 8700 blocked clauses in 2293504 steps
c [sweep-1] limit 5360468 based on 2680234 irredundant clauses
c [sweep-1-1] 124141 pos 33.1% + 250801 neg 66.9% = 374942 sched 100.0% ret 0
c [sweep-1-1] 5388569 steps 103 queries 119599.17 avg class size
c [sweep-1-1] 1347 decisions 90 SAT calls 35.94 avg env size
c [sweep-1-1] 374581 variables remain 100% (351 retained 0%)
c [decomp-11] removed 514 variables
c [sweep-1-1] removed 514 vars (0 failed, 28 eqs, 31 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 514 vars in TOTAL (1 rounds, 102 queries)
c [phase-count-5] 2562808 negative 95.7% of 2679107 except 116299 4.3%
c [phase-count-5] 2533639 positive 94.6% of 2679107 except 145468 5.4%
c [phase-5] phase bias: 1441 positive 55%, 1170 negative 45%
c [sort-queue-5] sorted 358234 enqueued variables after 3086 conflicts
c [score-dist-5] active 16194 (4%), one 0 (0%), zero 358234 (96%)
c [score-dist-5] max exp 520, different 19 (4%)
c [score-dist-5] median active exp 514, avg 514.0
c [simplification-5] removed 18620 variables 4.7% (374428 remain 25%)
c [simplification-5] removed 147234 irredundant clauses 5.2% (2679107 remain 45%)
c [simplification-5] maximum reduction of 5% = max (5%, 5%)
c [simplification-5] large reduction 5% >= 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 15086 (soft 5086 + delta 10000)
c [simplification-5] new conflict limit 5086 (hard 15086)
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  139.0  374427  2679107      3168   10400  42578 91790    3    68  236   5%      4   67    6    0 1998%
c 
c [simplification-6] limit 5086 conflicts (hard 15086) hit after 5086 conflicts
c [quatres-2] found 350604 quaternary clauses 39% in total
c [quatres-2-1] removed 6 duplicate quaternary clauses
c [quatres-2-1] added 66 double-self-subsuming ternary resolvents
c [quatres-2-2] added 2244 single-self-subsuming ternary resolvents
c [quatres-2-2] added 8597 quaternary resolvents
c [ternres-2] limit 10715660 based on 2678915 irredundant clauses
c [ternres-2] 265089 schedulable variables 71%
c [ternres-2] 46642 ternary resolvents (1014 bin, 45628 trn)
c [ternres-2] 176356 variables remain 47% (198071 retained 53%)
c [card-3] limit 669728 based on 2678915 irredundant clauses
c [card-3] found 347 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 669728 for elimination
c [card-3] 347 out of 347 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 308 variables
c [treelook-3] limit 669639 based on 2678557 irredundant clauses
c [treelook-3] scheduled 80376 literals 11%
c [treelook-3] scheduling used 669926 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 669639 based on 2678557 irredundant clauses
c [treelook-3] used 671857 steps
c [treelook-3] 80308 literals remain 11%
c [treelook-3] 46275 variables remain to probed next time 12%
c [decomp-13] removed 16 variables
c [treelook-3] removed 19 variables, found 831 hbrs
c [unhide-6] limit 167404 based on 2678464 irredundant clauses
c [unhide-6-6] 204 units, 623 failed, 4905 tauts, 0 hbrs, 69515 literals
c [transred-2] limit 2675480 based on 2675480 irredundant clauses
c [transred-2] removed 1049 transitive binary clauses
c [transred-2] found 23 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 373302 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 0 + 1
c [block-2] incomplete 11437 not tried 3%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 9329 blocked clauses
c [block-2] 9329 < 1/100 * 2674633 = 26746 considered unsuccessful
c [elim-6] 54351 variables 15% will be scheduled this time
c [elim-6] scheduled 54351 variables 15%
c [elim-6] limit of 46842341 steps penalty 1 = 0 + 1
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 23215 not tried 6% in round 1
c [gc-43] reconnected 92781 binary clauses (produced 0 empty 1 units)
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 609 = 1% variables out of 54351 scheduled
c [elim-6] 609 < 1/100 * 54351 = 543 considered unsuccessful
c [bca-2] limit of 10000000 steps and 5246676 added (scaled 2)
c [bca-2] 701072 out of 745180 literals actually usable 94%
c [bca-2] added 2346 blocked clauses in 2206493 steps
c [sweep-2] limit 5241826 based on 2620913 irredundant clauses
c [sweep-2-1] 126456 pos 34.0% + 245810 neg 66.0% = 372266 sched 99.9% ret 323
c [sweep-2-1] 5286542 steps 96 queries 113117.76 avg class size
c [sweep-2-1] 1315 decisions 89 SAT calls 43.94 avg env size
c [sweep-2-1] 371729 variables remain 100% (857 retained 0%)
c [decomp-14] removed 886 variables
c [sweep-2-1] removed 886 vars (0 failed, 19 eqs, 28 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 886 vars in TOTAL (1 rounds, 95 queries)
c [phase-count-6] 2502785 negative 95.6% of 2618819 except 116034 4.4%
c [phase-count-6] 2471246 positive 94.4% of 2618819 except 147573 5.6%
c [phase-6] phase bias: 710 positive 54%, 605 negative 46%
c [sort-queue-6] sorted 345941 enqueued variables after 5086 conflicts
c [score-dist-6] active 25762 (7%), one 0 (0%), zero 345941 (93%)
c [score-dist-6] max exp 522, different 21 (4%)
c [score-dist-6] median active exp 515, avg 515.1
c [simplification-6] removed 2724 variables 0.7% (371703 remain 25%)
c [simplification-6] removed 60286 irredundant clauses 2.3% (2618819 remain 44%)
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 21752 (soft 11752 + delta 10000)
c [simplification-6] new conflict limit 11752 (hard 21752)
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  176.3  371702  2618817      6657   20517  81343 94201   15   116  237  13%     38  110   56    1 4304%
c i  179.2  371701  2618814      7352   21021  81382 94224   17   126  237  14%     22  119   21    2 1283%
c i  179.9  371700  2618814      7445   21096  81386 94233   17   128  237  13%     20  121   17    2 1041%
c i  183.7  371699  2618813      9062   22535  81445 94252   20   129  238  16%     15  119   25    2 1121%
c 
c [simplification-7] limit 11752 conflicts (hard 21752) hit after 11755 conflicts
c [quatres-3] found 356324 quaternary clauses 41% in total
c [quatres-3-1] removed 10 duplicate quaternary clauses
c [quatres-3-1] added 21 double-self-subsuming ternary resolvents
c [quatres-3-2] added 957 single-self-subsuming ternary resolvents
c [quatres-3-2] added 5080 quaternary resolvents
c [ternres-3] limit 10475052 based on 2618763 irredundant clauses
c [ternres-3] 174911 schedulable variables 47%
c [ternres-3] 49271 ternary resolvents (1692 bin, 47579 trn)
c [ternres-3] 106842 variables remain 29% (264857 retained 71%)
c [gauss-2] limit 1309381 based on 2618763 irredundant clauses
c [gauss-2] extracted 5190 xors of average arity 3.0
c [gauss-2] connected 15510 occurrences of 6241 variables (average 2.5)
c [gauss-2] limit 1309369 based on 2618738 irredundant clauses
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 497 variables
c [basicprobe-3] limit 26020052 penalty 1 = 0 + 1
c [basicprobe-3-0] 240792 probes remain 65% after last round
c [basicprobe-3-0] 2107 units = 1959 failed (93%) + 148 lifted (7%)
c [basicprobe-3-0] removed 3255 variables, found 126275 hbrs
c [bate-1] eliminated 3532 asymmetric tautologies during probing
c [unhide-7] limit 260200 with penalty 3 = 0 + 3
c [unhide-7-7] 246 units, 316 failed, 47948 tauts, 0 hbrs, 38303 literals
c [transred-3] limit 2539967 based on 2539967 irredundant clauses
c [transred-3] removed 1086 transitive binary clauses
c [transred-3] found 8 units
c [cce-2] limit of 13010026 steps penalty 2 = 1 + 1
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 26
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 25
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 24
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 23
c [cce-2-1] eliminated 3 clauses out of 8 (38%) of length 22
c [cce-2-1] eliminated 8 clauses out of 14 (57%) of length 21
c [cce-2-1] eliminated 7 clauses out of 15 (47%) of length 20
c [cce-2-1] eliminated 3 clauses out of 15 (20%) of length 19
c [cce-2-1] eliminated 12 clauses out of 907 (1%) of length 18
c [cce-2-1] eliminated 29 clauses out of 1127 (3%) of length 17
c [cce-2-1] eliminated 18 clauses out of 839 (2%) of length 16
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 87 large clauses in 13010133 steps
c [cce-2-1] allowing another 6505066 steps for small clauses
c [cce-2-1] scheduling 1389727 clauses = 1105100 binary + 284627 ternary
c [cce-2-1] tried to eliminate 2854 small clauses 0%
c [cce-2-1] eliminated 437 binary clauses 0%
c [cce-2-1] eliminated 153 ternary clauses 0%
c [cce-2-1] eliminated 590 small clauses 0%
c [cce-2-1] eliminated 5910 small clauses in 13010070 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 5997 covered clauses in round 1
c [cce-2] eliminated 5997 covered clauses in TOTAL during 1 rounds
c [cce-2] 5997 < 1/100 * 2539465 = 25394 considered unsuccessful
c [bca-3] limit of 10000000 steps and 5072959 added (scaled 2)
c [bca-3] 676006 out of 734716 literals actually usable 92%
c [bca-3] added 349 blocked clauses in 2072518 steps
c [sweep-3] limit 5066936 based on 2533468 irredundant clauses
c [sweep-3-1] 131359 pos 35.8% + 235165 neg 64.2% = 366524 sched 99.8% ret 833
c [sweep-3-1] 5116943 steps 99 queries 117770.09 avg class size
c [sweep-3-1] 1477 decisions 98 SAT calls 36.48 avg env size
c [sweep-3-1] 365825 variables remain 100% (1530 retained 0%)
c [decomp-16] removed 3398 variables
c [sweep-3-1] removed 3398 vars (0 failed, 13 eqs, 18 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 3398 vars in TOTAL (1 rounds, 98 queries)
c [phase-count-7] 2410494 negative 95.4% of 2527771 except 117277 4.6%
c [phase-count-7] 2386348 positive 94.4% of 2527771 except 141423 5.6%
c [phase-7] phase bias: 722 positive 63%, 430 negative 37%
c [sort-queue-7] sorted 321741 enqueued variables after 11755 conflicts
c [score-dist-7] active 42218 (12%), one 0 (0%), zero 321741 (88%)
c [score-dist-7] max exp 525, different 23 (4%)
c [score-dist-7] median active exp 517, avg 517.3
c [simplification-7] removed 7740 variables 2.1% (363959 remain 24%)
c [simplification-7] removed 91039 irredundant clauses 3.5% (2527771 remain 42%)
c [simplification-7] maximum reduction of 3% = max (2%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 11666
c [simplification-7] penalized conflict interval 11666 = 1 * 11666
c [simplification-7] hard conflict limit 33421 (soft 23421 + delta 10000)
c [simplification-7] new conflict limit 23421 (hard 33421)
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  247.0  363958  2527759     19518   35677 112466 172673   28   145  241  19%    136  113   13    7  202%
c i  253.3  363877  2527759     21124   37161 112485 172700   23   125  241  18%     30   90   10    7  149%
c i  265.2  363824  2527759     23379   39236 112542 172753   18   116  241  15%     12   78   12    7  179%
c 
c [simplification-8] limit 23421 conflicts (hard 33421) hit after 23422 conflicts
c [quatres-4] found 352867 quaternary clauses 42% in total
c [quatres-4-1] removed 32 duplicate quaternary clauses
c [quatres-4-1] added 21 double-self-subsuming ternary resolvents
c [quatres-4-2] added 883 single-self-subsuming ternary resolvents
c [quatres-4-2] added 3569 quaternary resolvents
c [ternres-4] limit 10110764 based on 2527691 irredundant clauses
c [ternres-4] 104439 schedulable variables 29%
c [ternres-4] 47451 ternary resolvents (1974 bin, 45477 trn)
c [ternres-4] 55279 variables remain 15% (308545 retained 85%)
c [decomp-17] removed 824 variables
c [simpleprobe-4] 302939 schedulable variables 83%
c [simpleprobe-4] limit 40019386 penalty 1 = 0 + 1
c [decomp-18] removed 2544 variables
c [simpleprobe-4] 220341 variables remain 61% (140250 retained 39%)
c [simpleprobe-4] removed 2544 variables, found 85321 hbrs, 556 units
c [unhide-8] limit 500242 with penalty 3 = 0 + 3
c [unhide-8-8] 306 units, 441 failed, 24545 tauts, 0 hbrs, 55402 literals
c [transred-4] limit 2503393 based on 2503393 irredundant clauses
c [transred-4] removed 1122 transitive binary clauses
c [transred-4] found 11 units
c [block-3] 11261 variables 3% will be scheduled this time
c [block-3] scheduled 11261 variables 3%
c [block-3] limit of 50024233 steps penalty 2 = 1 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 31 blocked clauses
c [block-3] 31 < 1/100 * 2502909 = 25029 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 359817 variables 100%
c [elim-7] limit of 100048467 steps penalty 2 = 1 + 1
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 64588 not tried 18% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 17403 = 5% variables out of 359817 scheduled
c [bca-4] limit of 10000000 steps and 4888735 added (scaled 2)
c [bca-4] 624884 out of 684830 literals actually usable 91%
c [bca-4] added 785 blocked clauses in 1946855 steps
c [sweep-4] limit 4882538 based on 2441269 irredundant clauses
c [sweep-4-1] 125467 pos 36.8% + 215523 neg 63.2% = 340990 sched 99.6% ret 1424
c [sweep-4-1] 4888052 steps 90 queries 99617.88 avg class size
c [sweep-4-1] 1345 decisions 84 SAT calls 33.52 avg env size
c [sweep-4-1] 340604 variables remain 99% (1808 retained 1%)
c [decomp-19] removed 694 variables
c [sweep-4-1] removed 694 vars (0 failed, 19 eqs, 25 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 694 vars in TOTAL (1 rounds, 89 queries)
c [phase-count-8] 2325107 negative 95.3% of 2439442 except 114335 4.7%
c [phase-count-8] 2304734 positive 94.5% of 2439442 except 134708 5.5%
c [phase-8] phase bias: 501 positive 41%, 707 negative 59%
c [sort-queue-8] sorted 294108 enqueued variables after 23422 conflicts
c [score-dist-8] active 47612 (14%), one 0 (0%), zero 294108 (86%)
c [score-dist-8] max exp 527, different 23 (4%)
c [score-dist-8] median active exp 518, avg 518.6
c [simplification-8] removed 22104 variables 6.1% (341720 remain 23%)
c [simplification-8] removed 88317 irredundant clauses 3.5% (2439442 remain 41%)
c [simplification-8] maximum reduction of 6% = max (6%, 3%)
c [simplification-8] large reduction 6% >= 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 35422 (soft 25422 + delta 10000)
c [simplification-8] new conflict limit 25422 (hard 35422)
c 
c [simplification-9] limit 25422 conflicts (hard 35422) hit after 25422 conflicts
c [quatres-5] found 356612 quaternary clauses 43% in total
c [quatres-5-1] removed 178 duplicate quaternary clauses
c [quatres-5-1] added 18 double-self-subsuming ternary resolvents
c [quatres-5-2] added 2020 single-self-subsuming ternary resolvents
c [quatres-5-2] added 5116 quaternary resolvents
c [ternres-5] limit 11066984 with penalty 1 = 0 + 1
c [ternres-5] 51842 schedulable variables 15%
c [ternres-5] 51907 ternary resolvents (2125 bin, 49782 trn)
c [ternres-5] 15546 variables remain 5% (326174 retained 95%)
c [decomp-20] removed 587 variables
c [treelook-4] limit 1106698 penalty 1 = 0 + 1 boost 1
c [treelook-4] scheduled 102391 literals 15%
c [treelook-4] scheduling used 1106766 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1106698 penalty 1 = 0 + 1 boost 1
c [treelook-4] used 1123310 steps
c [treelook-4] 102236 literals remain 15%
c [treelook-4] 39639 variables remain to probed next time 12%
c [decomp-21] removed 12 variables
c [treelook-4] removed 25 variables, found 1595 hbrs
c [unhide-9] limit 553349 with penalty 3 = 0 + 3
c [unhide-9-9] 67 units, 171 failed, 27884 tauts, 0 hbrs, 28203 literals
c [transred-5] limit 2416494 based on 2416494 irredundant clauses
c [transred-5] removed 1189 transitive binary clauses
c [transred-5] found 11 units
c [elim-8] 22210 variables 7% will be scheduled this time
c [elim-8] scheduled 22210 variables 7%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4426793610 steps penalty 1 = 0 + 1
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 45 variables 0% in round 1 in 728057365 steps
c [elim-8-1] backward subsumption/strengthening limit 728057300
c [elim-8-1-1] backward checking 69463 touched variables 20%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1755 and strengthened 4880 clauses in 137743761 steps
c [elim-8-1] rescheduled 14045 variables 4% by backward subsumption
c [elim-8-2] eliminated 567 variables 0% in round 2 in 187381377 steps
c [elim-8-2] backward subsumption/strengthening limit 187381300
c [elim-8-2-1] backward checking 11350 touched variables 3%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 307 and strengthened 567 clauses in 33963410 steps
c [elim-8-2] rescheduled 2606 variables 1% by backward subsumption
c [elim-8-3] eliminated 105 variables 0% in round 3 in 43742741 steps
c [elim-8-3] backward subsumption/strengthening limit 43742700
c [elim-8-3-1] backward checking 1183 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 70 and strengthened 107 clauses in 4711865 steps
c [elim-8] incomplete 447 not tried 0% in round 3
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 862 = 4% variables out of 22210 scheduled
c [elim-8] 862 < 1/100 * 22210 = 222 considered unsuccessful
c [bca-5] limit of 10000000 steps and 4746898 added (scaled 2)
c [bca-5] 612552 out of 679960 literals actually usable 90%
c [bca-5] added 1221 blocked clauses in 1909595 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 33200950 penalty 1 = 0 + 1
c [sweep-5-1] 125006 pos 37.0% + 213195 neg 63.0% = 338201 sched 99.5% ret 1778
c [sweep-5-1] 33248199 steps 638 queries 67539.76 avg class size
c [sweep-5-1] 8259 decisions 599 SAT calls 33.48 avg env size
c [sweep-5-1] 333464 variables remain 98% (6415 retained 2%)
c [decomp-22] removed 1043 variables
c [sweep-5-1] removed 1043 vars (0 failed, 124 eqs, 146 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1043 vars in TOTAL (1 rounds, 637 queries)
c [phase-count-9] 2252011 negative 95.2% of 2366461 except 114450 4.8%
c [phase-count-9] 2232336 positive 94.3% of 2366461 except 134125 5.7%
c [phase-9] phase bias: 335 positive 61%, 217 negative 39%
c [sort-queue-9] sorted 288201 enqueued variables after 25422 conflicts
c [score-dist-9] active 50735 (15%), one 0 (0%), zero 288201 (85%)
c [score-dist-9] max exp 528, different 24 (5%)
c [score-dist-9] median active exp 518, avg 518.8
c [simplification-9] removed 2784 variables 0.8% (338936 remain 23%)
c [simplification-9] removed 72981 irredundant clauses 3.0% (2366461 remain 40%)
c [simplification-9] maximum reduction of 3% = max (1%, 3%)
c [simplification-9] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-9] new conflict interval 16666
c [simplification-9] penalized conflict interval 16666 = 1 * 16666
c [simplification-9] hard conflict limit 52088 (soft 42088 + delta 10000)
c [simplification-9] new conflict limit 42088 (hard 52088)
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  341.6  338935  2366461     26433   41255 154778 205141   17   139  237  13%     20   97   17    7  235%
c i  369.6  338934  2366461     31821   44573 154801 205171  168   246  246  68%     53  194  392   21 1908%
c i  370.1  338933  2366461     31959   44668 154802 205177  172   254  246  68%     44  202  349   21 1658%
c i  373.9  338932  2366461     33659   45404 154848 205215  246   349  250  71%      9  290  382   30 1254%
c i  375.1  338709  2366461     34757   45498 154852 205221  304   385  250  79%     -1  321  485   38 1271%
c i  381.6  338681  2366461     36318   46685 154918 205263  242   436  259  55%     -1  364  270   40  684%
c i  381.6  338680  2366461     36319   46685 154918 205263  242   436  259  55%     -1  364  269   40  681%
c i  383.0  338665  2366461     36652   46966 154922 205277  227   443  259  51%     -5  369  108   40  273%
c i  383.2  338664  2366461     36690   46996 154923 205280  225   444  259  51%     -5  370   95   40  241%
c i  387.7  338663  2366461     39369   47825 154942 205298  297   464  260  64%     12  374  464   52  894%
c i  388.7  338569  2366461     40439   47911 154947 205306  329   463  260  71%     -0  367  396   58  681%
c i  388.9  338568  2366461     40499   47966 154948 205307  324   464  260  70%     -1  368  317   58  546%
c 
c [simplification-10] limit 42098 conflicts (hard 52088) hit after 42175 conflicts
c [quatres-6] found 349608 quaternary clauses 44% in total
c [quatres-6-1] removed 89 duplicate quaternary clauses
c [quatres-6-1] added 30 double-self-subsuming ternary resolvents
c [quatres-6-2] added 642 single-self-subsuming ternary resolvents
c [quatres-6-2] added 3042 quaternary resolvents
c [ternres-6] limit 16388128 with penalty 1 = 0 + 1
c [ternres-6] 15319 schedulable variables 5%
c [ternres-6] 72719 ternary resolvents (2236 bin, 70483 trn)
c [ternres-6] 663 variables remain 0% (337890 retained 100%)
c [card-4] limit 1024258 penalty 4 = 3 + 1
c [card-4] found 551 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1024258 for elimination
c [card-4] 551 out of 551 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1183202 based on 2366405 irredundant clauses
c [gauss-3] extracted 3833 xors of average arity 3.0
c [gauss-3] connected 11387 occurrences of 4709 variables (average 2.4)
c [gauss-3] limit 1181075 based on 2362150 irredundant clauses
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 899 variables
c [basicprobe-4] limit 81940643 penalty 1 = 0 + 1
c [basicprobe-4-0] 121279 probes remain 37% after last round
c [basicprobe-4-0] 6121 units = 5600 failed (91%) + 521 lifted (9%)
c [basicprobe-4-0] removed 9007 variables, found 233489 hbrs
c [bate-2] eliminated 3804 asymmetric tautologies during probing
c [unhide-10] limit 819406 with penalty 3 = 0 + 3
c [unhide-10-10] 234 units, 414 failed, 52332 tauts, 0 hbrs, 123156 literals
c [transred-6] limit 2256952 based on 2256952 irredundant clauses
c [transred-6] removed 1574 transitive binary clauses
c [transred-6] found 5 units
c [cce-3] limit of 20485160 steps penalty 3 = 2 + 1
c [cce-3-1] eliminated 1 clauses out of 4 (25%) of length 21
c [cce-3-1] eliminated 1 clauses out of 6 (17%) of length 20
c [cce-3-1] eliminated 2 clauses out of 6 (33%) of length 19
c [cce-3-1] eliminated 14 clauses out of 801 (2%) of length 18
c [cce-3-1] eliminated 22 clauses out of 668 (3%) of length 17
c [cce-3-1] eliminated 20 clauses out of 484 (4%) of length 16
c [cce-3-1] eliminated 115 clauses out of 1328 (9%) of length 15
c [cce-3-1] eliminated 322 clauses out of 1901 (17%) of length 14
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 497 large clauses in 20485195 steps
c [cce-3-1] allowing another 10242597 steps for small clauses
c [cce-3-1] scheduling 1229417 clauses = 965559 binary + 263858 ternary
c [cce-3-1] tried to eliminate 3698 small clauses 0%
c [cce-3-1] eliminated 859 binary clauses 0%
c [cce-3-1] eliminated 171 ternary clauses 0%
c [cce-3-1] eliminated 1030 small clauses 0%
c [cce-3-1] eliminated 5963 small clauses in 20485163 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 6460 covered clauses in round 1
c [cce-3] eliminated 6460 covered clauses in TOTAL during 1 rounds
c [cce-3] 6460 < 1/100 * 2256356 = 22563 considered unsuccessful
c [bca-6] limit of 10000000 steps and 4506992 added (scaled 2)
c [bca-6] 583428 out of 656180 literals actually usable 89%
c [bca-6] added 594 blocked clauses in 1771026 steps
c [sweep-6] limit 4916438 penalty 1 = 0 + 1
c [sweep-6-1] 119668 pos 37.2% + 202408 neg 62.8% = 322076 sched 98.2% ret 6013
c [sweep-6-1] 4939493 steps 107 queries 98000.79 avg class size
c [sweep-6-1] 1179 decisions 98 SAT calls 31.19 avg env size
c [sweep-6-1] 321654 variables remain 98% (6435 retained 2%)
c [decomp-24] removed 6514 variables
c [sweep-6-1] removed 6514 vars (0 failed, 11 eqs, 24 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 6514 vars in TOTAL (1 rounds, 106 queries)
c [phase-count-10] 2122650 negative 94.9% of 2237478 except 114828 5.1%
c [phase-count-10] 2102563 positive 94.0% of 2237478 except 134915 6.0%
c [phase-10] phase bias: 398 positive 59%, 271 negative 41%
c [sort-queue-10] sorted 265612 enqueued variables after 42175 conflicts
c [score-dist-10] active 55963 (17%), one 0 (0%), zero 265612 (83%)
c [score-dist-10] max exp 530, different 26 (5%)
c [score-dist-10] median active exp 520, avg 520.0
c [simplification-10] removed 16978 variables 5.0% (321575 remain 22%)
c [simplification-10] removed 128983 irredundant clauses 5.5% (2237478 remain 37%)
c [simplification-10] maximum reduction of 5% = max (5%, 5%)
c [simplification-10] large reduction 5% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 54175 (soft 44175 + delta 10000)
c [simplification-10] new conflict limit 44175 (hard 54175)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  410.8  321574  2237478     42200   49156 162121 292432  356   456  238  78%      0  351  392   67  582%
c 
c [simplification-11] limit 44175 conflicts (hard 54175) hit after 44175 conflicts
c [quatres-7] found 338639 quaternary clauses 45% in total
c [quatres-7-1] removed 164 duplicate quaternary clauses
c [quatres-7-1] added 55 double-self-subsuming ternary resolvents
c [quatres-7-2] added 949 single-self-subsuming ternary resolvents
c [quatres-7-2] added 2552 quaternary resolvents
c [ternres-7] limit 16632263 with penalty 1 = 0 + 1
c [ternres-7] 594 schedulable variables 0%
c [ternres-7] 64334 ternary resolvents (1824 bin, 62510 trn)
c [ternres-7] 69 variables remain 0% (321505 retained 100%)
c [decomp-25] removed 444 variables
c [simpleprobe-5] 194664 schedulable variables 61%
c [simpleprobe-5] limit 66529052 penalty 1 = 0 + 1
c [decomp-26] removed 3889 variables
c [simpleprobe-5] 164909 variables remain 52% (152333 retained 48%)
c [simpleprobe-5] removed 3889 variables, found 117966 hbrs, 623 units
c [unhide-11] limit 831613 with penalty 3 = 0 + 3
c [unhide-11-11] 84 units, 146 failed, 21707 tauts, 0 hbrs, 50170 literals
c [transred-7] limit 2192498 based on 2192498 irredundant clauses
c [transred-7] removed 1756 transitive binary clauses
c [transred-7] found 15 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 316991 variables 100%
c [block-4] limit of 41580657 steps penalty 3 = 2 + 1
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 22674 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 316329 variables 100%
c [elim-9] limit of 166322630 steps penalty 2 = 1 + 1
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 10868 not tried 3% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 17556 = 6% variables out of 316329 scheduled
c [bca-7] limit of 10000000 steps and 4227677 added (scaled 2)
c [bca-7] 529076 out of 597548 literals actually usable 89%
c [bca-7] added 1919 blocked clauses in 1660338 steps
c [sweep-7] limit 4989678 penalty 1 = 0 + 1
c [sweep-7-1] 106951 pos 36.5% + 185905 neg 63.5% = 292856 sched 98.0% ret 5917
c [sweep-7-1] 5008004 steps 119 queries 89554.05 avg class size
c [sweep-7-1] 1585 decisions 117 SAT calls 36.20 avg env size
c [sweep-7-1] 291862 variables remain 98% (6907 retained 2%)
c [decomp-27] removed 568 variables
c [sweep-7-1] removed 568 vars (0 failed, 9 eqs, 11 impls)
c [sweep-7] removed 568 vars in TOTAL (1 rounds, 118 queries)
c [phase-count-11] 2002260 negative 95.0% of 2108561 except 106301 5.0%
c [phase-count-11] 1980739 positive 93.9% of 2108561 except 127822 6.1%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 336 positive 44%, 428 negative 56%
c [sort-queue-11] sorted 245055 enqueued variables after 44175 conflicts
c [score-dist-11] active 53150 (18%), one 0 (0%), zero 245055 (82%)
c [score-dist-11] max exp 530, different 26 (5%)
c [score-dist-11] median active exp 520, avg 520.1
c [simplification-11] removed 23369 variables 7.3% (298205 remain 20%)
c [simplification-11] removed 128917 irredundant clauses 5.8% (2108561 remain 35%)
c [simplification-11] maximum reduction of 7% = max (7%, 6%)
c [simplification-11] large reduction 7% >= 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 56175 (soft 46175 + delta 10000)
c [simplification-11] new conflict limit 46175 (hard 56175)
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  441.1  298204  2108561     45507   45080 167687 350461  224   449  231  50%     21  327  100   70  143%
c 
c [simplification-12] limit 46175 conflicts (hard 56175) hit after 46175 conflicts
c [quatres-8] found 333759 quaternary clauses 45% in total
c [quatres-8-1] removed 472 duplicate quaternary clauses
c [quatres-8-1] added 35 double-self-subsuming ternary resolvents
c [quatres-8-2] added 888 single-self-subsuming ternary resolvents
c [quatres-8-2] added 4018 quaternary resolvents
c [ternres-8] limit 16946303 with penalty 1 = 0 + 1
c [ternres-8] 62 schedulable variables 0%
c [ternres-8] 32527 ternary resolvents (656 bin, 31871 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 163 variables
c [treelook-5] limit 1694630 penalty 1 = 0 + 1 boost 1
c [treelook-5] scheduled 130112 literals 22%
c [treelook-5] scheduling used 1694635 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 1694630 penalty 1 = 0 + 1 boost 1
c [treelook-5] used 1704518 steps
c [treelook-5] 130013 literals remain 22%
c [treelook-5] 33550 variables remain to probed next time 11%
c [decomp-29] removed 5 variables
c [treelook-5] removed 18 variables, found 2010 hbrs
c [unhide-12] limit 847315 with penalty 3 = 0 + 3
c [unhide-12-12] 174 units, 292 failed, 34571 tauts, 0 hbrs, 68751 literals
c [transred-8] limit 2106729 based on 2106729 irredundant clauses
c [transred-8] removed 1777 transitive binary clauses
c [transred-8] found 19 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 297592 variables 100%
c [elim-10] limit of 338926070 steps penalty 1 = 0 + 1
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 2267 not tried 1% in round 1
c [gc-87] reconnected 320789 binary clauses (produced 0 empty 1 units)
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 4736 = 2% variables out of 297592 scheduled
c [bca-8] limit of 10000000 steps and 4155379 added (scaled 2)
c [bca-8] 515009 out of 585714 literals actually usable 88%
c [bca-8] added 885 blocked clauses in 1620228 steps
c [sweep-8] limit 5083891 penalty 1 = 0 + 1
c [sweep-8-1] 104310 pos 36.5% + 181790 neg 63.5% = 286100 sched 97.7% ret 6756
c [sweep-8-1] 5109455 steps 126 queries 90996.17 avg class size
c [sweep-8-1] 1756 decisions 115 SAT calls 41.98 avg env size
c [sweep-8-1] 285374 variables remain 97% (7480 retained 3%)
c [decomp-30] removed 790 variables
c [sweep-8-1] removed 790 vars (0 failed, 25 eqs, 24 impls)
c [sweep-8] removed 790 vars in TOTAL (1 rounds, 125 queries)
c [phase-count-12] 1966076 negative 94.9% of 2071563 except 105487 5.1%
c [phase-count-12] 1945244 positive 93.9% of 2071563 except 126319 6.1%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 137 positive 41%, 200 negative 59%
c [sort-queue-12] sorted 239099 enqueued variables after 46175 conflicts
c [score-dist-12] active 52967 (18%), one 0 (0%), zero 239099 (82%)
c [score-dist-12] max exp 530, different 26 (5%)
c [score-dist-12] median active exp 520, avg 520.1
c [simplification-12] removed 6138 variables 2.1% (292066 remain 20%)
c [simplification-12] removed 36998 irredundant clauses 1.8% (2071563 remain 35%)
c [simplification-12] maximum reduction of 2% = max (2%, 2%)
c [simplification-12] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-12] new conflict interval 23332
c [simplification-12] penalized conflict interval 23332 = 1 * 23332
c [simplification-12] hard conflict limit 81173 (soft 69507 + delta 11666)
c [simplification-12] new conflict limit 69507 (hard 81173)
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  465.9  292065  2071562     47045   47800 172663 310151  194   441  231  44%      3  311  121   71  170%
c i  466.6  292054  2071562     47685   48370 172686 310170  172   429  231  40%     -3  296   44   71   61%
c i  467.4  291986  2071562     48309   48958 172702 310176  159   421  231  38%     -7  286   83   71  117%
c i  480.9  291963  2071562     58352   51045 172769 310230  174   254  238  69%    117   91   29   92   32%
c i  486.4  291962  2071562     60975   53509 172816 310258   99   241  238  41%     12   75   16   89   18%
c i  502.0  291961  2071562     68597   58717 172897 310311   97   228  247  43%     75   54    8   89    9%
c 
c [simplification-13] limit 69507 conflicts (hard 81173) hit after 69507 conflicts
c [quatres-9] found 332874 quaternary clauses 46% in total
c [quatres-9-1] removed 52 duplicate quaternary clauses
c [quatres-9-1] added 46 double-self-subsuming ternary resolvents
c [quatres-9-2] added 338 single-self-subsuming ternary resolvents
c [quatres-9-2] added 2051 quaternary resolvents
c [ternres-9] limit 21507722 with penalty 1 = 0 + 1
c [ternres-9] all 291960 free variables schedulable
c [ternres-9] 22737 ternary resolvents (396 bin, 22341 trn)
c [ternres-9] 147206 variables remain 50% (144754 retained 50%)
c [decomp-31] removed 251 variables
c [basicprobe-5] limit 107538612 penalty 1 = 0 + 1
c [basicprobe-5-0] 105075 sched 38%, 6107 failed, 511 lifted, 197351 hbrs
c [decomp-32] removed 17545 variables
c [basicprobe-5-1] 185885 probes remain 68% after last round
c [basicprobe-5-1] 6829 units = 6284 failed (92%) + 545 lifted (8%)
c [basicprobe-5-1] removed 18554 variables, found 204109 hbrs
c [bate-3] eliminated 4742 asymmetric tautologies during probing
c [unhide-13] limit 1075386 with penalty 3 = 0 + 3
c [unhide-13-13] 99 units, 132 failed, 21401 tauts, 0 hbrs, 56287 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1275 transitive binary clauses
c [transred-9] found 3 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 273035 variables 100%
c [block-5] limit of 215077224 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 8884 blocked clauses
c [block-5] 8884 < 1/100 * 1904423 = 19044 considered unsuccessful
c [elim-11] 2243 variables 1% will be scheduled this time
c [elim-11] scheduled 2243 variables 1%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] no variable eliminated in round 1 in 350580785 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 5 = 0% variables out of 2243 scheduled
c [elim-11] 5 < 1/100 * 2243 = 22 considered unsuccessful
c [bca-9] limit of 10000000 steps and 3784717 added (scaled 2)
c [bca-9] 475799 out of 545234 literals actually usable 87%
c [bca-9] added 564 blocked clauses in 1494026 steps
c [sweep-9] limit 12904633 penalty 0 = 0 + 0
c [sweep-9-1] 96071 pos 36.2% + 169487 neg 63.8% = 265558 sched 97.4% ret 7058
c [sweep-9-1] 12933484 steps 313 queries 72152.70 avg class size
c [sweep-9-1] 4510 decisions 278 SAT calls 38.11 avg env size
c [sweep-9-1] 263428 variables remain 97% (9161 retained 3%)
c [decomp-33] removed 1067 variables
c [sweep-9-1] removed 1067 vars (0 failed, 52 eqs, 73 impls)
c [sweep-9] removed 1067 vars in TOTAL (1 rounds, 312 queries)
c [phase-count-13] 1786569 negative 94.8% of 1884955 except 98386 5.2%
c [phase-count-13] 1764861 positive 93.6% of 1884955 except 120094 6.4%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 366 positive 56%, 293 negative 44%
c [sort-queue-13] sorted 218815 enqueued variables after 69507 conflicts
c [score-dist-13] active 52734 (19%), one 0 (0%), zero 218815 (81%)
c [score-dist-13] max exp 532, different 28 (5%)
c [score-dist-13] median active exp 520, avg 520.7
c [simplification-13] removed 20411 variables 7.0% (271549 remain 18%)
c [simplification-13] removed 186607 irredundant clauses 9.0% (1884955 remain 31%)
c [simplification-13] maximum reduction of 9% = max (7%, 9%)
c [simplification-13] large reduction 9% >= 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 81507 (soft 71507 + delta 10000)
c [simplification-13] new conflict limit 71507 (hard 81507)
c 
c [simplification-14] limit 71507 conflicts (hard 81507) hit after 71509 conflicts
c [quatres-10] found 311696 quaternary clauses 46% in total
c [quatres-10-1] removed 171 duplicate quaternary clauses
c [quatres-10-1] added 74 double-self-subsuming ternary resolvents
c [quatres-10-2] added 947 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1940 quaternary resolvents
c [ternres-10] limit 43921289 with penalty 0 = 0 + 0
c [ternres-10] 136534 schedulable variables 50%
c [ternres-10] 48449 ternary resolvents (1353 bin, 47096 trn)
c [ternres-10] 1211 variables remain 0% (270338 retained 100%)
c [gauss-4] limit 1098032 penalty 3 = 3 + 0
c [gauss-4] extracted 2673 xors of average arity 3.0
c [gauss-4] connected 7974 occurrences of 3451 variables (average 2.3)
c [gauss-4] limit 1098032 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-34] removed 260 variables
c [simpleprobe-6] 138271 schedulable variables 51%
c [simpleprobe-6] limit 175685159 penalty 0 = 0 + 0
c [decomp-35] removed 7013 variables
c [simpleprobe-6] 68626 variables remain 26% (195650 retained 74%)
c [simpleprobe-6] removed 7013 variables, found 229521 hbrs, 545 units
c [unhide-14] limit 1098032 with penalty 3 = 0 + 3
c [unhide-14-14] 34 units, 177 failed, 82235 tauts, 0 hbrs, 145951 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2110 transitive binary clauses
c [transred-10] found 2 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 274508060 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-4-1] eliminated 6 clauses out of 753 (1%) of length 18
c [cce-4-1] eliminated 52 clauses out of 564 (9%) of length 17
c [cce-4-1] eliminated 26 clauses out of 433 (6%) of length 16
c [cce-4-1] eliminated 49 clauses out of 1463 (3%) of length 15
c [cce-4-1] eliminated 188 clauses out of 1571 (12%) of length 14
c [cce-4-1] eliminated 560 clauses out of 3632 (15%) of length 13
c [cce-4-1] eliminated 1917 clauses out of 6845 (28%) of length 12
c [cce-4-1] eliminated 1309 clauses out of 8182 (16%) of length 11
c [cce-4-1] eliminated 8830 clauses out of 22246 (40%) of length 10
c [cce-4-1] eliminated 5964 clauses out of 17836 (33%) of length 9
c [cce-4-1] eliminated 7060 clauses out of 30622 (23%) of length 8
c [cce-4-1] eliminated 3871 clauses out of 39349 (10%) of length 7
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 29833 large clauses in 274508162 steps
c [cce-4-1] allowing another 137254081 steps for small clauses
c [cce-4-1] scheduling 970922 clauses = 748866 binary + 222056 ternary
c [cce-4-1] tried to eliminate 74016 small clauses 8%
c [cce-4-1] eliminated 7835 binary clauses 1%
c [cce-4-1] eliminated 3384 ternary clauses 2%
c [cce-4-1] eliminated 11219 small clauses 1%
c [cce-4-1] eliminated 20032 small clauses in 274508085 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 49865 covered clauses in round 1
c [cce-4] eliminated 49865 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 3601609 added (scaled 2)
c [bca-10] 457207 out of 526038 literals actually usable 87%
c [bca-10] added 2022 blocked clauses in 1419367 steps
c [sweep-10] limit 13176386 penalty 0 = 0 + 0
c [sweep-10-1] 90894 pos 35.8% + 163182 neg 64.2% = 254076 sched 96.6% ret 8942
c [sweep-10-1] 13188295 steps 322 queries 61360.07 avg class size
c [sweep-10-1] 3926 decisions 310 SAT calls 34.28 avg env size
c [sweep-10-1] 251702 variables remain 96% (11286 retained 4%)
c [decomp-36] removed 607 variables
c [sweep-10-1] removed 607 vars (0 failed, 36 eqs, 35 impls)
c [sweep-10] removed 607 vars in TOTAL (1 rounds, 321 queries)
c [phase-count-14] 1696148 negative 94.5% of 1794422 except 98274 5.5%
c [phase-count-14] 1675047 positive 93.3% of 1794422 except 119375 6.7%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 287 positive 49%, 297 negative 51%
c [sort-queue-14] sorted 210576 enqueued variables after 71509 conflicts
c [score-dist-14] active 51835 (20%), one 0 (0%), zero 210576 (80%)
c [score-dist-14] max exp 532, different 28 (5%)
c [score-dist-14] median active exp 520, avg 520.7
c [simplification-14] removed 9138 variables 3.4% (262411 remain 18%)
c [simplification-14] removed 90532 irredundant clauses 4.8% (1794422 remain 30%)
c [simplification-14] maximum reduction of 5% = max (3%, 5%)
c [simplification-14] large reduction 5% >= 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 83509 (soft 73509 + delta 10000)
c [simplification-14] new conflict limit 73509 (hard 83509)
c 
c [simplification-15] limit 73509 conflicts (hard 83509) hit after 73509 conflicts
c [quatres-11] found 303398 quaternary clauses 48% in total
c [quatres-11-1] removed 1634 duplicate quaternary clauses
c [quatres-11-1] added 43 double-self-subsuming ternary resolvents
c [quatres-11-2] added 850 single-self-subsuming ternary resolvents
c [quatres-11-2] added 1305 quaternary resolvents
c [ternres-11] limit 44434880 with penalty 0 = 0 + 0
c [ternres-11] 1144 schedulable variables 0%
c [ternres-11] 40673 ternary resolvents (1463 bin, 39210 trn)
c [ternres-11] 64 variables remain 0% (262347 retained 100%)
c [card-5] limit 1388590 penalty 4 = 4 + 0
c [card-5] found 863 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1388590 for elimination
c [card-5] 863 out of 863 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-37] removed 396 variables
c [treelook-6] limit 4443488 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 208082 literals 40%
c [treelook-6] scheduling used 4443490 steps
c [treelook-6] not fully scheduled
c [treelook-6] limit 4443488 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 4445242 steps
c [treelook-6] 207547 literals remain 40%
c [treelook-6] 28344 variables remain to probed next time 11%
c [decomp-38] removed 52 variables
c [treelook-6] removed 69 variables, found 5052 hbrs
c [unhide-15] limit 1110872 with penalty 3 = 0 + 3
c [unhide-15-15] 31 units, 58 failed, 14180 tauts, 0 hbrs, 26690 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1970 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 261833 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 718 not tried 0% in round 1
c [gc-109] reconnected 503555 binary clauses (produced 0 empty 1 units)
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 17970 = 7% variables out of 261833 scheduled
c [bca-11] limit of 10000000 steps and 3434008 added (scaled 2)
c [bca-11] 423773 out of 487728 literals actually usable 87%
c [bca-11] added 2932 blocked clauses in 1335527 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 133304640 penalty 0 = 0 + 0
c [sweep-11-1] 82582 pos 35.4% + 150937 neg 64.6% = 233519 sched 95.8% ret 10344
c [sweep-11-1] 133336741 steps 2984 queries 18282.28 avg class size
c [sweep-11-1] 41618 decisions 2849 SAT calls 36.51 avg env size
c [sweep-11-1] 192382 variables remain 79% (51399 retained 21%)
c [decomp-39] removed 1330 variables
c [sweep-11-1] removed 1330 vars (0 failed, 512 eqs, 551 impls)
c [sweep-11] removed 1330 vars in TOTAL (1 rounds, 2983 queries)
c [phase-count-15] 1614804 negative 94.6% of 1707702 except 92898 5.4%
c [phase-count-15] 1594540 positive 93.4% of 1707702 except 113162 6.6%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 154 positive 32%, 330 negative 68%
c [sort-queue-15] sorted 184608 enqueued variables after 73509 conflicts
c [score-dist-15] active 57925 (24%), one 0 (0%), zero 184608 (76%)
c [score-dist-15] max exp 532, different 26 (5%)
c [score-dist-15] median active exp 520, avg 520.7
c [simplification-15] removed 19878 variables 7.6% (242533 remain 16%)
c [simplification-15] removed 86720 irredundant clauses 4.8% (1707702 remain 29%)
c [simplification-15] maximum reduction of 8% = max (8%, 5%)
c [simplification-15] large reduction 8% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 85509 (soft 75509 + delta 10000)
c [simplification-15] new conflict limit 75509 (hard 85509)
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  606.2  242532  1707701     74283   48009 170779 441384   33   259  210  13%     43   80   10   82   13%
c i  606.7  242531  1707701     74449   48150 170798 441386   32   274  210  12%     33   96    8   82    9%
c i  606.8  242530  1707701     74493   48172 170813 441388   31   281  210  11%     30  103    7   82    9%
c i  606.9  242529  1707701     74494   48172 170813 441388   31   281  210  11%     30  103    7   82    9%
c i  608.6  242527  1707701     75244   48768 170926 441392   27   366  211   7%      2  186    7   81    8%
c 
c [simplification-16] limit 75519 conflicts (hard 85509) hit after 77957 conflicts
c [quatres-12] found 296870 quaternary clauses 48% in total
c [quatres-12-1] removed 93 duplicate quaternary clauses
c [quatres-12-1] added 23 double-self-subsuming ternary resolvents
c [quatres-12-2] added 819 single-self-subsuming ternary resolvents
c [quatres-12-2] added 3421 quaternary resolvents
c [ternres-12] limit 46456792 with penalty 0 = 0 + 0
c [ternres-12] 59 schedulable variables 0%
c [ternres-12] 19695 ternary resolvents (1061 bin, 18634 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-40] removed 94 variables
c [basicprobe-6] limit 232283962 penalty 0 = 0 + 0
c [basicprobe-6-0] 157130 sched 67%, 3103 failed, 141 lifted, 94116 hbrs
c [decomp-41] removed 9025 variables
c [basicprobe-6-1] 80301 probes remain 35% after last round
c [basicprobe-6-1] 3729 units = 3550 failed (95%) + 179 lifted (5%)
c [basicprobe-6-1] removed 12491 variables, found 107907 hbrs
c [bate-4] eliminated 7481 asymmetric tautologies during probing
c [unhide-16] limit 1161419 with penalty 3 = 0 + 3
c [unhide-16-16] 34 units, 161 failed, 54640 tauts, 0 hbrs, 38321 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1956 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 229758 variables 100%
c [block-6] limit of 116141981 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 13208 blocked clauses
c [block-6] 13208 < 1/100 * 1602232 = 16022 considered unsuccessful
c [cce-5] limit of 58070990 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 22
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 19
c [cce-5-1] eliminated 3 clauses out of 711 (0%) of length 18
c [cce-5-1] eliminated 6 clauses out of 435 (1%) of length 16
c [cce-5-1] eliminated 13 clauses out of 1371 (1%) of length 15
c [cce-5-1] eliminated 60 clauses out of 1329 (5%) of length 14
c [cce-5-1] eliminated 616 clauses out of 2973 (21%) of length 13
c [cce-5-1] eliminated 754 clauses out of 4695 (16%) of length 12
c [cce-5-1] eliminated 908 clauses out of 6423 (14%) of length 11
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 2368 large clauses in 58071060 steps
c [cce-5-1] allowing another 29035530 steps for small clauses
c [cce-5-1] scheduling 833324 clauses = 642438 binary + 190886 ternary
c [cce-5-1] tried to eliminate 15281 small clauses 2%
c [cce-5-1] eliminated 2602 binary clauses 0%
c [cce-5-1] eliminated 890 ternary clauses 0%
c [cce-5-1] eliminated 3492 small clauses 0%
c [cce-5-1] eliminated 3492 small clauses in 58071059 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 5860 covered clauses in round 1
c [cce-5] eliminated 5860 covered clauses in TOTAL during 1 rounds
c [cce-5] 5860 < 1/100 * 1587618 = 15876 considered unsuccessful
c [elim-13] 714 variables 0% will be scheduled this time
c [elim-13] scheduled 714 variables 0%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] no variable eliminated in round 1 in 120230840 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 1 = 0% variables out of 714 scheduled
c [elim-13] 1 < 1/100 * 714 = 7 considered unsuccessful
c [bca-12] limit of 10000000 steps and 3171396 added (scaled 2)
c [bca-12] 390046 out of 458604 literals actually usable 85%
c [bca-12] added 2175 blocked clauses in 1209504 steps
c [sweep-12] limit 13937037 penalty 0 = 0 + 0
c [sweep-12-1] 69314 pos 38.2% + 112127 neg 61.8% = 181441 sched 79.1% ret 47860
c [sweep-12-1] 13953905 steps 470 queries 40634.94 avg class size
c [sweep-12-1] 5453 decisions 461 SAT calls 32.72 avg env size
c [sweep-12-1] 178830 variables remain 78% (50417 retained 22%)
c [decomp-42] removed 1170 variables
c [sweep-12-1] removed 1170 vars (0 failed, 87 eqs, 82 impls)
c [sweep-12] removed 1170 vars in TOTAL (1 rounds, 469 queries)
c [phase-count-16] 1488674 negative 94.4% of 1576242 except 87568 5.6%
c [phase-count-16] 1465571 positive 93.0% of 1576242 except 110671 7.0%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 19 positive 39%, 30 negative 61%
c [sort-queue-16] sorted 164277 enqueued variables after 77957 conflicts
c [score-dist-16] active 63854 (28%), one 0 (0%), zero 164277 (72%)
c [score-dist-16] max exp 532, different 25 (5%)
c [score-dist-16] median active exp 520, avg 520.8
c [simplification-16] removed 14396 variables 5.9% (228131 remain 15%)
c [simplification-16] removed 131459 irredundant clauses 7.7% (1576242 remain 26%)
c [simplification-16] maximum reduction of 8% = max (6%, 8%)
c [simplification-16] large reduction 8% >= 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 89957 (soft 79957 + delta 10000)
c [simplification-16] new conflict limit 79957 (hard 89957)
c 
c [simplification-17] limit 79957 conflicts (hard 89957) hit after 79957 conflicts
c [quatres-13] found 273734 quaternary clauses 48% in total
c [quatres-13-1] removed 166 duplicate quaternary clauses
c [quatres-13-1] added 75 double-self-subsuming ternary resolvents
c [quatres-13-2] added 875 single-self-subsuming ternary resolvents
c [quatres-13-2] added 1383 quaternary resolvents
c [ternres-13] limit 47085010 with penalty 0 = 0 + 0
c [ternres-13] all 228131 free variables schedulable
c [ternres-13] 25471 ternary resolvents (1268 bin, 24203 trn)
c [ternres-13] 3181 variables remain 1% (224950 retained 99%)
c [decomp-43] removed 114 variables
c [simpleprobe-7] 57235 schedulable variables 25%
c [simpleprobe-7] limit 188340042 penalty 0 = 0 + 0
c [decomp-44] removed 3429 variables
c [simpleprobe-7] 34068 variables remain 15% (190520 retained 85%)
c [simpleprobe-7] removed 3429 variables, found 160222 hbrs, 215 units
c [unhide-17] limit 1177125 with penalty 3 = 0 + 3
c [unhide-17-17] 15 units, 3 failed, 14296 tauts, 0 hbrs, 10686 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 2166 transitive binary clauses
c [bca-13] limit of 10000000 steps and 3108892 added (scaled 2)
c [bca-13] 379399 out of 449088 literals actually usable 84%
c [bca-13] added 173 blocked clauses in 1179602 steps
c [sweep-13] limit 14125503 penalty 0 = 0 + 0
c [sweep-13-1] 66753 pos 38.2% + 108193 neg 61.8% = 174946 sched 77.9% ret 49597
c [sweep-13-1] 14246327 steps 446 queries 35624.61 avg class size
c [sweep-13-1] 5238 decisions 432 SAT calls 35.71 avg env size
c [sweep-13-1] 171732 variables remain 76% (52805 retained 24%)
c [decomp-45] removed 233 variables
c [sweep-13-1] removed 233 vars (0 failed, 62 eqs, 60 impls)
c [sweep-13] removed 233 vars in TOTAL (1 rounds, 445 queries)
c [phase-count-17] 1458682 negative 94.3% of 1547185 except 88503 5.7%
c [phase-count-17] 1438205 positive 93.0% of 1547185 except 108980 7.0%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 10 positive 45%, 12 negative 55%
c [sort-queue-17] sorted 159920 enqueued variables after 79957 conflicts
c [score-dist-17] active 64390 (29%), one 0 (0%), zero 159920 (71%)
c [score-dist-17] max exp 532, different 25 (5%)
c [score-dist-17] median active exp 520, avg 520.9
c [simplification-17] removed 3821 variables 1.7% (224310 remain 15%)
c [simplification-17] removed 29057 irredundant clauses 1.8% (1547185 remain 26%)
c [simplification-17] maximum reduction of 2% = max (2%, 2%)
c [simplification-17] geometric conflict interval increment 7777 = 23332 / 3
c [simplification-17] new conflict interval 31109
c [simplification-17] penalized conflict interval 31109 = 1 * 31109
c [simplification-17] hard conflict limit 126620 (soft 111066 + delta 15554)
c [simplification-17] new conflict limit 111066 (hard 126620)
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  675.9  224309  1547185     87498   60756 172055 549598   28   356  209   8%    136  129   93   71  131%
c 
c [simplification-18] limit 111066 conflicts (hard 126620) hit after 126621 conflicts
c [quatres-14] found 269525 quaternary clauses 48% in total
c [quatres-14-1] removed 457 duplicate quaternary clauses
c [quatres-14-1] added 19 double-self-subsuming ternary resolvents
c [quatres-14-2] added 559 single-self-subsuming ternary resolvents
c [quatres-14-2] added 535 quaternary resolvents
c [ternres-14] limit 103354596 with penalty 0 = 0 + 0
c [ternres-14] 3030 schedulable variables 1%
c [ternres-14] 25517 ternary resolvents (1119 bin, 24398 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-46] removed 255 variables
c [treelook-7] limit 10335459 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 186406 literals 42%
c [treelook-7] scheduling used 4122647 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 10335459 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 10338372 steps
c [treelook-7] 185384 literals remain 41%
c [treelook-7] 24785 variables remain to probed next time 11%
c [decomp-47] removed 41 variables
c [treelook-7] removed 88 variables, found 6903 hbrs
c [unhide-18] limit 2500000 with penalty 3 = 0 + 3
c [unhide-18-18] 19 units, 82 failed, 88227 tauts, 0 hbrs, 77598 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 1892 transitive binary clauses
c [transred-14] found 2 units
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 223822 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14] incomplete 292 not tried 0% in round 1
c [gc-130] reconnected 468666 binary clauses (produced 0 empty 1 units)
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 12872 = 6% variables out of 223822 scheduled
c [bca-14] limit of 10000000 steps and 2999230 added (scaled 2)
c [bca-14] 354180 out of 421902 literals actually usable 84%
c [bca-14] added 2039 blocked clauses in 1141435 steps
c [sweep-14] limit 31006378 penalty 0 = 0 + 0
c [sweep-14-1] 61080 pos 37.8% + 100457 neg 62.2% = 161537 sched 76.6% ret 49413
c [sweep-14-1] 31008793 steps 960 queries 20650.75 avg class size
c [sweep-14-1] 13472 decisions 922 SAT calls 37.60 avg env size
c [sweep-14-1] 154535 variables remain 73% (56394 retained 27%)
c [decomp-48] removed 580 variables
c [sweep-14-1] removed 580 vars (0 failed, 182 eqs, 166 impls)
c [sweep-14] removed 580 vars in TOTAL (1 rounds, 959 queries)
c [phase-count-18] 1406638 negative 94.3% of 1491102 except 84464 5.7%
c [phase-count-18] 1386109 positive 93.0% of 1491102 except 104993 7.0%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 33 positive 59%, 23 negative 41%
c [sort-queue-18] sorted 144828 enqueued variables after 126621 conflicts
c [score-dist-18] active 65542 (31%), one 0 (0%), zero 144828 (69%)
c [score-dist-18] max exp 533, different 26 (5%)
c [score-dist-18] median active exp 521, avg 522.1
c [simplification-18] removed 13939 variables 6.2% (210370 remain 14%)
c [simplification-18] removed 56083 irredundant clauses 3.6% (1491102 remain 25%)
c [simplification-18] maximum reduction of 6% = max (6%, 4%)
c [simplification-18] large reduction 6% >= 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 138621 (soft 128621 + delta 10000)
c [simplification-18] new conflict limit 128621 (hard 138621)
c 
c [simplification-19] limit 128621 conflicts (hard 138621) hit after 138622 conflicts
c [quatres-15] found 265059 quaternary clauses 48% in total
c [quatres-15-1] removed 65 duplicate quaternary clauses
c [quatres-15-1] added 28 double-self-subsuming ternary resolvents
c [quatres-15-2] added 693 single-self-subsuming ternary resolvents
c [quatres-15-2] added 3687 quaternary resolvents
c [ternres-15] limit 115743492 with penalty 0 = 0 + 0
c [ternres-15] all 210370 free variables schedulable
c [ternres-15] 21115 ternary resolvents (1181 bin, 19934 trn)
c [ternres-15] 9 variables remain 0% (210361 retained 100%)
c [gauss-5] limit 1446793 penalty 4 = 4 + 0
c [gauss-5] extracted 2972 xors of average arity 3.0
c [gauss-5] connected 8899 occurrences of 3865 variables (average 2.3)
c [gauss-5] limit 1446793 penalty 4 = 4 + 0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-49] removed 59 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 74083 sched 36%, 791 failed, 44 lifted, 25505 hbrs
c [decomp-50] removed 2358 variables
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 22018 basic ate = 17022 trn 77% + 4996 lrg 23% in 4 updates
c bcas: 14 count, 26704 added (20505 skipped), 23260018 steps
c bkwd: tried 1327948 clauses, 2651362 lits, 2.00 lits/clause
c bkwd: checked 123202702 occs, 92.78 occs/clause, 46.47 occs/lit
c bkwd: subsumed 19 binary, 983 ternary, 1130 large
c bkwd: strengthened 41 binary, 43 ternary (100% self), 5470 large (0% self)
c blkd: 6 bces, 81996 removed, 53005435 resolutions, 138907686 steps
c blkd: 42441 blocking literals 1%, 2208 pure
c bump: 144922 bumped seen, 94464605 lits 651.8 on average
c card: 5 count, 0 units, 0 am1, 75534752 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 10046 subsumed
c card: 4245 at-most-one constraints found, average size 3.06
c card: 4245 at-most-one constraints used 100%, average size 3.06
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: 5 cces, 50666 eliminated, 47469 ate 94%, 3197 abce 6%
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: 21188985 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 135 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 50 decompositions, 157590 equivalent 10%
c deco: 38447 decision-only clauses 27%, 60% reduction
c decs: 2823357 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 14 elims, 880608 eliminated 57%, 12575 pure 1%
c elms: 17 rounds, 1.2 rounds/bve
c elms: 761468 small 86%, 104357 large 12%
c elms: 975779 tried small, 761468 succeeded 78%, 214311 failed 22%
c elms: 342505 subsumed, 434949 strengthened, 14162 blocked
c elms: 56763598 copies, 71210537 resolutions, 18928926 ipos
c elms: 44376964 subchks, 83383897 strchks
c gaus: 5 extractions, 21378 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12905110 steps, 6452555 extr 50%, 6478184 elim 50%
c glue: 94.6 orig avg, 94.6 real avg, 6.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1822535 = 656385 simple 36% + 1156977 trn 63% + 9173 lrg 1%, 47193 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 144922 clauses, 142.1 length
c lrnd: 20599586 lits = 40599754 orig - 20000168 removed 49%
c lrnd: 40393 uips 28%, 54564 flips 38%
c mins: 97255 mins 68%, 2045 bin 1%, 4322 size 3%
c mins: 32470859 poisoned searches, 3925855 hits, 12% hit rate
c mins: 42284586 used twice searches, 1738521 hits, 4% hit rate
c move: moved 143016, 51154 bin 36%, 91862 trn 64%
c otfs: 1056 driving 37%, 1769 restarting 63%
c otfs: str 2825, 2285 red 81%, 540 irr 19%
c otfs: str 2825, 0 bin 0%, 741 trn 26%, 2084 lrg 74%
c otfs: sub 136, 105 red 77%, 31 irr 23%
c otfs: sub 136, 0 bin 0%, 41 trn 30%, 95 lrg 70%
c phas: 18 computed, 1166732 set, 540753 pos (46%), 625979 neg (54%)
c prbs: 7 basic, 1382506 probed, 22450 failed, 3935 lifted
c prbs: 7 simple, 2484313 probed, 2905 failed, 19356 eqs
c prbs: 7 treelook, 2182 probed, 77 failed, 0 lifted
c prom: 0 locked 0% out of 686896 tried
c prps: 1743281634 props, 588 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 15 count, 57392 quat, 19075 self1, 660 self2, 6151 dup
c queu: 18 sorted, 2823357 next (83966 steps 0.03)
c queu: 102934482 enq (267910527 steps 2.60), 94464605 deq 92%
c redc: 3223 clauses 14%, 22284 tried 16%, 120 sat 1%
c redc: 6083 lits 3%, 192401 tried 0%, 120 sat 0%
c redc: 464 times jump level reduced, 53.1 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: 380228 removed, 255146 red 67%
c rsts: 5776 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 19 count, 17 confs 89%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 144922 count (298171 tried 2.1), 39869 sub out of 137497 (29.0%)
c swps: 14 count, 14 rounds, 6859 queries (489.9/round)
c swps: 6542 sat calls, 907 unsat (1.1% success rate)
c swps: 92480 decisions 14.1, 7356 conflicts 1.1
c swps; 39540.7 avg class size, 36.1 avg environment size
c swps: 0 failed, 1274 impls, 1179 equivs
c swp0: 2281 type 0 queries, 208 unsat (9.1%), 2225 sat (97.5%)
c swp1: 4578 type 1 queries, 2838 unsat (62.0%), 3455 sat (75.5%)
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: 5936970 calls to obtain time
c tops: 294825 fixed 19%, 65 its, 2132.65 confs/it
c trds: 14 transitive reductions, 22047 removed, 120 failed
c trds: 354130 nodes, 580565 edges, 31455355 steps
c trim: 1122664 words, 4.3 MB
c trnr: 15 count, 19454 bin, 595832 trn, 526140424 steps
c unhd: 18 count, 18 rounds, 287575940 steps
c unhd: 37751 non-trivial sccs of average size 2.4
c unhd: 5017 units, 4964 bin, 51 trn, 2 lrg
c unhd: 7343 failed, 6321 stamp, 0 lits, 39 bin, 839 trn, 2 lrg
c unhd: 647402 tauts, 10848 bin 2%, 160982 trn 25%, 51886 lrg 8%
c unhd: 647402 tauts, 423686 stamp 65%, 440864 red 68%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1082425 str, 4964 bin 0%, 86589 trn 8%, 990872 lrg 92%, 489390 red 45%
c vars: 207048 remaining 13% and 1333023 removed 87% out of 1540071
c vars: 294825 fixed 19%, 880608 eliminated 57%, 157590 equivalent 10%
c vsts: 12271576030 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 7.0 search visits per propagation, 83495.8 per conflict
c wchs: 1590175395 pushed, 248369312 enlarged, 203 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         194889             0             0      14168454       4421247         54314
c 
c  0 0         73204  38         0   0<        0   0< 10483340  74   2541551  57     15911  29     1.0
c  1 5          3950   2         0   0         0   0    959533   7<   436587  10<     3895   7     0.1
c  2 6          9181   5         0   0         0   0   1148462   8    556684  13      5692  10     0.5
c  3 9         12862   7         0   0         0   0    562176   4    294594   7      4222   8     1.2
c  4 14        11481   6         0   0         0   0    355334   3    183302   4      4472   8<    1.4
c  5 21        10184   5<        0   0         0   0    172913   1     95387   2      2496   5     2.0
c  6 30         8446   4         0   0         0   0    103086   1     55871   1      3487   6     2.0
c  7 41         5589   3         0   0         0   0     82784   1     53925   1      4127   8     1.6
c  8 54         4739   2         0   0         0   0     69770   0     44104   1      2359   4     2.1
c  9 69         4079   2         0   0         0   0     46750   0     30591   1      1025   2     2.2
c 10 86        12350   6         0   0         0   0     70960   1     51265   1      2317   4     6.2
c 11 126       20765  11         0   0         0   0     55195   0     37336   1      1443   3     9.0
c 12 230       17938   9         0   0         0   0     57937   0     39968   1      2859   5    16.5
c 13 534         121   0         0   0         0   0       214   0        82   0         9   0     0.1
c 
c avg                  4.6           0.0           0.0           0.8           1.4           3.9
c std                  4.6           0.0           0.0           1.9           2.5           3.8
c 
c  104.003  10% elim
c   98.236  10% probe
c   72.408   7% sweep
c   41.966   4% unhide
c   26.538   3% bump
c   21.869   2% block
c   20.559   2% bca
c   19.429   2% cce
c   16.970   2% quatres
c    7.798   1% gauss
c 
c   11.052 < 1% rest (below)
c 
c    5.726   1% ternres
c    2.618   0% decide
c    1.986   0% transred
c    0.722   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   18.921   2% preprocessing     4%
c  457.214  46% inprocessing     96%
c ==================================
c  476.135  48% simplifying
c  519.699  52% search
c ==================================
c  995.858 100% all
c 
c        138622 conflicts,         139.2 confs/sec
c          2398 ternaries,          57.8 confs/ternary
c          1158 binaries,          119.7 confs/binary
c            65 iterations,       2132.6 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          5776 restarts,            5.8 rests/sec,     24.0 confs/restart
c       2823357 decisions,        2835.1 decis/sec,     20.4 decis/conflict
c    1743281634 propagations,  1750532.7 props/sec,    617.4 props/decision
c 
c 995.9 seconds, 613.7 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
