c launch: /data/cnf/sc2014/app/SAT_dat.k85-24_1_rule_3.cnf.bz2
c host: atom16
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.k85-24_1_rule_3.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k85-24_1_rule_3.cnf.bz2
c no embedded options
c found 'p cnf 1376701 5395102' header
c read 1376701 variables, 5395102 clauses, 13543383 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=4
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 1333833 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0 1333833  5352100         0       0      0     0    0     0  276   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1338025 based on 5352100 irredundant clauses
c [card-1] found 1157 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1338025 for elimination
c [card-1] 1157 out of 1157 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 297359 variables
c [simpleprobe-1] all 1079342 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 8778580 based on 4389290 irredundant clauses
c [decomp-2] removed 5368 variables
c [simpleprobe-1] 881094 variables remain 82% (192880 retained 18%)
c [simpleprobe-1] removed 5368 variables, found 10747 hbrs, 950 units
c [unhide-1] limit 272568 based on 4361090 irredundant clauses
c [unhide-1-1] 1426 units, 1036 failed, 9528 tauts, 0 hbrs, 54975 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1067971 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 986657 not tried 92% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 81322 = 8% variables out of 1067971 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3883753 negative 95.2% of 4079881 except 196128 4.8%
c [phase-count-1] 3820819 positive 93.7% of 4079881 except 259062 6.3%
c [phase-1] phase bias: 458362 positive 46%, 528287 negative 54%
c [sort-queue-1] sorted 986649 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 986649 (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 178414 variables 15.3% (986649 remain 74%)
c [simplification-1] removed 1272219 irredundant clauses 23.8% (4079881 remain 76%)
c [simplification-1] maximum reduction of 24% = max (15%, 24%)
c [simplification-1] large reduction 24% >= 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   16.5  986648  4079881         4       2     10  9268    0     0  249   1%      0    0    0    0 25376%
c i   16.5  986515  4079881        11       6     10  9270    0     0  249   1%      0    0    0    0 24972%
c i   16.5  986463  4079881        12       6     10  9270    0     0  249   1%      0    0    0    0 24874%
c i   16.7  986461  4079881        83      58     18  9277    0     1  249   6%      0    1    1    0 22169%
c i   16.9  986460  4079881       154     116     24  9281    0     2  249   9%      0    2    2    0 20509%
c i   17.1  986305  4079881       232     174     36  9284    0     3  249   9%      0    3    3    0 17426%
c i   17.2  986304  4079881       250     185     38  9288    0     3  249   9%      0    3    3    0 16634%
c i   17.7  986303  4079881       353     253     53  9303    0     6  249   5%      0    6    3    0 13410%
c i   17.7  986302  4079881       356     255     53  9303    0     6  249   5%      0    6    3    0 13357%
c i   18.7  986301  4079881       526     387     70  9321    0    10  249   5%      0   10    4    0 10963%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 3809 variables
c [simpleprobe-2] 806583 schedulable variables 82%
c [simpleprobe-2] limit 8137872 based on 4068936 irredundant clauses
c [decomp-4] removed 1771 variables
c [simpleprobe-2] 715691 variables remain 73% (265378 retained 27%)
c [simpleprobe-2] removed 1771 variables, found 34767 hbrs, 288 units
c [treelook-1] limit 1015418 based on 4061673 irredundant clauses
c [treelook-1] scheduled 204020 literals 10%
c [treelook-1] scheduling used 1015734 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1015418 based on 4061673 irredundant clauses
c [treelook-1] used 1033079 steps
c [treelook-1] 203884 literals remain 10%
c [treelook-1] 201442 variables remain to probed next time 21%
c [decomp-5] removed 84 variables
c [treelook-1] removed 87 variables, found 4921 hbrs
c [basicprobe-1] limit 32490216 based on 4061277 irredundant clauses
c [basicprobe-1-0] 885806 probes remain 91% after last round
c [basicprobe-1-0] 2653 units = 1815 failed (68%) + 838 lifted (32%)
c [basicprobe-1-0] removed 8585 variables, found 215272 hbrs
c [unhide-2] limit 253829 based on 4061277 irredundant clauses
c [unhide-2-2] 806 units, 1031 failed, 13174 tauts, 0 hbrs, 32655 literals
c [elim-2] 969765 variables 100% will be scheduled this time
c [elim-2] scheduled 969765 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 889179 not tried 92% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 80586 = 8% variables out of 969765 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 3636308 negative 95.1% of 3823111 except 186803 4.9%
c [phase-count-2] 3572139 positive 93.4% of 3823111 except 250972 6.6%
c [phase-2] phase bias: 957 positive 32%, 2029 negative 68%
c [sort-queue-2] sorted 880071 enqueued variables after 526 conflicts
c [score-dist-2] active 9108 (1%), one 0 (0%), zero 880071 (99%)
c [score-dist-2] max exp 505, different 7 (1%)
c [score-dist-2] median active exp 501, avg 501.3
c [simplification-2] removed 96895 variables 9.8% (889179 remain 67%)
c [simplification-2] removed 256770 irredundant clauses 6.3% (3823111 remain 71%)
c [simplification-2] maximum reduction of 10% = max (10%, 6%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1016 (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   42.8  889178  3823111       851     539     85 188448    1    12  243   7%      1   12    5    0 8198%
c i   43.0  889168  3823111       881     560     89 188452    1    12  243   7%      1   12    4    0 7697%
c i   43.1  889161  3823111       885     563     89 188452    1    12  243   7%      1   12    4    0 7620%
c i   43.1  889160  3823111       886     563     89 188452    1    12  243   7%      1   12    4    0 7591%
c 
c [simplification-3] limit 1028 conflicts (hard 11000) hit after 1028 conflicts
c [card-2] limit 955777 based on 3823111 irredundant clauses
c [card-2] found 863 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 955777 for elimination
c [card-2] 863 out of 863 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 5286 variables
c [treelook-2] limit 953529 based on 3814117 irredundant clauses
c [treelook-2] scheduled 182287 literals 10%
c [treelook-2] scheduling used 954555 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 953529 based on 3814117 irredundant clauses
c [treelook-2] used 953993 steps
c [treelook-2] 182146 literals remain 10%
c [treelook-2] 113031 variables remain to probed next time 13%
c [decomp-7] removed 139 variables
c [treelook-2] removed 162 variables, found 3228 hbrs
c [unhide-3] limit 238320 based on 3813130 irredundant clauses
c [unhide-3-3] 433 units, 675 failed, 15900 tauts, 0 hbrs, 18432 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 882586 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 803236 not tried 91% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 79350 = 9% variables out of 882586 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 3436094 negative 95.0% of 3617560 except 181466 5.0%
c [phase-count-3] 3372567 positive 93.2% of 3617560 except 244993 6.8%
c [phase-3] phase bias: 510 positive 28%, 1311 negative 72%
c [sort-queue-3] sorted 788752 enqueued variables after 1028 conflicts
c [score-dist-3] active 14484 (2%), one 0 (0%), zero 788752 (98%)
c [score-dist-3] max exp 506, different 10 (2%)
c [score-dist-3] median active exp 501, avg 500.9
c [simplification-3] removed 85924 variables 9.7% (803236 remain 60%)
c [simplification-3] removed 205551 irredundant clauses 5.4% (3617560 remain 68%)
c [simplification-3] maximum reduction of 10% = max (10%, 5%)
c [simplification-3] large reduction 10% >= 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 13028 (soft 3028 + delta 10000)
c [simplification-3] new conflict limit 3028 (hard 13028)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   60.8  803235  3617560      1047     563    108 158851    1    16  236   6%      1   16    5    0 6791%
c i   63.1  803234  3617560      1648    1056    163 158884    2    24  237   7%      3   24    6    0 4458%
c i   63.6  803141  3617560      1769    1146    183 158894    2    25  237   7%      3   25    5    0 3632%
c i   63.9  803139  3617560      1810    1182    187 158894    2    26  237   7%      3   26    5    0 3392%
c i   64.2  803137  3617560      1826    1196    188 158894    2    27  238   7%      2   27    5    0 3294%
c i   64.3  803136  3617560      1842    1209    188 158896    2    27  238   7%      2   27    5    0 3343%
c i   64.4  803135  3617560      1852    1215    191 158896    2    28  238   7%      2   27    5    0 3317%
c i   64.7  803134  3617560      1897    1249    199 158897    2    29  238   7%      2   28    5    0 3168%
c i   64.7  803133  3617560      1911    1260    200 158898    2    29  238   7%      2   28    5    0 3167%
c i   65.9  803132  3617560      2142    1431    226 158925    2    31  238   7%      2   30    5    0 3274%
c 
c [simplification-4] limit of 178 binary hit after 178 binaries
c [decomp-8] removed 1219 variables
c [basicprobe-2] limit 28914936 based on 3614367 irredundant clauses
c [basicprobe-2-0] 614925 probes remain 77% after last round
c [basicprobe-2-0] 1433 units = 1310 failed (91%) + 123 lifted (9%)
c [basicprobe-2-0] removed 3267 variables, found 146332 hbrs
c [unhide-4] limit 225897 based on 3614367 irredundant clauses
c [unhide-4-4] 373 units, 606 failed, 14685 tauts, 0 hbrs, 34266 literals
c [elim-4] 797584 variables 100% will be scheduled this time
c [elim-4] scheduled 797584 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 194607320 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 63510 not tried 8% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 454313 = 57% variables out of 797584 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 2390195 negative 95.8% of 2496005 except 105810 4.2%
c [phase-count-4] 2346972 positive 94.0% of 2496005 except 149033 6.0%
c [phase-4] phase bias: 3050 positive 38%, 5083 negative 62%
c [sort-queue-4] sorted 328677 enqueued variables after 2416 conflicts
c [score-dist-4] active 14594 (4%), one 0 (0%), zero 328677 (96%)
c [score-dist-4] max exp 505, different 14 (3%)
c [score-dist-4] median active exp 500, avg 499.7
c [simplification-4] removed 459861 variables 57.3% (343271 remain 26%)
c [simplification-4] removed 1121555 irredundant clauses 31.0% (2496005 remain 47%)
c [simplification-4] maximum reduction of 57% = max (57%, 31%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3029 (hard 13028)
c [simplification-4] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   94.5  343270  2496005      2565     587    155 72067    2    43  213   5%      3   42    4    0 2286%
c i   94.5  343269  2496005      2567     588    155 72067    2    43  213   5%      3   42    4    0 2285%
c i   94.5  343268  2496005      2584     602    156 72068    2    43  213   5%      3   42    4    0 2310%
c 
c [simplification-5] limit 3034 conflicts (hard 13028) hit after 3035 conflicts
c [quatres-1] found 300419 quaternary clauses 36% in total
c [quatres-1-1] removed 4 duplicate quaternary clauses
c [quatres-1-1] added 113 double-self-subsuming ternary resolvents
c [quatres-1-2] added 4858 single-self-subsuming ternary resolvents
c [quatres-1-2] added 9616 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 10000000 with penalty 1 = 0 + 1
c [ternres-1] all 343268 free variables schedulable
c [ternres-1] 39982 ternary resolvents (52 bin, 39930 trn)
c [ternres-1] 235135 variables remain 68% (108133 retained 32%)
c [gauss-1] limit 1247474 based on 2494948 irredundant clauses
c [gauss-1] extracted 5553 xors of average arity 3.0
c [gauss-1] connected 16491 occurrences of 6422 variables (average 2.6)
c [gauss-1] limit 1247464 based on 2494929 irredundant clauses
c [gauss-1] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-9] removed 1553 variables
c [simpleprobe-3] 251493 schedulable variables 74%
c [simpleprobe-3] limit 4983278 based on 2491639 irredundant clauses
c [decomp-10] removed 175 variables
c [simpleprobe-3] 253961 variables remain 74% (87579 retained 26%)
c [simpleprobe-3] removed 175 variables, found 9457 hbrs, 29 units
c [unhide-5] limit 155637 based on 2490192 irredundant clauses
c [unhide-5-5] 100 units, 183 failed, 87202 tauts, 0 hbrs, 132783 literals
c [transred-1] limit 2417729 based on 2417729 irredundant clauses
c [transred-1] removed 878 transitive binary clauses
c [transred-1] found 19 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 341234 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 25940 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 22
c [cce-1-1] eliminated 2 clauses out of 7 (29%) of length 21
c [cce-1-1] eliminated 3 clauses out of 10 (30%) of length 20
c [cce-1-1] eliminated 2 clauses out of 49 (4%) of length 19
c [cce-1-1] eliminated 289 clauses out of 1328 (22%) of length 18
c [cce-1-1] eliminated 249 clauses out of 1413 (18%) of length 17
c [cce-1-1] eliminated 261 clauses out of 620 (42%) of length 16
c [cce-1-1] eliminated 1 clauses out of 2008 (0%) of length 15
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 808 large clauses in 15000006 steps
c [cce-1-1] allowing another 7500003 steps for small clauses
c [cce-1-1] scheduling 1358061 clauses = 1054029 binary + 304032 ternary
c [cce-1-1] tried to eliminate 2373 small clauses 0%
c [cce-1-1] eliminated 352 binary clauses 0%
c [cce-1-1] eliminated 90 ternary clauses 0%
c [cce-1-1] eliminated 442 small clauses 0%
c [cce-1-1] eliminated 442 small clauses in 15000005 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1250 covered clauses in round 1
c [cce-1] eliminated 1250 covered clauses in TOTAL during 1 rounds
c [cce-1] 1250 < 1/100 * 2387994 = 23879 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 340738 variables 100%
c [elim-5] limit of 23033480 steps penalty 1 = 0 + 1
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 224153 not tried 66% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 12378 = 4% variables out of 340738 scheduled
c [bca-1] limit of 10000000 steps and 4728784 added (scaled 2)
c [bca-1] 631595 out of 656722 literals actually usable 96%
c [bca-1] added 7355 blocked clauses in 2002322 steps
c [sweep-1] limit 4728284 based on 2364142 irredundant clauses
c [sweep-1-1] 110318 pos 33.6% + 218042 neg 66.4% = 328360 sched 100.0% ret 0
c [sweep-1-1] 4737349 steps 95 queries 102642.65 avg class size
c [sweep-1-1] 1504 decisions 89 SAT calls 37.55 avg env size
c [sweep-1-1] 327912 variables remain 100% (389 retained 0%)
c [decomp-11] removed 497 variables
c [sweep-1-1] removed 497 vars (0 failed, 25 eqs, 23 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 497 vars in TOTAL (1 rounds, 94 queries)
c [phase-count-5] 2260831 negative 95.7% of 2362542 except 101711 4.3%
c [phase-count-5] 2234585 positive 94.6% of 2362542 except 127957 5.4%
c [phase-5] phase bias: 1197 positive 54%, 1019 negative 46%
c [sort-queue-5] sorted 311480 enqueued variables after 3035 conflicts
c [score-dist-5] active 16383 (5%), one 0 (0%), zero 311480 (95%)
c [score-dist-5] max exp 508, different 19 (4%)
c [score-dist-5] median active exp 500, avg 499.3
c [simplification-5] removed 15405 variables 4.5% (327863 remain 25%)
c [simplification-5] removed 133463 irredundant clauses 5.3% (2362542 remain 44%)
c [simplification-5] maximum reduction of 5% = max (4%, 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 15035 (soft 5035 + delta 10000)
c [simplification-5] new conflict limit 5035 (hard 15035)
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  119.4  327862  2362542      3191    9240  37004 82945    3    48  210   6%      4   47    9    0 3496%
c i  120.8  327861  2362541      3788    9721  37053 82982    4    54  211   7%      4   53    9    0 2902%
c 
c [simplification-6] limit 5035 conflicts (hard 15035) hit after 5036 conflicts
c [quatres-2] found 307917 quaternary clauses 39% in total
c [quatres-2-1] removed 8 duplicate quaternary clauses
c [quatres-2-1] added 57 double-self-subsuming ternary resolvents
c [quatres-2-2] added 2029 single-self-subsuming ternary resolvents
c [quatres-2-2] added 7483 quaternary resolvents
c [ternres-2] limit 9449436 based on 2362359 irredundant clauses
c [ternres-2] 224493 schedulable variables 68%
c [ternres-2] 39878 ternary resolvents (990 bin, 38888 trn)
c [ternres-2] 141092 variables remain 43% (186684 retained 57%)
c [card-3] limit 590589 based on 2362359 irredundant clauses
c [card-3] found 350 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 590589 for elimination
c [card-3] 350 out of 350 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 1181179 based on 2362359 irredundant clauses
c [gauss-2] extracted 4904 xors of average arity 3.0
c [gauss-2] connected 14665 occurrences of 4947 variables (average 3.0)
c [gauss-2] limit 1180739 based on 2361478 irredundant clauses
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 351 variables
c [treelook-3] limit 590255 based on 2361022 irredundant clauses
c [treelook-3] scheduled 70197 literals 11%
c [treelook-3] scheduling used 590258 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 590255 based on 2361022 irredundant clauses
c [treelook-3] used 595420 steps
c [treelook-3] 70077 literals remain 11%
c [treelook-3] 41605 variables remain to probed next time 13%
c [decomp-13] removed 25 variables
c [treelook-3] removed 33 variables, found 1392 hbrs
c [unhide-6] limit 147552 based on 2360833 irredundant clauses
c [unhide-6-6] 207 units, 381 failed, 4103 tauts, 0 hbrs, 67408 literals
c [transred-2] limit 2358509 based on 2358509 irredundant clauses
c [transred-2] removed 838 transitive binary clauses
c [transred-2] found 19 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 326713 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 0 + 1
c [block-2] incomplete 3292 not tried 1%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 8735 blocked clauses
c [block-2] 8735 < 1/100 * 2357823 = 23578 considered unsuccessful
c [elim-6] 62229 variables 19% will be scheduled this time
c [elim-6] scheduled 62229 variables 19%
c [elim-6] limit of 33997665 steps penalty 1 = 0 + 1
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 31857 not tried 10% in round 1
c [gc-45] reconnected 84333 binary clauses (produced 0 empty 1 units)
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 660 = 1% variables out of 62229 scheduled
c [elim-6] 660 < 1/100 * 62229 = 622 considered unsuccessful
c [bca-2] limit of 10000000 steps and 4614473 added (scaled 2)
c [bca-2] 612253 out of 651910 literals actually usable 94%
c [bca-2] added 1757 blocked clauses in 1919002 steps
c [sweep-2] limit 4610296 based on 2305148 irredundant clauses
c [sweep-2-1] 113355 pos 34.8% + 212247 neg 65.2% = 325602 sched 99.9% ret 352
c [sweep-2-1] 4614732 steps 102 queries 98493.10 avg class size
c [sweep-2-1] 1525 decisions 92 SAT calls 32.76 avg env size
c [sweep-2-1] 325011 variables remain 100% (940 retained 0%)
c [decomp-14] removed 671 variables
c [sweep-2-1] removed 671 vars (0 failed, 13 eqs, 20 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 671 vars in TOTAL (1 rounds, 101 queries)
c [phase-count-6] 2201143 negative 95.6% of 2303584 except 102441 4.4%
c [phase-count-6] 2174362 positive 94.4% of 2303584 except 129222 5.6%
c [phase-6] phase bias: 422 positive 49%, 440 negative 51%
c [sort-queue-6] sorted 302576 enqueued variables after 5036 conflicts
c [score-dist-6] active 22707 (7%), one 0 (0%), zero 302576 (93%)
c [score-dist-6] max exp 508, different 26 (5%)
c [score-dist-6] median active exp 500, avg 498.4
c [simplification-6] removed 2493 variables 0.8% (325283 remain 24%)
c [simplification-6] removed 58957 irredundant clauses 2.5% (2303584 remain 43%)
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 21702 (soft 11702 + delta 10000)
c [simplification-6] new conflict limit 11702 (hard 21702)
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  145.5  325282  2303583      6002   17742  70375 84620    6    64  211  10%     21   60    8    1 1276%
c i  148.3  325281  2303579      6864   18457  70442 84644    7    75  211   9%     13   70    7    1  952%
c i  150.0  325280  2303578      7620   19103  70487 84669    8    72  211  11%      9   67   13    1 1505%
c i  155.1  325184  2303574      9945   21073  70608 84724    9    78  212  11%     22   70   10    1  811%
c i  157.6  325175  2303573     10683   21721  70643 84735    9    83  212  10%     13   75    8    1  634%
c i  158.4  325174  2303573     10859   21872  70655 84741    9    84  212  10%     11   76    8    1  594%
c i  159.4  325173  2303573     11316   22262  70677 84751    9    81  212  11%      8   72   15    1 1107%
c 
c [simplification-7] limit 11702 conflicts (hard 21702) hit after 11702 conflicts
c [quatres-3] found 310264 quaternary clauses 41% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 32 double-self-subsuming ternary resolvents
c [quatres-3-2] added 1155 single-self-subsuming ternary resolvents
c [quatres-3-2] added 4456 quaternary resolvents
c [ternres-3] limit 9214056 based on 2303514 irredundant clauses
c [ternres-3] 139825 schedulable variables 43%
c [ternres-3] 43761 ternary resolvents (1310 bin, 42451 trn)
c [ternres-3] 85247 variables remain 26% (239924 retained 74%)
c [decomp-15] removed 572 variables
c [basicprobe-3] limit 18413120 based on 2301640 irredundant clauses
c [basicprobe-3-0] 214999 probes remain 67% after last round
c [basicprobe-3-0] 1447 units = 1361 failed (94%) + 86 lifted (6%)
c [basicprobe-3-0] removed 2297 variables, found 93576 hbrs
c [bate-1] eliminated 2712 asymmetric tautologies during probing
c [unhide-7] limit 167597 with penalty 3 = 0 + 3
c [unhide-7-7] 188 units, 305 failed, 48284 tauts, 0 hbrs, 36950 literals
c [transred-3] limit 2236509 based on 2236509 irredundant clauses
c [transred-3] removed 959 transitive binary clauses
c [transred-3] found 16 units
c [cce-2] limit of 8379887 steps penalty 2 = 1 + 1
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 26
c [cce-2-1] eliminated 5 clauses out of 5 (100%) of length 25
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 24
c [cce-2-1] eliminated 7 clauses out of 10 (70%) of length 23
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 22
c [cce-2-1] eliminated 2 clauses out of 5 (40%) of length 21
c [cce-2-1] eliminated 3 clauses out of 8 (38%) of length 20
c [cce-2-1] eliminated 4 clauses out of 13 (31%) of length 19
c [cce-2-1] eliminated 5 clauses out of 818 (1%) of length 18
c [cce-2-1] eliminated 25 clauses out of 905 (3%) of length 17
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 57 large clauses in 8380119 steps
c [cce-2-1] allowing another 4190059 steps for small clauses
c [cce-2-1] scheduling 1226798 clauses = 972931 binary + 253867 ternary
c [cce-2-1] tried to eliminate 1592 small clauses 0%
c [cce-2-1] eliminated 174 binary clauses 0%
c [cce-2-1] eliminated 53 ternary clauses 0%
c [cce-2-1] eliminated 227 small clauses 0%
c [cce-2-1] eliminated 5498 small clauses in 8380087 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 5555 covered clauses in round 1
c [cce-2] eliminated 5555 covered clauses in TOTAL during 1 rounds
c [cce-2] 5555 < 1/100 * 2236021 = 22360 considered unsuccessful
c [bca-3] limit of 10000000 steps and 4465988 added (scaled 2)
c [bca-3] 592115 out of 643738 literals actually usable 92%
c [bca-3] added 334 blocked clauses in 1815888 steps
c [sweep-3] limit 4460932 based on 2230466 irredundant clauses
c [sweep-3-1] 117814 pos 36.7% + 203140 neg 63.3% = 320954 sched 99.7% ret 914
c [sweep-3-1] 4462254 steps 95 queries 99117.12 avg class size
c [sweep-3-1] 1024 decisions 82 SAT calls 32.48 avg env size
c [sweep-3-1] 320569 variables remain 100% (1283 retained 0%)
c [decomp-16] removed 2594 variables
c [sweep-3-1] removed 2594 vars (0 failed, 23 eqs, 28 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 2594 vars in TOTAL (1 rounds, 94 queries)
c [phase-count-7] 2123219 negative 95.4% of 2225873 except 102654 4.6%
c [phase-count-7] 2102441 positive 94.5% of 2225873 except 123432 5.5%
c [phase-7] phase bias: 584 positive 63%, 340 negative 37%
c [sort-queue-7] sorted 282407 enqueued variables after 11702 conflicts
c [score-dist-7] active 36867 (12%), one 0 (0%), zero 282407 (88%)
c [score-dist-7] max exp 509, different 53 (10%)
c [score-dist-7] median active exp 493, avg 489.1
c [simplification-7] removed 5897 variables 1.8% (319274 remain 24%)
c [simplification-7] removed 77700 irredundant clauses 3.4% (2225873 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 33368 (soft 23368 + delta 10000)
c [simplification-7] new conflict limit 23368 (hard 33368)
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  174.4  319273  2225873     11897   26488  99683 146834   11    75  211  15%      6   66   21    2 1360%
c i  176.1  319272  2225873     12925   27357  99711 146849   11    69  212  17%      7   59   10    2  562%
c i  189.0  319271  2225867     16628   30573  99858 146977   14    82  212  17%     40   67   19    2  767%
c i  194.1  319270  2225866     18393   32151  99897 147007   14    78  213  19%     19   62   13    3  468%
c i  200.7  319269  2225865     20179   33754  99950 147061   14    89  214  16%     15   71   12    3  397%
c i  201.6  319268  2225864     20352   33887  99969 147073   14    92  214  15%     12   74    9    3  305%
c i  204.1  319267  2225863     21097   34563  99997 147087   16    94  214  17%      7   75   30    3  890%
c i  209.6  319236  2225855     23322   36509 100083 147152   15    91  214  17%     18   70   15    4  394%
c i  209.6  319225  2225855     23323   36509 100083 147152   15    91  214  17%     18   70   15    4  392%
c i  209.7  319214  2225855     23369   36545 100087 147155   15    91  214  17%     17   70   13    4  353%
c 
c [simplification-8] limit 23378 conflicts (hard 33368) hit after 23378 conflicts
c [quatres-4] found 308461 quaternary clauses 42% in total
c [quatres-4-1] removed 19 duplicate quaternary clauses
c [quatres-4-1] added 23 double-self-subsuming ternary resolvents
c [quatres-4-2] added 735 single-self-subsuming ternary resolvents
c [quatres-4-2] added 3212 quaternary resolvents
c [ternres-4] limit 8903160 based on 2225790 irredundant clauses
c [ternres-4] 83579 schedulable variables 26%
c [ternres-4] 43598 ternary resolvents (1644 bin, 41954 trn)
c [ternres-4] 45602 variables remain 14% (273555 retained 86%)
c [gauss-3] limit 1112895 based on 2225790 irredundant clauses
c [gauss-3] extracted 4540 xors of average arity 3.0
c [gauss-3] connected 13532 occurrences of 5147 variables (average 2.6)
c [gauss-3] limit 1112257 based on 2224514 irredundant clauses
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 568 variables
c [simpleprobe-4] 236776 schedulable variables 74%
c [simpleprobe-4] limit 27749079 penalty 1 = 0 + 1
c [decomp-18] removed 2196 variables
c [simpleprobe-4] 165297 variables remain 52% (151096 retained 48%)
c [simpleprobe-4] removed 2196 variables, found 73401 hbrs, 615 units
c [unhide-8] limit 346863 with penalty 3 = 0 + 3
c [unhide-8-8] 149 units, 330 failed, 19326 tauts, 0 hbrs, 48817 literals
c [transred-4] limit 2204688 based on 2204688 irredundant clauses
c [transred-4] removed 924 transitive binary clauses
c [transred-4] found 15 units
c [block-3] 3238 variables 1% will be scheduled this time
c [block-3] scheduled 3238 variables 1%
c [block-3] limit of 34686349 steps penalty 2 = 1 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 26 blocked clauses
c [block-3] 26 < 1/100 * 2204233 = 22042 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 315908 variables 100%
c [elim-7] limit of 69372699 steps penalty 2 = 1 + 1
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 85232 not tried 27% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 14204 = 4% variables out of 315908 scheduled
c [bca-4] limit of 10000000 steps and 4323715 added (scaled 2)
c [bca-4] 546563 out of 603410 literals actually usable 91%
c [bca-4] added 616 blocked clauses in 1696020 steps
c [sweep-4] limit 4318492 based on 2159246 irredundant clauses
c [sweep-4-1] 111345 pos 37.0% + 189293 neg 63.0% = 300638 sched 99.6% ret 1066
c [sweep-4-1] 4344128 steps 101 queries 89084.90 avg class size
c [sweep-4-1] 1789 decisions 95 SAT calls 37.71 avg env size
c [sweep-4-1] 299960 variables remain 99% (1742 retained 1%)
c [decomp-19] removed 482 variables
c [sweep-4-1] removed 482 vars (0 failed, 5 eqs, 12 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 482 vars in TOTAL (1 rounds, 100 queries)
c [phase-count-8] 2057457 negative 95.4% of 2157396 except 99939 4.6%
c [phase-count-8] 2039806 positive 94.5% of 2157396 except 117590 5.5%
c [phase-8] phase bias: 420 positive 46%, 494 negative 54%
c [sort-queue-8] sorted 254650 enqueued variables after 23378 conflicts
c [score-dist-8] active 46572 (15%), one 0 (0%), zero 254650 (85%)
c [score-dist-8] max exp 508, different 98 (19%)
c [score-dist-8] median active exp 489, avg 478.7
c [simplification-8] removed 17935 variables 5.6% (301222 remain 23%)
c [simplification-8] removed 68459 irredundant clauses 3.1% (2157396 remain 40%)
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 35378 (soft 25378 + delta 10000)
c [simplification-8] new conflict limit 25378 (hard 35378)
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  236.5  301221  2157393     24951   33799 113873 176979   18   101  213  18%     12   78   19    4  465%
c i  236.6  301220  2157393     24971   33816 113874 176979   18   101  213  18%     12   78   20    4  490%
c i  237.0  301219  2157393     25028   33853 113877 176981   19   103  213  19%     11   80   38    4  884%
c 
c [simplification-9] limit 25378 conflicts (hard 35378) hit after 25379 conflicts
c [quatres-5] found 312663 quaternary clauses 42% in total
c [quatres-5-1] removed 120 duplicate quaternary clauses
c [quatres-5-1] added 13 double-self-subsuming ternary resolvents
c [quatres-5-2] added 1733 single-self-subsuming ternary resolvents
c [quatres-5-2] added 4628 quaternary resolvents
c [ternres-5] limit 8629160 based on 2157290 irredundant clauses
c [ternres-5] 42951 schedulable variables 14%
c [ternres-5] 44054 ternary resolvents (1528 bin, 42526 trn)
c [ternres-5] 19437 variables remain 6% (281782 retained 94%)
c [decomp-20] removed 436 variables
c [treelook-4] limit 776365 penalty 1 = 0 + 1 boost 1
c [treelook-4] scheduled 76818 literals 13%
c [treelook-4] scheduling used 777423 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 776365 penalty 1 = 0 + 1 boost 1
c [treelook-4] used 798762 steps
c [treelook-4] 76774 literals remain 13%
c [treelook-4] 34197 variables remain to probed next time 11%
c [decomp-21] removed 3 variables
c [treelook-4] removed 18 variables, found 1191 hbrs
c [unhide-9] limit 388182 with penalty 3 = 0 + 3
c [unhide-9-9] 61 units, 203 failed, 28004 tauts, 0 hbrs, 25177 literals
c [transred-5] limit 2134661 based on 2134661 irredundant clauses
c [transred-5] removed 1046 transitive binary clauses
c [transred-5] found 11 units
c [elim-8] 30293 variables 10% will be scheduled this time
c [elim-8] scheduled 30293 variables 10%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3105463140 steps penalty 1 = 0 + 1
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 84 variables 0% in round 1 in 655272762 steps
c [elim-8-1] backward subsumption/strengthening limit 655272700
c [elim-8-1-1] backward checking 71706 touched variables 24%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1375 and strengthened 4206 clauses in 120511735 steps
c [elim-8-1] rescheduled 12180 variables 4% by backward subsumption
c [elim-8-2] eliminated 529 variables 0% in round 2 in 149939033 steps
c [elim-8-2] backward subsumption/strengthening limit 149939000
c [elim-8-2-1] backward checking 9041 touched variables 3%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 282 and strengthened 450 clauses in 23331554 steps
c [elim-8-2] rescheduled 2153 variables 1% by backward subsumption
c [elim-8-3] eliminated 98 variables 0% in round 3 in 31464983 steps
c [elim-8-3] backward subsumption/strengthening limit 31464900
c [elim-8-3-1] backward checking 1243 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 50 and strengthened 60 clauses in 5404335 steps
c [elim-8] incomplete 336 not tried 0% in round 3
c [gc-68] reconnected 175739 binary clauses (produced 0 empty 1 units)
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 850 = 3% variables out of 30293 scheduled
c [elim-8] 850 < 1/100 * 30293 = 302 considered unsuccessful
c [bca-5] limit of 10000000 steps and 4172089 added (scaled 2)
c [bca-5] 535325 out of 599310 literals actually usable 89%
c [bca-5] added 1475 blocked clauses in 1659494 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 23290970 penalty 1 = 0 + 1
c [sweep-5-1] 110879 pos 37.2% + 187058 neg 62.8% = 297937 sched 99.4% ret 1717
c [sweep-5-1] 23332381 steps 482 queries 66930.39 avg class size
c [sweep-5-1] 6375 decisions 455 SAT calls 33.66 avg env size
c [sweep-5-1] 293759 variables remain 98% (5757 retained 2%)
c [decomp-22] removed 960 variables
c [sweep-5-1] removed 960 vars (0 failed, 64 eqs, 93 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 960 vars in TOTAL (1 rounds, 481 queries)
c [phase-count-9] 1980213 negative 95.2% of 2079457 except 99244 4.8%
c [phase-count-9] 1963211 positive 94.4% of 2079457 except 116246 5.6%
c [phase-9] phase bias: 304 positive 61%, 198 negative 39%
c [sort-queue-9] sorted 247883 enqueued variables after 25379 conflicts
c [score-dist-9] active 50811 (17%), one 0 (0%), zero 247883 (83%)
c [score-dist-9] max exp 508, different 106 (21%)
c [score-dist-9] median active exp 494, avg 480.8
c [simplification-9] removed 2525 variables 0.8% (298694 remain 22%)
c [simplification-9] removed 77936 irredundant clauses 3.6% (2079457 remain 39%)
c [simplification-9] maximum reduction of 4% = max (1%, 4%)
c [simplification-9] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-9] new conflict interval 15666
c [simplification-9] penalized conflict interval 15666 = 1 * 15666
c [simplification-9] hard conflict limit 51045 (soft 41045 + delta 10000)
c [simplification-9] new conflict limit 41045 (hard 51045)
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  274.7  298693  2079457     26854   39261 137415 178141   20   115  211  17%     13   89   19    5  396%
c i  291.6  298692  2079457     30607   42575 137558 178217   21   135  211  15%     38  103   19    6  330%
c i  291.9  298686  2079457     30734   42627 137577 178223   20   132  211  15%     33  100   13    6  237%
c i  299.6  298627  2079457     32164   43913 137623 178235   22   129  212  17%     14   95   19    6  304%
c i  305.6  298626  2079457     35063   46536 137732 178294   18   103  212  17%     25   66   11    6  172%
c i  306.1  298625  2079457     35369   46788 137754 178302   17   100  212  17%     17   62    9    6  140%
c i  309.9  298616  2079457     37535   48686 137875 178348   13    99  212  13%     16   59    8    6  117%
c i  311.1  298615  2079457     38362   49389 137936 178373   12    96  212  13%      7   55   11    7  166%
c i  311.8  298614  2079457     38784   49740 137967 178386   12    91  212  13%      3   50    9    7  138%
c 
c [simplification-10] limit 41045 conflicts (hard 51045) hit after 41045 conflicts
c [quatres-6] found 306239 quaternary clauses 44% in total
c [quatres-6-1] removed 64 duplicate quaternary clauses
c [quatres-6-1] added 23 double-self-subsuming ternary resolvents
c [quatres-6-2] added 557 single-self-subsuming ternary resolvents
c [quatres-6-2] added 2898 quaternary resolvents
c [ternres-6] limit 12444492 with penalty 1 = 0 + 1
c [ternres-6] 19228 schedulable variables 6%
c [ternres-6] 56285 ternary resolvents (2280 bin, 54005 trn)
c [ternres-6] 4356 variables remain 1% (294258 retained 99%)
c [card-4] limit 777780 penalty 4 = 3 + 1
c [card-4] found 438 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 777780 for elimination
c [card-4] 438 out of 438 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-23] removed 655 variables
c [basicprobe-4] limit 62222464 penalty 1 = 0 + 1
c [basicprobe-4-0] 126268 probes remain 43% after last round
c [basicprobe-4-0] 4231 units = 3869 failed (91%) + 362 lifted (9%)
c [basicprobe-4-0] removed 5572 variables, found 172442 hbrs
c [bate-2] eliminated 2620 asymmetric tautologies during probing
c [unhide-10] limit 622224 with penalty 3 = 0 + 3
c [unhide-10-10] 301 units, 433 failed, 40563 tauts, 0 hbrs, 44340 literals
c [transred-6] limit 2008772 based on 2008772 irredundant clauses
c [transred-6] removed 1226 transitive binary clauses
c [transred-6] found 6 units
c [cce-3] limit of 15555616 steps penalty 3 = 2 + 1
c [cce-3-1] eliminated 5 clauses out of 12 (42%) of length 20
c [cce-3-1] eliminated 1 clauses out of 5 (20%) of length 19
c [cce-3-1] eliminated 9 clauses out of 688 (1%) of length 18
c [cce-3-1] eliminated 7 clauses out of 547 (1%) of length 17
c [cce-3-1] eliminated 13 clauses out of 424 (3%) of length 16
c [cce-3-1] eliminated 133 clauses out of 1198 (11%) of length 15
c [cce-3-1] eliminated 131 clauses out of 1711 (8%) of length 14
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 299 large clauses in 15555623 steps
c [cce-3-1] allowing another 7777811 steps for small clauses
c [cce-3-1] scheduling 1100305 clauses = 863108 binary + 237197 ternary
c [cce-3-1] tried to eliminate 2145 small clauses 0%
c [cce-3-1] eliminated 548 binary clauses 0%
c [cce-3-1] eliminated 78 ternary clauses 0%
c [cce-3-1] eliminated 626 small clauses 0%
c [cce-3-1] eliminated 7840 small clauses in 15555732 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 8139 covered clauses in round 1
c [cce-3] eliminated 8139 covered clauses in TOTAL during 1 rounds
c [cce-3] 8139 < 1/100 * 2008298 = 20082 considered unsuccessful
c [bca-6] limit of 10000000 steps and 4006586 added (scaled 2)
c [bca-6] 512604 out of 583162 literals actually usable 88%
c [bca-6] added 552 blocked clauses in 1554661 steps
c [sweep-6] limit 4000318 based on 2000159 irredundant clauses
c [sweep-6-1] 107053 pos 37.4% + 179253 neg 62.6% = 286306 sched 98.2% ret 5274
c [sweep-6-1] 4030169 steps 79 queries 86043.63 avg class size
c [sweep-6-1] 1114 decisions 69 SAT calls 36.29 avg env size
c [sweep-6-1] 285974 variables remain 98% (5601 retained 2%)
c [decomp-24] removed 5119 variables
c [sweep-6-1] removed 5119 vars (0 failed, 20 eqs, 25 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 5119 vars in TOTAL (1 rounds, 78 queries)
c [phase-count-10] 1890624 negative 95.0% of 1990379 except 99755 5.0%
c [phase-count-10] 1872759 positive 94.1% of 1990379 except 117620 5.9%
c [phase-10] phase bias: 220 positive 48%, 235 negative 52%
c [sort-queue-10] sorted 227947 enqueued variables after 41045 conflicts
c [score-dist-10] active 58514 (20%), one 0 (0%), zero 227947 (80%)
c [score-dist-10] max exp 509, different 168 (33%)
c [score-dist-10] median active exp 460, avg 455.7
c [simplification-10] removed 12153 variables 4.1% (286461 remain 21%)
c [simplification-10] removed 89078 irredundant clauses 4.3% (1990379 remain 37%)
c [simplification-10] maximum reduction of 4% = max (4%, 4%)
c [simplification-10] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-10] new conflict interval 19666
c [simplification-10] penalized conflict interval 19666 = 1 * 19666
c [simplification-10] hard conflict limit 70711 (soft 60711 + delta 10000)
c [simplification-10] new conflict limit 60711 (hard 70711)
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  331.7  286460  1990379     41616   53086 142142 246545   15    68  211  22%     22   25   18    7  262%
c i  331.8  286459  1990379     41645   53106 142145 246547   15    68  211  22%     22   25   18    7  255%
c i  332.3  286458  1990379     41923   53327 142169 246564   15    66  211  22%     15   24   14    7  204%
c i  332.3  286453  1990379     41938   53341 142169 246564   15    66  211  23%     15   24   15    7  211%
c i  332.6  286452  1990379     42066   53449 142178 246569   15    66  211  22%     12   23   13    7  184%
c i  333.4  286365  1990379     42394   53741 142201 246571   14    69  211  21%      8   26   10    7  148%
c i  338.0  286364  1990379     43559   54758 142236 246581   17    69  212  24%      4   25   17    7  236%
c i  345.9  286359  1990379     45532   56522 142272 246598   18    68  212  26%     11   24   35    8  461%
c i  427.6  286358  1990379     53326   63500 142323 246628   48    78  220  61%     93   31   19   13  146%
c i  428.6  286357  1990379     53629   63770 142337 246638   46    80  220  58%     66   33   19   13  147%
c i  449.2  286355  1990379     56969   66564 142389 246649   41    86  221  47%     26   37   36   14  251%
c 
c [simplification-11] limit 60711 conflicts (hard 70711) hit after 60711 conflicts
c [quatres-7] found 298993 quaternary clauses 45% in total
c [quatres-7-1] removed 139 duplicate quaternary clauses
c [quatres-7-1] added 28 double-self-subsuming ternary resolvents
c [quatres-7-2] added 925 single-self-subsuming ternary resolvents
c [quatres-7-2] added 2215 quaternary resolvents
c [ternres-7] limit 50136795 with penalty 0 = 0 + 0
c [ternres-7] 4137 schedulable variables 1%
c [ternres-7] 100845 ternary resolvents (2385 bin, 98460 trn)
c [ternres-7] 40 variables remain 0% (286307 retained 100%)
c [gauss-4] limit 2506839 penalty 2 = 2 + 0
c [gauss-4] extracted 7068 xors of average arity 3.0
c [gauss-4] connected 20985 occurrences of 7927 variables (average 2.6)
c [gauss-4] limit 2506839 penalty 2 = 2 + 0
c [decomp-25] removed 759 variables
c [gauss-4] exported 0 unary, 2 binary and 0 ternary equations
c [decomp-26] removed 1 variables
c [simpleprobe-5] 147634 schedulable variables 52%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-27] removed 12163 variables
c [simpleprobe-5] 76729 variables remain 28% (196695 retained 72%)
c [simpleprobe-5] removed 12163 variables, found 314981 hbrs, 1784 units
c [unhide-11] limit 1253419 with penalty 3 = 0 + 3
c [unhide-11-11] 49 units, 80 failed, 19949 tauts, 0 hbrs, 78735 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 2164 transitive binary clauses
c [transred-7] found 15 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 273208 variables 100%
c [block-4] limit of 125341989 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 19545 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 272470 variables 100%
c [elim-9] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 1178 not tried 0% in round 1
c [gc-84] reconnected 485685 binary clauses (produced 0 empty 1 units)
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 17266 = 6% variables out of 272470 scheduled
c [bca-7] limit of 10000000 steps and 3623084 added (scaled 2)
c [bca-7] 445445 out of 510410 literals actually usable 87%
c [bca-7] added 1730 blocked clauses in 1412007 steps
c [sweep-7] limit 15041038 penalty 0 = 0 + 0
c [sweep-7-1] 90223 pos 36.0% + 160157 neg 64.0% = 250380 sched 98.1% ret 4824
c [sweep-7-1] 15062223 steps 373 queries 54997.11 avg class size
c [sweep-7-1] 5297 decisions 355 SAT calls 41.79 avg env size
c [sweep-7-1] 247172 variables remain 97% (8020 retained 3%)
c [decomp-28] removed 699 variables
c [sweep-7-1] removed 699 vars (0 failed, 47 eqs, 66 impls)
c [sweep-7] removed 699 vars in TOTAL (1 rounds, 372 queries)
c [phase-count-11] 1712813 negative 94.8% of 1806602 except 93789 5.2%
c [phase-count-11] 1695218 positive 93.8% of 1806602 except 111384 6.2%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 427 positive 48%, 461 negative 52%
c [sort-queue-11] sorted 199065 enqueued variables after 60711 conflicts
c [score-dist-11] active 55440 (22%), one 0 (0%), zero 199065 (78%)
c [score-dist-11] max exp 509, different 238 (47%)
c [score-dist-11] median active exp 408, avg 419.8
c [simplification-11] removed 31842 variables 11.1% (254505 remain 19%)
c [simplification-11] removed 183777 irredundant clauses 9.2% (1806602 remain 34%)
c [simplification-11] maximum reduction of 11% = max (11%, 9%)
c [simplification-11] large reduction 11% >= 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 72711 (soft 62711 + delta 10000)
c [simplification-11] new conflict limit 62711 (hard 72711)
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  489.9  254504  1806602     62670   56709 162159 432960   18    68  208  26%     57   17    9   14   67%
c 
c [simplification-12] limit 62711 conflicts (hard 72711) hit after 62711 conflicts
c [quatres-8] found 285145 quaternary clauses 45% in total
c [quatres-8-1] removed 1742 duplicate quaternary clauses
c [quatres-8-1] added 29 double-self-subsuming ternary resolvents
c [quatres-8-2] added 689 single-self-subsuming ternary resolvents
c [quatres-8-2] added 4907 quaternary resolvents
c [ternres-8] limit 50642232 with penalty 0 = 0 + 0
c [ternres-8] 35 schedulable variables 0%
c [ternres-8] 61551 ternary resolvents (1107 bin, 60444 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-29] removed 315 variables
c [treelook-5] limit 5064223 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 195069 literals 38%
c [treelook-5] scheduling used 4414971 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 5064223 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 5074381 steps
c [treelook-5] 194561 literals remain 38%
c [treelook-5] 28089 variables remain to probed next time 11%
c [decomp-30] removed 21 variables
c [treelook-5] removed 79 variables, found 4599 hbrs
c [unhide-12] limit 1266055 with penalty 3 = 0 + 3
c [unhide-12-12] 162 units, 486 failed, 61759 tauts, 0 hbrs, 43227 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2212 transitive binary clauses
c [transred-8] found 16 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 253654 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 5167 variables 2% in round 1 in 625853530 steps
c [elim-10-1] backward subsumption/strengthening limit 174146470
c [elim-10-1-1] backward checking 41611 touched variables 16%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 702 and strengthened 1059 clauses in 73923027 steps
c [elim-10-1] rescheduled 4282 variables 2% by backward subsumption
c [elim-10-2] eliminated 239 variables 0% in round 2 in 65596998 steps
c [elim-10-2] backward subsumption/strengthening limit 34626445
c [elim-10-2-1] backward checking 1963 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 96 and strengthened 211 clauses in 8342590 steps
c [elim-10-2] rescheduled 769 variables 0% by backward subsumption
c [elim-10-3] eliminated 17 variables 0% in round 3 in 15438781 steps
c [elim-10-3] backward subsumption/strengthening limit 10845074
c [elim-10-3-1] backward checking 193 touched variables 0%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 10 and strengthened 10 clauses in 1696266 steps
c [elim-10] incomplete 62 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 5523 = 2% variables out of 253654 scheduled
c [bca-8] limit of 10000000 steps and 3554411 added (scaled 2)
c [bca-8] 429316 out of 496264 literals actually usable 87%
c [bca-8] added 946 blocked clauses in 1358809 steps
c [sweep-8] limit 15192669 penalty 0 = 0 + 0
c [sweep-8-1] 87531 pos 36.4% + 152797 neg 63.6% = 240328 sched 96.9% ret 7803
c [sweep-8-1] 15371144 steps 356 queries 46860.96 avg class size
c [sweep-8-1] 5027 decisions 349 SAT calls 36.39 avg env size
c [sweep-8-1] 236801 variables remain 95% (11219 retained 5%)
c [decomp-31] removed 946 variables
c [sweep-8-1] removed 946 vars (0 failed, 43 eqs, 45 impls)
c [sweep-8] removed 946 vars in TOTAL (1 rounds, 355 queries)
c [phase-count-12] 1677132 negative 94.7% of 1770581 except 93449 5.3%
c [phase-count-12] 1661608 positive 93.8% of 1770581 except 108973 6.2%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 145 positive 38%, 240 negative 62%
c [sort-queue-12] sorted 191639 enqueued variables after 62711 conflicts
c [score-dist-12] active 55546 (22%), one 0 (0%), zero 191639 (78%)
c [score-dist-12] max exp 509, different 245 (48%)
c [score-dist-12] median active exp 411, avg 418.3
c [simplification-12] removed 7305 variables 2.9% (247185 remain 19%)
c [simplification-12] removed 36021 irredundant clauses 2.0% (1770581 remain 33%)
c [simplification-12] maximum reduction of 3% = max (3%, 2%)
c [simplification-12] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-12] new conflict interval 24666
c [simplification-12] penalized conflict interval 24666 = 1 * 24666
c [simplification-12] hard conflict limit 99710 (soft 87377 + delta 12333)
c [simplification-12] new conflict limit 87377 (hard 99710)
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  523.9  247184  1770581     69841   62053 172252 364171   10    29  206  34%     76  -21    9   13   64%
c i  525.5  247063  1770581     71040   63161 172287 364182   10    45  207  23%     17   -5   11   13   82%
c i  525.6  247062  1770581     71136   63242 172293 364183   10    46  207  22%     13   -5    9   13   69%
c i  541.6  247061  1770581     82783   73789 172334 364200   10    27  210  38%    135  -21    9   13   70%
c i  541.7  247060  1770581     82942   73933 172338 364205   10    28  210  36%    111  -20    8   13   60%
c i  541.9  246989  1770581     83184   74147 172348 364206   10    29  210  34%     81  -19    8   13   58%
c i  544.0  246988  1770581     84375   75203 172403 364220   11    69  211  15%     11   21   14   13  107%
c i  544.1  246950  1770581     84448   75267 172405 364221   11    68  211  15%      8   21   13   13   97%
c 
c [simplification-13] limit 87377 conflicts (hard 99710) hit after 87377 conflicts
c [quatres-9] found 283920 quaternary clauses 45% in total
c [quatres-9-1] removed 46 duplicate quaternary clauses
c [quatres-9-1] added 38 double-self-subsuming ternary resolvents
c [quatres-9-2] added 300 single-self-subsuming ternary resolvents
c [quatres-9-2] added 2308 quaternary resolvents
c [ternres-9] limit 58577158 with penalty 0 = 0 + 0
c [ternres-9] all 246950 free variables schedulable
c [ternres-9] 55447 ternary resolvents (1224 bin, 54223 trn)
c [ternres-9] 2806 variables remain 1% (244144 retained 99%)
c [gauss-5] limit 5857715 penalty 1 = 1 + 0
c [gauss-5] extracted 14067 xors of average arity 3.0
c [gauss-5] connected 41975 occurrences of 13283 variables (average 3.2)
c [gauss-5] limit 5857715 penalty 1 = 1 + 0
c [decomp-32] removed 347 variables
c [gauss-5] exported 0 unary, 1 binary and 1 ternary equations
c [decomp-33] removed 2 variables
c [basicprobe-5] limit 292885792 penalty 0 = 0 + 0
c [basicprobe-5-0] 98793 sched 42%, 5735 failed, 624 lifted, 160398 hbrs
c [decomp-34] removed 18403 variables
c [basicprobe-5-1] 94255 probes remain 42% after last round
c [basicprobe-5-1] 7633 units = 6962 failed (91%) + 671 lifted (9%)
c [basicprobe-5-1] removed 23365 variables, found 193127 hbrs
c [bate-3] eliminated 6425 asymmetric tautologies during probing
c [unhide-13] limit 1464428 with penalty 3 = 0 + 3
c [unhide-13-13] 116 units, 130 failed, 22509 tauts, 0 hbrs, 36031 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 2546 transitive binary clauses
c [transred-9] found 6 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 223019 variables 100%
c [block-5] limit of 292885792 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 9806 blocked clauses
c [block-5] 9806 < 1/100 * 1555087 = 15550 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 222528 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 10913 variables 5% in round 1 in 524193273 steps
c [elim-11-1] backward subsumption/strengthening limit 275806727
c [elim-11-1-1] backward checking 57945 touched variables 26%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1286 and strengthened 988 clauses in 65551046 steps
c [elim-11-1] rescheduled 7257 variables 3% by backward subsumption
c [elim-11-2] eliminated 451 variables 0% in round 2 in 87604468 steps
c [elim-11-2] backward subsumption/strengthening limit 87604400
c [elim-11-2-1] backward checking 3059 touched variables 1%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 208 and strengthened 130 clauses in 7383908 steps
c [elim-11-2] rescheduled 815 variables 0% by backward subsumption
c [elim-11-3] eliminated 23 variables 0% in round 3 in 10267240 steps
c [elim-11-3] backward subsumption/strengthening limit 10267200
c [elim-11-3-1] backward checking 219 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 23 and strengthened 30 clauses in 1511583 steps
c [elim-11] incomplete 126 not tried 0% in round 3
c [gc-101] reconnected 160088 ternary clauses  (produced 0 empty 1 units 12 binary)
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 11898 = 5% variables out of 222528 scheduled
c [bca-9] limit of 10000000 steps and 2996314 added (scaled 2)
c [bca-9] 360904 out of 421262 literals actually usable 86%
c [bca-9] added 642 blocked clauses in 1163918 steps
c [sweep-9] limit 17573147 penalty 0 = 0 + 0
c [sweep-9-1] 71817 pos 35.7% + 129439 neg 64.3% = 201256 sched 95.5% ret 9374
c [sweep-9-1] 17750106 steps 457 queries 34943.73 avg class size
c [sweep-9-1] 6114 decisions 425 SAT calls 40.33 avg env size
c [sweep-9-1] 196715 variables remain 93% (13894 retained 7%)
c [decomp-35] removed 1686 variables
c [sweep-9-1] removed 1686 vars (0 failed, 74 eqs, 90 impls)
c [sweep-9] removed 1686 vars in TOTAL (1 rounds, 456 queries)
c [phase-count-13] 1410246 negative 94.6% of 1490264 except 80018 5.4%
c [phase-count-13] 1391527 positive 93.4% of 1490264 except 98737 6.6%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 242 positive 41%, 349 negative 59%
c [sort-queue-13] sorted 157414 enqueued variables after 87377 conflicts
c [score-dist-13] active 51530 (25%), one 0 (0%), zero 157414 (75%)
c [score-dist-13] max exp 508, different 337 (66%)
c [score-dist-13] median active exp 407, avg 392.7
c [simplification-13] removed 38006 variables 15.4% (208944 remain 16%)
c [simplification-13] removed 280317 irredundant clauses 15.8% (1490264 remain 28%)
c [simplification-13] maximum reduction of 16% = max (15%, 16%)
c [simplification-13] large reduction 16% >= 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 99377 (soft 89377 + delta 10000)
c [simplification-13] new conflict limit 89377 (hard 99377)
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  592.2  208943  1490264     87744   66882 140325 368981   10    95  191  11%      6   45    8   13   63%
c 
c [simplification-14] limit 89377 conflicts (hard 99377) hit after 90566 conflicts
c [quatres-10] found 250286 quaternary clauses 45% in total
c [quatres-10-1] removed 262 duplicate quaternary clauses
c [quatres-10-1] added 26 double-self-subsuming ternary resolvents
c [quatres-10-2] added 631 single-self-subsuming ternary resolvents
c [quatres-10-2] added 3118 quaternary resolvents
c [ternres-10] limit 59303370 with penalty 0 = 0 + 0
c [ternres-10] 1970 schedulable variables 1%
c [ternres-10] 36897 ternary resolvents (978 bin, 35919 trn)
c [ternres-10] 30 variables remain 0% (208911 retained 100%)
c [gauss-6] limit 11860674 penalty 0 = 0 + 0
c [gauss-6] extracted 26388 xors of average arity 3.0
c [gauss-6] connected 78767 occurrences of 17812 variables (average 4.4)
c [gauss-6] limit 11860674 penalty 0 = 0 + 0
c [decomp-36] removed 220 variables
c [gauss-6] exported 0 unary, 1 binary and 0 ternary equations
c [simpleprobe-6] 54920 schedulable variables 26%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-38] removed 5346 variables
c [simpleprobe-6] 33868 variables remain 17% (169507 retained 83%)
c [simpleprobe-6] removed 5346 variables, found 176295 hbrs, 508 units
c [unhide-14] limit 2965168 with penalty 2 = 0 + 2
c [unhide-14-14] 29 units, 132 failed, 86788 tauts, 0 hbrs, 54320 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2439 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 370646066 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 24
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-4-1] eliminated 3 clauses out of 7 (43%) of length 22
c [cce-4-1] eliminated 9 clauses out of 599 (2%) of length 18
c [cce-4-1] eliminated 24 clauses out of 372 (6%) of length 17
c [cce-4-1] eliminated 70 clauses out of 493 (14%) of length 16
c [cce-4-1] eliminated 68 clauses out of 1296 (5%) of length 15
c [cce-4-1] eliminated 277 clauses out of 1329 (21%) of length 14
c [cce-4-1] eliminated 451 clauses out of 2895 (16%) of length 13
c [cce-4-1] eliminated 1341 clauses out of 5422 (25%) of length 12
c [cce-4-1] eliminated 1255 clauses out of 6537 (19%) of length 11
c [cce-4-1] eliminated 5839 clauses out of 15622 (37%) of length 10
c [cce-4-1] eliminated 4076 clauses out of 14662 (28%) of length 9
c [cce-4-1] eliminated 5764 clauses out of 24807 (23%) of length 8
c [cce-4-1] eliminated 5950 clauses out of 31637 (19%) of length 7
c [cce-4-1] eliminated 8574 clauses out of 56986 (15%) of length 6
c [cce-4-1] eliminated 5809 clauses out of 116918 (5%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 39514 large clauses in 370646071 steps
c [cce-4-1] allowing another 185323035 steps for small clauses
c [cce-4-1] scheduling 777761 clauses = 583932 binary + 193829 ternary
c [cce-4-1] tried to eliminate 114435 small clauses 15%
c [cce-4-1] eliminated 13290 binary clauses 2%
c [cce-4-1] eliminated 4796 ternary clauses 2%
c [cce-4-1] eliminated 18086 small clauses 2%
c [cce-4-1] eliminated 19524 small clauses in 370646075 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 59038 covered clauses in round 1
c [cce-4] eliminated 59038 covered clauses in TOTAL during 1 rounds
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 203211 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 11835 variables 6% in round 1 in 417331259 steps
c [elim-12-1] backward subsumption/strengthening limit 382668741
c [elim-12-1-1] backward checking 63429 touched variables 31%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 695 and strengthened 1047 clauses in 59853556 steps
c [elim-12-1] rescheduled 4887 variables 2% by backward subsumption
c [elim-12-2] eliminated 268 variables 0% in round 2 in 45569406 steps
c [elim-12-2] backward subsumption/strengthening limit 45569400
c [elim-12-2-1] backward checking 2101 touched variables 1%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 125 and strengthened 214 clauses in 5606224 steps
c [elim-12-2] rescheduled 729 variables 0% by backward subsumption
c [elim-12-3] eliminated 17 variables 0% in round 3 in 11332713 steps
c [elim-12-3] backward subsumption/strengthening limit 11332700
c [elim-12-3-1] backward checking 278 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 12 and strengthened 8 clauses in 1732199 steps
c [elim-12] incomplete 58 not tried 0% in round 3
c [gc-110] reconnected 429031 binary clauses (produced 0 empty 2 units)
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 12173 = 6% variables out of 203211 scheduled
c [bca-10] limit of 10000000 steps and 2708109 added (scaled 2)
c [bca-10] 324044 out of 382078 literals actually usable 85%
c [bca-10] added 1944 blocked clauses in 1035882 steps
c [sweep-10] limit 17791011 penalty 0 = 0 + 0
c [sweep-10-1] 62042 pos 34.8% + 116398 neg 65.2% = 178440 sched 93.4% ret 12598
c [sweep-10-1] 17792059 steps 408 queries 33246.39 avg class size
c [sweep-10-1] 5572 decisions 378 SAT calls 40.82 avg env size
c [sweep-10-1] 174628 variables remain 91% (16382 retained 9%)
c [decomp-39] removed 463 variables
c [sweep-10-1] removed 463 vars (0 failed, 77 eqs, 75 impls)
c [sweep-10] removed 463 vars in TOTAL (1 rounds, 407 queries)
c [phase-count-14] 1273512 negative 94.4% of 1348613 except 75101 5.6%
c [phase-count-14] 1257494 positive 93.2% of 1348613 except 91119 6.8%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 227 positive 42%, 308 negative 58%
c [sort-queue-14] sorted 141414 enqueued variables after 90566 conflicts
c [score-dist-14] active 49161 (26%), one 0 (0%), zero 141414 (74%)
c [score-dist-14] max exp 509, different 347 (68%)
c [score-dist-14] median active exp 475, avg 396.9
c [simplification-14] removed 18366 variables 8.8% (190575 remain 14%)
c [simplification-14] removed 141651 irredundant clauses 9.5% (1348613 remain 25%)
c [simplification-14] maximum reduction of 10% = max (9%, 10%)
c [simplification-14] large reduction 10% >= 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 102566 (soft 92566 + delta 10000)
c [simplification-14] new conflict limit 92566 (hard 102566)
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  632.9  190574  1348613     90900   63387 144378 382925    9    97  184  10%      4   46    7   13   55%
c i  633.8  190564  1348613     91471   63828 144442 382947   10    95  184  10%     -9   43   11   13   87%
c i  634.4  190563  1348613     92006   64295 144470 382965    9    93  184  10%    -16   40    7   13   53%
c i  634.5  190562  1348613     92057   64327 144487 382966    9    92  184  10%    -17   40    6   13   50%
c i  634.5  190542  1348613     92118   64378 144492 382969    9    92  184  10%    -18   40    7   13   53%
c i  634.5  190529  1348613     92123   64379 144494 382970    9    92  184  10%    -18   40    6   13   52%
c i  634.5  190517  1348613     92124   64379 144494 382970    9    92  184  10%    -18   39    6   13   52%
c 
c [simplification-15] limit 92578 conflicts (hard 102566) hit after 94999 conflicts
c [quatres-11] found 239828 quaternary clauses 49% in total
c [quatres-11-1] removed 673 duplicate quaternary clauses
c [quatres-11-1] added 18 double-self-subsuming ternary resolvents
c [quatres-11-2] added 392 single-self-subsuming ternary resolvents
c [quatres-11-2] added 3179 quaternary resolvents
c [ternres-11] limit 60598655 with penalty 0 = 0 + 0
c [ternres-11] 29 schedulable variables 0%
c [ternres-11] 18732 ternary resolvents (489 bin, 18243 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1893707 penalty 4 = 4 + 0
c [card-5] found 1225 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1893707 for elimination
c [card-5] 1225 out of 1225 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-7] limit 12119731 penalty 0 = 0 + 0
c [gauss-7] extracted 24819 xors of average arity 3.0
c [gauss-7] connected 74258 occurrences of 13689 variables (average 5.4)
c [gauss-7] limit 12119731 penalty 0 = 0 + 0
c [decomp-40] removed 121 variables
c [gauss-7] exported 0 unary, 4 binary and 0 ternary equations
c [treelook-6] limit 6059865 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 154718 literals 41%
c [treelook-6] scheduling used 3457449 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 6059865 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 6105300 steps
c [treelook-6] 154280 literals remain 41%
c [treelook-6] 20823 variables remain to probed next time 11%
c [decomp-42] removed 15 variables
c [treelook-6] removed 29 variables, found 12783 hbrs
c [unhide-15] limit 3029932 with penalty 2 = 0 + 2
c [unhide-15-15] 16 units, 81 failed, 8985 tauts, 0 hbrs, 13958 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1843 transitive binary clauses
c [transred-11] found 2 units
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 190287 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 2454 variables 1% in round 1 in 401634119 steps
c [elim-13-1] backward subsumption/strengthening limit 401634100
c [elim-13-1-1] backward checking 17282 touched variables 9%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 189 and strengthened 160 clauses in 25307787 steps
c [elim-13-1] rescheduled 944 variables 0% by backward subsumption
c [elim-13-2] eliminated 55 variables 0% in round 2 in 10141837 steps
c [elim-13-2] backward subsumption/strengthening limit 10141800
c [elim-13-2-1] backward checking 401 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 28 and strengthened 42 clauses in 1274182 steps
c [elim-13-2] rescheduled 167 variables 0% by backward subsumption
c [elim-13-3] eliminated 6 variables 0% in round 3 in 1747600 steps
c [elim-13-3] backward subsumption/strengthening limit 1747600
c [elim-13-3-1] backward checking 89 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 12 and strengthened 3 clauses in 677106 steps
c [elim-13] incomplete 29 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 2518 = 1% variables out of 190287 scheduled
c [bca-11] limit of 10000000 steps and 2670555 added (scaled 2)
c [bca-11] 314354 out of 375540 literals actually usable 84%
c [bca-11] added 190 blocked clauses in 1010844 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 181795960 penalty 0 = 0 + 0
c [sweep-11-1] 59950 pos 34.9% + 111813 neg 65.1% = 171763 sched 91.5% ret 16006
c [sweep-11-1] 181838995 steps 4187 queries 5531.30 avg class size
c [sweep-11-1] 54651 decisions 4034 SAT calls 35.13 avg env size
c [sweep-11-1] 111698 variables remain 60% (75711 retained 40%)
c [decomp-43] removed 1614 variables
c [sweep-11-1] removed 1614 vars (0 failed, 769 eqs, 745 impls)
c [sweep-11] removed 1614 vars in TOTAL (1 rounds, 4186 queries)
c [phase-count-15] 1246242 negative 94.2% of 1322352 except 76110 5.8%
c [phase-count-15] 1231591 positive 93.1% of 1322352 except 90761 6.9%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 37 positive 40%, 56 negative 60%
c [sort-queue-15] sorted 127105 enqueued variables after 94999 conflicts
c [score-dist-15] active 59050 (32%), one 0 (0%), zero 127105 (68%)
c [score-dist-15] max exp 508, different 360 (71%)
c [score-dist-15] median active exp 491, avg 429.5
c [simplification-15] removed 4353 variables 2.3% (186155 remain 14%)
c [simplification-15] removed 26261 irredundant clauses 1.9% (1322352 remain 25%)
c [simplification-15] maximum reduction of 2% = max (2%, 2%)
c [simplification-15] geometric conflict interval increment 8222 = 24666 / 3
c [simplification-15] new conflict interval 32888
c [simplification-15] penalized conflict interval 32888 = 1 * 32888
c [simplification-15] hard conflict limit 144331 (soft 127887 + delta 16444)
c [simplification-15] new conflict limit 127887 (hard 144331)
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  680.7  186154  1322352     95833   70481 148157 383147   11    89  184  12%     12   35   11   12   87%
c i  682.0  186153  1322352     96923   71486 148194 383153   11    88  184  12%     -9   33   11   12   92%
c i  682.7  186152  1322352     97750   72260 148210 383164   11    79  184  14%    -17   24   15   12  124%
c i  682.8  186142  1322352     97875   72360 148213 383167   11    78  184  15%    -18   22   15   12  123%
c i  682.8  186133  1322352     97876   72360 148213 383167   11    78  184  15%    -18   22   15   12  122%
c i  682.9  186121  1322352     98003   72481 148214 383168   11    77  184  15%    -20   21   12   12   99%
c i  683.0  186120  1322352     98037   72512 148214 383169   11    76  184  15%    -20   21   12   12   93%
c i  683.0  186115  1322352     98083   72548 148220 383171   11    76  184  15%    -20   21   11   12   85%
c i  683.0  186112  1322352     98084   72548 148220 383171   11    76  184  15%    -20   20   11   12   84%
c i  683.0  186093  1322352     98085   72548 148220 383171   11    76  184  15%    -20   20   10   12   84%
c i  683.5  186067  1322352     99181   73540 148245 383177   10    68  184  15%    -20   13    6   12   47%
c i  685.7  186050  1322352    103317   77390 148353 383212   10    73  184  14%     19   16    8   12   62%
c i  702.9  186048  1322352    116351   88371 148433 383244   12    54  186  22%    146   -0   15   12  125%
c i  705.1  186047  1322352    118534   90379 148464 383298   12    60  186  20%     -0    5   10   12   80%
c i  705.7  186046  1322352    119209   90955 148500 383317   11    58  186  20%    -18    4    8   12   68%
c i  705.8  186045  1322352    119285   91024 148506 383317   11    58  186  20%    -20    3    8   12   69%
c i  706.1  186044  1322352    119441   91145 148522 383326   11    58  186  19%    -23    3    7   12   59%
c i  706.1  186043  1322352    119502   91190 148526 383335   11    58  186  19%    -24    3    7   12   58%
c i  707.2  186037  1322352    120592   92238 148544 383342   11    61  186  18%    -29    6    9   12   77%
c -  707.6  186037  1322352    121035   62702 148568 383364   11    65  178  16%    -32   10    9   12   74%
c i  708.6  186036  1322352    121947   63531 148607 383375   10    71  181  14%    -28   16    7   12   62%
c i  708.8  186031  1322352    122170   63733 148614 383377   10    70  181  14%    -31   15    6   12   53%
c i  709.0  186030  1322352    122589   64091 148627 383381    9    66  181  14%    -33   11    6   12   47%
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  709.2  186029  1322352    122812   64296 148629 383385    9    69  181  14%    -34   14    9   12   77%
c i  709.3  186028  1322352    122909   64382 148632 383387   10    69  181  14%    -34   14   13   12  105%
c i  711.7  186027  1322352    127613   68867 148658 383398   10    63  181  17%     18    7   14   12  116%
c 
c [simplification-16] limit 127917 conflicts (hard 144331) hit after 127918 conflicts
c [quatres-12] found 238239 quaternary clauses 48% in total
c [quatres-12-1] removed 61 duplicate quaternary clauses
c [quatres-12-1] added 43 double-self-subsuming ternary resolvents
c [quatres-12-2] added 468 single-self-subsuming ternary resolvents
c [quatres-12-2] added 1764 quaternary resolvents
c [ternres-12] limit 68672930 with penalty 0 = 0 + 0
c [ternres-12] all 186005 free variables schedulable
c [ternres-12] 30388 ternary resolvents (928 bin, 29460 trn)
c [ternres-12] 341 variables remain 0% (185664 retained 100%)
c [gauss-8] limit 13734586 penalty 0 = 0 + 0
c [gauss-8] extracted 27918 xors of average arity 3.0
c [gauss-8] connected 83419 occurrences of 17547 variables (average 4.8)
c [gauss-8] limit 13734586 penalty 0 = 0 + 0
c [gauss-8] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-44] removed 207 variables
c [basicprobe-6] limit 343364654 penalty 0 = 0 + 0
c [basicprobe-6-0] 76986 sched 42%, 1664 failed, 84 lifted, 57163 hbrs
c [decomp-45] removed 4216 variables
c [basicprobe-6-1] 70539 probes remain 39% after last round
c [basicprobe-6-1] 2139 units = 2052 failed (96%) + 87 lifted (4%)
c [basicprobe-6-1] removed 5008 variables, found 71877 hbrs
c [bate-4] eliminated 3148 asymmetric tautologies during probing
c [unhide-16] limit 3433646 with penalty 2 = 0 + 2
c [unhide-16-16] 18 units, 130 failed, 50872 tauts, 0 hbrs, 57753 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1575 transitive binary clauses
c [transred-12] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 180631 variables 100%
c [block-6] limit of 171682327 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 17165 blocked clauses
c [cce-5] limit of 85841163 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 3 clauses out of 7 (43%) of length 20
c [cce-5-1] eliminated 1 clauses out of 89 (1%) of length 19
c [cce-5-1] eliminated 15 clauses out of 543 (3%) of length 18
c [cce-5-1] eliminated 26 clauses out of 482 (5%) of length 17
c [cce-5-1] eliminated 37 clauses out of 595 (6%) of length 16
c [cce-5-1] eliminated 44 clauses out of 1044 (4%) of length 15
c [cce-5-1] eliminated 132 clauses out of 1095 (12%) of length 14
c [cce-5-1] eliminated 512 clauses out of 2133 (24%) of length 13
c [cce-5-1] eliminated 662 clauses out of 3440 (19%) of length 12
c [cce-5-1] eliminated 907 clauses out of 4426 (20%) of length 11
c [cce-5-1] eliminated 1278 clauses out of 8358 (15%) of length 10
c [cce-5-1] eliminated 1095 clauses out of 11981 (9%) of length 9
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 4712 large clauses in 85841166 steps
c [cce-5-1] allowing another 42920583 steps for small clauses
c [cce-5-1] scheduling 652951 clauses = 490189 binary + 162762 ternary
c [cce-5-1] tried to eliminate 23959 small clauses 4%
c [cce-5-1] eliminated 4433 binary clauses 1%
c [cce-5-1] eliminated 1514 ternary clauses 1%
c [cce-5-1] eliminated 5947 small clauses 1%
c [cce-5-1] eliminated 5947 small clauses in 85841204 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 10659 covered clauses in round 1
c [cce-5] eliminated 10659 covered clauses in TOTAL during 1 rounds
c [cce-5] 10659 < 1/100 * 1250800 = 12508 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 180155 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 6875 variables 4% in round 1 in 358032288 steps
c [elim-14-1] backward subsumption/strengthening limit 358032200
c [elim-14-1-1] backward checking 44507 touched variables 25%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 489 and strengthened 741 clauses in 47317447 steps
c [elim-14-1] rescheduled 4337 variables 2% by backward subsumption
c [elim-14-2] eliminated 141 variables 0% in round 2 in 30367377 steps
c [elim-14-2] backward subsumption/strengthening limit 30367300
c [elim-14-2-1] backward checking 1226 touched variables 1%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 64 and strengthened 88 clauses in 2847223 steps
c [elim-14-2] rescheduled 338 variables 0% by backward subsumption
c [elim-14-3] eliminated 14 variables 0% in round 3 in 3260398 steps
c [elim-14-3] backward subsumption/strengthening limit 3260300
c [elim-14-3-1] backward checking 126 touched variables 0%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 11 and strengthened 3 clauses in 891779 steps
c [elim-14] incomplete 32 not tried 0% in round 3
c [gc-129] reconnected 365255 binary clauses (produced 0 empty 9 units)
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 7116 = 4% variables out of 180155 scheduled
c [bca-12] limit of 10000000 steps and 2432072 added (scaled 2)
c [bca-12] 286952 out of 346080 literals actually usable 83%
c [bca-12] added 2316 blocked clauses in 923487 steps
c [sweep-12] limit 20601879 penalty 0 = 0 + 0
c [sweep-12-1] 37103 pos 35.8% + 66471 neg 64.2% = 103574 sched 59.9% ret 69465
c [sweep-12-1] 20606589 steps 835 queries 13486.83 avg class size
c [sweep-12-1] 10991 decisions 801 SAT calls 32.83 avg env size
c [sweep-12-1] 97434 variables remain 56% (75548 retained 44%)
c [decomp-46] removed 637 variables
c [sweep-12-1] removed 637 vars (0 failed, 118 eqs, 113 impls)
c [sweep-12] removed 637 vars in TOTAL (1 rounds, 834 queries)
c [phase-count-16] 1140420 negative 94.3% of 1209549 except 69129 5.7%
c [phase-count-16] 1124170 positive 92.9% of 1209549 except 85379 7.1%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 96 positive 40%, 143 negative 60%
c [sort-queue-16] sorted 114017 enqueued variables after 127918 conflicts
c [score-dist-16] active 58385 (34%), one 0 (0%), zero 114017 (66%)
c [score-dist-16] max exp 509, different 477 (94%)
c [score-dist-16] median active exp 375, avg 362.1
c [simplification-16] removed 13603 variables 7.3% (172402 remain 13%)
c [simplification-16] removed 112803 irredundant clauses 8.5% (1209549 remain 23%)
c [simplification-16] maximum reduction of 9% = max (7%, 9%)
c [simplification-16] large reduction 9% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 139918 (soft 129918 + delta 10000)
c [simplification-16] new conflict limit 129918 (hard 139918)
c 
c [simplification-17] limit 129918 conflicts (hard 139918) hit after 130987 conflicts
c [quatres-13] found 222992 quaternary clauses 49% in total
c [quatres-13-1] removed 76 duplicate quaternary clauses
c [quatres-13-1] added 13 double-self-subsuming ternary resolvents
c [quatres-13-2] added 578 single-self-subsuming ternary resolvents
c [quatres-13-2] added 2814 quaternary resolvents
c [ternres-13] limit 69379035 with penalty 0 = 0 + 0
c [ternres-13] 316 schedulable variables 0%
c [ternres-13] 22878 ternary resolvents (947 bin, 21931 trn)
c [ternres-13] fully completed ternary resolution
c [gauss-9] limit 13875807 penalty 0 = 0 + 0
c [gauss-9] extracted 27938 xors of average arity 3.0
c [gauss-9] connected 83618 occurrences of 13259 variables (average 6.3)
c [gauss-9] limit 13875807 penalty 0 = 0 + 0
c [decomp-47] removed 91 variables
c [gauss-9] exported 0 unary, 2 binary and 0 ternary equations
c [simpleprobe-7] 26436 schedulable variables 15%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-49] removed 2619 variables
c [simpleprobe-7] 19786 variables remain 12% (149906 retained 88%)
c [simpleprobe-7] removed 2619 variables, found 123468 hbrs, 315 units
c [unhide-17] limit 3468951 with penalty 2 = 0 + 2
c [unhide-17-17] 8 units, 11 failed, 9517 tauts, 0 hbrs, 7895 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 2331 transitive binary clauses
c [transred-13] found 3 units
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 169672 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 2380 variables 1% in round 1 in 344501642 steps
c [elim-15-1] backward subsumption/strengthening limit 344501600
c [elim-15-1-1] backward checking 20991 touched variables 12%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 332 and strengthened 311 clauses in 28868019 steps
c [elim-15-1] rescheduled 1841 variables 1% by backward subsumption
c [elim-15-2] eliminated 77 variables 0% in round 2 in 20001325 steps
c [elim-15-2] backward subsumption/strengthening limit 20001300
c [elim-15-2-1] backward checking 826 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 42 and strengthened 31 clauses in 1696477 steps
c [elim-15-2] rescheduled 176 variables 0% by backward subsumption
c [elim-15-3] eliminated 12 variables 0% in round 3 in 1679033 steps
c [elim-15-3] backward subsumption/strengthening limit 1679000
c [elim-15-3-1] backward checking 98 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 11 and strengthened 12 clauses in 601624 steps
c [elim-15] incomplete 41 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 2486 = 1% variables out of 169672 scheduled
c [bca-13] limit of 10000000 steps and 2359780 added (scaled 2)
c [bca-13] 273973 out of 334374 literals actually usable 82%
c [bca-13] added 248 blocked clauses in 888280 steps
c [sweep-13] limit 20813710 penalty 0 = 0 + 0
c [sweep-13-1] 34142 pos 36.4% + 59700 neg 63.6% = 93842 sched 56.1% ret 73344
c [sweep-13-1] 20944772 steps 723 queries 14717.64 avg class size
c [sweep-13-1] 8314 decisions 682 SAT calls 32.41 avg env size
c [sweep-13-1] 89989 variables remain 54% (77158 retained 46%)
c [decomp-50] removed 318 variables
c [sweep-13-1] removed 318 vars (0 failed, 161 eqs, 146 impls)
c [sweep-13] removed 318 vars in TOTAL (1 rounds, 722 queries)
c [phase-count-17] 1103877 negative 94.0% of 1173723 except 69846 6.0%
c [phase-count-17] 1089714 positive 92.8% of 1173723 except 84009 7.2%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 47 positive 38%, 76 negative 62%
c [sort-queue-17] sorted 109403 enqueued variables after 130987 conflicts
c [score-dist-17] active 57465 (34%), one 289 (0%), zero 109114 (65%)
c [score-dist-17] max exp 509, different 473 (93%)
c [score-dist-17] median active exp 364, avg 365.9
c [simplification-17] removed 5534 variables 3.2% (166868 remain 13%)
c [simplification-17] removed 35826 irredundant clauses 3.0% (1173723 remain 22%)
c [simplification-17] maximum reduction of 3% = max (3%, 3%)
c [simplification-17] geometric conflict interval increment 8222 = 32888 / 4
c [simplification-17] new conflict interval 41110
c [simplification-17] penalized conflict interval 41110 = 1 * 41110
c [simplification-17] hard conflict limit 192652 (soft 172097 + delta 20555)
c [simplification-17] new conflict limit 172097 (hard 192652)
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  779.0  166867  1173723    131323   69534 163468 422122   10    66  176  16%      4   10   13   12  109%
c i  782.1  166866  1173723    133441   71488 163499 422138   12    62  177  20%    -14    5   15   12  130%
c i  782.4  166865  1173723    133641   71656 163507 422146   12    72  177  17%    -18   15   11   12   91%
c i  784.6  166864  1173723    136265   74012 163627 422201   11    97  177  12%    -10   40    8   12   69%
c i  784.9  166863  1173723    136417   74142 163642 422203   11   107  177  10%    -14   50    8   12   66%
c i  798.7  166862  1173723    149462   86492 163832 422263   12   107  180  12%    140   35   14   12  119%
c i  799.3  166861  1173723    149951   86910 163870 422283   12   114  180  10%     69   41    7   12   60%
c i  799.5  166825  1173723    150165   87105 163880 422284   11   113  180  10%     47   40    9   12   76%
c i  799.5  166824  1173723    150288   87207 163892 422285   11   111  180  10%     36   38    8   12   72%
c i  799.5  166823  1173723    150385   87292 163896 422286   11   109  180  10%     29   36    9   12   73%
c i  800.0  166796  1173723    150657   87530 163916 422288   11   112  180  10%     11   39    8   12   71%
c i  800.1  166795  1173723    150710   87573 163918 422293   11   112  180  10%      8   39    8   12   72%
c i  800.1  166794  1173723    150719   87578 163920 422293   11   112  180  10%      8   39    8   12   73%
c i  800.1  166793  1173723    150726   87584 163920 422293   11   112  180  10%      7   38    8   12   73%
c i  801.9  166787  1173723    152324   89064 163953 422312   11   149  181   7%    -25   75   16   12  134%
c i  804.2  166780  1173723    153296   89906 164009 422347   11   147  181   7%    -33   72    6   12   55%
c i  805.5  166736  1173723    154379   90898 164050 422357   11   133  181   8%    -36   56   10   12   90%
c i  806.8  166735  1173723    156202   92537 164073 422362   10   115  182   9%    -29   37    9   12   76%
c i  806.8  166734  1173723    156220   92552 164074 422363   10   114  182   9%    -30   36    8   12   74%
c i  809.4  166733  1173723    159742   95783 164129 422388   11   107  182  10%     -5   27   13   12  110%
c i  809.4  166692  1173723    159743   95783 164129 422388   11   107  182  10%     -5   27   13   12  110%
c i  809.6  166689  1173723    159969   95965 164150 422396   11   105  182  10%    -13   25    9   11   77%
c i  809.8  166684  1173723    160166   96149 164154 422397   11   104  182  10%    -18   24    9   11   75%
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  814.4  166677  1173723    165304  100908 164245 422428   11   124  182   8%     20   43   12   11  103%
c i  814.7  166658  1173723    165516  101089 164263 422439   10   132  182   8%      9   51    8   11   72%
c -  815.5  166652  1173723    167047   73375 164292 422451   10   107  173   9%    -21   26   12   11  108%
c i  817.3  166651  1173723    170094   76274 164317 422466   10   129  177   8%     13   45   10   11   85%
c 
c [simplification-18] limit 172109 conflicts (hard 192652) hit after 173741 conflicts
c [quatres-14] found 219164 quaternary clauses 48% in total
c [quatres-14-1] removed 83 duplicate quaternary clauses
c [quatres-14-1] added 33 double-self-subsuming ternary resolvents
c [quatres-14-2] added 371 single-self-subsuming ternary resolvents
c [quatres-14-2] added 1617 quaternary resolvents
c [ternres-14] limit 81059479 with penalty 0 = 0 + 0
c [ternres-14] all 166648 free variables schedulable
c [ternres-14] 17239 ternary resolvents (509 bin, 16730 trn)
c [ternres-14] 105 variables remain 0% (166543 retained 100%)
c [gauss-10] limit 16211895 penalty 0 = 0 + 0
c [gauss-10] extracted 29581 xors of average arity 3.0
c [gauss-10] connected 88361 occurrences of 16636 variables (average 5.3)
c [gauss-10] limit 16211895 penalty 0 = 0 + 0
c [decomp-51] removed 184 variables
c [gauss-10] exported 1 unary, 1 binary and 0 ternary equations
c [treelook-7] limit 8105947 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 143841 literals 43%
c [treelook-7] scheduling used 3265200 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 8105947 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 8332609 steps
c [treelook-7] 143661 literals remain 43%
c [treelook-7] 18390 variables remain to probed next time 11%
c [decomp-53] removed 26 variables
c [treelook-7] removed 38 variables, found 25387 hbrs
c [unhide-18] limit 4052973 with penalty 2 = 0 + 2
c [unhide-18-18] 3 units, 115 failed, 72633 tauts, 0 hbrs, 38116 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 1513 transitive binary clauses
c [transred-14] found 2 units
c [block-7] scheduling all variables this time
c [block-7] scheduled 166363 variables 100%
c [block-7] limit of 400000000 steps penalty 1 = 1 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 5034 blocked clauses
c [block-7] 5034 < 1/100 * 1167720 = 11677 considered unsuccessful
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 166312 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 2094 variables 1% in round 1 in 332079487 steps
c [elim-16-1] backward subsumption/strengthening limit 332079400
c [elim-16-1-1] backward checking 19072 touched variables 11%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 287 and strengthened 460 clauses in 25269176 steps
c [elim-16-1] rescheduled 1582 variables 1% by backward subsumption
c [elim-16-2] eliminated 60 variables 0% in round 2 in 10196218 steps
c [elim-16-2] backward subsumption/strengthening limit 10196200
c [elim-16-2-1] backward checking 532 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 18 and strengthened 31 clauses in 1399524 steps
c [elim-16-2] rescheduled 132 variables 0% by backward subsumption
c [elim-16-3] eliminated 6 variables 0% in round 3 in 1611955 steps
c [elim-16-3] backward subsumption/strengthening limit 1611900
c [elim-16-3-1] backward checking 79 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 0 and strengthened 0 clauses in 594396 steps
c [elim-16] fully completed in 3 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 2175 = 1% variables out of 166312 scheduled
c [bca-14] limit of 10000000 steps and 2315640 added (scaled 2)
c [bca-14] 262676 out of 328276 literals actually usable 80%
c [bca-14] added 1014 blocked clauses in 858464 steps
c [sweep-14] limit 24317843 penalty 0 = 0 + 0
c [sweep-14-1] 32496 pos 36.8% + 55836 neg 63.2% = 88332 sched 53.8% ret 75805
c [sweep-14-1] 24324784 steps 655 queries 11980.29 avg class size
c [sweep-14-1] 7795 decisions 603 SAT calls 32.82 avg env size
c [sweep-14-1] 84908 variables remain 52% (79144 retained 48%)
c [decomp-54] removed 388 variables
c [sweep-14-1] removed 388 vars (0 failed, 122 eqs, 135 impls)
c [sweep-14] removed 388 vars in TOTAL (1 rounds, 654 queries)
c [phase-count-18] 1082899 negative 94.1% of 1151024 except 68125 5.9%
c [phase-count-18] 1068535 positive 92.8% of 1151024 except 82489 7.2%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 21 positive 48%, 23 negative 52%
c [sort-queue-18] sorted 101652 enqueued variables after 173741 conflicts
c [score-dist-18] active 62097 (38%), one 4355 (3%), zero 97297 (59%)
c [score-dist-18] max exp 509, different 453 (89%)
c [score-dist-18] median active exp 424, avg 382.7
c [simplification-18] removed 2899 variables 1.7% (163749 remain 12%)
c [simplification-18] removed 22699 irredundant clauses 1.9% (1151024 remain 22%)
c [simplification-18] maximum reduction of 2% = max (2%, 2%)
c [simplification-18] geometric conflict interval increment 13703 = 41110 / 3
c [simplification-18] new conflict interval 54813
c [simplification-18] penalized conflict interval 54813 = 1 * 54813
c [simplification-18] hard conflict limit 255960 (soft 228554 + delta 27406)
c [simplification-18] new conflict limit 228554 (hard 255960)
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  861.6  163748  1151024    181134   85786 168346 366888   27    91  178  30%    107    5   37   13  282%
c i  861.7  163746  1151024    181174   85820 168349 366889   27    91  178  30%    101    6   35   13  265%
c i  863.0  163744  1151024    181999   86573 168366 366901   27    94  178  29%     21    8   28   13  211%
c i  956.8  163743  1151024    203869  105298 168410 366931   15    44  185  33%    242  -33   17   17  101%
c -  957.0  163743  1151024    204041   77672 168410 366931   15    46  172  32%    191  -31   16   17   93%
c i  959.9  163742  1151024    207637   80949 168417 366933   16    62  176  26%    -33  -14   17   17   96%
c i  973.3  163741  1151024    223938   96566 168488 366972   12    58  179  20%    146  -16    8   16   52%
c i  975.4  163739  1151024    225110   97653 168506 366978   13    64  179  21%    -10  -10   23   16  138%
c i  977.7  163738  1151024    227150   99558 168537 366985   13    51  179  25%    -62  -22   13   16   81%
c i  978.0  163737  1151024    227336   99739 168539 366985   13    50  179  25%    -67  -23   13   16   80%
c i  982.2  163736  1151024    233506  105534 168562 367003   11    49  183  23%     -6  -22   16   16  106%
c i  982.4  163734  1151024    233667  105680 168566 367003   11    48  183  24%    -18  -22   16   16  103%
c i  984.5  163732  1151024    236158  108088 168571 367004   11   103  185  10%    -55   32    9   15   57%
c i  984.6  163731  1151024    236290  108205 168579 367004   10   104  185  10%    -58   32    7   15   47%
c i  984.7  163730  1151024    236466  108357 168583 367010   10   103  185  10%    -62   32    6   15   38%
c i  984.7  163722  1151024    236467  108357 168583 367010   10   103  185  10%    -62   32    6   15   38%
c i  985.0  163717  1151024    236986  108846 168595 367017   10   102  185  10%    -69   30    6   15   41%
c -  985.6  163717  1151024    238233   80102 168600 367017   11    87  172  12%    -70   15   11   15   74%
c i  986.3  163716  1151024    239545   81352 168604 367017   11    71  176  15%    -55   -1   12   15   77%
c i  989.3  163715  1151024    243351   84590 168629 367043   11    72  176  16%    -34    0   10   15   68%
c i  993.5  163714  1151024    247770   88738 168695 367087   13    72  177  18%    -21    0   13   15   84%
c i  993.6  163710  1151024    247805   88770 168696 367088   13    72  177  18%    -23    0   13   15   88%
c i  993.6  163691  1151024    247856   88811 168695 367089   13    71  177  18%    -26   -0   14   15   92%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 14905 basic ate = 11488 trn 77% + 3417 lrg 23% in 4 updates
c bcas: 14 count, 21119 added (9280 skipped), 19299078 steps
c bkwd: tried 4537668 clauses, 9065278 lits, 2.00 lits/clause
c bkwd: checked 352921154 occs, 77.78 occs/clause, 38.93 occs/lit
c bkwd: subsumed 88 binary, 2166 ternary, 4093 large
c bkwd: strengthened 102 binary, 42 ternary (100% self), 10151 large (0% self)
c blkd: 7 bces, 86251 removed, 50928440 resolutions, 133776245 steps
c blkd: 39710 blocking literals 1%, 2351 pure
c bump: 260368 bumped seen, 55709832 lits 214.0 on average
c card: 5 count, 0 units, 0 am1, 93340218 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 9908 subsumed
c card: 4033 at-most-one constraints found, average size 3.09
c card: 4033 at-most-one constraints used 100%, average size 3.09
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, 70718 eliminated, 66499 ate 94%, 4219 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: 18938485 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 149 gcs, 0 rescored clauses, 983 rescored vars
c dcps: 54 decompositions, 144602 equivalent 11%
c deco: 1123 decision-only clauses 0%, 75% reduction
c decs: 1758879 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 786083 eliminated 57%, 11661 pure 1%
c elms: 40 rounds, 2.5 rounds/bve
c elms: 676828 small 86%, 95243 large 12%
c elms: 933907 tried small, 676828 succeeded 72%, 257079 failed 28%
c elms: 314168 subsumed, 417682 strengthened, 0 blocked
c elms: 73182051 copies, 90672260 resolutions, 19510872 ipos
c elms: 69864599 subchks, 128747242 strchks
c gaus: 10 extractions, 172776 extracted, 3.0 size, 3 max
c gaus: exported 1 units, 11 binary and 4 ternary equations
c gaus: 0 gc, 159426346 steps, 79713173 extr 50%, 79920747 elim 50%
c glue: 15.2 orig avg, 15.2 real avg, 2.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1729783 = 743116 simple 43% + 973986 trn 56% + 12681 lrg 1%, 40864 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 260368 clauses, 42.1 length
c lrnd: 10948757 lits = 19935681 orig - 8986924 removed 45%
c lrnd: 81783 uips 31%, 136744 flips 53%
c mins: 247384 mins 95%, 2581 bin 1%, 9276 size 4%
c mins: 40526869 poisoned searches, 4645598 hits, 11% hit rate
c mins: 54869819 used twice searches, 2018858 hits, 4% hit rate
c move: moved 141283, 58929 bin 42%, 82354 trn 58%
c otfs: 2338 driving 37%, 3922 restarting 63%
c otfs: str 6260, 5392 red 86%, 868 irr 14%
c otfs: str 6260, 0 bin 0%, 1221 trn 20%, 5039 lrg 80%
c otfs: sub 191, 154 red 81%, 37 irr 19%
c otfs: sub 191, 0 bin 0%, 69 trn 36%, 122 lrg 64%
c phas: 18 computed, 1008360 set, 467268 pos (46%), 541092 neg (54%)
c prbs: 6 basic, 862837 probed, 17369 failed, 2167 lifted
c prbs: 7 simple, 1840671 probed, 4489 failed, 26724 eqs
c prbs: 7 treelook, 1468 probed, 126 failed, 0 lifted
c prom: 22062 locked 4% out of 584034 tried
c prps: 1744226651 props, 944 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 14 count, 54215 quat, 15421 self1, 489 self2, 5866 dup
c queu: 18 sorted, 1758879 next (107115 steps 0.06)
c queu: 118998564 enq (170546655 steps 1.43), 55709832 deq 47%
c redc: 9620 clauses 13%, 72944 tried 29%, 271 sat 0%
c redc: 16723 lits 2%, 700775 tried 4%, 272 sat 0%
c redc: 1096 times jump level reduced, 26.8 levels on average
c reds: 4 count, 63066.8 conflicts per reduce
c reds: 0 memlim 0%, 4 arith 100%
c reds: 103005 collected 88%, 13724 retired 12%
c rmbd: 345418 removed, 237344 red 69%
c rsts: 7041 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: 18 count, 16 confs 89%, 0 vars 0%
c simp: 1 its 6%, 1 bin 6%, 0 trns 0%
c subl: 260368 count (264662 tried 1.0), 16916 sub out of 248049 (6.8%)
c swps: 14 count, 14 rounds, 8934 queries (638.1/round)
c swps: 8509 sat calls, 1208 unsat (1.2% success rate)
c swps: 117092 decisions 13.8, 10439 conflicts 1.2
c swps; 22040.3 avg class size, 35.3 avg environment size
c swps: 0 failed, 1616 impls, 1561 equivs
c swp0: 2974 type 0 queries, 478 unsat (16.1%), 2834 sat (95.3%)
c swp1: 5960 type 1 queries, 3622 unsat (60.8%), 4539 sat (76.2%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 4040977 calls to obtain time
c tops: 282325 fixed 21%, 158 its, 1596.63 confs/it
c trds: 14 transitive reductions, 22494 removed, 132 failed
c trds: 310645 nodes, 516387 edges, 29372854 steps
c trim: 607526 words, 2.3 MB
c trnr: 14 count, 16371 bin, 595164 trn, 557009967 steps
c unhd: 18 count, 18 rounds, 248880225 steps
c unhd: 31103 non-trivial sccs of average size 2.4
c unhd: 4445 units, 4393 bin, 50 trn, 2 lrg
c unhd: 6348 failed, 5468 stamp, 0 lits, 42 bin, 715 trn, 2 lrg
c unhd: 613781 tauts, 10665 bin 2%, 147934 trn 24%, 52064 lrg 8%
c unhd: 613781 tauts, 403118 stamp 66%, 428111 red 70%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 825838 str, 4393 bin 1%, 76535 trn 9%, 744910 lrg 90%, 276686 red 34%
c vars: 163691 remaining 12% and 1213010 removed 88% out of 1376701
c vars: 282325 fixed 21%, 786083 eliminated 57%, 144602 equivalent 11%
c vsts: 12813617840 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 7.3 search visits per propagation, 47895.3 per conflict
c wchs: 1714201051 pushed, 226209654 enlarged, 221 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         302264        103005         13724      21662446       4251527         98643
c 
c  0 0        102651  34      2270   2         0   0  18322863  85<  2883015  68     48442  49     1.8
c  1 5         15109   5      2912   3      1748  13   1226004   6    386062   9<     9734  10<    0.5
c  2 6         41553  14<    16304  16      3789  28   1255808   6    485940  11     17071  17     1.5
c  3 9         51885  17     31205  30      3309  24<   500488   2    271538   6     11760  12     2.1
c  4 14        41421  14     25445  25<     2106  15    169354   1    106432   3      4346   4     2.0
c  5 21        18417   6     10188  10      1216   9     90336   0     56669   1      5247   5     1.0
c  6 30         8285   3      3949   4       713   5     41472   0     23193   1      1078   1     0.8
c  7 41         7750   3      4453   4       376   3     27212   0     19427   0       331   0     1.5
c  8 54        10622   4      5074   5       192   1     19099   0     13335   0       336   0     4.2
c  9 69         2415   1       709   1       115   1      5539   0      3647   0       207   0     1.4
c 10 86         1557   1       460   0       113   1      3134   0      1753   0        79   0     0.6
c 11 126         540   0        36   0        47   0      1047   0       460   0         9   0     0.1
c 12 230          59   0         0   0         0   0        90   0        56   0         3   0     0.0
c 
c avg                  2.5           3.8           3.3           0.3           0.8           1.4
c std                  2.4           1.8           1.8           0.9           1.4           1.7
c 
c  130.116  13% elim
c   87.277   9% probe
c   69.074   7% sweep
c   33.828   3% unhide
c   25.699   3% gauss
c   20.989   2% cce
c   20.515   2% block
c   16.916   2% bca
c   13.520   1% quatres
c   12.122   1% rescore
c   12.022   1% bump
c 
c   10.387 < 1% rest (below)
c 
c    6.219   1% ternres
c    1.891   0% transred
c    1.631   0% decide
c    0.646   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c   16.266   2% preprocessing     3%
c  461.866  46% inprocessing     97%
c ==================================
c  478.132  48% simplifying
c  518.240  52% search
c ==================================
c  996.397 100% all
c 
c        252267 conflicts,         253.2 confs/sec
c          5273 ternaries,          47.8 confs/ternary
c          2072 binaries,          121.8 confs/binary
c           158 iterations,       1596.6 confs/iteration
c 
c             4 reductions,          0.0 redus/sec,  63066.8 confs/reduction
c          7041 restarts,            7.1 rests/sec,     35.8 confs/restart
c       1758879 decisions,        1765.2 decis/sec,      7.0 decis/conflict
c    1744226651 propagations,  1750534.4 props/sec,    991.7 props/decision
c 
c 996.4 seconds, 539.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
