c launch: /data/cnf/sc2014/app/openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_3.025-NOTKNOWN.cnf.bz2
c host: atom31
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/openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_3.025-NOTKNOWN.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_3.025-NOTKNOWN.cnf.bz2
c no embedded options
c found 'p cnf 95456 483561' header
c read 95456 variables, 483561 clauses, 1149911 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=6
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 67515 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] AVG (--score=6)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   67515   276407         0       0      0     0    0     0   14   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 12010 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 12010 out of 12010 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 29475 variables
c [simpleprobe-1] all 65981 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 910 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 910 variables, found 1430 hbrs, 62 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 6 failed, 5772 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 65049 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 36545 variables 56% in round 1 in 6207747 steps
c [elim-1-1] backward subsumption/strengthening limit 6207700
c [elim-1-1-1] backward checking 27951 touched variables 43%
c [elim-1-1-1] incomplete backward checking 27413 remain 98%
c [elim-1-1] subsumed 30 and strengthened 878 clauses in 6207793 steps
c [elim-1-1] rescheduled 1455 variables 2% by backward subsumption
c [elim-1-2] eliminated 24 variables 0% in round 2 in 522052 steps
c [elim-1-2] backward subsumption/strengthening limit 522000
c [elim-1-2-1] backward checking 27713 touched variables 43%
c [elim-1-2-1] incomplete backward checking 27712 remain 100%
c [elim-1-2] subsumed 3 and strengthened 101 clauses in 522057 steps
c [elim-1-2] rescheduled 248 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 26402 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 36569 = 56% variables out of 65049 scheduled
c [phase-count-1] 172899 negative 99.9% of 173017 except 118 0.1%
c [phase-count-1] 114442 positive 66.1% of 173017 except 58575 33.9%
c [phase-count-1] less non-negative clauses 118 than limit 17300 (10.0%)
c [phase-count-1] non-pos/non-neg = 58575/118 = 496.40 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 28480 negative 100%
c [sort-queue-1] sorted 28480 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 28480 (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 38285 variables 57.3% (28480 remain 42%)
c [simplification-1] removed 103390 irredundant clauses 37.4% (173017 remain 63%)
c [simplification-1] maximum reduction of 57% = max (57%, 37%)
c [simplification-1] large reduction 57% >= 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    1.1   28479   173017        89      73      2  1279    0     1   10  19%      0    1    4    0 21846%
c i    1.1   28463   173017       265     235      6  1286    1     9   10   9%      0    9    9    0 15632%
c i    1.1   28458   173017       282     250      6  1287    1    10   11   9%      0   10    8    0 15010%
c i    1.3   28447   173017       870     761     17  1319    3    31   11  10%      2   30   15    0 7526%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 45 variables
c [simpleprobe-2] all 28435 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 51 variables
c [simpleprobe-2] 207 variables remain 1% (28177 retained 99%)
c [simpleprobe-2] removed 51 variables, found 1866 hbrs, 16 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 47098 literals 83%
c [treelook-1] scheduling used 300002 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 530038 steps
c [treelook-1] 47093 literals remain 83%
c [treelook-1] 28203 variables remain to probed next time 99%
c [treelook-1] removed 0 variables, found 277 hbrs
c [basicprobe-1] limit 1377184 based on 172148 irredundant clauses
c [basicprobe-1-0] 17014 probes remain 60% after last round
c [basicprobe-1-0] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3 variables, found 54 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 7 units, 1 failed, 194 tauts, 0 hbrs, 12513 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 28363 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 134 blocked clauses
c [block-1] 134 < 1/100 * 172112 = 1721 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 325 clauses out of 415 (78%) of length 63
c [cce-1-1] eliminated 216 clauses out of 439 (49%) of length 62
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 541 large clauses in 30000094 steps
c [cce-1-1] allowing another 15000047 steps for small clauses
c [cce-1-1] scheduling 167476 clauses = 166389 binary + 1087 ternary
c [cce-1-1] tried to eliminate 552 small clauses 0%
c [cce-1-1] eliminated 256 binary clauses 0%
c [cce-1-1] eliminated 256 small clauses 0%
c [cce-1-1] eliminated 256 small clauses in 30000007 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 797 covered clauses in round 1
c [cce-1] eliminated 797 covered clauses in TOTAL during 1 rounds
c [cce-1] 797 < 1/100 * 171826 = 1718 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 28352 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 9 not tried 0% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 217 = 1% variables out of 28352 scheduled
c [elim-2] 217 < 1/100 * 28352 = 283 considered unsuccessful
c [bca-1] limit of 10000000 steps and 341852 added (scaled 2)
c [bca-1] 40725 out of 56272 literals actually usable 72%
c [bca-1] added 137 blocked clauses in 95311 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2148 pos 7.6% + 25987 neg 92.4% = 28135 sched 100.0% ret 0
c [sweep-1-1] 1001050 steps 18 queries 3015.67 avg class size
c [sweep-1-1] 262 decisions 17 SAT calls 125.18 avg env size
c [sweep-1-1] 27997 variables remain 100% (138 retained 0%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 17 queries)
c [phase-count-2] 170552 negative 99.9% of 170676 except 124 0.1%
c [phase-count-2] 112636 positive 66.0% of 170676 except 58040 34.0%
c [phase-count-2] less non-negative clauses 124 than limit 17000 (10.0%)
c [phase-count-2] non-pos/non-neg = 58040/124 = 468.06 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 5797 negative 100%
c [sort-queue-2] sorted 10327 enqueued variables after 1001 conflicts
c [score-dist-2] active 17808 (63%), one 0 (0%), zero 10327 (37%)
c [score-dist-2] max exp 511, different 10 (2%)
c [score-dist-2] median active exp 511, avg 510.7
c [simplification-2] removed 300 variables 1.1% (28135 remain 42%)
c [simplification-2] removed 2341 irredundant clauses 1.4% (170676 remain 62%)
c [simplification-2] maximum reduction of 1% = max (1%, 1%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 10000
c [simplification-2] penalized conflict interval 10000 = 1 * 10000
c [simplification-2] hard conflict limit 21001 (soft 11001 + delta 10000)
c [simplification-2] new conflict limit 11001 (hard 21001)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    3.3   28134   170676      1140     994     23  3750    4    43   13   9%      2   42   14    0 5440%
c i    4.6   28121   170676      4469    4089     73  3807   12   127   18  10%     36  123   22    1 1916%
c i    4.6   28116   170676      4471    4090     73  3807   12   127   18  10%     36  123   22    1 1904%
c 
c [simplification-3] limit of 143 binary hit after 143 binaries
c [quatres-1] found 223 quaternary clauses 6% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 28098 free variables schedulable
c [ternres-1] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3644 at-most-one constraints of average size 3.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3644 out of 3644 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 3 xors of average arity 3.0
c [gauss-1] connected 9 occurrences of 3 variables (average 3.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-3] limit 119472 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 1 failed, 3480 tauts, 0 hbrs, 102963 literals
c [transred-1] limit 597360 with penalty 0 = 0 + 0
c [transred-1] removed 5 transitive binary clauses
c [bca-2] limit of 10000000 steps and 334202 added (scaled 2)
c [bca-2] 34068 out of 56180 literals actually usable 61%
c [bca-2] added 0 blocked clauses in 73961 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4481 pos 16.0% + 23470 neg 84.0% = 27951 sched 99.5% ret 138
c [sweep-2-1] 1006094 steps 20 queries 4002.15 avg class size
c [sweep-2-1] 416 decisions 18 SAT calls 377.89 avg env size
c [sweep-2-1] 27756 variables remain 99% (333 retained 1%)
c [decomp-8] removed 1 variables
c [sweep-2-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 1 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-3] 166693 negative 99.9% of 166817 except 124 0.1%
c [phase-count-3] 111977 positive 67.1% of 166817 except 54840 32.9%
c [phase-count-3] less non-negative clauses 124 than limit 16600 (10.0%)
c [phase-count-3] non-pos/non-neg = 54840/124 = 442.26 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1803 negative 100%
c [sort-queue-3] sorted 5053 enqueued variables after 6333 conflicts
c [score-dist-3] active 23035 (82%), one 0 (0%), zero 5053 (18%)
c [score-dist-3] max exp 514, different 12 (2%)
c [score-dist-3] median active exp 514, avg 513.8
c [simplification-3] removed 10 variables 0.0% (28088 remain 42%)
c [simplification-3] removed 3859 irredundant clauses 2.3% (166817 remain 60%)
c [simplification-3] maximum reduction of 2% = max (0%, 2%)
c [simplification-3] forced so keeping old conflict interval 10000
c [simplification-3] conflict limit remains at 11006 (hard 21001)
c [simplification-3] 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    7.7   28087   166817      8969    8172    172  3916   22   179   24  12%     52  163   20    3  698%
c i    7.8   28063   166817      9160    8336    180  3918   22   179   24  12%     43  163   28    3  950%
c 
c [simplification-4] limit 11006 conflicts (hard 21001) hit after 11006 conflicts
c [decomp-9] removed 26 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 25243 literals 45%
c [treelook-2] scheduling used 150215 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 212266 steps
c [treelook-2] 25235 literals remain 45%
c [treelook-2] 23007 variables remain to probed next time 82%
c [treelook-2] removed 4 variables, found 563 hbrs
c [unhide-4] limit 210287 with penalty 0 = 0 + 0
c [unhide-4-4] 7 units, 27 failed, 199 tauts, 0 hbrs, 127942 literals
c [transred-2] limit 1051435 with penalty 0 = 0 + 0
c [transred-2] removed 11 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 28028 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 30 blocked clauses
c [block-2] 30 < 1/100 * 166511 = 1665 considered unsuccessful
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 22 clauses out of 103 (21%) of length 61
c [cce-2-1] eliminated 12 clauses out of 133 (9%) of length 60
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 59
c [cce-2-1] eliminated 1 clauses out of 3 (33%) of length 58
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 57
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 52
c [cce-2-1] eliminated 3 clauses out of 4 (75%) of length 51
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 44
c [cce-2-1] eliminated 40 clauses out of 353 (11%) of length 33
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 85 large clauses in 15000070 steps
c [cce-2-1] allowing another 7500035 steps for small clauses
c [cce-2-1] scheduling 161890 clauses = 161447 binary + 443 ternary
c [cce-2-1] tried to eliminate 319 small clauses 0%
c [cce-2-1] eliminated 64 binary clauses 0%
c [cce-2-1] eliminated 64 small clauses 0%
c [cce-2-1] eliminated 64 small clauses in 15000002 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 149 covered clauses in round 1
c [cce-2] eliminated 149 covered clauses in TOTAL during 1 rounds
c [cce-2] 149 < 1/100 * 166202 = 1662 considered unsuccessful
c [elim-3] 9 variables 0% will be scheduled this time
c [elim-3] scheduled 9 variables 0%
c [elim-3] limit of 10514350 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 399599 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 0 = 0% variables out of 9 scheduled
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 5113 pos 18.5% + 22574 neg 81.5% = 27687 sched 98.8% ret 333
c [sweep-3-1] 1234138 steps 32 queries 4320.84 avg class size
c [sweep-3-1] 1071 decisions 29 SAT calls 390.52 avg env size
c [sweep-3-1] 27121 variables remain 97% (898 retained 3%)
c [decomp-11] removed 3 variables
c [sweep-3-1] removed 3 vars (0 failed, 2 eqs, 6 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 3 vars in TOTAL (1 rounds, 31 queries)
c [phase-count-4] 165918 negative 99.9% of 166042 except 124 0.1%
c [phase-count-4] 111434 positive 67.1% of 166042 except 54608 32.9%
c [phase-count-4] less non-negative clauses 124 than limit 16600 (10.0%)
c [phase-count-4] non-pos/non-neg = 54608/124 = 440.39 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1212 negative 100%
c [sort-queue-4] sorted 4282 enqueued variables after 11006 conflicts
c [score-dist-4] active 23735 (85%), one 0 (0%), zero 4282 (15%)
c [score-dist-4] max exp 515, different 13 (3%)
c [score-dist-4] median active exp 515, avg 514.8
c [simplification-4] removed 46 variables 0.2% (28017 remain 41%)
c [simplification-4] removed 775 irredundant clauses 0.5% (166042 remain 60%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 56006 (soft 41006 + delta 15000)
c [simplification-4] new conflict limit 41006 (hard 56006)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.7   28016   166042     13548   12348    265  4608   27   200   33  13%     49  173   30    5  642%
c i   11.8   28015   166042     13617   12412    266  4609   27   201   33  13%     45  174   32    5  684%
c i   12.1   27990   166042     14227   12958    280  4628   27   204   33  13%     25  175   32    5  641%
c i   14.0   27989   166042     17600   16026    346  4682   32   204   36  16%     32  166   39    6  606%
c i   15.1   27984   166042     19302   17567    382  4708   34   205   42  17%     14  164   27    7  378%
c i   17.3   27983   166042     22817   20768    441  4759   36   205   51  18%     33  155   39    9  435%
c i   17.3   27982   166042     22893   20839    441  4759   36   203   51  18%     30  153   35    9  393%
c i   17.3   27981   166042     22896   20838    441  4759   36   203   51  18%     30  153   35    9  392%
c i   19.4   27980   166042     25974   23730    475  4780   39   210   57  19%     26  153   45   10  438%
c i   20.2   27979   166042     27263   24920    493  4795   39   203   60  19%     10  143   34   11  317%
c 
c [simplification-5] limit of 19 iterations hit after 19 iterations
c [quatres-2] found 527 quaternary clauses 10% in total
c [ternres-2] limit 2000000 with penalty 1 = 1 + 0
c [ternres-2] all 27979 free variables schedulable
c [ternres-2] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 5 xors of average arity 2.2
c [gauss-2] connected 11 occurrences of 7 variables (average 1.6)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 2 variables
c [basicprobe-2] limit 13392762 penalty 0 = 0 + 0
c [basicprobe-2-0] 16613 probes remain 59% after last round
c [basicprobe-2-0] 30 units = 30 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 30 variables, found 1604 hbrs
c [unhide-5] limit 267855 with penalty 1 = 0 + 1
c [unhide-5-5] 0 units, 1 failed, 2094 tauts, 0 hbrs, 538041 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 11 transitive binary clauses
c [bca-3] limit of 10000000 steps and 327218 added (scaled 2)
c [bca-3] 30364 out of 55894 literals actually usable 54%
c [bca-3] added 0 blocked clauses in 85055 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 5489 pos 20.3% + 21568 neg 79.7% = 27057 sched 96.8% ret 889
c [sweep-4-1] 1096506 steps 19 queries 3628.05 avg class size
c [sweep-4-1] 956 decisions 18 SAT calls 1175.50 avg env size
c [sweep-4-1] 26818 variables remain 96% (1128 retained 4%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 18 queries)
c [phase-count-5] 163202 negative 99.9% of 163325 except 123 0.1%
c [phase-count-5] 110860 positive 67.9% of 163325 except 52465 32.1%
c [phase-count-5] less non-negative clauses 123 than limit 16300 (10.0%)
c [phase-count-5] non-pos/non-neg = 52465/123 = 426.54 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 674 negative 100%
c [sort-queue-5] sorted 3326 enqueued variables after 27263 conflicts
c [score-dist-5] active 24620 (88%), one 0 (0%), zero 3326 (12%)
c [score-dist-5] max exp 516, different 9 (2%)
c [score-dist-5] median active exp 516, avg 515.8
c [simplification-5] removed 33 variables 0.1% (27946 remain 41%)
c [simplification-5] removed 2717 irredundant clauses 1.6% (163325 remain 59%)
c [simplification-5] maximum reduction of 2% = max (0%, 2%)
c [simplification-5] forced so keeping old conflict interval 30000
c [simplification-5] conflict limit remains at 41009 (hard 56006)
c [simplification-5] 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   29.3   27945   163325     35441   32241    521  6424   44   209   76  21%     98  131   49   15  337%
c i   31.3   27884   163325     38175   34800    540  6442   42   206   76  20%     20  123   49   16  315%
c 
c [simplification-6] limit 41009 conflicts (hard 56006) hit after 41009 conflicts
c [ternres-3] limit 4178386 with penalty 0 = 0 + 0
c [ternres-3] all 27884 free variables schedulable
c [ternres-3] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-3] fully completed ternary resolution
c [card-3] limit 522298 penalty 2 = 2 + 0
c [card-3] found 1618 at-most-one constraints of average size 3.6
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 522298 for elimination
c [card-3] 1618 out of 1618 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-14] removed 63 variables
c [simpleprobe-3] 196 schedulable variables 1%
c [simpleprobe-3] limit 16713547 penalty 0 = 0 + 0
c [decomp-15] removed 112 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 112 variables, found 1777 hbrs, 75 units
c [unhide-6] limit 208919 with penalty 2 = 0 + 2
c [unhide-6-6] 0 units, 0 failed, 337 tauts, 0 hbrs, 963671 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 20 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 12535160 penalty 0 = 0 + 0
c [sweep-5-1] 5630 pos 21.1% + 21041 neg 78.9% = 26671 sched 96.0% ret 1100
c [sweep-5-1] 12840581 steps 208 queries 1075.46 avg class size
c [sweep-5-1] 9950 decisions 193 SAT calls 1415.13 avg env size
c [sweep-5-1] 10021 variables remain 36% (17750 retained 64%)
c [decomp-16] removed 15 variables
c [sweep-5-1] removed 15 vars (0 failed, 14 eqs, 29 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 15 vars in TOTAL (1 rounds, 207 queries)
c [phase-count-6] 161608 negative 99.9% of 161731 except 123 0.1%
c [phase-count-6] 109758 positive 67.9% of 161731 except 51973 32.1%
c [phase-count-6] less non-negative clauses 123 than limit 16100 (10.0%)
c [phase-count-6] non-pos/non-neg = 51973/123 = 422.54 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 258 negative 100%
c [sort-queue-6] sorted 2764 enqueued variables after 41009 conflicts
c [score-dist-6] active 24992 (90%), one 0 (0%), zero 2764 (10%)
c [score-dist-6] max exp 517, different 10 (2%)
c [score-dist-6] median active exp 517, avg 516.7
c [simplification-6] removed 128 variables 0.5% (27756 remain 41%)
c [simplification-6] removed 1594 irredundant clauses 1.0% (161731 remain 59%)
c [simplification-6] maximum reduction of 1% = max (0%, 1%)
c [simplification-6] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-6] new conflict interval 45000
c [simplification-6] penalized conflict interval 45000 = 1 * 45000
c [simplification-6] hard conflict limit 108509 (soft 86009 + delta 22500)
c [simplification-6] new conflict limit 86009 (hard 108509)
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   44.4   27755   161731     48208   44120    633  7839   43   200  114  21%    118  101   44   20  224%
c -   51.5   27755   161731     58675   15043    699  7910   38   172   24  22%    116   59   18   23   79%
c i   52.2   27754   161731     61922   18041    724  7928   30   130   31  23%    160   16   40   22  177%
c i   53.3   27753   161731     63715   19727    726  7942   33   147   35  22%      9   32   49   23  213%
c i   53.4   27744   161731     63845   19853    727  7942   32   147   35  22%      3   32   38   23  165%
c i   58.2   27743   161731     71986   27439    780  7981   41   187   59  22%     69   65   36   25  143%
c i   60.4   27742   161731     75255   30507    793  7992   38   164   71  23%     -2   40   19   26   75%
c i   60.7   27741   161731     76997   32104    805  7995   31   134   71  23%    -20    9   29   25  115%
c i   60.7   27740   161731     77003   32109    805  7995   31   134   71  23%    -20    9   29   25  116%
c i   60.8   27738   161731     77258   32343    807  7996   31   135   71  23%    -25   10   38   25  149%
c i   63.0   27737   161731     81167   35970    823  8012   37   159   74  23%      5   33   31   26  118%
c i   64.5   27736   161731     83469   38142    830  8022   38   149   93  26%    -14   22   65   27  245%
c 
c [simplification-7] limit 86010 conflicts (hard 108509) hit after 86917 conflicts
c [ternres-4] limit 7809855 with penalty 0 = 0 + 0
c [ternres-4] all 27736 free variables schedulable
c [ternres-4] 14 ternary resolvents (0 bin, 14 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 20 variables
c [treelook-3] limit 780985 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 55410 literals 100%
c [treelook-3] scheduling used 542662 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 780985 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 812142 steps
c [treelook-3] 55396 literals remain 100%
c [treelook-3] 22694 variables remain to probed next time 82%
c [treelook-3] removed 0 variables, found 366 hbrs
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 20 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 27736 variables 100%
c [block-3] limit of 19524638 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 50 blocked clauses
c [block-3] 50 < 1/100 * 161502 = 1615 considered unsuccessful
c [cce-3] limit of 9762319 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 75 clauses out of 75 (100%) of length 61
c [cce-3-1] eliminated 118 clauses out of 118 (100%) of length 60
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 59
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 58
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 57
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 56
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 52
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 50
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 49
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 46
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 41
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 209 large clauses in 9762405 steps
c [cce-3-1] allowing another 4881202 steps for small clauses
c [cce-3-1] scheduling 157312 clauses = 156882 binary + 430 ternary
c [cce-3-1] tried to eliminate 228 small clauses 0%
c [cce-3-1] eliminated 40 binary clauses 0%
c [cce-3-1] eliminated 40 small clauses 0%
c [cce-3-1] eliminated 40 small clauses in 9762329 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 249 covered clauses in round 1
c [cce-3] eliminated 249 covered clauses in TOTAL during 1 rounds
c [cce-3] 249 < 1/100 * 161452 = 1614 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 27703 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 780985545 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 171 variables 1% in round 1 in 17291626 steps
c [elim-4-1] backward subsumption/strengthening limit 17291600
c [elim-4-1-1] backward checking 832 touched variables 3%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 2 and strengthened 0 clauses in 216273 steps
c [elim-4-1] rescheduled 4 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 14857 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 176 = 1% variables out of 27703 scheduled
c [elim-4] 176 < 1/100 * 27703 = 277 considered unsuccessful
c [sweep-6] limit 2342956 penalty 0 = 0 + 0
c [sweep-6-1] 4401 pos 44.8% + 5427 neg 55.2% = 9828 sched 35.7% ret 17699
c [sweep-6-1] 2477580 steps 56 queries 2349.02 avg class size
c [sweep-6-1] 1890 decisions 55 SAT calls 814.93 avg env size
c [sweep-6-1] 9527 variables remain 35% (18000 retained 65%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 55 queries)
c [phase-count-7] 160285 negative 99.9% of 160408 except 123 0.1%
c [phase-count-7] 109051 positive 68.0% of 160408 except 51357 32.0%
c [phase-count-7] less non-negative clauses 123 than limit 16000 (10.0%)
c [phase-count-7] non-pos/non-neg = 51357/123 = 417.54 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 163 negative 100%
c [sort-queue-7] sorted 2307 enqueued variables after 86917 conflicts
c [score-dist-7] active 25220 (92%), one 0 (0%), zero 2307 (8%)
c [score-dist-7] max exp 518, different 11 (2%)
c [score-dist-7] median active exp 518, avg 517.7
c [simplification-7] removed 209 variables 0.8% (27527 remain 41%)
c [simplification-7] removed 1323 irredundant clauses 0.8% (160408 remain 58%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 22500 = 45000 / 2
c [simplification-7] new conflict interval 67500
c [simplification-7] penalized conflict interval 67500 = 1 * 67500
c [simplification-7] hard conflict limit 188167 (soft 154417 + delta 33750)
c [simplification-7] new conflict limit 154417 (hard 188167)
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   73.9   27526   160408     94348   48285    868  8486   31   187  120  16%    108   53   22   28   78%
c i   77.6   27525   160408     99660   53283    891  8505   38   176  132  21%     21   38   27   29   93%
c -   79.0   27521   160408    101998   23253    897  8506   32   137   29  23%    -17   -2   23   29   80%
c i   80.1   27520   160408    103079   24295    897  8506   31   121   46  26%     -5  -18   24   29   84%
c i   81.7   27519   160408    106181   27259    910  8510   31   138   59  22%    -10   -0   23   29   80%
c i   90.2   27518   160408    138630   56939   1067  8627   28   167  101  17%    362   19   43   27  162%
c -   90.6   27518   160408    139050   28966   1068  8629   29   164   28  18%    196   16   37   27  139%
c i   93.0   27517   160408    145898   35427   1093  8642   24   105   44  23%    -29  -40   18   27   68%
c i   98.1   27516   160408    156279   45250   1115  8679   33   136   76  25%     27   -7   34   27  125%
c i   98.2   27515   160408    156434   45393   1115  8679   34   138   76  25%      6   -6   39   27  141%
c -  104.6   27515   160408    170771   28776   1144  8696   27   103   28  26%     90  -37   28   28   99%
c i  106.3   27514   160408    176898   34594   1159  8697   21    93   46  23%    174  -43   18   27   65%
c i  106.5   27512   160408    177697   35303   1163  8706   21    92   46  23%     12  -44   20   27   73%
c i  111.0   27511   160408    186506   43720   1190  8725   30   161   75  19%     -2   27   48   27  175%
c 
c [simplification-8] limit 154417 conflicts (hard 188167) hit after 188174 conflicts
c [quatres-3] found 1428 quaternary clauses 16% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [quatres-3-2] added 6 quaternary resolvents
c [ternres-5] limit 13054849 with penalty 0 = 0 + 0
c [ternres-5] all 27511 free variables schedulable
c [ternres-5] 27 ternary resolvents (0 bin, 27 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-3] limit 652742 penalty 2 = 2 + 0
c [gauss-3] extracted 2 xors of average arity 2.5
c [gauss-3] connected 5 occurrences of 5 variables (average 1.0)
c [gauss-3] limit 652742 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 1 variables
c [basicprobe-3] limit 65274245 penalty 0 = 0 + 0
c [basicprobe-3-0] 14969 probes remain 55% after last round
c [basicprobe-3-0] 159 units = 159 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 289 variables, found 1044 hbrs
c [bate-1] eliminated 1 asymmetric tautologies during probing
c [unhide-7] limit 652742 with penalty 2 = 1 + 1
c [unhide-7-7] 0 units, 2 failed, 1593 tauts, 0 hbrs, 1499314 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 17 transitive binary clauses
c [transred-6] found 1 units
c [bca-4] limit of 10000000 steps and 312840 added (scaled 2)
c [bca-4] 30192 out of 54440 literals actually usable 55%
c [bca-4] added 330 blocked clauses in 105664 steps
c [sweep-7] limit 3916454 penalty 0 = 0 + 0
c [sweep-7-1] 4147 pos 44.2% + 5232 neg 55.8% = 9379 sched 34.5% ret 17840
c [sweep-7-1] 4089470 steps 106 queries 2250.97 avg class size
c [sweep-7-1] 2541 decisions 101 SAT calls 296.22 avg env size
c [sweep-7-1] 8981 variables remain 33% (18238 retained 67%)
c [decomp-21] removed 3 variables
c [sweep-7-1] removed 3 vars (0 failed, 3 eqs, 5 impls)
c [sweep-7] 3 < 1/1000 * 27219 = 27 considered unsuccessful
c [sweep-7] removed 3 vars in TOTAL (1 rounds, 105 queries)
c [phase-count-8] 156012 negative 99.9% of 156135 except 123 0.1%
c [phase-count-8] 107286 positive 68.7% of 156135 except 48849 31.3%
c [phase-count-8] less non-negative clauses 123 than limit 15600 (10.0%)
c [phase-count-8] non-pos/non-neg = 48849/123 = 397.15 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 137 negative 100%
c [sort-queue-8] sorted 2089 enqueued variables after 188174 conflicts
c [score-dist-8] active 25127 (92%), one 0 (0%), zero 2089 (8%)
c [score-dist-8] max exp 519, different 12 (2%)
c [score-dist-8] median active exp 519, avg 518.7
c [simplification-8] removed 295 variables 1.1% (27216 remain 40%)
c [simplification-8] removed 4273 irredundant clauses 2.7% (156135 remain 56%)
c [simplification-8] maximum reduction of 3% = max (1%, 3%)
c [simplification-8] geometric conflict interval increment 16875 = 67500 / 4
c [simplification-8] new conflict interval 84375
c [simplification-8] penalized conflict interval 84375 = 1 * 84375
c [simplification-8] hard conflict limit 314736 (soft 272549 + delta 42187)
c [simplification-8] new conflict limit 272549 (hard 314736)
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  117.5   27215   156135    189818   46719   1098  9677   31   151   78  21%    -79   16   34   27  125%
c i  117.7   27214   156135    190183   47069   1102  9680   31   147   78  21%    -90   12   26   27   94%
c i  120.7   27213   156135    196186   52660   1127  9695   31   124   86  25%    -35  -10   26   28   95%
c i  122.5   27212   156135    199090   55364   1133  9705   36   144   90  25%    -74    9   34   28  122%
c i  124.1   27211   156135    203242   59338   1140  9709   32   146  107  22%    -55   11   45   28  159%
c -  125.1   27211   156135    204495   29171   1143  9712   34   157   28  21%    -80   22   26   28   91%
c i  126.8   27210   156135    207368   31853   1167  9720   41   178   40  23%    -50   42   58   29  199%
c i  127.8   27209   156135    209078   33443   1173  9724   45   180   43  25%    -75   43   42   30  140%
c i  132.2   27207   156135    215660   39641   1207  9755   46   191   66  24%     -6   49   45   31  144%
c i  134.0   27206   156135    219389   43151   1215  9758   34   139   72  24%    -45   -5   19   31   63%
c i  135.1   27205   156135    220344   44036   1217  9758   35   128   91  27%    -66  -16   40   31  129%
c i  137.2   27204   156135    223502   46982   1235  9770   41   165   95  25%    -51   20   39   32  122%
c i  138.2   27203   156135    224553   48006   1235  9770   38   169  105  23%    -66   24   35   32  109%
c i  138.9   27202   156135    225512   48912   1238  9774   40   171  106  23%    -71   26   47   32  146%
c i  139.7   27201   156135    226562   49894   1244  9778   41   176  106  24%    -72   30   40   32  123%
c i  141.1   27200   156135    228532   51705   1247  9782   47   183  108  25%    -62   37   46   33  139%
c i  143.0   27199   156135    231363   54425   1246  9787   41   174  132  23%    -47   26   36   33  109%
c i  143.7   27198   156135    232635   55666   1248  9787   38   147  157  26%    -59   -1   36   33  109%
c i  145.0   27197   156135    233732   56702   1248  9787   37   141  157  26%    -63   -7   30   33   90%
c i  145.6   27196   156135    235610   58450   1260  9792   30   188  157  16%    -56   39   23   33   70%
c i  145.8   27195   156135    236028   58803   1267  9795   35   196  157  18%    -60   47   80   33  244%
c i  147.2   27194   156135    237826   60462   1272  9802   41   193  157  21%    -55   43   54   33  162%
c -  148.2   27194   156135    239620   28875   1275  9808   38   151   28  25%    -53   -0   28   33   84%
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  148.9   27193   156135    241660   30856   1278  9808   34   113   41  30%    -24  -38   31   33   93%
c i  151.0   27192   156135    246066   35022   1293  9812   31   134   54  23%    -13  -15   23   33   71%
c i  152.0   27191   156135    248340   37086   1305  9820   33   121   58  28%    -38  -28   22   33   67%
c i  152.2   27190   156135    249247   37935   1306  9822   31   108   58  28%    -49  -40   26   33   78%
c i  152.6   27189   156135    249781   38440   1306  9822   31   118   58  26%    -53  -30   28   33   85%
c i  159.4   27188   156135    265703   53697   1341  9842   30    64  101  47%    157  -73   29   33   88%
c i  160.9   27187   156135    268051   55887   1346  9847   36   121  106  30%    -30  -14   36   33  108%
c -  165.0   27187   156135    275736   32086   1357  9855   29    91   29  32%     31  -42   27   33   82%
c -  176.0   27187   156135    309673   34479   1427  9869   17    36   41  48%    432  -63   17   28   62%
c 
c [simplification-9] limit 272549 conflicts (hard 314736) hit after 314736 conflicts
c [ternres-6] limit 20556338 with penalty 0 = 0 + 0
c [ternres-6] all 27187 free variables schedulable
c [ternres-6] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-22] removed 30 variables
c [simpleprobe-4] all 27186 free variables schedulable
c [simpleprobe-4] limit 82225353 penalty 0 = 0 + 0
c [decomp-23] removed 167 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 167 variables, found 1916 hbrs, 129 units
c [unhide-8] limit 4111267 with penalty 0 = 0 + 0
c [unhide-8-11] 9 units, 1 failed, 3255 tauts, 0 hbrs, 687796 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 18 transitive binary clauses
c [transred-7] found 1 units
c [phase-count-9] 151565 negative 99.9% of 151688 except 123 0.1%
c [phase-count-9] 105858 positive 69.8% of 151688 except 45830 30.2%
c [phase-count-9] less non-negative clauses 123 than limit 15100 (10.0%)
c [phase-count-9] non-pos/non-neg = 45830/123 = 372.60 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 108 negative 100%
c [sort-queue-9] sorted 1882 enqueued variables after 314736 conflicts
c [score-dist-9] active 25126 (93%), one 0 (0%), zero 1882 (7%)
c [score-dist-9] max exp 520, different 13 (2%)
c [score-dist-9] median active exp 520, avg 519.6
c [simplification-9] removed 179 variables 0.7% (27008 remain 40%)
c [simplification-9] removed 4447 irredundant clauses 2.8% (151688 remain 55%)
c [simplification-9] maximum reduction of 3% = max (1%, 3%)
c [simplification-9] geometric conflict interval increment 21093 = 84375 / 4
c [simplification-9] new conflict interval 105468
c [simplification-9] penalized conflict interval 105468 = 1 * 105468
c [simplification-9] hard conflict limit 472938 (soft 420204 + delta 52734)
c [simplification-9] new conflict limit 420204 (hard 472938)
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  185.9   27007   151688    325125   49040   1471 10959   37   162   63  23%    556   64   50   28  181%
c i  188.4   27006   151688    328730   52439   1495 10976   38   165   82  23%   -249   64   41   28  146%
c i  188.7   27005   151688    329075   52762   1496 10976   38   164   82  23%   -266   62   40   28  142%
c i  190.6   27004   151688    333786   57333   1501 10979   28   184   96  15%   -237   78   27   28   94%
c i  192.1   27003   151688    336152   59508   1509 10985   42   188  102  22%   -257   78   56   29  191%
c -  198.7   27003   151688    342851   32564   1520 10991   30   149   28  20%   -174   36   20   29   69%
c i  207.9   27002   151688    367041   55196   1564 11031   38   177   76  22%    196   38   44   28  156%
c i  208.1   27001   151688    367236   55364   1565 11031   41   182   77  23%    115   43   72   28  252%
c i  210.1   27000   151688    370345   58278   1573 11033   43   172   92  25%   -213   31   16   29   55%
c i  212.6   26999   151688    374505   62269   1576 11041   41   167   99  25%   -200   24   53   30  177%
c i  213.9   26998   151688    376299   63985   1579 11044   41   177  109  23%   -221   33   32   30  107%
c -  216.1   26998   151688    379763   33330   1581 11049   35   144   28  24%   -194   -0   40   30  134%
c i  219.1   26997   151688    383337   36746   1589 11057   32   136   56  23%   -130   -8   21   30   70%
c i  224.1   26957   151688    389147   42185   1602 11064   41   135   94  30%   -134   -8   41   31  131%
c i  225.0   26956   151688    390655   43623   1606 11066   42   143   94  29%   -177   -0   40   32  127%
c i  225.1   26955   151688    390856   43814   1606 11066   41   143   94  29%   -181   -0   37   32  118%
c i  229.4   26954   151688    397551   50250   1621 11077   28   118  157  23%   -101  -24   21   31   66%
c i  230.8   26952   151688    403482   55905   1627 11078   32   193  157  16%   -100   48   52   31  165%
c i  232.3   26951   151688    405897   58213   1627 11078   33   166  158  20%   -142   19   26   31   81%
c i  234.4   26950   151688    410451   62606   1638 11080   28   149  165  19%   -107    2   21   31   67%
c -  238.2   26950   151688    416816   34665   1640 11082   30    95   28  31%    -68  -50   36   31  116%
c i  239.5   26949   151688    419236   36982   1650 11087   30   131   41  23%    -29  -13   26   31   83%
c -  259.5   26949   151688    453137   37023   1662 11106   22    69   45  32%    313  -53   19   28   69%
c 
c [simplification-10] limit 420204 conflicts (hard 472938) hit after 469682 conflicts
c [quatres-4] found 2037 quaternary clauses 18% in total
c [quatres-4-1] removed 5 duplicate quaternary clauses
c [quatres-4-2] added 4 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1 quaternary resolvents
c [ternres-7] limit 29446383 with penalty 0 = 0 + 0
c [ternres-7] all 26949 free variables schedulable
c [ternres-7] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-7] fully completed ternary resolution
c [card-4] limit 1840398 penalty 3 = 3 + 0
c [card-4] found 5098 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1840398 for elimination
c [card-4] 5098 out of 5098 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-24] removed 60 variables
c [unhide-9] limit 1472319 with penalty 2 = 0 + 2
c [unhide-9-13] 2 units, 1 failed, 1424 tauts, 0 hbrs, 3635441 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 23 transitive binary clauses
c [bca-5] limit of 10000000 steps and 300595 added (scaled 2)
c [bca-5] 30095 out of 53892 literals actually usable 56%
c [bca-5] added 558 blocked clauses in 113631 steps
c [sweep-8] limit 4416957 penalty 1 = 1 + 0
c [sweep-8-1] 3929 pos 43.8% + 5046 neg 56.2% = 8975 sched 33.3% ret 17970
c [sweep-8-1] 4468655 steps 131 queries 1707.12 avg class size
c [sweep-8-1] 2411 decisions 125 SAT calls 242.89 avg env size
c [sweep-8-1] 8585 variables remain 32% (18360 retained 68%)
c [decomp-25] removed 2 variables
c [sweep-8-1] removed 2 vars (0 failed, 5 eqs, 7 impls)
c [sweep-8] 2 < 1/1000 * 26945 = 26 considered unsuccessful
c [sweep-8] removed 2 vars in TOTAL (1 rounds, 130 queries)
c [phase-count-10] 149804 negative 99.9% of 149929 except 125 0.1%
c [phase-count-10] 105390 positive 70.3% of 149929 except 44539 29.7%
c [phase-count-10] less non-negative clauses 125 than limit 14900 (10.0%)
c [phase-count-10] non-pos/non-neg = 44539/125 = 356.31 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 97 negative 100%
c [sort-queue-10] sorted 1703 enqueued variables after 469682 conflicts
c [score-dist-10] active 25240 (94%), one 0 (0%), zero 1703 (6%)
c [score-dist-10] max exp 520, different 13 (2%)
c [score-dist-10] median active exp 520, avg 519.8
c [simplification-10] removed 6 variables 0.0% (26943 remain 40%)
c [simplification-10] removed 1759 irredundant clauses 1.2% (149929 remain 54%)
c [simplification-10] maximum reduction of 1% = max (0%, 1%)
c [simplification-10] geometric conflict interval increment 52734 = 105468 / 2
c [simplification-10] new conflict interval 158202
c [simplification-10] penalized conflict interval 158202 = 1 * 158202
c [simplification-10] hard conflict limit 706985 (soft 627884 + delta 79101)
c [simplification-10] new conflict limit 627884 (hard 706985)
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  277.0   26942   149929    471745   55090   1656 11530   27   128  122  21%    489   17   39   27  146%
c i  281.3   26941   149929    477816   60878   1671 11537   34   155  135  22%   -221   41   61   27  223%
c -  287.6   26941   149929    488603   36856   1696 11549   29   134   31  22%   -116   13   22   28   81%
c i  289.8   26940   149929    495535   43391   1718 11562   26    97   52  27%     -1  -22   37   27  137%
c i  298.8   26939   149929    514289   61220   1770 11597   41   143   89  29%     43   27   51   28  182%
c -  304.9   26939   149929    526710   37322   1786 11612   27    69   30  39%    -34  -47   19   29   64%
c i  307.0   26938   149929    533294   43640   1791 11616   17    39   45  44%     67  -72   20   28   74%
c i  312.3   26937   149929    541309   51010   1799 11636   54   171   68  32%    -90   58   51   32  160%
c i  324.2   26936   149929    557194   66093   1841 11657   46   140  181  33%     50   29   35   33  108%
c -  327.1   26936   149929    565844   38462   1844 11657   31   135   31  23%    -50   19   24   32   76%
c i  328.3   26935   149929    568706   41142   1847 11663   40   162   43  25%     -5   46   59   33  180%
c i  337.0   26934   149929    592423   63871   1891 11687   30   118   95  26%    180   -4   47   31  149%
c i  339.7   26933   149929    596165   67292   1906 11695   53   185   98  29%   -119   61   79   33  236%
c i  340.0   26932   149929    596596   67703   1908 11696   51   182  108  28%   -134   57   44   33  133%
c -  343.0   26932   149929    605180   39670   1914 11696   27   113   43  24%    -38  -14   23   32   70%
c i  347.5   26931   149929    618810   52745   1931 11705   35   134   79  26%    161   12   70   32  221%
c i  349.5   26930   149929    621716   55362   1936 11714   58   184   92  31%   -118   61   95   34  281%
c i  351.2   26929   149929    624407   57910   1945 11722   48   184   98  26%   -131   58   21   34   62%
c 
c [simplification-11] limit 627884 conflicts (hard 706985) hit after 634948 conflicts
c [quatres-5] found 2490 quaternary clauses 18% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [quatres-5-2] added 2 quaternary resolvents
c [ternres-8] limit 39896705 with penalty 0 = 0 + 0
c [ternres-8] all 26929 free variables schedulable
c [ternres-8] 14 ternary resolvents (0 bin, 14 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-26] removed 15 variables
c [treelook-4] limit 1994835 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 53749 literals 100%
c [treelook-4] scheduling used 583293 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1994835 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 1998898 steps
c [treelook-4] 53412 literals remain 100%
c [treelook-4] 21881 variables remain to probed next time 82%
c [treelook-4] removed 108 variables, found 2816 hbrs
c [unhide-10] limit 1994835 with penalty 2 = 0 + 2
c [unhide-10-15] 3 units, 6 failed, 1031 tauts, 0 hbrs, 2664584 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 26 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 26803 variables 100%
c [block-4] limit of 49870881 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 139 blocked clauses
c [block-4] 139 < 1/100 * 147890 = 1478 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 249354408 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 52 clauses out of 277 (19%) of length 33
c [cce-4-1] eliminated 20 clauses out of 25 (80%) of length 32
c [cce-4-1] eliminated 33 clauses out of 73 (45%) of length 31
c [cce-4-1] eliminated 20 clauses out of 45 (44%) of length 30
c [cce-4-1] eliminated 4 clauses out of 13 (31%) of length 29
c [cce-4-1] eliminated 1 clauses out of 6 (17%) of length 28
c [cce-4-1] eliminated 1 clauses out of 6 (17%) of length 27
c [cce-4-1] eliminated 1 clauses out of 8 (12%) of length 26
c [cce-4-1] eliminated 21 clauses out of 107 (20%) of length 24
c [cce-4-1] eliminated 83 clauses out of 179 (46%) of length 23
c [cce-4-1] eliminated 74 clauses out of 151 (49%) of length 22
c [cce-4-1] eliminated 73 clauses out of 146 (50%) of length 21
c [cce-4-1] eliminated 69 clauses out of 136 (51%) of length 20
c [cce-4-1] eliminated 63 clauses out of 128 (49%) of length 19
c [cce-4-1] eliminated 68 clauses out of 134 (51%) of length 18
c [cce-4-1] eliminated 35 clauses out of 70 (50%) of length 17
c [cce-4-1] eliminated 59 clauses out of 118 (50%) of length 16
c [cce-4-1] eliminated 58 clauses out of 117 (50%) of length 15
c [cce-4-1] eliminated 60 clauses out of 119 (50%) of length 14
c [cce-4-1] eliminated 85 clauses out of 171 (50%) of length 13
c [cce-4-1] eliminated 52 clauses out of 105 (50%) of length 12
c [cce-4-1] eliminated 54 clauses out of 109 (50%) of length 11
c [cce-4-1] eliminated 45 clauses out of 92 (49%) of length 10
c [cce-4-1] eliminated 51 clauses out of 104 (49%) of length 9
c [cce-4-1] eliminated 35 clauses out of 72 (49%) of length 8
c [cce-4-1] eliminated 28 clauses out of 69 (41%) of length 7
c [cce-4-1] eliminated 27 clauses out of 85 (32%) of length 6
c [cce-4-1] eliminated 12 clauses out of 55 (22%) of length 5
c [cce-4-1] eliminated 62 clauses out of 167 (37%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 1246 large clauses in 20834408 steps
c [cce-4-1] allowing another 10417204 steps for small clauses
c [cce-4-1] scheduling 144430 clauses = 143463 binary + 967 ternary
c [cce-4-1] tried to eliminate 13554 small clauses 9%
c [cce-4-1] eliminated 2499 binary clauses 2%
c [cce-4-1] eliminated 1 ternary clauses 0%
c [cce-4-1] eliminated 2500 small clauses 2%
c [cce-4-1] eliminated 2500 small clauses in 249354408 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 3746 covered clauses in round 1
c [cce-4] eliminated 3746 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 26680 variables 100%
c [elim-5] limit of 99741763 steps penalty 3 = 3 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 884 variables 3% in round 1 in 16236014 steps
c [elim-5-1] backward subsumption/strengthening limit 16236000
c [elim-5-1-1] backward checking 11381 touched variables 43%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 137 clauses in 6645110 steps
c [elim-5-1] rescheduled 470 variables 2% by backward subsumption
c [elim-5-2] no variable eliminated in round 2 in 539102 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 884 = 3% variables out of 26680 scheduled
c [bca-6] limit of 10000000 steps and 275602 added (scaled 2)
c [bca-6] 35078 out of 51594 literals actually usable 68%
c [bca-6] added 42025 blocked clauses in 196332 steps
c [phase-count-11] 137045 negative 99.8% of 137295 except 250 0.2%
c [phase-count-11] 96803 positive 70.5% of 137295 except 40492 29.5%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 11 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 1254 enqueued variables after 634948 conflicts
c [score-dist-11] active 24542 (95%), one 0 (0%), zero 1254 (5%)
c [score-dist-11] max exp 521, different 14 (3%)
c [score-dist-11] median active exp 521, avg 520.7
c [simplification-11] removed 1133 variables 4.2% (25796 remain 38%)
c [simplification-11] removed 12634 irredundant clauses 8.4% (137295 remain 50%)
c [simplification-11] maximum reduction of 8% = max (4%, 8%)
c [simplification-11] large reduction 8% >= 5% limit
c [simplification-11] next conflict interval 6349 = min (634948/100, 158202)
c [simplification-11] penalized conflict interval 6349 = 1 * 6349
c [simplification-11] hard conflict limit 651297 (soft 641297 + delta 10000)
c [simplification-11] new conflict limit 641297 (hard 651297)
c 
c [simplification-12] limit 641297 conflicts (hard 651297) hit after 651299 conflicts
c [quatres-6] found 2477 quaternary clauses 20% in total
c [quatres-6-2] added 11 quaternary resolvents
c [ternres-9] limit 40783976 with penalty 0 = 0 + 0
c [ternres-9] all 25796 free variables schedulable
c [ternres-9] 382 ternary resolvents (0 bin, 382 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 1019599 penalty 3 = 3 + 0
c [gauss-4] extracted 5 xors of average arity 2.2
c [gauss-4] connected 11 occurrences of 9 variables (average 1.2)
c [gauss-4] limit 1019599 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-28] removed 2 variables
c [basicprobe-4] limit 203919883 penalty 0 = 0 + 0
c [basicprobe-4-0] 9645 probes remain 38% after last round
c [basicprobe-4-0] 356 units = 356 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 375 variables, found 3571 hbrs
c [bate-2] eliminated 3 asymmetric tautologies during probing
c [unhide-11] limit 8156795 with penalty 0 = 0 + 0
c [unhide-11-21] 40 units, 13 failed, 6655 tauts, 0 hbrs, 1639747 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 115 transitive binary clauses
c [transred-10] found 1 units
c [bca-7] limit of 10000000 steps and 283063 added (scaled 2)
c [bca-7] 31894 out of 50744 literals actually usable 63%
c [bca-7] added 1118 blocked clauses in 149825 steps
c [phase-count-12] 130271 negative 99.8% of 130519 except 248 0.2%
c [phase-count-12] 93236 positive 71.4% of 130519 except 37283 28.6%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 7 positive 58%, 5 negative 42%
c [sort-queue-12] sorted 1252 enqueued variables after 651299 conflicts
c [score-dist-12] active 24119 (95%), one 0 (0%), zero 1252 (5%)
c [score-dist-12] max exp 521, different 14 (3%)
c [score-dist-12] median active exp 521, avg 520.7
c [simplification-12] removed 425 variables 1.6% (25371 remain 38%)
c [simplification-12] removed 6776 irredundant clauses 4.9% (130519 remain 47%)
c [simplification-12] maximum reduction of 5% = max (2%, 5%)
c [simplification-12] large reduction 5% >= 5% limit
c [simplification-12] next conflict interval 6512 = min (651299/100, 158202)
c [simplification-12] penalized conflict interval 6512 = 1 * 6512
c [simplification-12] hard conflict limit 667811 (soft 657811 + delta 10000)
c [simplification-12] new conflict limit 657811 (hard 667811)
c 
c [simplification-13] limit 657811 conflicts (hard 667811) hit after 667812 conflicts
c [quatres-7] found 2539 quaternary clauses 20% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 5 quaternary resolvents
c [ternres-10] limit 41731032 with penalty 0 = 0 + 0
c [ternres-10] all 25371 free variables schedulable
c [ternres-10] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-29] removed 1 variables
c [simpleprobe-5] all 25370 free variables schedulable
c [simpleprobe-5] limit 166924129 penalty 0 = 0 + 0
c [decomp-30] removed 48 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 48 variables, found 1913 hbrs, 46 units
c [unhide-12] limit 2086551 with penalty 2 = 0 + 2
c [unhide-12-23] 1 units, 0 failed, 1595 tauts, 0 hbrs, 2414604 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 113 transitive binary clauses
c [cce-5] limit of 52163790 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 45
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 42
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 39
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 38
c [cce-5-1] eliminated 2 clauses out of 5 (40%) of length 37
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 35
c [cce-5-1] eliminated 4 clauses out of 229 (2%) of length 33
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 32
c [cce-5-1] eliminated 33 clauses out of 39 (85%) of length 31
c [cce-5-1] eliminated 23 clauses out of 25 (92%) of length 30
c [cce-5-1] eliminated 1 clauses out of 5 (20%) of length 29
c [cce-5-1] eliminated 7 clauses out of 13 (54%) of length 28
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 27
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 26
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 25
c [cce-5-1] eliminated 32 clauses out of 148 (22%) of length 24
c [cce-5-1] eliminated 26 clauses out of 253 (10%) of length 23
c [cce-5-1] eliminated 13 clauses out of 219 (6%) of length 22
c [cce-5-1] eliminated 18 clauses out of 202 (9%) of length 21
c [cce-5-1] eliminated 22 clauses out of 155 (14%) of length 20
c [cce-5-1] eliminated 17 clauses out of 156 (11%) of length 19
c [cce-5-1] eliminated 19 clauses out of 208 (9%) of length 18
c [cce-5-1] eliminated 23 clauses out of 134 (17%) of length 17
c [cce-5-1] eliminated 5 clauses out of 132 (4%) of length 16
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 261 large clauses in 52163815 steps
c [cce-5-1] allowing another 26081907 steps for small clauses
c [cce-5-1] scheduling 124760 clauses = 123900 binary + 860 ternary
c [cce-5-1] tried to eliminate 947 small clauses 1%
c [cce-5-1] eliminated 232 binary clauses 0%
c [cce-5-1] eliminated 1 ternary clauses 0%
c [cce-5-1] eliminated 233 small clauses 0%
c [cce-5-1] eliminated 233 small clauses in 52163790 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 494 covered clauses in round 1
c [cce-5] eliminated 494 covered clauses in TOTAL during 1 rounds
c [cce-5] 494 < 1/100 * 129608 = 1296 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 25321 variables 100%
c [elim-6] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 373 variables 1% in round 1 in 12926939 steps
c [elim-6-1] backward subsumption/strengthening limit 12926900
c [elim-6-1-1] backward checking 3097 touched variables 12%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 74 clauses in 1735795 steps
c [elim-6-1] rescheduled 182 variables 1% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 250038 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 373 = 1% variables out of 25321 scheduled
c [bca-8] limit of 10000000 steps and 275266 added (scaled 2)
c [bca-8] 30585 out of 49898 literals actually usable 61%
c [bca-8] added 4704 blocked clauses in 149358 steps
c [sweep-9] limit 3129827 penalty 2 = 2 + 0
c [sweep-9-1] 3369 pos 43.1% + 4453 neg 56.9% = 7822 sched 31.4% ret 17126
c [sweep-9-1] 3180948 steps 127 queries 2193.33 avg class size
c [sweep-9-1] 971 decisions 123 SAT calls 73.42 avg env size
c [sweep-9-1] 7621 variables remain 31% (17327 retained 69%)
c [decomp-31] removed 2 variables
c [sweep-9-1] removed 2 vars (0 failed, 2 eqs, 4 impls)
c [sweep-9] 2 < 1/1000 * 24948 = 24 considered unsuccessful
c [sweep-9] removed 2 vars in TOTAL (1 rounds, 126 queries)
c [phase-count-13] 126055 negative 99.8% of 126340 except 285 0.2%
c [phase-count-13] 90315 positive 71.5% of 126340 except 36025 28.5%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 1 positive 12%, 7 negative 88%
c [sort-queue-13] sorted 1040 enqueued variables after 667812 conflicts
c [score-dist-13] active 23906 (96%), one 0 (0%), zero 1040 (4%)
c [score-dist-13] max exp 521, different 14 (3%)
c [score-dist-13] median active exp 521, avg 520.7
c [simplification-13] removed 425 variables 1.7% (24946 remain 37%)
c [simplification-13] removed 4179 irredundant clauses 3.2% (126340 remain 46%)
c [simplification-13] maximum reduction of 3% = max (2%, 3%)
c [simplification-13] geometric conflict interval increment 39550 = 158202 / 4
c [simplification-13] new conflict interval 197752
c [simplification-13] penalized conflict interval 197752 = 1 * 197752
c [simplification-13] hard conflict limit 964440 (soft 865564 + delta 98876)
c [simplification-13] new conflict limit 865564 (hard 964440)
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  401.7   24945   126340    684716   74311   2305 60615   28   110   85  25%    545    1   35   29  121%
c -  402.4   24945   126340    685803   39486   2313 60624   28   117   30  24%    -58    8   22   29   75%
c i  410.3   24944   126340    704213   57391   2352 60653   25    81   91  31%    -43  -26   29   28  101%
c i  410.9   24943   126340    705252   58360   2360 60654   30   101   91  29%   -218   -6   48   29  167%
c -  419.3   24940   126340    724569   41363   2413 60671   20    41   33  49%      3  -54   20   27   74%
c -  435.5   24940   126340    763388   43360   2508 60686   16    27   35  58%    459  -39   16   22   70%
c i  444.2   24939   126340    780418   59806   2559 60712   22    73  129  30%    589   15   32   21  152%
c i  444.2   24938   126340    780486   59865   2560 60712   22    74  129  30%    514   16   33   21  153%
c i  444.4   24937   126340    780895   60227   2568 60720   23    80  129  29%    156   22   32   21  150%
c i  444.4   24936   126340    780932   60261   2568 60722   23    82  129  28%    130   23   34   21  160%
c i  444.9   24935   126340    781826   61075   2573 60749   27   104  130  26%   -273   46   38   22  175%
c i  445.1   24934   126340    782343   61562   2573 60757   27   110  130  25%   -387   51   29   22  133%
c i  445.2   24933   126340    782459   61657   2573 60759   28   112  130  25%   -406   53   41   22  190%
c i  450.2   24932   126340    792336   71196   2606 60785   27    96  150  28%   -361   31   42   22  187%
c i  452.7   24931   126340    796315   74925   2615 60802   38   131  154  29%   -424   63   42   24  176%
c i  455.5   24930   126340    800617   78989   2630 60812   41   142  158  29%   -393   69   37   25  147%
c -  456.7   24930   126340    802159   40336   2641 60829   44   148   31  30%   -413   74   40   26  158%
c i  457.3   24929   126340    803246   41343   2647 60829   44   151   40  29%   -399   75   37   26  142%
c i  459.3   24928   126340    806990   44852   2657 60839   47   168   46  28%   -363   87   40   27  148%
c i  466.4   24927   126340    819228   56535   2698 60865   41   142   77  29%   -177   51   65   29  227%
c i  475.4   24926   126340    832997   69554   2725 60892   44   161  138  27%   -107   61   61   32  192%
c -  483.5   24913   126340    845827   39862   2737 60911   42   129   45  33%    -85   22   50   33  151%
c i  488.5   24912   126340    860302   53798   2758 60914   26    65   74  41%    134  -34   45   31  145%
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  488.6   24911   126340    860436   53912   2763 60916   28    69   74  40%     84  -29   53   31  170%
c i  495.8   24910   126340    874210   66974   2785 60942   37   118  100  31%    -48   15   29   33   90%
c -  501.9   24910   126340    891302   44218   2806 60944   19    59   46  32%     30  -41   15   30   49%
c i  504.6   24909   126340    900525   53094   2813 60945   16    51   64  31%    160  -43   20   28   71%
c i  507.4   24908   126340    904357   56676   2821 60949   35    99   80  35%   -175    6   66   29  226%
c i  508.5   24907   126340    906311   58511   2826 60953   43   129   83  33%   -198   36   52   30  175%
c i  509.4   24906   126340    907757   59874   2833 60963   42   140   86  30%   -201   45   40   30  131%
c i  513.6   24905   126340    914765   66301   2847 60987   57   172   94  33%   -107   71   58   33  176%
c 
c [simplification-14] limit 865564 conflicts (hard 964440) hit after 928614 conflicts
c [quatres-8] found 3100 quaternary clauses 20% in total
c [quatres-8-2] added 4 single-self-subsuming ternary resolvents
c [quatres-8-2] added 1 quaternary resolvents
c [ternres-11] limit 59376702 with penalty 0 = 0 + 0
c [ternres-11] all 24900 free variables schedulable
c [ternres-11] 50 ternary resolvents (0 bin, 50 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-32] removed 46 variables
c [treelook-5] limit 5937670 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 49747 literals 100%
c [treelook-5] scheduling used 649949 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 5937670 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 5938427 steps
c [treelook-5] 49468 literals remain 99%
c [treelook-5] 20420 variables remain to probed next time 82%
c [treelook-5] removed 0 variables, found 4606 hbrs
c [unhide-13] limit 1484417 with penalty 3 = 0 + 3
c [unhide-13-24] 0 units, 0 failed, 615 tauts, 0 hbrs, 3365872 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 118 transitive binary clauses
c [transred-12] found 3 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 24897 variables 100%
c [elim-7] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 43 variables 0% in round 1 in 12394864 steps
c [elim-7-1] backward subsumption/strengthening limit 12394800
c [elim-7-1-1] backward checking 630 touched variables 3%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 146855 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 43 = 0% variables out of 24897 scheduled
c [elim-7] 43 < 1/100 * 24897 = 248 considered unsuccessful
c [bca-9] limit of 10000000 steps and 275364 added (scaled 2)
c [bca-9] 27295 out of 49710 literals actually usable 55%
c [bca-9] added 238 blocked clauses in 130473 steps
c [phase-count-14] 124961 negative 99.8% of 125214 except 253 0.2%
c [phase-count-14] 89844 positive 71.8% of 125214 except 35370 28.2%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 950 enqueued variables after 928614 conflicts
c [score-dist-14] active 23904 (96%), one 0 (0%), zero 950 (4%)
c [score-dist-14] max exp 521, different 14 (3%)
c [score-dist-14] median active exp 521, avg 520.8
c [simplification-14] removed 46 variables 0.2% (24854 remain 37%)
c [simplification-14] removed 1126 irredundant clauses 0.9% (125214 remain 45%)
c [simplification-14] maximum reduction of 1% = max (0%, 1%)
c [simplification-14] geometric conflict interval increment 98876 = 197752 / 2
c [simplification-14] new conflict interval 296628
c [simplification-14] penalized conflict interval 296628 = 1 * 296628
c [simplification-14] hard conflict limit 1373556 (soft 1225242 + delta 148314)
c [simplification-14] new conflict limit 1225242 (hard 1373556)
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  532.4   24853   125214    935171   72449   2924 65209   38   115   94  33%    114    8   46   33  137%
c i  532.8   24852   125214    935865   73099   2926 65211   42   131   94  32%    -32   23   61   34  180%
c i  535.7   24851   125214    940104   77177   2932 65211   38   110  107  35%   -128    1   33   34   96%
c -  538.8   24851   125214    947721   43485   2932 65212   24   134   34  18%    -64   25   25   33   76%
c i  542.1   24850   125214    952381   48034   2933 65214   27    99   69  27%     11  -11   31   32   95%
c -  560.7   24850   125214    991382   46880   2964 65224   28    50   35  57%    358  -45   30   31   97%
c i  561.0   24849   125214    991979   47455   2965 65225   30    54   48  55%    364  -40   39   31  127%
c i  561.4   24848   125214    992844   48272   2965 65225   33    79   49  42%     22  -14   50   31  162%
c i  562.1   24847   125214    994354   49677   2971 65233   42   122   51  34%   -167   28   68   32  216%
c i  575.2   24846   125214   1017924   72588   2994 65248   29    84  145  34%    131  -10   27   31   86%
c i  576.9   24845   125214   1020831   75268   3008 65262   46   142  145  32%   -167   47   74   33  227%
c i  583.0   24844   125214   1029930   83837   3036 65294   43   124  197  35%    -72   21   62   34  183%
c i  583.0   24843   125214   1029936   83839   3037 65295   43   123  197  35%    -72   21   62   34  181%
c -  586.3   24843   125214   1033892   44743   3048 65309   48   144   34  34%   -140   40   53   35  150%
c i  586.4   24842   125214   1034121   44965   3049 65310   49   149   44  33%   -137   44   51   35  145%
c i  586.6   24841   125214   1034493   45315   3050 65310   48   151   44  32%   -151   46   44   35  124%
c i  604.2   24840   125214   1069758   79472   3087 65350   41   138  164  30%    307   36   57   34  168%
c i  604.4   24839   125214   1070031   79727   3091 65351   42   141  178  30%    181   39   59   34  174%
c -  608.6   24839   125214   1079561   47953   3100 65355   31   129   51  24%    -79   23   33   33   99%
c i  615.3   24838   125214   1095821   63753   3129 65364   31    98  104  32%    163  -11   36   33  110%
c i  615.8   24837   125214   1096687   64564   3129 65365   36   108  104  33%    -54   -1   63   33  190%
c i  622.2   24836   125214   1110245   77521   3162 65386   26    79  137  33%     -7  -34   22   33   67%
c i  622.6   24835   125214   1110973   78160   3165 65391   31    95  137  32%   -102  -17   56   33  167%
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  627.7   24834   125214   1118819   85245   3179 65437   58   173  151  34%    -79   56   73   37  198%
c i  628.0   24833   125214   1119256   85640   3182 65448   56   172  151  33%   -114   55   51   37  139%
c i  630.0   24832   125214   1123278   89420   3190 65454   48   137  155  35%   -128   19   59   37  160%
c -  631.1   24832   125214   1124670   47266   3191 65457   49   144   48  34%   -151   26   32   37   86%
c i  631.9   24831   125214   1126334   48813   3197 65467   50   162   60  31%   -135   42   55   38  146%
c i  645.8   24830   125214   1155777   77309   3245 65489   47   166  137  28%    252   52   70   35  202%
c i  648.7   24829   125214   1160148   81280   3255 65500   61   194  144  32%   -129   75   63   37  170%
c i  651.6   24828   125214   1164742   85495   3266 65518   58   182  148  32%   -121   58   74   38  192%
c i  654.5   24827   125214   1169002   89524   3270 65530   49   165  162  30%   -117   38   61   39  157%
c i  655.5   24826   125214   1170487   90901   3270 65533   51   166  162  31%   -143   38   47   39  121%
c -  656.5   24826   125214   1171986   48351   3275 65536   48   158   48  30%   -146   30   39   39  101%
c i  671.6   24825   125214   1203615   79178   3298 65547   42   110  147  38%    296    1   61   36  169%
c i  675.6   24824   125214   1210910   86083   3305 65555   51   173  178  29%    -97   61   72   37  192%
c i  677.6   24823   125214   1213974   88913   3316 65567   55   187  183  29%   -151   71   52   38  137%
c i  679.8   24822   125214   1217365   92003   3324 65594   56   187  183  30%   -141   68   55   39  141%
c -  681.0   24822   125214   1219148   50084   3323 65603   49   177   48  27%   -155   57   26   39   67%
c 
c [simplification-15] limit 1225243 conflicts (hard 1373556) hit after 1228903 conflicts
c [quatres-9] found 3700 quaternary clauses 19% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-2] added 1 quaternary resolvents
c [ternres-12] limit 81113060 with penalty 0 = 0 + 0
c [ternres-12] all 24822 free variables schedulable
c [ternres-12] 39 ternary resolvents (0 bin, 39 trn)
c [ternres-12] fully completed ternary resolution
c [card-5] limit 2534783 penalty 4 = 4 + 0
c [card-5] found 5019 at-most-one constraints of average size 3.7
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2534783 for elimination
c [card-5] 5019 out of 5019 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-34] removed 32 variables
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 907 probes remain 4% after last round
c [basicprobe-5-0] 650 units = 650 failed (100%) + 0 lifted (0%)
c [basicprobe-5-0] removed 706 variables, found 9629 hbrs
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 89 transitive binary clauses
c [bca-10] limit of 10000000 steps and 264859 added (scaled 2)
c [bca-10] 27394 out of 48234 literals actually usable 57%
c [bca-10] added 145 blocked clauses in 124292 steps
c [phase-count-15] 119649 negative 99.8% of 119902 except 253 0.2%
c [phase-count-15] 86324 positive 72.0% of 119902 except 33578 28.0%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 3 positive 50%, 3 negative 50%
c [sort-queue-15] sorted 898 enqueued variables after 1228903 conflicts
c [score-dist-15] active 23218 (96%), one 0 (0%), zero 898 (4%)
c [score-dist-15] max exp 522, different 15 (3%)
c [score-dist-15] median active exp 522, avg 521.8
c [simplification-15] removed 706 variables 2.8% (24116 remain 36%)
c [simplification-15] removed 5312 irredundant clauses 4.2% (119902 remain 43%)
c [simplification-15] maximum reduction of 4% = max (3%, 4%)
c [simplification-15] geometric conflict interval increment 59325 = 296628 / 5
c [simplification-15] new conflict interval 355953
c [simplification-15] penalized conflict interval 355953 = 1 * 355953
c [simplification-15] hard conflict limit 1762832 (soft 1584856 + delta 177976)
c [simplification-15] new conflict limit 1584856 (hard 1762832)
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  702.0   24115   119902   1241827   71279   3217 70114   48   135  104  36%    183    9   82   40  207%
c -  714.9   24115   119902   1266096   51529   3242 70119   26   110   35  24%    175  -10   35   37   96%
c i  731.7   24114   119902   1298278   82480   3351 70139   31   129  150  24%    505   18   52   34  151%
c i  732.1   24113   119902   1298854   83024   3353 70141   33   139  152  24%    131   27   52   34  152%
c -  740.4   24113   119902   1312898   51314   3379 70156   51   170   33  30%   -116   48   52   37  140%
c i  758.6   24112   119902   1354414   91393   3433 70178   43   128  122  33%    419   18   55   34  159%
c i  762.2   24111   119902   1360103   96777   3439 70184   49   155  185  31%   -336   42   55   36  152%
c -  763.1   24111   119902   1361231   52693   3440 70185   52   164   47  32%   -374   50   52   36  143%
c -  787.0   24111   119902   1408883   55146   3486 70202   29    39   52  73%    334  -73   27   34   82%
c -  818.9   24111   119902   1455098   55219   3497 70204   30    74   55  41%    683  -23   33   32  104%
c i  827.1   24110   119902   1469975   69561   3518 70216   49   169  117  29%    752   71   74   33  224%
c -  844.4   24110   119902   1503629   53315   3554 70249   55   165   49  33%   -182   48   45   38  117%
c -  871.1   24110   119902   1555323   55495   3617 70283   48   133   50  36%    476   10   60   38  161%
c 
c [simplification-16] limit 1584856 conflicts (hard 1762832) hit after 1594829 conflicts
c [quatres-10] found 4161 quaternary clauses 19% in total
c [quatres-10-1] removed 3 duplicate quaternary clauses
c [quatres-10-2] added 2 single-self-subsuming ternary resolvents
c [quatres-10-2] added 3 quaternary resolvents
c [ternres-13] limit 106741592 with penalty 0 = 0 + 0
c [ternres-13] all 24110 free variables schedulable
c [ternres-13] 26 ternary resolvents (0 bin, 26 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-35] removed 6 variables
c [simpleprobe-6] all 24110 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-36] removed 19 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 19 variables, found 3239 hbrs, 14 units
c [unhide-14] limit 1250000 with penalty 4 = 1 + 3
c [unhide-14-25] 3 units, 0 failed, 1500 tauts, 0 hbrs, 4922091 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 130 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 24088 variables 100%
c [block-5] limit of 50000000 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 302 blocked clauses
c [block-5] 302 < 1/100 * 119722 = 1197 considered unsuccessful
c [cce-6] limit of 66713495 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 42
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 39
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 38
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 35
c [cce-6-1] eliminated 2 clauses out of 212 (1%) of length 33
c [cce-6-1] eliminated 2 clauses out of 9 (22%) of length 32
c [cce-6-1] eliminated 5 clauses out of 12 (42%) of length 31
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 30
c [cce-6-1] eliminated 1 clauses out of 9 (11%) of length 29
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 25
c [cce-6-1] eliminated 1 clauses out of 126 (1%) of length 24
c [cce-6-1] eliminated 31 clauses out of 171 (18%) of length 22
c [cce-6-1] eliminated 4 clauses out of 179 (2%) of length 21
c [cce-6-1] eliminated 5 clauses out of 183 (3%) of length 20
c [cce-6-1] eliminated 6 clauses out of 167 (4%) of length 19
c [cce-6-1] eliminated 10 clauses out of 175 (6%) of length 18
c [cce-6-1] eliminated 12 clauses out of 172 (7%) of length 17
c [cce-6-1] eliminated 8 clauses out of 156 (5%) of length 16
c [cce-6-1] eliminated 9 clauses out of 198 (5%) of length 15
c [cce-6-1] eliminated 10 clauses out of 146 (7%) of length 14
c [cce-6-1] eliminated 15 clauses out of 157 (10%) of length 13
c [cce-6-1] eliminated 4 clauses out of 164 (2%) of length 12
c [cce-6-1] eliminated 4 clauses out of 112 (4%) of length 11
c [cce-6-1] eliminated 3 clauses out of 126 (2%) of length 10
c [cce-6-1] eliminated 11 clauses out of 122 (9%) of length 9
c [cce-6-1] eliminated 8 clauses out of 127 (6%) of length 8
c [cce-6-1] eliminated 8 clauses out of 121 (7%) of length 7
c [cce-6-1] eliminated 12 clauses out of 133 (9%) of length 6
c [cce-6-1] eliminated 6 clauses out of 92 (7%) of length 5
c [cce-6-1] eliminated 47 clauses out of 184 (26%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 234 large clauses in 62567974 steps
c [cce-6-1] allowing another 31283987 steps for small clauses
c [cce-6-1] scheduling 114663 clauses = 113797 binary + 866 ternary
c [cce-6-1] tried to eliminate 1510 small clauses 1%
c [cce-6-1] eliminated 124 binary clauses 0%
c [cce-6-1] eliminated 2 ternary clauses 0%
c [cce-6-1] eliminated 126 small clauses 0%
c [cce-6-1] eliminated 126 small clauses in 66713495 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 360 covered clauses in round 1
c [cce-6] eliminated 360 covered clauses in TOTAL during 1 rounds
c [cce-6] 360 < 1/100 * 119407 = 1194 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 23989 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 329 variables 1% in round 1 in 11490354 steps
c [elim-8-1] backward subsumption/strengthening limit 11490300
c [elim-8-1-1] backward checking 1315 touched variables 5%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 10 clauses in 685230 steps
c [elim-8-1] rescheduled 17 variables 0% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 84539 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 330 = 1% variables out of 23989 scheduled
c [bca-11] limit of 10000000 steps and 262599 added (scaled 2)
c [bca-11] 25756 out of 47320 literals actually usable 54%
c [bca-11] added 113 blocked clauses in 150909 steps
c [phase-count-16] 118484 negative 99.8% of 118736 except 252 0.2%
c [phase-count-16] 85130 positive 71.7% of 118736 except 33606 28.3%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-16] sorted 677 enqueued variables after 1594829 conflicts
c [score-dist-16] active 22982 (97%), one 0 (0%), zero 677 (3%)
c [score-dist-16] max exp 522, different 15 (3%)
c [score-dist-16] median active exp 522, avg 521.8
c [simplification-16] removed 451 variables 1.9% (23659 remain 35%)
c [simplification-16] removed 1166 irredundant clauses 1.0% (118736 remain 43%)
c [simplification-16] maximum reduction of 2% = max (2%, 1%)
c [simplification-16] geometric conflict interval increment 118651 = 355953 / 3
c [simplification-16] new conflict interval 474604
c [simplification-16] penalized conflict interval 474604 = 1 * 474604
c [simplification-16] hard conflict limit 2306735 (soft 2069433 + delta 237302)
c [simplification-16] new conflict limit 2069433 (hard 2306735)
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  911.5   23658   118736   1606017  101847   3668 71954   54   179  214  30%    771   60   50   38  130%
c -  913.7   23658   118736   1608911   56365   3668 71954   41   124   56  33%  -1156    4   42   38  110%
c -  941.5   23658   118736   1660990   57182   3731 71996   22    44   56  50%    -19  -74   20   39   51%
c -  970.6   23658   118736   1712145   59829   3748 72005   38   171   60  22%    546   68   74   34  220%
c -  996.5   23658   118736   1762531   59079   3803 72028   31    79   57  39%    803  -43   52   34  154%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 4 basic ate = 4 trn 100% + 0 lrg 0% in 2 updates
c bcas: 11 count, 49368 added (2949 skipped), 1374811 steps
c bkwd: tried 206689 clauses, 413290 lits, 2.00 lits/clause
c bkwd: checked 14348170 occs, 69.42 occs/clause, 34.72 occs/lit
c bkwd: subsumed 0 binary, 8 ternary, 27 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1200 large (0% self)
c blkd: 5 bces, 655 removed, 2282942 resolutions, 6060604 steps
c blkd: 12345 blocking literals 6%, 274 pure
c bump: 1758225 bumped seen, 1332695840 lits 758.0 on average
c card: 5 count, 0 units, 0 am1, 22710354 steps
c card: 33 rescheduled, 0 eliminated, 0 resolved, 42642 subsumed
c card: 27389 at-most-one constraints found, average size 3.33
c card: 27389 at-most-one constraints used 100%, average size 3.33
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 6 cces, 5795 eliminated, 5320 ate 92%, 475 abce 8%
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: 1633472 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 94 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 36 decompositions, 1001 equivalent 1%
c deco: 37444 decision-only clauses 2%, 77% reduction
c decs: 9314866 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 38860 eliminated 41%, 27967 pure 72%
c elms: 15 rounds, 1.9 rounds/bve
c elms: 9316 small 24%, 1303 large 3%
c elms: 62510 tried small, 9316 succeeded 15%, 53194 failed 85%
c elms: 488 subsumed, 35722 strengthened, 8970 blocked
c elms: 2773450 copies, 2961771 resolutions, 764282 ipos
c elms: 4603326 subchks, 4514796 strchks
c gaus: 4 extractions, 15 extracted, 2.4 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 9346680 steps, 4673340 extr 50%, 67 elim 0%
c glue: 32.8 orig avg, 32.8 real avg, 5.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 37745 = 12141 simple 32% + 18758 trn 50% + 6846 lrg 18%, 662 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1758225 clauses, 561.0 length
c lrnd: 986386404 lits = 1270785728 orig - 284399324 removed 22%
c lrnd: 480943 uips 27%, 1126188 flips 64%
c mins: 1656891 mins 97%, 1386 bin 0%, 4880 size 0%
c mins: 1151069350 poisoned searches, 542836256 hits, 47% hit rate
c mins: 1511103818 used twice searches, 19158872 hits, 1% hit rate
c move: moved 3577, 3556 bin 99%, 21 trn 1%
c otfs: 10931 driving 14%, 65047 restarting 86%
c otfs: str 75978, 75811 red 100%, 167 irr 0%
c otfs: str 75978, 0 bin 0%, 322 trn 0%, 75656 lrg 100%
c otfs: sub 30, 30 red 100%, 0 irr 0%
c otfs: sub 30, 0 bin 0%, 0 trn 0%, 30 lrg 100%
c phas: 16 computed, 38766 set, 22 pos (0%), 38744 neg (100%)
c prbs: 5 basic, 28376 probed, 1198 failed, 0 lifted
c prbs: 6 simple, 351585 probed, 342 failed, 444 eqs
c prbs: 5 treelook, 427 probed, 112 failed, 0 lifted
c prom: 421050 locked 11% out of 3767283 tried
c prps: 1185935600 props, 116 props/dec
c prps: 91% srch, 9% simp, 0% lkhd
c quat: 10 count, 30 quat, 13 self1, 0 self2, 12 dup
c queu: 16 sorted, 9314866 next (3121 steps 0.00)
c queu: 1332859580 enq (9215732315 steps 6.91), 1332695840 deq 100%
c redc: 22230 clauses 62%, 35663 tried 2%, 31 sat 0%
c redc: 138873 lits 27%, 506577 tried 0%, 31 sat 0%
c redc: 2675 times jump level reduced, 16.9 levels on average
c reds: 40 count, 44221.2 conflicts per reduce
c reds: 0 memlim 0%, 40 arith 100%
c reds: 1390242 collected 89%, 177728 retired 11%
c rmbd: 4467 removed, 1110 red 25%
c rsts: 28000 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: 16 count, 14 confs 88%, 0 vars 0%
c simp: 1 its 6%, 1 bin 6%, 0 trns 0%
c subl: 1758225 count (2000311 tried 1.1), 59286 sub out of 1751445 (3.4%)
c swps: 9 count, 9 rounds, 708 queries (78.7/round)
c swps: 679 sat calls, 1 unsat (0.5% success rate)
c swps: 20468 decisions 30.1, 310 conflicts 0.5
c swps; 2030.4 avg class size, 631.3 avg environment size
c swps: 0 failed, 54 impls, 27 equivs
c swp0: 234 type 0 queries, 32 unsat (13.7%), 225 sat (96.2%)
c swp1: 474 type 1 queries, 146 unsat (30.8%), 456 sat (96.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: 22146668 calls to obtain time
c tops: 31937 fixed 33%, 168 its, 10528.85 confs/it
c trds: 14 transitive reductions, 716 removed, 6 failed
c trds: 6409 nodes, 23362 edges, 25672512 steps
c trim: 3070503 words, 11.7 MB
c trnr: 13 count, 0 bin, 603 trn, 15029677 steps
c unhd: 14 count, 25 rounds, 33910946 steps
c unhd: 12 non-trivial sccs of average size 2.0
c unhd: 72 units, 72 bin, 0 trn, 0 lrg
c unhd: 59 failed, 57 stamp, 0 lits, 1 bin, 0 trn, 0 lrg
c unhd: 29744 tauts, 614 bin 2%, 89 trn 0%, 77 lrg 0%
c unhd: 29744 tauts, 28964 stamp 97%, 8110 red 27%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 22574579 str, 72 bin 0%, 268 trn 0%, 22574239 lrg 100%, 22566710 red 100%
c vars: 23658 remaining 25% and 71798 removed 75% out of 95456
c vars: 31937 fixed 33%, 38860 eliminated 41%, 1001 equivalent 1%
c vsts: 12439575176 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 11.0 search visits per propagation, 6750.1 per conflict
c wchs: 3236475846 pushed, 116155889 enlarged, 146 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1751475       1390242        177728      70193174      15747558       1119945
c 
c  0 0         29644   2      6184   0         0   0  17321664  25   2625072  17    122497  11     1.0
c  1 5         16945   1      9209   1      3688   2   4607522   7    841200   5     42663   4     0.7
c  2 6         92295   5     60002   4     15206   9  15012968  21<  3106279  20    182613  16     4.2
c  3 9        242428  14    190211  14     23472  13  16408158  23   4057138  26<   298564  27<   13.6
c  4 14       367091  21    318716  23     26374  15   7896639  11   2250829  14    194922  17    59.8
c  5 21       376924  22<   328266  24<    26881  15   3846088   5   1236291   8    117345  10    68.3
c  6 30       292192  17    248341  18     23629  13<  2171299   3    761541   5     73919   7    70.7
c  7 41       153673   9    124340   9     17632  10   1203416   2    409090   3     39611   4    61.9
c  8 54        72812   4     55771   4     12419   7    729861   1    202184   1     20508   2    23.8
c  9 69        38005   2     26719   2      8578   5    371892   1    101376   1     11001   1    10.0
c 10 86        23897   1     14558   1      6338   4    410896   1     89387   1      9392   1     4.0
c 11 126       22178   1      5016   0      6593   4    158952   0     46008   0      4800   0     1.1
c 12 230       21888   1      2712   0      6465   4     51853   0     19965   0      1969   0     1.5
c 13 534        1496   0       196   0       448   0      1944   0      1173   0       129   0     0.5
c 14 1526          7   0         1   0         5   0        22   0        25   0        12   0     0.1
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                  5.0           5.0           5.7           2.4           2.9           3.4
c std                  2.1           1.8           2.7           2.1           2.1           2.1
c 
c  359.221  36% bump
c   36.455   4% unhide
c   17.800   2% probe
c    6.690   1% cce
c    6.525   1% decide
c 
c   12.039 < 1% rest (below)
c 
c    4.136   0% elim
c    3.207   0% sweep
c    1.520   0% block
c    1.424   0% bca
c    0.652   0% gauss
c    0.637   0% transred
c    0.248   0% card
c    0.118   0% quatres
c    0.095   0% ternres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.035   0% preprocessing     1%
c   80.235   8% inprocessing     99%
c ==================================
c   81.270   8% simplifying
c  918.609  92% search
c ==================================
c  999.881 100% all
c 
c       1768846 conflicts,        1769.1 confs/sec
c          4030 ternaries,         438.9 confs/ternary
c          2539 binaries,          696.7 confs/binary
c           168 iterations,      10528.8 confs/iteration
c 
c            40 reductions,          0.0 redus/sec,  44221.2 confs/reduction
c         28000 restarts,           28.0 rests/sec,     63.2 confs/restart
c       9314866 decisions,        9316.0 decis/sec,      5.3 decis/conflict
c    1185935600 propagations,  1186077.2 props/sec,    127.3 props/decision
c 
c 999.9 seconds, 394.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
