c launch: /data/cnf/sc2014/app/openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_1.025-NOTKNOWN.cnf.bz2
c host: atom13
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_1.025-NOTKNOWN.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_1.025-NOTKNOWN.cnf.bz2
c no embedded options
c found 'p cnf 95456 477186' header
c read 95456 variables, 477186 clauses, 1137161 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   270800         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 12589 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] 12589 out of 12589 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 902 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 902 variables, found 1272 hbrs, 61 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 13 failed, 5444 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 65052 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 36570 variables 56% in round 1 in 6085626 steps
c [elim-1-1] backward subsumption/strengthening limit 6085600
c [elim-1-1-1] backward checking 27948 touched variables 43%
c [elim-1-1-1] incomplete backward checking 27556 remain 99%
c [elim-1-1] subsumed 15 and strengthened 1203 clauses in 6085716 steps
c [elim-1-1] rescheduled 1060 variables 2% by backward subsumption
c [elim-1-2] eliminated 24 variables 0% in round 2 in 162901 steps
c [elim-1-2] backward subsumption/strengthening limit 162900
c [elim-1-2-1] backward checking 27575 touched variables 42%
c [elim-1-2-1] incomplete backward checking 27575 remain 100%
c [elim-1-2] subsumed 0 and strengthened 18 clauses in 162990 steps
c [elim-1-2] rescheduled 30 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 0 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 36594 = 56% variables out of 65052 scheduled
c [phase-count-1] 170571 negative 99.9% of 170682 except 111 0.1%
c [phase-count-1] 112074 positive 65.7% of 170682 except 58608 34.3%
c [phase-count-1] less non-negative clauses 111 than limit 17000 (10.0%)
c [phase-count-1] non-pos/non-neg = 58608/111 = 528.00 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 28458 negative 100%
c [sort-queue-1] sorted 28458 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 28458 (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 38307 variables 57.4% (28458 remain 42%)
c [simplification-1] removed 100118 irredundant clauses 37.0% (170682 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   28457   170682       113      88      1  1121    0     2   10  21%      0    2    7    0 21523%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 41 variables
c [simpleprobe-2] all 28417 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 29 variables
c [simpleprobe-2] 60 variables remain 0% (28328 retained 100%)
c [simpleprobe-2] removed 29 variables, found 1628 hbrs, 17 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 47506 literals 84%
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 480847 steps
c [treelook-1] 47502 literals remain 84%
c [treelook-1] 28211 variables remain to probed next time 99%
c [treelook-1] removed 0 variables, found 285 hbrs
c [basicprobe-1] limit 1360504 based on 170063 irredundant clauses
c [basicprobe-1-0] 17020 probes remain 60% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1 variables, found 0 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 15 units, 2 failed, 196 tauts, 0 hbrs, 12165 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 28361 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 92 blocked clauses
c [block-1] 92 < 1/100 * 170050 = 1700 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 354 clauses out of 470 (75%) of length 63
c [cce-1-1] eliminated 162 clauses out of 411 (39%) of length 62
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 516 large clauses in 30000000 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 165274 clauses = 164307 binary + 967 ternary
c [cce-1-1] tried to eliminate 500 small clauses 0%
c [cce-1-1] eliminated 185 binary clauses 0%
c [cce-1-1] eliminated 185 small clauses 0%
c [cce-1-1] eliminated 185 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 701 covered clauses in round 1
c [cce-1] eliminated 701 covered clauses in TOTAL during 1 rounds
c [cce-1] 701 < 1/100 * 169724 = 1697 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 28358 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 7 not tried 0% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 207 = 1% variables out of 28358 scheduled
c [elim-2] 207 < 1/100 * 28358 = 283 considered unsuccessful
c [bca-1] limit of 10000000 steps and 337822 added (scaled 2)
c [bca-1] 42100 out of 56304 literals actually usable 75%
c [bca-1] added 4594 blocked clauses in 107501 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2469 pos 8.8% + 25682 neg 91.2% = 28151 sched 100.0% ret 0
c [sweep-1-1] 1007309 steps 18 queries 2754.89 avg class size
c [sweep-1-1] 288 decisions 16 SAT calls 296.81 avg env size
c [sweep-1-1] 27993 variables remain 99% (158 retained 1%)
c [decomp-6] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 17 queries)
c [phase-count-2] 168547 negative 99.9% of 168661 except 114 0.1%
c [phase-count-2] 110508 positive 65.5% of 168661 except 58153 34.5%
c [phase-count-2] less non-negative clauses 114 than limit 16800 (10.0%)
c [phase-count-2] non-pos/non-neg = 58153/114 = 510.11 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 5005 negative 100%
c [sort-queue-2] sorted 9989 enqueued variables after 1000 conflicts
c [score-dist-2] active 18161 (65%), one 0 (0%), zero 9989 (35%)
c [score-dist-2] max exp 511, different 9 (2%)
c [score-dist-2] median active exp 511, avg 509.9
c [simplification-2] removed 267 variables 0.9% (28150 remain 42%)
c [simplification-2] removed 2021 irredundant clauses 1.2% (168661 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 21000 (soft 11000 + delta 10000)
c [simplification-2] new conflict limit 11000 (hard 21000)
c 
c [simplification-3] limit of 119 binary hit after 119 binaries
c [quatres-1] found 262 quaternary clauses 7% in total
c [quatres-1-2] added 1 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 28150 free variables schedulable
c [ternres-1] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3558 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] 3558 out of 3558 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 130534 with penalty 0 = 0 + 0
c [unhide-3-3] 4 units, 2 failed, 3091 tauts, 0 hbrs, 57005 literals
c [transred-1] limit 652674 with penalty 0 = 0 + 0
c [transred-1] removed 13 transitive binary clauses
c [bca-2] limit of 10000000 steps and 333743 added (scaled 2)
c [bca-2] 39511 out of 56278 literals actually usable 70%
c [bca-2] added 54 blocked clauses in 105479 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 3892 pos 13.9% + 24088 neg 86.1% = 27980 sched 99.4% ret 158
c [sweep-2-1] 1001386 steps 27 queries 3295.07 avg class size
c [sweep-2-1] 625 decisions 26 SAT calls 301.35 avg env size
c [sweep-2-1] 27539 variables remain 98% (599 retained 2%)
c [decomp-8] removed 1 variables
c [sweep-2-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 1 vars in TOTAL (1 rounds, 26 queries)
c [phase-count-3] 165358 negative 99.9% of 165471 except 113 0.1%
c [phase-count-3] 110100 positive 66.5% of 165471 except 55371 33.5%
c [phase-count-3] less non-negative clauses 113 than limit 16500 (10.0%)
c [phase-count-3] non-pos/non-neg = 55371/113 = 490.01 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 2640 negative 100%
c [sort-queue-3] sorted 8346 enqueued variables after 6991 conflicts
c [score-dist-3] active 19791 (70%), one 0 (0%), zero 8346 (30%)
c [score-dist-3] max exp 514, different 11 (2%)
c [score-dist-3] median active exp 514, avg 512.3
c [simplification-3] removed 13 variables 0.0% (28137 remain 42%)
c [simplification-3] removed 3190 irredundant clauses 1.9% (165471 remain 61%)
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 11000 (hard 21000)
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   28136   165471     10481    9506    190  8086   32   196   22  16%    136  175   39    5  844%
c 
c [simplification-4] limit 11000 conflicts (hard 21000) hit after 11000 conflicts
c [quatres-2] found 304 quaternary clauses 7% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 28136 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-9] removed 1 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 25290 literals 45%
c [treelook-2] scheduling used 150164 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 157228 steps
c [treelook-2] 25283 literals remain 45%
c [treelook-2] 22882 variables remain to probed next time 81%
c [treelook-2] removed 2 variables, found 193 hbrs
c [unhide-4] limit 209519 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 8 failed, 99 tauts, 0 hbrs, 66906 literals
c [transred-2] limit 1047597 with penalty 0 = 0 + 0
c [transred-2] removed 13 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 28124 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 13 blocked clauses
c [block-2] 13 < 1/100 * 165437 = 1654 considered unsuccessful
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 51 clauses out of 152 (34%) of length 61
c [cce-2-1] eliminated 19 clauses out of 123 (15%) of length 60
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 59
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 57
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 56
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 52
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 49
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 42
c [cce-2-1] eliminated 20 clauses out of 358 (6%) of length 33
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 98 large clauses in 15000004 steps
c [cce-2-1] allowing another 7500002 steps for small clauses
c [cce-2-1] scheduling 161069 clauses = 160524 binary + 545 ternary
c [cce-2-1] tried to eliminate 214 small clauses 0%
c [cce-2-1] eliminated 22 binary clauses 0%
c [cce-2-1] eliminated 22 small clauses 0%
c [cce-2-1] eliminated 22 small clauses in 15000004 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 120 covered clauses in round 1
c [cce-2] eliminated 120 covered clauses in TOTAL during 1 rounds
c [cce-2] 120 < 1/100 * 165344 = 1653 considered unsuccessful
c [elim-3] 7 variables 0% will be scheduled this time
c [elim-3] scheduled 7 variables 0%
c [elim-3] limit of 10475971 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 305627 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 7 scheduled
c [bca-3] limit of 10000000 steps and 333272 added (scaled 2)
c [bca-3] 35732 out of 56246 literals actually usable 64%
c [bca-3] added 22 blocked clauses in 87953 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 4046 pos 14.7% + 23477 neg 85.3% = 27523 sched 97.9% ret 599
c [sweep-3-1] 1010284 steps 19 queries 3702.37 avg class size
c [sweep-3-1] 1018 decisions 18 SAT calls 700.06 avg env size
c [sweep-3-1] 27186 variables remain 97% (936 retained 3%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 18 queries)
c [phase-count-4] 165111 negative 99.9% of 165224 except 113 0.1%
c [phase-count-4] 109911 positive 66.5% of 165224 except 55313 33.5%
c [phase-count-4] less non-negative clauses 113 than limit 16500 (10.0%)
c [phase-count-4] non-pos/non-neg = 55313/113 = 489.50 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1625 negative 100%
c [sort-queue-4] sorted 6168 enqueued variables after 11000 conflicts
c [score-dist-4] active 21954 (78%), one 0 (0%), zero 6168 (22%)
c [score-dist-4] max exp 515, different 12 (2%)
c [score-dist-4] median active exp 515, avg 514.5
c [simplification-4] removed 14 variables 0.0% (28122 remain 42%)
c [simplification-4] removed 247 irredundant clauses 0.1% (165224 remain 61%)
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 56000 (soft 41000 + delta 15000)
c [simplification-4] new conflict limit 41000 (hard 56000)
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.0   28121   165224     14159   12880    238  8242   32   198   28  16%     33  168   33    6  543%
c i   11.6   28120   165224     15344   13929    247  8270   33   203   28  16%      9  170   34    7  517%
c i   12.6   28119   165224     17342   15763    274  8306   33   206   30  16%      8  167   38    7  512%
c i   13.8   28118   165224     19492   17740    307  8348   33   204   37  16%      9  161   39    8  481%
c i   14.6   28117   165224     20949   19081    334  8372   33   205   41  16%      3  158   22    9  253%
c i   14.6   28113   165224     20950   19081    334  8372   33   205   41  16%      3  158   22    9  252%
c i   16.7   28106   165224     24612   22453    377  8425   32   193   45  17%     29  138   33   10  327%
c i   17.1   28105   165224     25245   23039    384  8431   34   195   45  17%     11  139   39   10  376%
c i   17.2   27962   165224     25434   23212    388  8432   34   197   45  17%      7  140   43   10  416%
c i   18.8   27961   165224     28143   25748    411  8459   35   198   50  18%     15  135   28   11  248%
c 
c [simplification-5] limit of 12 iterations hit after 12 iterations
c [quatres-3] found 507 quaternary clauses 10% in total
c [quatres-3-2] added 4 single-self-subsuming ternary resolvents
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 6 xors of average arity 2.3
c [gauss-2] connected 14 occurrences of 7 variables (average 2.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 2 variables
c [basicprobe-2] limit 13692737 penalty 0 = 0 + 0
c [basicprobe-2-0] 16570 probes remain 59% after last round
c [basicprobe-2-0] 21 units = 21 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 21 variables, found 1401 hbrs
c [unhide-5] limit 273854 with penalty 1 = 0 + 1
c [unhide-5-5] 0 units, 0 failed, 2111 tauts, 0 hbrs, 395228 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 14 transitive binary clauses
c [bca-4] limit of 10000000 steps and 325399 added (scaled 2)
c [bca-4] 30448 out of 55878 literals actually usable 54%
c [bca-4] added 0 blocked clauses in 86197 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 4426 pos 16.4% + 22576 neg 83.6% = 27002 sched 96.6% ret 936
c [sweep-4-1] 1016780 steps 17 queries 2117.29 avg class size
c [sweep-4-1] 632 decisions 14 SAT calls 516.29 avg env size
c [sweep-4-1] 26856 variables remain 96% (1082 retained 4%)
c [decomp-13] removed 2 variables
c [sweep-4-1] removed 2 vars (0 failed, 2 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 2 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-5] 161169 negative 99.9% of 161282 except 113 0.1%
c [phase-count-5] 108626 positive 67.4% of 161282 except 52656 32.6%
c [phase-count-5] less non-negative clauses 113 than limit 16100 (10.0%)
c [phase-count-5] non-pos/non-neg = 52656/113 = 465.98 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 624 negative 100%
c [sort-queue-5] sorted 3517 enqueued variables after 28143 conflicts
c [score-dist-5] active 24419 (87%), one 0 (0%), zero 3517 (13%)
c [score-dist-5] max exp 516, different 12 (2%)
c [score-dist-5] median active exp 516, avg 515.9
c [simplification-5] removed 25 variables 0.1% (27936 remain 41%)
c [simplification-5] removed 3942 irredundant clauses 2.4% (161282 remain 60%)
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 41010 (hard 56000)
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   23.8   27935   161282     31767   28984    391  9794   38   199   63  19%     27  129   37   13  286%
c i   25.7   27934   161282     34562   31642    408  9814   39   202   63  19%     16  127   41   14  295%
c i   26.7   27933   161282     36134   33130    427  9824   40   204   68  19%      4  125   46   15  316%
c 
c [simplification-6] limit 41010 conflicts (hard 56000) hit after 41010 conflicts
c [quatres-4] found 566 quaternary clauses 10% in total
c [ternres-3] limit 2040955 with penalty 1 = 1 + 0
c [ternres-3] all 27933 free variables schedulable
c [ternres-3] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-3] fully completed ternary resolution
c [card-3] limit 510238 penalty 2 = 2 + 0
c [card-3] found 1580 at-most-one constraints of average size 3.6
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 510238 for elimination
c [card-3] 1580 out of 1580 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-14] removed 5 variables
c [simpleprobe-3] 59 schedulable variables 0%
c [simpleprobe-3] limit 16327647 penalty 0 = 0 + 0
c [decomp-15] removed 87 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 87 variables, found 1899 hbrs, 63 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 17 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 12245730 penalty 0 = 0 + 0
c [sweep-5-1] 4507 pos 16.8% + 22258 neg 83.2% = 26765 sched 96.1% ret 1079
c [sweep-5-1] 12270228 steps 263 queries 1087.16 avg class size
c [sweep-5-1] 10070 decisions 242 SAT calls 866.00 avg env size
c [sweep-5-1] 10383 variables remain 37% (17461 retained 63%)
c [decomp-16] removed 18 variables
c [sweep-5-1] removed 18 vars (0 failed, 20 eqs, 35 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 18 vars in TOTAL (1 rounds, 262 queries)
c [phase-count-6] 160416 negative 99.9% of 160529 except 113 0.1%
c [phase-count-6] 108050 positive 67.3% of 160529 except 52479 32.7%
c [phase-count-6] less non-negative clauses 113 than limit 16000 (10.0%)
c [phase-count-6] non-pos/non-neg = 52479/113 = 464.42 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 378 negative 100%
c [sort-queue-6] sorted 3067 enqueued variables after 41010 conflicts
c [score-dist-6] active 24759 (89%), one 0 (0%), zero 3067 (11%)
c [score-dist-6] max exp 517, different 12 (2%)
c [score-dist-6] median active exp 517, avg 516.8
c [simplification-6] removed 107 variables 0.4% (27826 remain 41%)
c [simplification-6] removed 753 irredundant clauses 0.5% (160529 remain 59%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 30000
c [simplification-6] new conflict interval 60000
c [simplification-6] penalized conflict interval 60000 = 1 * 60000
c [simplification-6] hard conflict limit 131010 (soft 101010 + delta 30000)
c [simplification-6] new conflict limit 101010 (hard 131010)
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 -   43.0   27826   160529     57450   14428    563 12106   50   209   24  24%    261   95   34   23  147%
c i   43.6   27825   160529     58501   15389    580 12122   47   200   30  24%    274   85   34   23  145%
c i   43.9   27824   160529     59165   15988    582 12124   48   204   31  24%    115   88   53   24  225%
c i   59.9   27763   160529     87879   42829    728 12298   35   162  112  22%    311   19   30   29  103%
c i   61.0   27762   160529     89746   44566    734 12304   37   171  115  22%    -38   28   34   30  115%
c -   65.8   27762   160529    100714   21923    784 12341   32   126   27  25%     38  -21   38   30  127%
c i   66.4   27761   160529    101838   22969    791 12349   32   137   34  24%     55   -9   30   30   98%
c i   72.5   27760   160529    112210   32703    817 12388   35   140   79  25%     33   -6   43   31  139%
c i   74.1   27755   160529    116833   37042    829 12393   30   123   97  24%    -51  -22   27   31   86%
c i   74.9   27754   160529    118656   38729    830 12396   31   131   97  23%    -82  -14   32   31  104%
c 
c [simplification-7] limit 101010 conflicts (hard 131010) hit after 128763 conflicts
c [ternres-4] limit 10115585 with penalty 0 = 0 + 0
c [ternres-4] all 27754 free variables schedulable
c [ternres-4] 34 ternary resolvents (0 bin, 34 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 72 variables
c [treelook-3] limit 1011558 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 55441 literals 100%
c [treelook-3] scheduling used 562339 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1011558 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 1033327 steps
c [treelook-3] 55396 literals remain 100%
c [treelook-3] 22491 variables remain to probed next time 81%
c [treelook-3] removed 12 variables, found 657 hbrs
c [unhide-6] limit 126444 with penalty 4 = 1 + 3
c [unhide-6-6] 6 units, 40 failed, 252 tauts, 0 hbrs, 5002574 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 22 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 27727 variables 100%
c [block-3] limit of 25288963 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 66 blocked clauses
c [block-3] 66 < 1/100 * 159774 = 1597 considered unsuccessful
c [cce-3] limit of 12644481 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 85 clauses out of 85 (100%) of length 61
c [cce-3-1] eliminated 97 clauses out of 97 (100%) of length 60
c [cce-3-1] eliminated 10 clauses out of 10 (100%) of length 59
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 58
c [cce-3-1] eliminated 5 clauses out of 5 (100%) of length 56
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 55
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 54
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 52
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 37
c [cce-3-1] eliminated 24 clauses out of 322 (7%) of length 33
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 234 large clauses in 12644506 steps
c [cce-3-1] allowing another 6322253 steps for small clauses
c [cce-3-1] scheduling 155502 clauses = 154983 binary + 519 ternary
c [cce-3-1] tried to eliminate 250 small clauses 0%
c [cce-3-1] eliminated 104 binary clauses 0%
c [cce-3-1] eliminated 104 small clauses 0%
c [cce-3-1] eliminated 104 small clauses in 12644482 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 338 covered clauses in round 1
c [cce-3] eliminated 338 covered clauses in TOTAL during 1 rounds
c [cce-3] 338 < 1/100 * 159569 = 1595 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 27684 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1011558525 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 169 variables 1% in round 1 in 17106101 steps
c [elim-4-1] backward subsumption/strengthening limit 17106100
c [elim-4-1-1] backward checking 945 touched variables 3%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 1 clauses in 302488 steps
c [elim-4-1] rescheduled 5 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 20661 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 172 = 1% variables out of 27684 scheduled
c [elim-4] 172 < 1/100 * 27684 = 276 considered unsuccessful
c [bca-5] limit of 10000000 steps and 319807 added (scaled 2)
c [bca-5] 29788 out of 55026 literals actually usable 54%
c [bca-5] added 112 blocked clauses in 107180 steps
c [sweep-6] limit 3034675 penalty 0 = 0 + 0
c [sweep-6-1] 4046 pos 39.9% + 6102 neg 60.1% = 10148 sched 36.9% ret 17364
c [sweep-6-1] 3043307 steps 65 queries 1938.11 avg class size
c [sweep-6-1] 2088 decisions 58 SAT calls 1064.60 avg env size
c [sweep-6-1] 9784 variables remain 36% (17727 retained 64%)
c [decomp-19] removed 7 variables
c [sweep-6-1] removed 7 vars (0 failed, 5 eqs, 10 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 7 vars in TOTAL (1 rounds, 64 queries)
c [phase-count-7] 158363 negative 99.9% of 158476 except 113 0.1%
c [phase-count-7] 106846 positive 67.4% of 158476 except 51630 32.6%
c [phase-count-7] less non-negative clauses 113 than limit 15800 (10.0%)
c [phase-count-7] non-pos/non-neg = 51630/113 = 456.90 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 196 negative 100%
c [sort-queue-7] sorted 2241 enqueued variables after 128763 conflicts
c [score-dist-7] active 25264 (92%), one 0 (0%), zero 2241 (8%)
c [score-dist-7] max exp 518, different 11 (2%)
c [score-dist-7] median active exp 518, avg 517.9
c [simplification-7] removed 249 variables 0.9% (27505 remain 41%)
c [simplification-7] removed 2053 irredundant clauses 1.3% (158476 remain 59%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 30000 = 60000 / 2
c [simplification-7] new conflict interval 90000
c [simplification-7] penalized conflict interval 90000 = 1 * 90000
c [simplification-7] hard conflict limit 263763 (soft 218763 + delta 45000)
c [simplification-7] new conflict limit 218763 (hard 263763)
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   92.1   27504   158476    134740   52627    893 12587   25    95  141  27%    126  -44   35   30  116%
c -   95.2   27504   158476    138566   26224    909 12613   39   145   29  27%    -58    8   50   31  158%
c i   96.8   27503   158476    141442   28919    917 12622   39   144   44  27%    -17    7   37   32  118%
c i  103.9   27502   158476    154480   41314    948 12645   31   124   80  25%     83  -15   27   31   87%
c i  108.6   27501   158476    171325   57211    977 12656   29   136  115  21%    137   -1   26   30   88%
c -  109.0   27501   158476    171732   28207    977 12656   29   138   29  21%     56    1   35   30  116%
c i  112.6   27500   158476    182451   38413    996 12668   38   188   54  20%     50   44   51   30  170%
c i  113.9   27499   158476    185584   41388   1009 12676   37   161   55  23%    -65   16   36   31  119%
c i  116.8   27498   158476    190841   46297   1018 12683   44   201   68  22%    -34   53   67   32  209%
c -  120.9   27498   158476    204250   28219   1038 12711   30    74   29  40%     93  -71   28   31   89%
c i  130.7   27497   158476    235303   57573   1109 12757   34    96   85  35%    444  -20   41   31  134%
c -  132.5   27497   158476    238286   29961   1114 12761   34   105   29  33%   -166  -11   30   31   99%
c i  138.0   27496   158476    250871   41949   1136 12781   27   100   72  27%     11  -13   24   30   79%
c i  142.8   27495   158476    262967   53184   1173 12831   38   146  100  26%    -24   33   31   31  100%
c 
c [simplification-8] limit 218763 conflicts (hard 263763) hit after 263766 conflicts
c [quatres-5] found 1330 quaternary clauses 16% in total
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [quatres-5-2] added 1 quaternary resolvents
c [ternres-5] limit 17006872 with penalty 0 = 0 + 0
c [ternres-5] all 27495 free variables schedulable
c [ternres-5] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-3] limit 850343 penalty 2 = 2 + 0
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 85034363 penalty 0 = 0 + 0
c [basicprobe-3-0] 14348 probes remain 53% after last round
c [basicprobe-3-0] 197 units = 197 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 474 variables, found 1717 hbrs
c [bate-1] eliminated 1 asymmetric tautologies during probing
c [unhide-7] limit 850343 with penalty 2 = 0 + 2
c [unhide-7-7] 0 units, 1 failed, 1753 tauts, 0 hbrs, 2141484 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 28 transitive binary clauses
c [bca-6] limit of 10000000 steps and 307801 added (scaled 2)
c [bca-6] 29907 out of 54042 literals actually usable 55%
c [bca-6] added 238 blocked clauses in 113405 steps
c [sweep-7] limit 5102061 penalty 0 = 0 + 0
c [sweep-7-1] 3995 pos 41.9% + 5529 neg 58.1% = 9524 sched 35.2% ret 17496
c [sweep-7-1] 5123434 steps 154 queries 1906.03 avg class size
c [sweep-7-1] 3854 decisions 146 SAT calls 435.42 avg env size
c [sweep-7-1] 8837 variables remain 33% (18168 retained 67%)
c [decomp-21] removed 20 variables
c [sweep-7-1] removed 20 vars (0 failed, 8 eqs, 9 impls)
c [sweep-7] 20 < 1/1000 * 27020 = 27 considered unsuccessful
c [sweep-7] removed 20 vars in TOTAL (1 rounds, 153 queries)
c [phase-count-8] 152214 negative 99.9% of 152329 except 115 0.1%
c [phase-count-8] 104044 positive 68.3% of 152329 except 48285 31.7%
c [phase-count-8] less non-negative clauses 115 than limit 15200 (10.0%)
c [phase-count-8] non-pos/non-neg = 48285/115 = 419.87 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 190 negative 100%
c [sort-queue-8] sorted 2163 enqueued variables after 263766 conflicts
c [score-dist-8] active 24837 (92%), one 0 (0%), zero 2163 (8%)
c [score-dist-8] max exp 519, different 12 (2%)
c [score-dist-8] median active exp 519, avg 518.8
c [simplification-8] removed 495 variables 1.8% (27000 remain 40%)
c [simplification-8] removed 6147 irredundant clauses 3.9% (152329 remain 56%)
c [simplification-8] maximum reduction of 4% = max (2%, 4%)
c [simplification-8] geometric conflict interval increment 18000 = 90000 / 5
c [simplification-8] new conflict interval 108000
c [simplification-8] penalized conflict interval 108000 = 1 * 108000
c [simplification-8] hard conflict limit 425766 (soft 371766 + delta 54000)
c [simplification-8] new conflict limit 371766 (hard 425766)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  150.0   26999   152329    266350   56255   1081 13681   36   114   95  31%   -147   -0   52   31  169%
c i  150.8   26998   152329    267639   57455   1082 13684   40   127  101  32%   -166   13   56   31  178%
c i  150.9   26997   152329    267754   57562   1082 13685   40   129  101  31%   -168   14   51   31  161%
c -  153.6   26997   152329    272158   29671   1086 13691   35   127   28  28%   -123   11   37   32  116%
c i  154.1   26996   152329    273522   30951   1086 13698   39   136   36  28%   -100   21   49   32  153%
c i  154.3   26995   152329    273918   31323   1088 13699   39   137   37  28%   -122   21   44   32  139%
c -  167.7   26995   152329    307308   31048   1154 13743   31   146   29  21%    294   32   32   32  101%
c i  169.4   26994   152329    311766   35230   1162 13757   34   163   44  21%    342   46   45   32  140%
c i  178.3   26993   152329    335876   58120   1193 13778   29    81   94  36%    136  -32   51   31  165%
c i  178.6   26992   152329    336630   58834   1194 13781   30    89   95  34%    -49  -23   32   31  104%
c i  179.1   26991   152329    337355   59523   1195 13782   32    97   95  33%   -134  -16   35   31  113%
c -  181.8   26991   152329    342686   31949   1222 13807   34   108   29  31%   -142   -5   23   31   75%
c i  183.1   26990   152329    345996   35077   1239 13812   34   108   44  32%    -85   -4   31   31   98%
c i  183.1   26983   152329    346019   35088   1239 13812   35   108   44  32%    -88   -4   36   31  115%
c i  183.6   26982   152329    347061   36101   1241 13813   31    93   44  34%   -154  -19   19   31   61%
c i  184.6   26981   152329    350298   39207   1243 13819   29    74   51  38%   -156  -36   34   31  109%
c i  188.2   26980   152329    358439   46961   1254 13841   36   109   68  33%    -66   -1   31   32   97%
c i  194.4   26979   152329    370531   58457   1277 13869   36   101  107  36%     10   -3   45   32  142%
c -  198.6   26979   152329    378357   32433   1291 13876   38   146   30  26%    -46   39   33   33  101%
c 
c [simplification-9] limit 371766 conflicts (hard 425766) hit after 381253 conflicts
c [quatres-6] found 1594 quaternary clauses 17% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 2 quaternary resolvents
c [ternres-6] limit 23828364 with penalty 0 = 0 + 0
c [ternres-6] all 26979 free variables schedulable
c [ternres-6] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-22] removed 22 variables
c [simpleprobe-4] all 26978 free variables schedulable
c [simpleprobe-4] limit 95313457 penalty 0 = 0 + 0
c [decomp-23] removed 197 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 197 variables, found 1724 hbrs, 176 units
c [unhide-8] limit 4765672 with penalty 0 = 0 + 0
c [unhide-8-12] 4 units, 46 failed, 3626 tauts, 0 hbrs, 309223 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 29 transitive binary clauses
c [transred-7] found 2 units
c [bca-7] limit of 10000000 steps and 298150 added (scaled 2)
c [bca-7] 30803 out of 53534 literals actually usable 58%
c [bca-7] added 625 blocked clauses in 96944 steps
c [phase-count-9] 147454 negative 99.9% of 147570 except 116 0.1%
c [phase-count-9] 102499 positive 69.5% of 147570 except 45071 30.5%
c [phase-count-9] less non-negative clauses 116 than limit 14700 (10.0%)
c [phase-count-9] non-pos/non-neg = 45071/116 = 388.54 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 178 negative 100%
c [sort-queue-9] sorted 2110 enqueued variables after 381253 conflicts
c [score-dist-9] active 24656 (92%), one 0 (0%), zero 2110 (8%)
c [score-dist-9] max exp 520, different 13 (2%)
c [score-dist-9] median active exp 520, avg 519.7
c [simplification-9] removed 213 variables 0.8% (26766 remain 40%)
c [simplification-9] removed 4759 irredundant clauses 3.1% (147570 remain 54%)
c [simplification-9] maximum reduction of 3% = max (1%, 3%)
c [simplification-9] geometric conflict interval increment 27000 = 108000 / 4
c [simplification-9] new conflict interval 135000
c [simplification-9] penalized conflict interval 135000 = 1 * 135000
c [simplification-9] hard conflict limit 583753 (soft 516253 + delta 67500)
c [simplification-9] new conflict limit 516253 (hard 583753)
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  209.4   26765   147570    394713   47701   1316 15184   37   129   85  29%    190   20   44   33  132%
c -  217.5   26765   147570    414942   33406   1339 15205   29    95   27  31%    130  -22   30   33   92%
c i  218.4   26764   147570    417276   35685   1339 15205   30    85   40  35%    161  -31   26   33   79%
c i  229.2   26763   147570    443455   60878   1372 15228   36   110  118  33%    205    3   65   32  203%
c -  231.9   26763   147570    451235   34992   1382 15233   34   114   27  30%    -72    5   25   32   78%
c -  245.0   26763   147570    487720   36116   1425 15263   20    34   27  59%    396  -59   19   29   64%
c i  249.3   26762   147570    500353   48155   1439 15267   25    42   53  59%    506  -40   39   28  139%
c i  254.7   26761   147570    508679   56209   1447 15270   32    89   93  36%   -227    8   40   28  140%
c i  259.3   26760   147570    519308   66408   1460 15287   26   100  110  26%   -153   14   22   28   77%
c -  261.4   26760   147570    524141   35661   1470 15294   31   117   37  27%   -224   29   22   28   78%
c i  263.9   26759   147570    531980   43077   1481 15316   24    95   55  25%    -85    6   40   28  144%
c i  267.2   26758   147570    539669   50511   1485 15317   28    74   67  38%   -141  -16   22   28   78%
c 
c [simplification-10] limit 516253 conflicts (hard 583753) hit after 562196 conflicts
c [quatres-7] found 1969 quaternary clauses 17% in total
c [quatres-7-2] added 2 single-self-subsuming ternary resolvents
c [quatres-7-2] added 2 quaternary resolvents
c [ternres-7] limit 34185796 with penalty 0 = 0 + 0
c [ternres-7] all 26758 free variables schedulable
c [ternres-7] 10 ternary resolvents (0 bin, 10 trn)
c [ternres-7] fully completed ternary resolution
c [card-4] limit 2136612 penalty 3 = 3 + 0
c [card-4] found 5833 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2136612 for elimination
c [card-4] 5833 out of 5833 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-24] removed 8 variables
c [treelook-4] limit 3418579 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 53367 literals 100%
c [treelook-4] scheduling used 589066 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 3418579 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 3419260 steps
c [treelook-4] 53297 literals remain 100%
c [treelook-4] 21639 variables remain to probed next time 81%
c [treelook-4] removed 3 variables, found 2190 hbrs
c [unhide-9] limit 1709289 with penalty 2 = 0 + 2
c [unhide-9-14] 0 units, 7 failed, 1613 tauts, 0 hbrs, 2648741 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 30 transitive binary clauses
c [bca-8] limit of 10000000 steps and 295366 added (scaled 2)
c [bca-8] 30563 out of 53494 literals actually usable 57%
c [bca-8] added 159 blocked clauses in 132911 steps
c [sweep-8] limit 5127869 penalty 1 = 1 + 0
c [sweep-8-1] 3715 pos 42.1% + 5102 neg 57.9% = 8817 sched 33.0% ret 17929
c [sweep-8-1] 5174035 steps 146 queries 2420.04 avg class size
c [sweep-8-1] 1708 decisions 134 SAT calls 144.22 avg env size
c [sweep-8-1] 8549 variables remain 32% (18197 retained 68%)
c [decomp-26] removed 12 variables
c [sweep-8-1] removed 12 vars (0 failed, 9 eqs, 21 impls)
c [sweep-8] 12 < 1/1000 * 26746 = 26 considered unsuccessful
c [sweep-8] removed 12 vars in TOTAL (1 rounds, 145 queries)
c [phase-count-10] 145881 negative 99.9% of 145997 except 116 0.1%
c [phase-count-10] 102362 positive 70.1% of 145997 except 43635 29.9%
c [phase-count-10] less non-negative clauses 116 than limit 14500 (10.0%)
c [phase-count-10] non-pos/non-neg = 43635/116 = 376.16 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 140 negative 100%
c [sort-queue-10] sorted 2017 enqueued variables after 562196 conflicts
c [score-dist-10] active 24717 (92%), one 0 (0%), zero 2017 (8%)
c [score-dist-10] max exp 521, different 14 (3%)
c [score-dist-10] median active exp 521, avg 520.6
c [simplification-10] removed 24 variables 0.1% (26734 remain 40%)
c [simplification-10] removed 1573 irredundant clauses 1.1% (145997 remain 54%)
c [simplification-10] maximum reduction of 1% = max (0%, 1%)
c [simplification-10] geometric conflict interval increment 67500 = 135000 / 2
c [simplification-10] new conflict interval 202500
c [simplification-10] penalized conflict interval 202500 = 1 * 202500
c [simplification-10] hard conflict limit 865946 (soft 764696 + delta 101250)
c [simplification-10] new conflict limit 764696 (hard 865946)
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 -  282.9   26734   145997    563049   37343   1535 17058   28    97   24  29%    123    9   42   26  158%
c i  292.0   26733   145997    587471   60888   1573 17086   29    95   78  30%    403    1   23   28   84%
c -  299.9   26733   145997    601098   36132   1587 17115   36   103   30  35%    -96    4   32   30  108%
c i  304.0   26732   145997    614567   49236   1594 17122   29    97   54  30%    112   -3   29   30   96%
c i  309.5   26731   145997    626234   60653   1597 17123   26    48  106  53%    -99  -46   21   29   74%
c i  316.9   26730   145997    638940   72747   1619 17164   34   110  136  31%    -54   15   22   31   71%
c -  318.4   26730   145997    641357   38184   1619 17166   38   113   31  34%   -190   17   55   31  178%
c i  322.2   26729   145997    649240   45736   1625 17172   28    88   61  32%    -70   -8   18   31   58%
c -  335.0   26729   145997    681631   39766   1664 17194   31    88   31  35%    257   -9   20   30   65%
c i  343.0   26728   145997    700587   58045   1694 17227   30    79   82  38%    450  -18   24   30   78%
c -  353.3   26728   145997    721230   40222   1708 17231   35   119   33  29%     10   20   57   29  195%
c -  371.1   26728   145997    761635   40525   1745 17259   34    99   46  35%    477    3   34   29  117%
c 
c [simplification-11] limit 764696 conflicts (hard 865946) hit after 764701 conflicts
c [quatres-8] found 2283 quaternary clauses 18% in total
c [quatres-8-1] removed 2 duplicate quaternary clauses
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [ternres-8] limit 47055327 with penalty 0 = 0 + 0
c [ternres-8] all 26728 free variables schedulable
c [ternres-8] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-27] removed 7 variables
c [basicprobe-4] limit 235276637 penalty 0 = 0 + 0
c [basicprobe-4-0] 9084 probes remain 35% after last round
c [basicprobe-4-0] 466 units = 466 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 565 variables, found 3217 hbrs
c [bate-2] eliminated 35 asymmetric tautologies during probing
c [unhide-10] limit 9411065 with penalty 0 = 0 + 0
c [unhide-10-22] 28 units, 53 failed, 3731 tauts, 0 hbrs, 399403 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 30 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 26110 variables 100%
c [block-4] limit of 58819159 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 381 blocked clauses
c [block-4] 381 < 1/100 * 137388 = 1373 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 294095796 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 64 clauses out of 273 (23%) of length 33
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 32
c [cce-4-1] eliminated 21 clauses out of 52 (40%) of length 31
c [cce-4-1] eliminated 22 clauses out of 49 (45%) of length 30
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 27
c [cce-4-1] eliminated 1 clauses out of 7 (14%) of length 26
c [cce-4-1] eliminated 32 clauses out of 128 (25%) of length 23
c [cce-4-1] eliminated 56 clauses out of 142 (39%) of length 22
c [cce-4-1] eliminated 104 clauses out of 206 (50%) of length 21
c [cce-4-1] eliminated 69 clauses out of 141 (49%) of length 20
c [cce-4-1] eliminated 66 clauses out of 137 (48%) of length 19
c [cce-4-1] eliminated 63 clauses out of 130 (48%) of length 18
c [cce-4-1] eliminated 65 clauses out of 130 (50%) of length 17
c [cce-4-1] eliminated 68 clauses out of 142 (48%) of length 16
c [cce-4-1] eliminated 63 clauses out of 129 (49%) of length 15
c [cce-4-1] eliminated 60 clauses out of 123 (49%) of length 14
c [cce-4-1] eliminated 60 clauses out of 122 (49%) of length 13
c [cce-4-1] eliminated 47 clauses out of 94 (50%) of length 12
c [cce-4-1] eliminated 59 clauses out of 121 (49%) of length 11
c [cce-4-1] eliminated 52 clauses out of 106 (49%) of length 10
c [cce-4-1] eliminated 44 clauses out of 94 (47%) of length 9
c [cce-4-1] eliminated 52 clauses out of 108 (48%) of length 8
c [cce-4-1] eliminated 40 clauses out of 90 (44%) of length 7
c [cce-4-1] eliminated 42 clauses out of 104 (40%) of length 6
c [cce-4-1] eliminated 19 clauses out of 58 (33%) of length 5
c [cce-4-1] eliminated 39 clauses out of 140 (28%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 1228 large clauses in 17760330 steps
c [cce-4-1] allowing another 8880165 steps for small clauses
c [cce-4-1] scheduling 133691 clauses = 132842 binary + 849 ternary
c [cce-4-1] tried to eliminate 16689 small clauses 12%
c [cce-4-1] eliminated 2591 binary clauses 2%
c [cce-4-1] eliminated 3 ternary clauses 0%
c [cce-4-1] eliminated 2594 small clauses 2%
c [cce-4-1] eliminated 2594 small clauses in 294095865 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 3822 covered clauses in round 1
c [cce-4] eliminated 3822 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 25936 variables 100%
c [elim-5] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 1161 variables 4% in round 1 in 14115791 steps
c [elim-5-1] backward subsumption/strengthening limit 14115700
c [elim-5-1-1] backward checking 10958 touched variables 42%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 177 clauses in 6017749 steps
c [elim-5-1] rescheduled 471 variables 2% by backward subsumption
c [elim-5-2] no variable eliminated in round 2 in 568522 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 1162 = 4% variables out of 25936 scheduled
c [bca-9] limit of 10000000 steps and 256634 added (scaled 2)
c [bca-9] 35070 out of 49550 literals actually usable 71%
c [bca-9] added 41052 blocked clauses in 201862 steps
c [phase-count-11] 126381 negative 99.8% of 126616 except 235 0.2%
c [phase-count-11] 90573 positive 71.5% of 126616 except 36043 28.5%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 16 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 1410 enqueued variables after 764701 conflicts
c [score-dist-11] active 23364 (94%), one 0 (0%), zero 1410 (6%)
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 1954 variables 7.3% (24774 remain 37%)
c [simplification-11] removed 19381 irredundant clauses 13.3% (126616 remain 47%)
c [simplification-11] maximum reduction of 13% = max (7%, 13%)
c [simplification-11] large reduction 13% >= 5% limit
c [simplification-11] next conflict interval 7647 = min (764701/100, 202500)
c [simplification-11] penalized conflict interval 7647 = 1 * 7647
c [simplification-11] hard conflict limit 782348 (soft 772348 + delta 10000)
c [simplification-11] new conflict limit 772348 (hard 782348)
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  386.8   24773   126616    767245   33882   1599 61540   34    96   29  36%    522   -1   33   29  113%
c 
c [simplification-12] limit 772348 conflicts (hard 782348) hit after 782348 conflicts
c [quatres-9] found 2253 quaternary clauses 19% in total
c [quatres-9-2] added 2 quaternary resolvents
c [ternres-9] limit 48025834 with penalty 0 = 0 + 0
c [ternres-9] all 24773 free variables schedulable
c [ternres-9] 239 ternary resolvents (0 bin, 239 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 1200645 penalty 3 = 3 + 0
c [gauss-4] extracted 7 xors of average arity 2.1
c [gauss-4] connected 15 occurrences of 9 variables (average 1.7)
c [gauss-4] limit 1200645 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 3 variables
c [simpleprobe-5] all 24770 free variables schedulable
c [simpleprobe-5] limit 192103336 penalty 0 = 0 + 0
c [decomp-29] removed 34 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 34 variables, found 2302 hbrs, 33 units
c [unhide-11] limit 9605166 with penalty 0 = 0 + 0
c [unhide-11-30] 23 units, 0 failed, 7815 tauts, 0 hbrs, 1084429 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 117 transitive binary clauses
c [bca-10] limit of 10000000 steps and 270374 added (scaled 2)
c [bca-10] 32741 out of 49428 literals actually usable 66%
c [bca-10] added 2603 blocked clauses in 182858 steps
c [phase-count-12] 122998 negative 99.8% of 123223 except 225 0.2%
c [phase-count-12] 89023 positive 72.2% of 123223 except 34200 27.8%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-12] sorted 1409 enqueued variables after 782348 conflicts
c [score-dist-12] active 23304 (94%), one 0 (0%), zero 1409 (6%)
c [score-dist-12] max exp 521, different 14 (3%)
c [score-dist-12] median active exp 521, avg 520.8
c [simplification-12] removed 60 variables 0.2% (24713 remain 37%)
c [simplification-12] removed 3393 irredundant clauses 2.7% (123223 remain 46%)
c [simplification-12] maximum reduction of 3% = max (0%, 3%)
c [simplification-12] geometric conflict interval increment 50625 = 202500 / 4
c [simplification-12] new conflict interval 253125
c [simplification-12] penalized conflict interval 253125 = 1 * 253125
c [simplification-12] hard conflict limit 1162035 (soft 1035473 + delta 126562)
c [simplification-12] new conflict limit 1035473 (hard 1162035)
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.9   24712   123223    788882   54152   1956 60497   32   109   56  29%    -98   12   48   30  157%
c i  405.4   24711   123223    795729   60678   1966 60525   43   147   60  29%   -295   46   47   32  147%
c i  407.3   24710   123223    799980   64744   1970 60526   40   129   73  31%   -313   25   45   32  141%
c i  410.4   24709   123223    805938   70352   1980 60552   47   158   89  30%   -260   51   40   34  119%
c i  413.2   24708   123223    812595   76725   1989 60563   39   151   91  26%   -221   42   46   34  135%
c -  414.1   24708   123223    814601   37393   1994 60563   32   118   28  27%   -271    7   17   33   50%
c i  430.4   24707   123223    856125   77692   2036 60583   38   112  137  34%    329   29   37   31  121%
c -  431.4   24707   123223    858445   42243   2036 60588   32    90   31  36%   -243    7   20   30   67%
c i  432.0   24706   123223    860078   43768   2047 60597   33    99   42  33%   -267   16   40   31  132%
c i  434.7   24705   123223    868144   51557   2062 60602   35   105   58  33%   -185   22   59   31  193%
c i  435.8   24704   123223    870886   54178   2066 60609   33    98   77  34%   -250   14   35   31  115%
c i  435.9   24703   123223    870991   54274   2067 60610   33   100   77  33%   -253   16   39   31  127%
c i  447.2   24702   123223    895771   77863   2100 60631   37   143  118  26%    116   41   39   34  114%
c -  448.9   24698   123223    899382   40468   2108 60635   36   136   42  26%   -196   31   40   34  117%
c i  449.8   24697   123223    901389   42369   2113 60643   41   146   52  28%   -169   41   52   34  152%
c i  455.5   24696   123223    916629   57097   2132 60646   36   110   83  33%      6    2   45   34  130%
c i  455.5   24695   123223    916673   57135   2132 60646   36   111   83  33%     -3    3   46   34  133%
c i  457.5   24694   123223    921415   61672   2132 60659   35    91   87  38%   -145  -16   38   34  110%
c i  462.7   24693   123223    931672   71259   2159 60698   48   153  125  32%    -42   42   53   36  144%
c i  463.1   24692   123223    932200   71747   2160 60699   49   153  125  32%    -98   42   53   37  144%
c -  468.4   24692   123223    943493   41135   2169 60712   36    92   41  39%     -9  -18   42   36  118%
c i  471.1   24691   123223    950237   47664   2174 60714   31    86   70  36%     92  -22   45   35  128%
c i  474.1   24690   123223    956398   53583   2179 60740   35    92   93  38%    -84  -14   29   35   82%
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 -  487.2   24690   123223    987845   44875   2197 60758   26    38   43  68%    277  -46   22   32   68%
c -  505.1   24690   123223   1030242   43831   2264 60801   26    47   43  55%    633  -40   22   32   68%
c 
c [simplification-13] limit 1035473 conflicts (hard 1162035) hit after 1046418 conflicts
c [quatres-10] found 2667 quaternary clauses 19% in total
c [quatres-10-1] removed 4 duplicate quaternary clauses
c [quatres-10-2] added 2 single-self-subsuming ternary resolvents
c [quatres-10-2] added 5 quaternary resolvents
c [ternres-10] limit 65387217 with penalty 0 = 0 + 0
c [ternres-10] all 24690 free variables schedulable
c [ternres-10] 37 ternary resolvents (0 bin, 37 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-30] removed 23 variables
c [treelook-5] limit 6538721 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 49366 literals 100%
c [treelook-5] scheduling used 602431 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 6538721 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 6612521 steps
c [treelook-5] 49232 literals remain 100%
c [treelook-5] 20033 variables remain to probed next time 81%
c [treelook-5] removed 7 variables, found 4705 hbrs
c [unhide-12] limit 6538721 with penalty 1 = 0 + 1
c [unhide-12-35] 1 units, 1 failed, 3875 tauts, 0 hbrs, 2677100 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 143 transitive binary clauses
c [cce-5] limit of 81734021 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 42
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 38
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 37
c [cce-5-1] eliminated 1 clauses out of 215 (0%) of length 33
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 32
c [cce-5-1] eliminated 34 clauses out of 38 (89%) of length 31
c [cce-5-1] eliminated 20 clauses out of 30 (67%) of length 30
c [cce-5-1] eliminated 5 clauses out of 7 (71%) of length 29
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 28
c [cce-5-1] eliminated 3 clauses out of 9 (33%) of length 27
c [cce-5-1] eliminated 1 clauses out of 9 (11%) of length 26
c [cce-5-1] eliminated 2 clauses out of 5 (40%) of length 25
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 24
c [cce-5-1] eliminated 5 clauses out of 217 (2%) of length 23
c [cce-5-1] eliminated 23 clauses out of 257 (9%) of length 22
c [cce-5-1] eliminated 13 clauses out of 253 (5%) of length 21
c [cce-5-1] eliminated 11 clauses out of 170 (6%) of length 20
c [cce-5-1] eliminated 12 clauses out of 181 (7%) of length 19
c [cce-5-1] eliminated 16 clauses out of 173 (9%) of length 18
c [cce-5-1] eliminated 10 clauses out of 161 (6%) of length 17
c [cce-5-1] eliminated 5 clauses out of 181 (3%) of length 16
c [cce-5-1] eliminated 7 clauses out of 140 (5%) of length 15
c [cce-5-1] eliminated 6 clauses out of 158 (4%) of length 14
c [cce-5-1] eliminated 10 clauses out of 164 (6%) of length 13
c [cce-5-1] eliminated 9 clauses out of 115 (8%) of length 12
c [cce-5-1] eliminated 8 clauses out of 154 (5%) of length 11
c [cce-5-1] eliminated 15 clauses out of 123 (12%) of length 10
c [cce-5-1] eliminated 15 clauses out of 116 (13%) of length 9
c [cce-5-1] eliminated 12 clauses out of 128 (9%) of length 8
c [cce-5-1] eliminated 8 clauses out of 119 (7%) of length 7
c [cce-5-1] eliminated 7 clauses out of 155 (5%) of length 6
c [cce-5-1] eliminated 10 clauses out of 80 (12%) of length 5
c [cce-5-1] eliminated 41 clauses out of 187 (22%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 320 large clauses in 67744739 steps
c [cce-5-1] allowing another 33872369 steps for small clauses
c [cce-5-1] scheduling 117811 clauses = 116615 binary + 1196 ternary
c [cce-5-1] tried to eliminate 2077 small clauses 2%
c [cce-5-1] eliminated 689 binary clauses 1%
c [cce-5-1] eliminated 3 ternary clauses 0%
c [cce-5-1] eliminated 692 small clauses 1%
c [cce-5-1] eliminated 699 small clauses in 81734021 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1019 covered clauses in round 1
c [cce-5] eliminated 1019 covered clauses in TOTAL during 1 rounds
c [cce-5] 1019 < 1/100 * 122229 = 1222 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 24681 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 188 variables 1% in round 1 in 11518228 steps
c [elim-6-1] backward subsumption/strengthening limit 11518200
c [elim-6-1-1] backward checking 2562 touched variables 10%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 31 clauses in 1547108 steps
c [elim-6-1] rescheduled 55 variables 0% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 133653 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 188 = 1% variables out of 24681 scheduled
c [elim-6] 188 < 1/100 * 24681 = 246 considered unsuccessful
c [bca-11] limit of 10000000 steps and 262723 added (scaled 2)
c [bca-11] 32293 out of 48988 literals actually usable 66%
c [bca-11] added 9859 blocked clauses in 176850 steps
c [sweep-9] limit 4904041 penalty 2 = 2 + 0
c [sweep-9-1] 3307 pos 43.1% + 4361 neg 56.9% = 7668 sched 31.3% ret 16825
c [sweep-9-1] 4906903 steps 344 queries 1549.22 avg class size
c [sweep-9-1] 1879 decisions 335 SAT calls 37.72 avg env size
c [sweep-9-1] 7100 variables remain 29% (17393 retained 71%)
c [decomp-32] removed 6 variables
c [sweep-9-1] removed 6 vars (0 failed, 7 eqs, 14 impls)
c [sweep-9] 6 < 1/1000 * 24493 = 24 considered unsuccessful
c [sweep-9] removed 6 vars in TOTAL (1 rounds, 343 queries)
c [phase-count-13] 118493 negative 99.8% of 118747 except 254 0.2%
c [phase-count-13] 86085 positive 72.5% of 118747 except 32662 27.5%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-13] sorted 1326 enqueued variables after 1046418 conflicts
c [score-dist-13] active 23161 (95%), one 0 (0%), zero 1326 (5%)
c [score-dist-13] max exp 521, different 14 (3%)
c [score-dist-13] median active exp 521, avg 520.8
c [simplification-13] removed 203 variables 0.8% (24487 remain 36%)
c [simplification-13] removed 4476 irredundant clauses 3.6% (118747 remain 44%)
c [simplification-13] maximum reduction of 4% = max (1%, 4%)
c [simplification-13] geometric conflict interval increment 50625 = 253125 / 5
c [simplification-13] new conflict interval 303750
c [simplification-13] penalized conflict interval 303750 = 1 * 303750
c [simplification-13] hard conflict limit 1502043 (soft 1350168 + delta 151875)
c [simplification-13] new conflict limit 1350168 (hard 1502043)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  523.6   24486   118747   1051550   55490   2298 70666   35    95   42  36%    741   17   43   31  140%
c -  536.8   24486   118747   1083678   43507   2337 70702   41   108   30  38%    -74   19   49   33  145%
c i  537.1   24485   118747   1084332   44142   2339 70703   41   114   40  36%    -63   24   41   34  122%
c i  548.8   24484   118747   1111695   70502   2360 70717   37    90   89  41%    -35    3   30   34   88%
c i  551.7   24483   118747   1119207   77825   2363 70719   37    82  125  45%   -307   -4   35   34  102%
c i  552.4   24482   118747   1121038   79593   2368 70724   34    86  138  40%   -367   -1   23   34   67%
c -  555.6   24482   118747   1129542   45836   2376 70732   33    70   32  47%   -241  -17   30   34   89%
c i  561.5   24481   118747   1146077   61783   2382 70743   31    84   78  37%     41   -1   36   33  109%
c i  564.4   24480   118747   1152551   67950   2391 70744   38   125   86  30%   -226   38   47   34  140%
c i  570.1   24479   118747   1165549   80404   2404 70772   40   114  117  35%    -86   22   39   35  111%
c i  572.4   24478   118747   1171705   86372   2416 70782   35   100  127  35%   -173    6   37   35  108%
c -  573.7   24478   118747   1174476   45941   2418 70784   34    93   45  36%   -211   -1   23   35   67%
c i  583.6   24477   118747   1205207   75272   2442 70785   20    31   96  65%    247  -46   19   30   64%
c -  591.5   24477   118747   1221118   47014   2461 70793   39   106   44  37%     -3   25   30   33   93%
c i  602.7   24476   118747   1252668   77546   2477 70806   28    46  110  61%    390  -33   33   32  103%
c -  608.5   24476   118747   1267059   48574   2485 70815   28    65   45  43%    -90   -8   41   31  134%
c -  629.0   24476   118747   1312972   46806   2519 70839   39   102   44  38%    471   21   43   34  127%
c i  642.3   24475   118747   1344331   77121   2558 70880   28    60  108  47%    681  -26   25   33   76%
c -  649.5   24475   118747   1361874   49465   2568 70892   32   120   46  27%   -351   32   30   33   90%
c i  654.9   24474   118747   1375293   62285   2577 70903   37   100   75  37%    -97   11   43   33  129%
c i  656.7   24473   118747   1379436   66299   2577 70906   29    59   91  49%   -481  -29   24   33   73%
c i  659.8   24472   118747   1386887   73327   2602 70920   40   120   95  33%   -385   32   44   33  131%
c i  660.0   24471   118747   1387226   73645   2603 70922   41   124   95  33%   -411   35   46   34  137%
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 -  669.3   24471   118747   1409722   49335   2620 70925   32    70   45  45%    -58  -20   26   34   78%
c -  688.0   24471   118747   1458805   51928   2649 70932   25    37   47  67%    512  -36   33   31  104%
c i  695.9   24470   118747   1475157   67903   2652 70933   19    26   98  74%    625  -38   14   29   48%
c i  697.2   24469   118747   1477994   70607   2660 70939   30    78   99  38%   -607   14   40   30  136%
c 
c [simplification-14] limit 1350168 conflicts (hard 1502043) hit after 1502043 conflicts
c [quatres-11] found 3168 quaternary clauses 20% in total
c [quatres-11-2] added 8 single-self-subsuming ternary resolvents
c [quatres-11-2] added 17 quaternary resolvents
c [ternres-11] limit 97083419 with penalty 0 = 0 + 0
c [ternres-11] all 24469 free variables schedulable
c [ternres-11] 38 ternary resolvents (0 bin, 38 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-33] removed 19 variables
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 106 probes remain 0% after last round
c [basicprobe-5-0] 501 units = 501 failed (100%) + 0 lifted (0%)
c [basicprobe-5-0] removed 517 variables, found 8771 hbrs
c [bate-3] eliminated 6 asymmetric tautologies during probing
c [unhide-13] limit 2427085 with penalty 3 = 0 + 3
c [unhide-13-37] 0 units, 1 failed, 1446 tauts, 0 hbrs, 3043836 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 116 transitive binary clauses
c [bca-12] limit of 10000000 steps and 259459 added (scaled 2)
c [bca-12] 28785 out of 47902 literals actually usable 60%
c [bca-12] added 315 blocked clauses in 171018 steps
c [phase-count-14] 114403 negative 99.8% of 114650 except 247 0.2%
c [phase-count-14] 83694 positive 73.0% of 114650 except 30956 27.0%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-14] sorted 1304 enqueued variables after 1502043 conflicts
c [score-dist-14] active 22646 (95%), one 0 (0%), zero 1304 (5%)
c [score-dist-14] max exp 522, different 14 (3%)
c [score-dist-14] median active exp 522, avg 521.7
c [simplification-14] removed 519 variables 2.1% (23950 remain 35%)
c [simplification-14] removed 4097 irredundant clauses 3.5% (114650 remain 42%)
c [simplification-14] maximum reduction of 3% = max (2%, 3%)
c [simplification-14] geometric conflict interval increment 75937 = 303750 / 4
c [simplification-14] new conflict interval 379687
c [simplification-14] penalized conflict interval 379687 = 1 * 379687
c [simplification-14] hard conflict limit 2071573 (soft 1881730 + delta 189843)
c [simplification-14] new conflict limit 1881730 (hard 2071573)
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 -  727.8   23950   114650   1506369   50663   2530 74020   32    86   36  37%   -120    6   30   31   95%
c -  750.2   23950   114650   1556654   50661   2583 74059   29    55   36  52%    493  -31   20   33   60%
c -  772.2   23950   114650   1607906   52435   2613 74081   33    70   37  47%    781  -14   49   33  149%
c -  793.3   23950   114650   1658776   53072   2639 74088   35    86   53  41%    912   -4   36   35  104%
c -  815.2   23950   114650   1710703   53872   2678 74123   29    65   54  45%    973  -21   27   34   78%
c -  834.1   23950   114650   1762771   56235   2706 74125   27    46   56  58%   1001  -33   26   30   85%
c -  855.0   23950   114650   1813787   54560   2749 74139   44   124   55  35%   1014   39   37   32  118%
c -  878.2   23950   114650   1867826   56386   2796 74166   30    86   55  35%   1019   -4   29   32   91%
c 
c [simplification-15] limit 1881730 conflicts (hard 2071573) hit after 1881798 conflicts
c [quatres-12] found 3492 quaternary clauses 19% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [quatres-12-2] added 2 single-self-subsuming ternary resolvents
c [quatres-12-2] added 6 quaternary resolvents
c [ternres-12] limit 122708969 with penalty 0 = 0 + 0
c [ternres-12] all 23950 free variables schedulable
c [ternres-12] 25 ternary resolvents (0 bin, 25 trn)
c [ternres-12] fully completed ternary resolution
c [card-5] limit 3834655 penalty 4 = 4 + 0
c [card-5] found 6360 at-most-one constraints of average size 3.7
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 3834655 for elimination
c [card-5] 6360 out of 6360 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [simpleprobe-6] all 23950 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-35] removed 7 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 7 variables, found 2028 hbrs, 2 units
c [unhide-14] limit 5000000 with penalty 2 = 0 + 2
c [unhide-14-41] 0 units, 0 failed, 2204 tauts, 0 hbrs, 3829950 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 124 transitive binary clauses
c [bca-13] limit of 10000000 steps and 258486 added (scaled 2)
c [bca-13] 28149 out of 47888 literals actually usable 59%
c [bca-13] added 368 blocked clauses in 140979 steps
c [phase-count-15] 113847 negative 99.8% of 114085 except 238 0.2%
c [phase-count-15] 83555 positive 73.2% of 114085 except 30530 26.8%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 1284 enqueued variables after 1881798 conflicts
c [score-dist-15] active 22659 (95%), one 0 (0%), zero 1284 (5%)
c [score-dist-15] max exp 522, different 14 (3%)
c [score-dist-15] median active exp 522, avg 521.7
c [simplification-15] removed 7 variables 0.0% (23943 remain 35%)
c [simplification-15] removed 565 irredundant clauses 0.5% (114085 remain 42%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 379687
c [simplification-15] new conflict interval 759374
c [simplification-15] penalized conflict interval 759374 = 1 * 759374
c [simplification-15] hard conflict limit 3020859 (soft 2641172 + delta 379687)
c [simplification-15] new conflict limit 2641172 (hard 3020859)
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 -  910.4   23943   114085   1921337   56879   2868 74865   36    85   36  42%   1022   -8   49   31  157%
c -  934.9   23943   114085   1975497   57462   2892 74881   29    60   51  49%   1023  -27   22   32   69%
c -  957.9   23943   114085   2030335   58202   2935 74901   32    78   51  41%   1024  -14   36   31  117%
c -  980.3   23943   114085   2085780   60778   2982 74907   23    33   53  70%   1024  -42   21   27   75%
c i  988.3   23942   114085   2107409   81431   2988 74907   22    35  113  62%   1024  -27   29   26  113%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 42 basic ate = 42 trn 100% + 0 lrg 0% in 3 updates
c bcas: 13 count, 60001 added (4205 skipped), 1711137 steps
c bkwd: tried 180512 clauses, 360987 lits, 2.00 lits/clause
c bkwd: checked 12528758 occs, 69.41 occs/clause, 34.71 occs/lit
c bkwd: subsumed 1 binary, 8 ternary, 6 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1430 large (0% self)
c blkd: 4 bces, 552 removed, 1926238 resolutions, 5047543 steps
c blkd: 11922 blocking literals 6%, 222 pure
c bump: 2122196 bumped seen, 1230461915 lits 579.8 on average
c card: 5 count, 0 units, 0 am1, 27158660 steps
c card: 56 rescheduled, 0 eliminated, 0 resolved, 46944 subsumed
c card: 29920 at-most-one constraints found, average size 3.35
c card: 29920 at-most-one constraints used 100%, average size 3.35
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 5 cces, 5993 eliminated, 5281 ate 88%, 712 abce 12%
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: 1614347 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 99 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 35 decompositions, 1025 equivalent 1%
c deco: 31274 decision-only clauses 1%, 76% reduction
c decs: 9133522 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 38541 eliminated 40%, 27937 pure 72%
c elms: 11 rounds, 1.8 rounds/bve
c elms: 9175 small 24%, 1207 large 3%
c elms: 48459 tried small, 9175 succeeded 19%, 39284 failed 81%
c elms: 340 subsumed, 31453 strengthened, 8397 blocked
c elms: 1983977 copies, 2107456 resolutions, 577219 ipos
c elms: 3136047 subchks, 3177681 strchks
c gaus: 4 extractions, 16 extracted, 2.4 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10111806 steps, 5055903 extr 50%, 90 elim 0%
c glue: 31.8 orig avg, 31.8 real avg, 5.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 35177 = 10853 simple 31% + 17279 trn 49% + 7045 lrg 20%, 598 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2122195 clauses, 373.7 length
c lrnd: 793163182 lits = 1162798902 orig - 369635720 removed 32%
c lrnd: 514684 uips 24%, 1435759 flips 68%
c mins: 2064856 mins 98%, 1437 bin 0%, 4710 size 0%
c mins: 1253597749 poisoned searches, 516934922 hits, 41% hit rate
c mins: 1737771003 used twice searches, 26508873 hits, 2% hit rate
c move: moved 3994, 3900 bin 98%, 94 trn 2%
c otfs: 11220 driving 16%, 56806 restarting 84%
c otfs: str 68026, 67808 red 100%, 218 irr 0%
c otfs: str 68026, 0 bin 0%, 343 trn 1%, 67683 lrg 99%
c otfs: sub 25, 25 red 100%, 0 irr 0%
c otfs: sub 25, 0 bin 0%, 0 trn 0%, 25 lrg 100%
c phas: 15 computed, 39455 set, 18 pos (0%), 39437 neg (100%)
c prbs: 5 basic, 30165 probed, 1186 failed, 0 lifted
c prbs: 6 simple, 349410 probed, 352 failed, 434 eqs
c prbs: 5 treelook, 230 probed, 24 failed, 0 lifted
c prom: 486036 locked 11% out of 4328008 tried
c prps: 1489240250 props, 151 props/dec
c prps: 92% srch, 8% simp, 0% lkhd
c quat: 12 count, 36 quat, 21 self1, 0 self2, 8 dup
c queu: 15 sorted, 9133522 next (1096 steps 0.00)
c queu: 1230632180 enq (8505235461 steps 6.91), 1230461915 deq 100%
c redc: 17888 clauses 63%, 28580 tried 1%, 18 sat 0%
c redc: 101906 lits 27%, 379806 tried 0%, 18 sat 0%
c redc: 2205 times jump level reduced, 13.1 levels on average
c reds: 47 count, 45388.0 conflicts per reduce
c reds: 0 memlim 0%, 47 arith 100%
c reds: 1715797 collected 90%, 198176 retired 10%
c rmbd: 4099 removed, 971 red 24%
c rsts: 32192 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: 15 count, 13 confs 87%, 0 vars 0%
c simp: 1 its 7%, 1 bin 7%, 0 trns 0%
c subl: 2122195 count (2267148 tried 1.1), 72824 sub out of 2116178 (3.4%)
c swps: 9 count, 9 rounds, 1044 queries (116.0/round)
c swps: 989 sat calls, 3 unsat (0.2% success rate)
c swps: 22162 decisions 22.4, 181 conflicts 0.2
c swps; 1759.2 avg class size, 403.7 avg environment size
c swps: 0 failed, 95 impls, 52 equivs
c swp0: 345 type 0 queries, 43 unsat (12.5%), 332 sat (96.2%)
c swp1: 699 type 1 queries, 270 unsat (38.6%), 660 sat (94.4%)
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: 22511853 calls to obtain time
c tops: 31951 fixed 33%, 101 its, 21121.14 confs/it
c trds: 13 transitive reductions, 696 removed, 2 failed
c trds: 6236 nodes, 20175 edges, 23734147 steps
c trim: 3064225 words, 11.7 MB
c trnr: 12 count, 0 bin, 434 trn, 12276873 steps
c unhd: 14 count, 41 rounds, 55435186 steps
c unhd: 108 non-trivial sccs of average size 2.0
c unhd: 81 units, 81 bin, 0 trn, 0 lrg
c unhd: 174 failed, 170 stamp, 0 lits, 3 bin, 0 trn, 0 lrg
c unhd: 37256 tauts, 853 bin 2%, 221 trn 1%, 143 lrg 0%
c unhd: 37256 tauts, 36039 stamp 97%, 12799 red 34%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 21668044 str, 81 bin 0%, 373 trn 0%, 21667590 lrg 100%, 21660393 red 100%
c vars: 23939 remaining 25% and 71517 removed 75% out of 95456
c vars: 31951 fixed 33%, 38541 eliminated 40%, 1025 equivalent 1%
c vsts: 14504887724 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 10.1 search visits per propagation, 6545.4 per conflict
c wchs: 3590993688 pushed, 120591902 enlarged, 149 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2116214       1715797        198176      77900485      18847439       1434096
c 
c  0 0         23219   1      3684   0         0   0  15122033  19   2223654  12    114201   8     1.0
c  1 5         13532   1      6495   0      3416   2   4261757   5    772727   4     40307   3     0.6
c  2 6         76669   4     45290   3     14402   7  15209468  20   3302485  18    192680  13     4.0
c  3 9        228356  11    172103  10     24340  12  22817000  29<  5521819  29<   405241  28    10.3
c  4 14       413812  20    355700  21     27263  14  11617806  15   3547607  19    318363  22<   19.4
c  5 21       518557  25<   453416  26<    31532  16   4502281   6   1720137   9    178388  12    32.0
c  6 30       420340  20    366141  21     30129  15<  2222512   3    921153   5     94339   7    35.8
c  7 41       219734  10    184019  11     23343  12    963593   1    435889   2     45773   3    18.7
c  8 54        95732   5     74664   4     15816   8    469525   1    185967   1     20210   1     9.3
c  9 69        45722   2     32870   2     10460   5    335173   0     96530   1     10778   1     5.7
c 10 86        25197   1     15943   1      6708   3    230472   0     64481   0      7611   1     4.3
c 11 126       22421   1      3945   0      6657   3    130149   0     44391   0      5182   0     1.2
c 12 230       12507   1      1471   0      3959   2     18157   0     10318   0      1006   0     1.5
c 13 534         416   0        56   0       151   0       559   0       281   0        17   0     0.2
c 
c avg                  5.2           5.2           5.7           2.6           3.1           3.6
c std                  1.9           1.6           2.5           1.8           1.9           1.9
c 
c  325.582  33% bump
c   44.179   4% unhide
c   19.082   2% probe
c    6.430   1% cce
c    6.067   1% decide
c 
c   10.620 < 1% rest (below)
c 
c    3.421   0% sweep
c    2.824   0% elim
c    1.562   0% bca
c    1.022   0% block
c    0.732   0% gauss
c    0.574   0% transred
c    0.291   0% card
c    0.117   0% quatres
c    0.076   0% ternres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.023   0% preprocessing     1%
c   86.131   9% inprocessing     99%
c ==================================
c   87.153   9% simplifying
c  912.647  91% search
c ==================================
c  999.803 100% all
c 
c       2133235 conflicts,        2133.7 confs/sec
c          3403 ternaries,         626.9 confs/ternary
c          2482 binaries,          859.5 confs/binary
c           101 iterations,      21121.1 confs/iteration
c 
c            47 reductions,          0.0 redus/sec,  45388.0 confs/reduction
c         32192 restarts,           32.2 rests/sec,     66.3 confs/restart
c       9133522 decisions,        9135.3 decis/sec,      4.3 decis/conflict
c    1489240250 propagations,  1489533.9 props/sec,    163.1 props/decision
c 
c 999.8 seconds, 194.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
