c launch: /data/cnf/sc2014/app/10pipe_q0_k.cnf.bz2
c host: atom19
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/10pipe_q0_k.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/10pipe_q0_k.cnf.bz2
c no embedded options
c found 'p cnf 77639 2082017' header
c read 77639 variables, 2082017 clauses, 6164595 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=1
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 77638 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] INC (--score=1)
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   77638  2082016         0       0      0     0    0     0   47   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1000000 penalty 1 = 0 + 1
c [card-1] found 4 at-most-one constraints of average size 3.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1000000 for elimination
c [card-1] 4 out of 4 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 12 variables
c [simpleprobe-1] all 77627 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 10000000 penalty 1 = 0 + 1
c [simpleprobe-1] 69795 variables remain 90% (7832 retained 10%)
c [simpleprobe-1] removed 0 variables, found 4594 hbrs, 0 units
c [unhide-1] limit 130084 based on 2081358 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 77627 variables 100%
c [elim-1] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 68503 not tried 88% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 9082 = 12% variables out of 77627 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 2062384 negative 100.0% of 2063156 except 772 0.0%
c [phase-count-1] 327464 positive 15.9% of 2063156 except 1735692 84.1%
c [phase-count-1] less non-negative clauses 772 than limit 206300 (10.0%)
c [phase-count-1] non-pos/non-neg = 1735692/772 = 2248.31 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 68545 negative 100%
c [sort-queue-1] sorted 68545 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 68545 (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 9082 variables 11.7% (68545 remain 88%)
c [simplification-1] removed 18860 irredundant clauses 0.9% (2063156 remain 99%)
c [simplification-1] maximum reduction of 12% = max (12%, 1%)
c [simplification-1] large reduction 12% >= 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 [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [treelook-1] limit 515789 based on 2063156 irredundant clauses
c [treelook-1] scheduled 45749 literals 33%
c [treelook-1] scheduling used 515840 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 515789 based on 2063156 irredundant clauses
c [treelook-1] used 1293700 steps
c [treelook-1] 45743 literals remain 33%
c [treelook-1] 43176 variables remain to probed next time 63%
c [treelook-1] removed 0 variables, found 52 hbrs
c [basicprobe-1] limit 16505248 based on 2063156 irredundant clauses
c [basicprobe-1-0] 41692 probes remain 61% after last round
c [basicprobe-1-0] 55 units = 55 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 55 variables, found 13245 hbrs
c [elim-2] 68448 variables 100% will be scheduled this time
c [elim-2] scheduled 68448 variables 100%
c [elim-2] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 62381 not tried 91% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 6067 = 9% variables out of 68448 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 59775 enqueued variables after 1001 conflicts
c [score-dist-2] active 2648 (4%), one 0 (0%), zero 59775 (96%)
c [score-dist-2] max exp 511, different 11 (2%)
c [score-dist-2] median active exp 505, avg 505.1
c [simplification-2] removed 6122 variables 8.9% (62423 remain 80%)
c [simplification-2] removed 22618 irredundant clauses 1.1% (2040538 remain 98%)
c [simplification-2] maximum reduction of 9% = max (9%, 1%)
c [simplification-2] large reduction 9% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
c 
c [simplification-3] limit 3001 conflicts (hard 13001) hit after 3001 conflicts
c [card-2] limit 510134 based on 2040538 irredundant clauses
c [card-2] found 3 at-most-one constraints of average size 3.3
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 510134 for elimination
c [card-2] 3 out of 3 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [simpleprobe-2] 56190 schedulable variables 90%
c [simpleprobe-2] limit 4081076 based on 2040538 irredundant clauses
c [simpleprobe-2] 53568 variables remain 86% (8855 retained 14%)
c [simpleprobe-2] removed 0 variables, found 1317 hbrs, 0 units
c [unhide-2] limit 127533 based on 2040538 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 4 tauts, 0 hbrs, 10331 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 62423 variables 100%
c [elim-3] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 56743 not tried 91% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 5680 = 9% variables out of 62423 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 54077 enqueued variables after 3001 conflicts
c [score-dist-3] active 2666 (5%), one 0 (0%), zero 54077 (95%)
c [score-dist-3] max exp 513, different 13 (3%)
c [score-dist-3] median active exp 506, avg 506.4
c [simplification-3] removed 5680 variables 9.1% (56743 remain 73%)
c [simplification-3] removed 11540 irredundant clauses 0.6% (2028998 remain 97%)
c [simplification-3] maximum reduction of 9% = max (9%, 1%)
c [simplification-3] large reduction 9% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15001 (soft 5001 + delta 10000)
c [simplification-3] new conflict limit 5001 (hard 15001)
c 
c [simplification-4] limit 5001 conflicts (hard 15001) hit after 5002 conflicts
c [elim-4] 56704 variables 100% will be scheduled this time
c [elim-4] scheduled 56704 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 200000000 steps penalty 1 = 0 + 1
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 19403 not tried 34% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 13104 = 23% variables out of 56704 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 41380 enqueued variables after 5002 conflicts
c [score-dist-4] active 2259 (5%), one 0 (0%), zero 41380 (95%)
c [score-dist-4] max exp 514, different 14 (3%)
c [score-dist-4] median active exp 507, avg 507.2
c [simplification-4] removed 13104 variables 23.1% (43639 remain 56%)
c [simplification-4] removed 28531 irredundant clauses 1.4% (2000467 remain 96%)
c [simplification-4] maximum reduction of 23% = max (23%, 1%)
c [simplification-4] large reduction 23% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 17002 (soft 7002 + delta 10000)
c [simplification-4] new conflict limit 7002 (hard 17002)
c 
c [simplification-5] limit 7002 conflicts (hard 17002) hit after 7002 conflicts
c [quatres-1] found 10387 quaternary clauses 9% in total
c [quatres-1-2] added 299 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 10000000 with penalty 1 = 0 + 1
c [ternres-1] all 43639 free variables schedulable
c [ternres-1] 2809 ternary resolvents (0 bin, 2809 trn)
c [ternres-1] 600 variables remain 1% (43039 retained 99%)
c [gauss-1] limit 1000233 based on 2000467 irredundant clauses
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-2] limit 500116 based on 2000467 irredundant clauses
c [treelook-2] scheduled 40545 literals 46%
c [treelook-2] scheduling used 500137 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 500116 based on 2000467 irredundant clauses
c [treelook-2] used 3268780 steps
c [treelook-2] 40542 literals remain 46%
c [treelook-2] 37337 variables remain to probed next time 86%
c [treelook-2] removed 0 variables, found 79 hbrs
c [transred-1] limit 2000467 based on 2000467 irredundant clauses
c [transred-1] removed 0 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 43639 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 250000000 steps penalty 1 = 0 + 1
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 128955 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 262
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 260
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 259
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 258
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 257
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 256
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 255
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 254
c [cce-1-1] eliminated 2 clauses out of 9 (22%) of length 253
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 23 large clauses in 30002487 steps
c [cce-1-1] allowing another 15001243 steps for small clauses
c [cce-1-1] scheduling 1741865 clauses = 1740743 binary + 1122 ternary
c [cce-1-1] tried to eliminate 176 small clauses 0%
c [cce-1-1] eliminated 3 binary clauses 0%
c [cce-1-1] eliminated 3 small clauses 0%
c [cce-1-1] eliminated 3 small clauses in 30000170 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 26 covered clauses in round 1
c [cce-1] eliminated 26 covered clauses in TOTAL during 1 rounds
c [cce-1] 26 < 1/100 * 1871512 = 18715 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 43639 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 32605 not tried 75% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2556 = 6% variables out of 43639 scheduled
c [bca-1] limit of 10000000 steps and 3738322 added (scaled 2)
c [bca-1] 79270 out of 82168 literals actually usable 96%
c [bca-1] added 2931 blocked clauses in 402681 steps
c [sweep-1] limit 3737822 based on 1868911 irredundant clauses
c [sweep-1-1] 457 pos 1.1% + 40626 neg 98.9% = 41083 sched 100.0% ret 0
c [sweep-1-1] 3742989 steps 168 queries 1194.27 avg class size
c [sweep-1-1] 5009 decisions 165 SAT calls 246.28 avg env size
c [sweep-1-1] 20733 variables remain 50% (20350 retained 50%)
c [decomp-10] removed 4 variables
c [sweep-1-1] removed 4 vars (0 failed, 4 eqs, 19 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 4 vars in TOTAL (1 rounds, 167 queries)
c [sort-queue-5] sorted 38175 enqueued variables after 7002 conflicts
c [score-dist-5] active 2904 (7%), one 0 (0%), zero 38175 (93%)
c [score-dist-5] max exp 514, different 14 (3%)
c [score-dist-5] median active exp 508, avg 507.3
c [simplification-5] removed 2560 variables 5.9% (41079 remain 53%)
c [simplification-5] removed 131556 irredundant clauses 6.6% (1868911 remain 90%)
c [simplification-5] maximum reduction of 7% = max (6%, 7%)
c [simplification-5] large reduction 7% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 19002 (soft 9002 + delta 10000)
c [simplification-5] new conflict limit 9002 (hard 19002)
c 
c [simplification-6] limit 9002 conflicts (hard 19002) hit after 9003 conflicts
c [quatres-2] found 10116 quaternary clauses 9% in total
c [quatres-2-2] added 3 single-self-subsuming ternary resolvents
c [quatres-2-2] added 212 quaternary resolvents
c [ternres-2] limit 7475644 based on 1868911 irredundant clauses
c [ternres-2] 576 schedulable variables 1%
c [ternres-2] 1702 ternary resolvents (1 bin, 1701 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 1 out of 1 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 14951288 based on 1868911 irredundant clauses
c [basicprobe-2-0] 33831 probes remain 83% after last round
c [basicprobe-2-0] 82 units = 82 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 82 variables, found 3737 hbrs
c [unhide-3] limit 116806 based on 1868911 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 3853 tauts, 0 hbrs, 24039 literals
c [block-2] scheduling all variables this time
c [block-2] scheduled 40997 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 1185 blocked clauses
c [block-2] 1185 < 1/100 * 1851592 = 18515 considered unsuccessful
c [elim-6] 18480 variables 45% will be scheduled this time
c [elim-6] scheduled 18480 variables 45%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 16456 not tried 40% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 69 = 0% variables out of 18480 scheduled
c [elim-6] 69 < 1/100 * 18480 = 184 considered unsuccessful
c [bca-2] limit of 10000000 steps and 3702341 added (scaled 2)
c [bca-2] 78773 out of 81858 literals actually usable 96%
c [bca-2] added 9 blocked clauses in 374238 steps
c [sweep-2] limit 3700376 based on 1850188 irredundant clauses
c [sweep-2-1] 313 pos 1.5% + 20323 neg 98.5% = 20636 sched 50.4% ret 20292
c [sweep-2-1] 3701647 steps 183 queries 972.66 avg class size
c [sweep-2-1] 5472 decisions 180 SAT calls 118.34 avg env size
c [sweep-2-1] 11132 variables remain 27% (29796 retained 73%)
c [decomp-12] removed 3 variables
c [sweep-2-1] removed 3 vars (0 failed, 3 eqs, 15 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 3 vars in TOTAL (1 rounds, 182 queries)
c [sort-queue-6] sorted 37757 enqueued variables after 9003 conflicts
c [score-dist-6] active 3168 (8%), one 0 (0%), zero 37757 (92%)
c [score-dist-6] max exp 514, different 14 (3%)
c [score-dist-6] median active exp 507, avg 507.2
c [simplification-6] removed 154 variables 0.4% (40925 remain 53%)
c [simplification-6] removed 18723 irredundant clauses 1.0% (1850188 remain 89%)
c [simplification-6] maximum reduction of 1% = max (0%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 10000
c [simplification-6] penalized conflict interval 10000 = 1 * 10000
c [simplification-6] hard conflict limit 29003 (soft 19003 + delta 10000)
c [simplification-6] new conflict limit 19003 (hard 29003)
c 
c [simplification-7] limit 19003 conflicts (hard 29003) hit after 19003 conflicts
c [quatres-3] found 10732 quaternary clauses 9% in total
c [quatres-3-2] added 255 quaternary resolvents
c [ternres-3] limit 7400752 based on 1850188 irredundant clauses
c [ternres-3] all 40925 free variables schedulable
c [ternres-3] 14 ternary resolvents (0 bin, 14 trn)
c [ternres-3] 9766 variables remain 24% (31159 retained 76%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-2] limit 1850188 based on 1850188 irredundant clauses
c [transred-2] removed 0 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 4 clauses out of 6 (67%) of length 253
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 4 large clauses in 15001518 steps
c [cce-2-1] allowing another 7500759 steps for small clauses
c [cce-2-1] scheduling 1723868 clauses = 1722486 binary + 1382 ternary
c [cce-2-1] tried to eliminate 37 small clauses 0%
c [cce-2-1] eliminated 3 binary clauses 0%
c [cce-2-1] eliminated 3 small clauses 0%
c [cce-2-1] eliminated 3 small clauses in 15000611 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 7 covered clauses in round 1
c [cce-2] eliminated 7 covered clauses in TOTAL during 1 rounds
c [cce-2] 7 < 1/100 * 1850188 = 18501 considered unsuccessful
c [bca-3] limit of 10000000 steps and 3702332 added (scaled 2)
c [bca-3] 77770 out of 81852 literals actually usable 95%
c [bca-3] added 380 blocked clauses in 359048 steps
c [sweep-3] limit 3700362 based on 1850181 irredundant clauses
c [sweep-3-1] 292 pos 2.6% + 10840 neg 97.4% = 11132 sched 27.2% ret 29793
c [sweep-3-1] 3721730 steps 147 queries 927.28 avg class size
c [sweep-3-1] 6692 decisions 140 SAT calls 225.14 avg env size
c [sweep-3-1] 7594 variables remain 19% (33331 retained 81%)
c [decomp-14] removed 8 variables
c [sweep-3-1] removed 8 vars (0 failed, 8 eqs, 18 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 8 vars in TOTAL (1 rounds, 146 queries)
c [sort-queue-7] sorted 36504 enqueued variables after 19003 conflicts
c [score-dist-7] active 4413 (11%), one 0 (0%), zero 36504 (89%)
c [score-dist-7] max exp 516, different 16 (3%)
c [score-dist-7] median active exp 507, avg 507.2
c [simplification-7] removed 8 variables 0.0% (40917 remain 53%)
c [simplification-7] removed 7 irredundant clauses 0.0% (1850181 remain 89%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20000
c [simplification-7] new conflict interval 30000
c [simplification-7] penalized conflict interval 30000 = 1 * 30000
c [simplification-7] hard conflict limit 64003 (soft 49003 + delta 15000)
c [simplification-7] new conflict limit 49003 (hard 64003)
c 
c [simplification-8] limit 49003 conflicts (hard 64003) hit after 49004 conflicts
c [quatres-4] found 10993 quaternary clauses 10% in total
c [quatres-4-2] added 179 quaternary resolvents
c [ternres-4] limit 7400724 based on 1850181 irredundant clauses
c [ternres-4] 9765 schedulable variables 24%
c [ternres-4] 263 ternary resolvents (0 bin, 263 trn)
c [ternres-4] fully completed ternary resolution
c [block-3] scheduling all variables this time
c [block-3] scheduled 40917 variables 100%
c [block-3] limit of 25229633 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 379 blocked clauses
c [block-3] 379 < 1/100 * 1850181 = 18501 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 40917 variables 100%
c [elim-7] limit of 50459266 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 16951 not tried 41% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 45 = 0% variables out of 40917 scheduled
c [elim-7] 45 < 1/100 * 40917 = 409 considered unsuccessful
c [bca-4] limit of 10000000 steps and 3701414 added (scaled 2)
c [bca-4] 77066 out of 81746 literals actually usable 94%
c [bca-4] added 26 blocked clauses in 375575 steps
c [sweep-4] limit 3699254 based on 1849627 irredundant clauses
c [sweep-4-1] 241 pos 3.2% + 7321 neg 96.8% = 7562 sched 18.5% ret 33310
c [sweep-4-1] 3706136 steps 162 queries 721.02 avg class size
c [sweep-4-1] 6765 decisions 156 SAT calls 156.31 avg env size
c [sweep-4-1] 5461 variables remain 13% (35409 retained 87%)
c [decomp-16] removed 9 variables
c [sweep-4-1] removed 9 vars (0 failed, 6 eqs, 23 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 9 vars in TOTAL (1 rounds, 161 queries)
c [sort-queue-8] sorted 35813 enqueued variables after 49004 conflicts
c [score-dist-8] active 5050 (12%), one 0 (0%), zero 35813 (88%)
c [score-dist-8] max exp 517, different 17 (3%)
c [score-dist-8] median active exp 508, avg 508.0
c [simplification-8] removed 54 variables 0.1% (40863 remain 53%)
c [simplification-8] removed 1232 irredundant clauses 0.1% (1848949 remain 89%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 30000
c [simplification-8] new conflict interval 60000
c [simplification-8] penalized conflict interval 60000 = 1 * 60000
c [simplification-8] hard conflict limit 139004 (soft 109004 + delta 30000)
c [simplification-8] new conflict limit 109004 (hard 139004)
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 -   68.8   40863  1848949     61097   24271   5122 22948   67    75   81  90%    615   24   66   42  158%
c -   78.0   40863  1848949     93309   24942   5124 22951   75    93   81  81%    774   26   78   54  146%
c 
c [simplification-9] limit 109004 conflicts (hard 139004) hit after 109007 conflicts
c [quatres-5] found 11095 quaternary clauses 10% in total
c [quatres-5-2] added 181 quaternary resolvents
c [ternres-5] limit 11235958 with penalty 0 = 0 + 0
c [ternres-5] all 40863 free variables schedulable
c [ternres-5] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-5] 1660 variables remain 4% (39203 retained 96%)
c [decomp-17] removed 1 variables
c [simpleprobe-3] 35215 schedulable variables 86%
c [simpleprobe-3] limit 11235958 penalty 2 = 2 + 0
c [simpleprobe-3] 35723 variables remain 87% (5139 retained 13%)
c [simpleprobe-3] removed 0 variables, found 3975 hbrs, 0 units
c [bca-5] limit of 10000000 steps and 3700071 added (scaled 2)
c [bca-5] 76853 out of 81726 literals actually usable 94%
c [bca-5] added 0 blocked clauses in 373449 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 33707870 penalty 0 = 0 + 0
c [sweep-5-1] 207 pos 3.8% + 5252 neg 96.2% = 5459 sched 13.4% ret 35403
c [sweep-5-1] 29286770 steps 1189 queries 153.31 avg class size
c [sweep-5-1] 69689 decisions 1150 SAT calls 172.28 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-19] removed 222 variables
c [sweep-5-1] removed 222 vars (0 failed, 42 eqs, 93 impls)
c [sweep-5-2] 599 pos 1.5% + 40041 neg 98.5% = 40640 sched 100.0% ret 0
c [sweep-5-2] 4444817 steps 175 queries 1370.94 avg class size
c [sweep-5-2] 4524 decisions 169 SAT calls 182.08 avg env size
c [sweep-5-2] 18715 variables remain 46% (21865 retained 54%)
c [decomp-20] removed 70 variables
c [sweep-5-2] removed 70 vars (0 failed, 10 eqs, 31 impls)
c [sweep-5] removed 292 vars in TOTAL (2 rounds, 1362 queries)
c [sort-queue-9] sorted 34271 enqueued variables after 109007 conflicts
c [score-dist-9] active 6299 (16%), one 0 (0%), zero 34271 (84%)
c [score-dist-9] max exp 518, different 18 (3%)
c [score-dist-9] median active exp 507, avg 508.0
c [simplification-9] removed 293 variables 0.7% (40570 remain 52%)
c [simplification-9] removed 28993 irredundant clauses 1.6% (1819956 remain 87%)
c [simplification-9] maximum reduction of 2% = max (1%, 2%)
c [simplification-9] geometric conflict interval increment 20000 = 60000 / 3
c [simplification-9] new conflict interval 80000
c [simplification-9] penalized conflict interval 80000 = 1 * 80000
c [simplification-9] hard conflict limit 229007 (soft 189007 + delta 40000)
c [simplification-9] new conflict limit 189007 (hard 229007)
c 
c [simplification-10] limit 189007 conflicts (hard 229007) hit after 189008 conflicts
c [quatres-6] found 10932 quaternary clauses 10% in total
c [quatres-6-2] added 194 quaternary resolvents
c [ternres-6] limit 18281358 with penalty 0 = 0 + 0
c [ternres-6] 1644 schedulable variables 4%
c [ternres-6] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1142584 penalty 3 = 3 + 0
c [card-4] found 1 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1142584 for elimination
c [card-4] 1 out of 1 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 914067 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 [unhide-4] limit 113747 based on 1819956 irredundant clauses
c [unhide-4-4] 64 units, 7 failed, 547 tauts, 0 hbrs, 75324 literals
c [transred-3] limit 1813329 based on 1813329 irredundant clauses
c [transred-3] removed 0 transitive binary clauses
c [cce-3] limit of 22851698 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 251
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 250
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 249
c [cce-3-1] eliminated 9 clauses out of 11 (82%) of length 248
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 247
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 246
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 22 large clauses in 22863592 steps
c [cce-3-1] allowing another 11431796 steps for small clauses
c [cce-3-1] scheduling 1688707 clauses = 1686342 binary + 2365 ternary
c [cce-3-1] tried to eliminate 123 small clauses 0%
c [cce-3-1] eliminated 11 binary clauses 0%
c [cce-3-1] eliminated 11 small clauses 0%
c [cce-3-1] eliminated 11276 small clauses in 22851712 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 11298 covered clauses in round 1
c [cce-3] eliminated 11298 covered clauses in TOTAL during 1 rounds
c [cce-3] 11298 < 1/100 * 1813329 = 18133 considered unsuccessful
c [sweep-6] limit 5484407 penalty 0 = 0 + 0
c [sweep-6-1] 679 pos 3.6% + 18031 neg 96.4% = 18710 sched 46.2% ret 21793
c [sweep-6-1] 5486958 steps 285 queries 782.68 avg class size
c [sweep-6-1] 11999 decisions 278 SAT calls 199.93 avg env size
c [sweep-6-1] 7202 variables remain 18% (32983 retained 82%)
c [decomp-22] removed 341 variables
c [sweep-6-1] removed 341 vars (0 failed, 7 eqs, 29 impls)
c [sweep-6] removed 341 vars in TOTAL (1 rounds, 284 queries)
c [sort-queue-10] sorted 32373 enqueued variables after 189008 conflicts
c [score-dist-10] active 7789 (19%), one 0 (0%), zero 32373 (81%)
c [score-dist-10] max exp 519, different 19 (4%)
c [score-dist-10] median active exp 509, avg 509.1
c [simplification-10] removed 408 variables 1.0% (40162 remain 52%)
c [simplification-10] removed 52420 irredundant clauses 2.9% (1767536 remain 85%)
c [simplification-10] maximum reduction of 3% = max (1%, 3%)
c [simplification-10] geometric conflict interval increment 20000 = 80000 / 4
c [simplification-10] new conflict interval 100000
c [simplification-10] penalized conflict interval 100000 = 1 * 100000
c [simplification-10] hard conflict limit 339008 (soft 289008 + delta 50000)
c [simplification-10] new conflict limit 289008 (hard 339008)
c 
c [simplification-11] limit 289008 conflicts (hard 339008) hit after 339008 conflicts
c [quatres-7] found 10619 quaternary clauses 11% in total
c [quatres-7-2] added 344 single-self-subsuming ternary resolvents
c [quatres-7-2] added 270 quaternary resolvents
c [ternres-7] limit 31716975 with penalty 0 = 0 + 0
c [ternres-7] all 40162 free variables schedulable
c [ternres-7] 784 ternary resolvents (0 bin, 784 trn)
c [ternres-7] fully completed ternary resolution
c [block-4] scheduling all variables this time
c [block-4] scheduled 40162 variables 100%
c [block-4] limit of 79292437 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 149348 blocked clauses
c [elim-8] 14960 variables 40% will be scheduled this time
c [elim-8] scheduled 14960 variables 40%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3171697505 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 282 variables 1% in round 1 in 231118497 steps
c [elim-8-1] backward subsumption/strengthening limit 231118400
c [elim-8-1-1] backward checking 8367 touched variables 22%
c [elim-8-1-1] incomplete backward checking 8441 remain 101%
c [elim-8-1] subsumed 6 and strengthened 111 clauses in 231119744 steps
c [elim-8-1] rescheduled 813 variables 2% by backward subsumption
c [elim-8-2] eliminated 2 variables 0% in round 2 in 7792783 steps
c [elim-8-2] backward subsumption/strengthening limit 7792700
c [elim-8-2-1] backward checking 8464 touched variables 23%
c [elim-8-2-1] incomplete backward checking 8457 remain 100%
c [elim-8-2] subsumed 0 and strengthened 189 clauses in 7793061 steps
c [elim-8-2] rescheduled 957 variables 3% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 1181186 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 284 = 2% variables out of 14960 scheduled
c [elim-8] 284 < 1/100 * 14960 = 149 considered unsuccessful
c [bca-6] limit of 10000000 steps and 3234049 added (scaled 2)
c [bca-6] 66941 out of 74144 literals actually usable 90%
c [bca-6] added 20822 blocked clauses in 309397 steps
c [sweep-7] limit 9515092 penalty 0 = 0 + 0
c [sweep-7-1] 451 pos 6.6% + 6342 neg 93.4% = 6793 sched 18.3% ret 30278
c [sweep-7-1] 9539575 steps 410 queries 343.40 avg class size
c [sweep-7-1] 20925 decisions 395 SAT calls 189.59 avg env size
c [sweep-7-1] 2817 variables remain 8% (34042 retained 92%)
c [decomp-24] removed 246 variables
c [sweep-7-1] removed 246 vars (0 failed, 15 eqs, 54 impls)
c [sweep-7] removed 246 vars in TOTAL (1 rounds, 409 queries)
c [sort-queue-11] sorted 29024 enqueued variables after 339008 conflicts
c [score-dist-11] active 7801 (21%), one 0 (0%), zero 29024 (79%)
c [score-dist-11] max exp 520, different 20 (4%)
c [score-dist-11] median active exp 509, avg 509.2
c [simplification-11] removed 3337 variables 8.3% (36825 remain 47%)
c [simplification-11] removed 177626 irredundant clauses 10.0% (1589910 remain 76%)
c [simplification-11] maximum reduction of 10% = max (8%, 10%)
c [simplification-11] large reduction 10% >= 5% limit
c [simplification-11] next conflict interval 3390 = min (339008/100, 100000)
c [simplification-11] penalized conflict interval 3390 = 1 * 3390
c [simplification-11] hard conflict limit 352398 (soft 342398 + delta 10000)
c [simplification-11] new conflict limit 342398 (hard 352398)
c 
c [simplification-12] limit 342398 conflicts (hard 352398) hit after 342399 conflicts
c [quatres-8] found 12086 quaternary clauses 12% in total
c [quatres-8-2] added 18 single-self-subsuming ternary resolvents
c [quatres-8-2] added 421 quaternary resolvents
c [ternres-8] limit 31916715 with penalty 0 = 0 + 0
c [ternres-8] all 36825 free variables schedulable
c [ternres-8] 2046 ternary resolvents (0 bin, 2046 trn)
c [ternres-8] fully completed ternary resolution
c [treelook-3] limit 797917 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 37828 literals 51%
c [treelook-3] scheduling used 798038 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 797917 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 939516 steps
c [treelook-3] 37821 literals remain 51%
c [treelook-3] 31460 variables remain to probed next time 85%
c [treelook-3] removed 0 variables, found 6 hbrs
c [unhide-5] limit 199479 with penalty 5 = 2 + 3
c [unhide-5-5] 0 units, 0 failed, 13082 tauts, 0 hbrs, 22250 literals
c [bca-7] limit of 10000000 steps and 3162972 added (scaled 2)
c [bca-7] 66346 out of 73652 literals actually usable 90%
c [bca-7] added 17 blocked clauses in 305944 steps
c [sweep-8] limit 9575014 penalty 0 = 0 + 0
c [sweep-8-1] 215 pos 7.7% + 2588 neg 92.3% = 2803 sched 7.6% ret 34022
c [sweep-8-1] 9578414 steps 413 queries 227.78 avg class size
c [sweep-8-1] 20522 decisions 379 SAT calls 171.58 avg env size
c [sweep-8-1] 1297 variables remain 4% (35283 retained 96%)
c [decomp-27] removed 439 variables
c [sweep-8-1] removed 439 vars (0 failed, 33 eqs, 66 impls)
c [sweep-8] removed 439 vars in TOTAL (1 rounds, 412 queries)
c [sort-queue-12] sorted 28638 enqueued variables after 342399 conflicts
c [score-dist-12] active 7748 (21%), one 0 (0%), zero 28638 (79%)
c [score-dist-12] max exp 520, different 20 (4%)
c [score-dist-12] median active exp 509, avg 509.2
c [simplification-12] removed 439 variables 1.2% (36386 remain 47%)
c [simplification-12] removed 47524 irredundant clauses 3.0% (1542386 remain 74%)
c [simplification-12] maximum reduction of 3% = max (1%, 3%)
c [simplification-12] geometric conflict interval increment 25000 = 100000 / 4
c [simplification-12] new conflict interval 125000
c [simplification-12] penalized conflict interval 125000 = 1 * 125000
c [simplification-12] hard conflict limit 529899 (soft 467399 + delta 62500)
c [simplification-12] new conflict limit 467399 (hard 529899)
c 
c [simplification-13] limit 467399 conflicts (hard 529899) hit after 467400 conflicts
c [quatres-9] found 11897 quaternary clauses 13% in total
c [quatres-9-2] added 236 single-self-subsuming ternary resolvents
c [quatres-9-2] added 376 quaternary resolvents
c [ternres-9] limit 43433555 with penalty 0 = 0 + 0
c [ternres-9] all 36386 free variables schedulable
c [ternres-9] 246 ternary resolvents (0 bin, 246 trn)
c [ternres-9] fully completed ternary resolution
c [basicprobe-3] limit 217167777 penalty 0 = 0 + 0
c [basicprobe-3-0] 286 probes remain 1% after last round
c [basicprobe-3-0] 304 units = 304 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 324 variables, found 44259 hbrs
c [bate-1] eliminated 28 asymmetric tautologies during probing
c [block-5] scheduling all variables this time
c [block-5] scheduled 36062 variables 100%
c [block-5] limit of 217167777 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 164653 blocked clauses
c [bca-8] limit of 10000000 steps and 2687712 added (scaled 2)
c [bca-8] 56863 out of 65268 literals actually usable 87%
c [bca-8] added 0 blocked clauses in 269788 steps
c [sweep-9] limit 13030066 penalty 0 = 0 + 0
c [sweep-9-1] 161 pos 13.2% + 1056 neg 86.8% = 1217 sched 3.7% ret 31416
c [sweep-9-1] 12150713 steps 489 queries 93.24 avg class size
c [sweep-9-1] 25102 decisions 479 SAT calls 152.24 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-29] removed 11 variables
c [sweep-9-1] removed 11 vars (0 failed, 9 eqs, 10 impls)
c [sweep-9-2] 1118 pos 3.4% + 31504 neg 96.6% = 32622 sched 100.0% ret 0
c [sweep-9-2] 890913 steps 29 queries 3569.45 avg class size
c [sweep-9-2] 1300 decisions 28 SAT calls 240.50 avg env size
c [sweep-9-2] 31407 variables remain 96% (1215 retained 4%)
c [sweep-9-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-9] 11 < 1/1000 * 32633 = 32 considered unsuccessful
c [sweep-9] removed 11 vars in TOTAL (2 rounds, 516 queries)
c [sort-queue-13] sorted 23667 enqueued variables after 467400 conflicts
c [score-dist-13] active 8955 (27%), one 0 (0%), zero 23667 (73%)
c [score-dist-13] max exp 520, different 20 (4%)
c [score-dist-13] median active exp 509, avg 509.2
c [simplification-13] removed 3764 variables 10.3% (32622 remain 42%)
c [simplification-13] removed 204867 irredundant clauses 13.3% (1337519 remain 64%)
c [simplification-13] maximum reduction of 13% = max (10%, 13%)
c [simplification-13] large reduction 13% >= 5% limit
c [simplification-13] next conflict interval 4674 = min (467400/100, 125000)
c [simplification-13] penalized conflict interval 4674 = 1 * 4674
c [simplification-13] hard conflict limit 482074 (soft 472074 + delta 10000)
c [simplification-13] new conflict limit 472074 (hard 482074)
c 
c [simplification-14] limit 472074 conflicts (hard 482074) hit after 472074 conflicts
c [quatres-10] found 11841 quaternary clauses 13% in total
c [quatres-10-2] added 209 quaternary resolvents
c [ternres-10] limit 43763679 with penalty 0 = 0 + 0
c [ternres-10] all 32622 free variables schedulable
c [ternres-10] 80 ternary resolvents (0 bin, 80 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1094091 penalty 3 = 3 + 0
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-4] limit 1337519 based on 1337519 irredundant clauses
c [transred-4] removed 9 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 32622 variables 100%
c [block-6] limit of 437636798 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 53 blocked clauses
c [block-6] 53 < 1/100 * 1337515 = 13375 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 273522998 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 225
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 223
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 222
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 221
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 219
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 218
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 206
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 205
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 204
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 203
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 202
c [cce-4-1] eliminated 5 clauses out of 5 (100%) of length 201
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 200
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 194
c [cce-4-1] eliminated 8 clauses out of 12 (67%) of length 188
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 187
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 186
c [cce-4-1] eliminated 5 clauses out of 5 (100%) of length 185
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 184
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 183
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 178
c [cce-4-1] eliminated 3 clauses out of 5 (60%) of length 177
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 176
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 172
c [cce-4-1] eliminated 14 clauses out of 20 (70%) of length 171
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 170
c [cce-4-1] eliminated 5 clauses out of 5 (100%) of length 169
c [cce-4-1] eliminated 3 clauses out of 6 (50%) of length 168
c [cce-4-1] eliminated 1 clauses out of 8 (12%) of length 164
c [cce-4-1] eliminated 2 clauses out of 9 (22%) of length 163
c [cce-4-1] eliminated 7 clauses out of 12 (58%) of length 162
c [cce-4-1] eliminated 1 clauses out of 16 (6%) of length 158
c [cce-4-1] eliminated 6 clauses out of 18 (33%) of length 157
c [cce-4-1] eliminated 12 clauses out of 18 (67%) of length 156
c [cce-4-1] eliminated 17 clauses out of 29 (59%) of length 155
c [cce-4-1] eliminated 8 clauses out of 15 (53%) of length 154
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 153
c [cce-4-1] eliminated 3 clauses out of 14 (21%) of length 152
c [cce-4-1] eliminated 1 clauses out of 23 (4%) of length 150
c [cce-4-1] eliminated 1 clauses out of 26 (4%) of length 148
c [cce-4-1] eliminated 6 clauses out of 10 (60%) of length 143
c [cce-4-1] eliminated 8 clauses out of 14 (57%) of length 142
c [cce-4-1] eliminated 7 clauses out of 11 (64%) of length 141
c [cce-4-1] eliminated 10 clauses out of 39 (26%) of length 140
c [cce-4-1] eliminated 5 clauses out of 15 (33%) of length 139
c [cce-4-1] eliminated 3 clauses out of 20 (15%) of length 138
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 137
c [cce-4-1] eliminated 13 clauses out of 22 (59%) of length 136
c [cce-4-1] eliminated 2 clauses out of 16 (12%) of length 135
c [cce-4-1] eliminated 2 clauses out of 17 (12%) of length 134
c [cce-4-1] eliminated 1 clauses out of 11 (9%) of length 133
c [cce-4-1] eliminated 2 clauses out of 7 (29%) of length 130
c [cce-4-1] eliminated 4 clauses out of 27 (15%) of length 129
c [cce-4-1] eliminated 8 clauses out of 9 (89%) of length 128
c [cce-4-1] eliminated 6 clauses out of 10 (60%) of length 127
c [cce-4-1] eliminated 4 clauses out of 16 (25%) of length 126
c [cce-4-1] eliminated 4 clauses out of 9 (44%) of length 125
c [cce-4-1] eliminated 4 clauses out of 8 (50%) of length 124
c [cce-4-1] eliminated 6 clauses out of 14 (43%) of length 123
c [cce-4-1] eliminated 3 clauses out of 27 (11%) of length 122
c [cce-4-1] eliminated 9 clauses out of 29 (31%) of length 121
c [cce-4-1] eliminated 10 clauses out of 26 (38%) of length 120
c [cce-4-1] eliminated 9 clauses out of 32 (28%) of length 119
c [cce-4-1] eliminated 12 clauses out of 25 (48%) of length 118
c [cce-4-1] eliminated 15 clauses out of 30 (50%) of length 117
c [cce-4-1] eliminated 25 clauses out of 32 (78%) of length 116
c [cce-4-1] eliminated 39 clauses out of 62 (63%) of length 115
c [cce-4-1] eliminated 23 clauses out of 26 (88%) of length 114
c [cce-4-1] eliminated 27 clauses out of 41 (66%) of length 113
c [cce-4-1] eliminated 27 clauses out of 31 (87%) of length 112
c [cce-4-1] eliminated 28 clauses out of 54 (52%) of length 111
c [cce-4-1] eliminated 5 clauses out of 8 (62%) of length 110
c [cce-4-1] eliminated 1 clauses out of 9 (11%) of length 109
c [cce-4-1] eliminated 5 clauses out of 14 (36%) of length 108
c [cce-4-1] eliminated 5 clauses out of 11 (45%) of length 107
c [cce-4-1] eliminated 3 clauses out of 12 (25%) of length 106
c [cce-4-1] eliminated 6 clauses out of 37 (16%) of length 105
c [cce-4-1] eliminated 6 clauses out of 19 (32%) of length 104
c [cce-4-1] eliminated 5 clauses out of 27 (19%) of length 103
c [cce-4-1] eliminated 1 clauses out of 16 (6%) of length 102
c [cce-4-1] eliminated 6 clauses out of 45 (13%) of length 99
c [cce-4-1] eliminated 20 clauses out of 93 (22%) of length 98
c [cce-4-1] eliminated 18 clauses out of 97 (19%) of length 96
c [cce-4-1] eliminated 1 clauses out of 49 (2%) of length 95
c [cce-4-1] eliminated 19 clauses out of 142 (13%) of length 94
c [cce-4-1] eliminated 1 clauses out of 133 (1%) of length 92
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 587 large clauses in 273526360 steps
c [cce-4-1] allowing another 136763180 steps for small clauses
c [cce-4-1] scheduling 1236447 clauses = 1233370 binary + 3077 ternary
c [cce-4-1] tried to eliminate 1550 small clauses 0%
c [cce-4-1] eliminated 65 binary clauses 0%
c [cce-4-1] eliminated 65 small clauses 0%
c [cce-4-1] eliminated 65 small clauses in 273523489 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 652 covered clauses in round 1
c [cce-4] eliminated 652 covered clauses in TOTAL during 1 rounds
c [cce-4] 652 < 1/100 * 1337462 = 13374 considered unsuccessful
c [sort-queue-14] sorted 23666 enqueued variables after 472074 conflicts
c [score-dist-14] active 8955 (27%), one 0 (0%), zero 23666 (73%)
c [score-dist-14] max exp 520, different 20 (4%)
c [score-dist-14] median active exp 509, avg 509.2
c [simplification-14] removed 1 variables 0.0% (32621 remain 42%)
c [simplification-14] removed 709 irredundant clauses 0.1% (1336810 remain 64%)
c [simplification-14] maximum reduction of 0% = max (0%, 0%)
c [simplification-14] full geometric conflict interval increment 125000
c [simplification-14] new conflict interval 250000
c [simplification-14] penalized conflict interval 250000 = 1 * 250000
c [simplification-14] hard conflict limit 847074 (soft 722074 + delta 125000)
c [simplification-14] new conflict limit 722074 (hard 847074)
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 -  287.2   32621  1336810    631641   24179   4871 81006  187   190   72  98%   1024   -6  175  195   90%
c 
c [simplification-15] limit 722074 conflicts (hard 847074) hit after 722075 conflicts
c [quatres-11] found 12050 quaternary clauses 13% in total
c [quatres-11-2] added 136 quaternary resolvents
c [ternres-11] limit 63588437 with penalty 0 = 0 + 0
c [ternres-11] all 32621 free variables schedulable
c [ternres-11] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1987138 penalty 4 = 4 + 0
c [card-5] found 6 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1987138 for elimination
c [card-5] 6 out of 6 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [unhide-6] limit 397427 with penalty 5 = 3 + 2
c [unhide-6-6] 0 units, 0 failed, 1764 tauts, 0 hbrs, 47706 literals
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 32621 variables 100%
c [elim-9] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 5479 not tried 17% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 975 = 3% variables out of 32621 scheduled
c [bca-9] limit of 10000000 steps and 2665786 added (scaled 2)
c [bca-9] 55972 out of 63294 literals actually usable 88%
c [bca-9] added 556 blocked clauses in 247474 steps
c [sweep-10] limit 9538265 penalty 1 = 1 + 0
c [sweep-10-1] 850 pos 2.8% + 29583 neg 97.2% = 30433 sched 96.2% ret 1213
c [sweep-10-1] 9588439 steps 395 queries 383.69 avg class size
c [sweep-10-1] 16364 decisions 393 SAT calls 233.05 avg env size
c [sweep-10-1] 5302 variables remain 17% (26344 retained 83%)
c [decomp-33] removed 5 variables
c [sweep-10-1] removed 5 vars (0 failed, 5 eqs, 62 impls)
c [sweep-10] 5 < 1/1000 * 31646 = 31 considered unsuccessful
c [sweep-10] removed 5 vars in TOTAL (1 rounds, 394 queries)
c [sort-queue-15] sorted 22940 enqueued variables after 722075 conflicts
c [score-dist-15] active 8701 (27%), one 0 (0%), zero 22940 (73%)
c [score-dist-15] max exp 521, different 21 (4%)
c [score-dist-15] median active exp 509, avg 509.4
c [simplification-15] removed 980 variables 3.0% (31641 remain 41%)
c [simplification-15] removed 10273 irredundant clauses 0.8% (1326537 remain 64%)
c [simplification-15] maximum reduction of 3% = max (3%, 1%)
c [simplification-15] geometric conflict interval increment 62500 = 250000 / 4
c [simplification-15] new conflict interval 312500
c [simplification-15] penalized conflict interval 312500 = 1 * 312500
c [simplification-15] hard conflict limit 1190825 (soft 1034575 + delta 156250)
c [simplification-15] new conflict limit 1034575 (hard 1190825)
c 
c [simplification-16] limit 1034575 conflicts (hard 1190825) hit after 1190825 conflicts
c [quatres-12] found 11013 quaternary clauses 12% in total
c [quatres-12-1] removed 2 duplicate quaternary clauses
c [quatres-12-2] added 36 single-self-subsuming ternary resolvents
c [quatres-12-2] added 146 quaternary resolvents
c [transred-5] limit 1326537 based on 1326537 irredundant clauses
c [transred-5] removed 2 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 31641 variables 100%
c [block-7] limit of 400000000 steps penalty 1 = 1 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 1867 blocked clauses
c [block-7] 1867 < 1/100 * 1326536 = 13265 considered unsuccessful
c [bca-10] limit of 10000000 steps and 2662208 added (scaled 2)
c [bca-10] 55381 out of 63246 literals actually usable 88%
c [bca-10] added 1 blocked clauses in 252588 steps
c [sort-queue-16] sorted 22716 enqueued variables after 1190825 conflicts
c [score-dist-16] active 8906 (28%), one 0 (0%), zero 22716 (72%)
c [score-dist-16] max exp 522, different 22 (4%)
c [score-dist-16] median active exp 509, avg 509.8
c [simplification-16] removed 19 variables 0.1% (31622 remain 41%)
c [simplification-16] removed 1868 irredundant clauses 0.1% (1324669 remain 64%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] full geometric conflict interval increment 312500
c [simplification-16] new conflict interval 625000
c [simplification-16] penalized conflict interval 625000 = 1 * 625000
c [simplification-16] hard conflict limit 2128325 (soft 1815825 + delta 312500)
c [simplification-16] new conflict limit 1815825 (hard 2128325)
c 
c [simplification-17] limit 1815825 conflicts (hard 2128325) hit after 1948914 conflicts
c [quatres-13] found 11118 quaternary clauses 12% in total
c [quatres-13-2] added 61 quaternary resolvents
c [ternres-12] limit 63739061 with penalty 1 = 1 + 0
c [ternres-12] all 31622 free variables schedulable
c [ternres-12] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-12] fully completed ternary resolution
c [simpleprobe-4] 27701 schedulable variables 88%
c [simpleprobe-4] limit 25000000 penalty 3 = 3 + 0
c [simpleprobe-4] 21909 variables remain 69% (9713 retained 31%)
c [simpleprobe-4] removed 0 variables, found 1927 hbrs, 0 units
c [transred-6] limit 1324669 based on 1324669 irredundant clauses
c [transred-6] removed 7 transitive binary clauses
c [elim-10] 5465 variables 17% will be scheduled this time
c [elim-10] scheduled 5465 variables 17%
c [elim-10] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 965 not tried 3% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 5 = 0% variables out of 5465 scheduled
c [elim-10] 5 < 1/100 * 5465 = 54 considered unsuccessful
c [bca-11] limit of 10000000 steps and 2660157 added (scaled 2)
c [bca-11] 55121 out of 63236 literals actually usable 87%
c [bca-11] added 6 blocked clauses in 259781 steps
c [sort-queue-17] sorted 22579 enqueued variables after 1948914 conflicts
c [score-dist-17] active 9038 (29%), one 0 (0%), zero 22579 (71%)
c [score-dist-17] max exp 522, different 22 (4%)
c [score-dist-17] median active exp 510, avg 510.0
c [simplification-17] removed 5 variables 0.0% (31617 remain 41%)
c [simplification-17] removed 1026 irredundant clauses 0.1% (1323643 remain 64%)
c [simplification-17] maximum reduction of 0% = max (0%, 0%)
c [simplification-17] full geometric conflict interval increment 625000
c [simplification-17] conflict interval soft limit 1000000 reached
c [simplification-17] new conflict interval 1000000
c [simplification-17] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-17] hard conflict limit 3448914 (soft 2948914 + delta 500000)
c [simplification-17] new conflict limit 2948914 (hard 3448914)
c 
c [simplification-18] limit 2948914 conflicts (hard 3448914) hit after 2974485 conflicts
c [quatres-14] found 11178 quaternary clauses 12% in total
c [quatres-14-2] added 69 quaternary resolvents
c [ternres-13] limit 180152441 with penalty 0 = 0 + 0
c [ternres-13] all 31617 free variables schedulable
c [ternres-13] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-13] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 11 transitive binary clauses
c [bca-12] limit of 10000000 steps and 2660156 added (scaled 2)
c [bca-12] 54757 out of 63236 literals actually usable 87%
c [bca-12] added 4 blocked clauses in 267785 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 135114330 penalty 2 = 2 + 0
c [sweep-11-1] 396 pos 7.5% + 4900 neg 92.5% = 5296 sched 16.8% ret 26321
c [sweep-11-1] 22411571 steps 934 queries 116.50 avg class size
c [sweep-11-1] 49088 decisions 899 SAT calls 182.42 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-38] removed 36 variables
c [sweep-11-1] removed 36 vars (0 failed, 36 eqs, 113 impls)
c [sweep-11-2] 894 pos 2.8% + 30687 neg 97.2% = 31581 sched 100.0% ret 0
c [sweep-11-2] 28080637 steps 1084 queries 159.32 avg class size
c [sweep-11-2] 52905 decisions 1066 SAT calls 190.22 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-39] removed 26 variables
c [sweep-11-2] removed 26 vars (0 failed, 32 eqs, 157 impls)
c [sweep-11-3] 894 pos 2.8% + 30661 neg 97.2% = 31555 sched 100.0% ret 0
c [sweep-11-3] 30735567 steps 1263 queries 153.14 avg class size
c [sweep-11-3] 56651 decisions 1252 SAT calls 185.56 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-40] removed 14 variables
c [sweep-11-3] removed 14 vars (0 failed, 21 eqs, 172 impls)
c [sweep-11] removed 76 vars in TOTAL (3 rounds, 3278 queries)
c [sort-queue-18] sorted 21950 enqueued variables after 2974485 conflicts
c [score-dist-18] active 9591 (30%), one 0 (0%), zero 21950 (70%)
c [score-dist-18] max exp 523, different 23 (4%)
c [score-dist-18] median active exp 509, avg 510.0
c [simplification-18] removed 76 variables 0.2% (31541 remain 41%)
c [simplification-18] removed 139 irredundant clauses 0.0% (1323504 remain 64%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 1000000
c [simplification-18] conflict interval soft limit 1000000 reached
c [simplification-18] new conflict interval 1000000
c [simplification-18] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-18] hard conflict limit 4474485 (soft 3974485 + delta 500000)
c [simplification-18] new conflict limit 3974485 (hard 4474485)
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 -  760.2   31541  1323504   3118558   12861   4454 77132  144   144   67 100%   1024    5  144  140  103%
c -  858.3   31541  1323504   3799578   15742   4456 77132  138   484   70  28%   1024  191  140  135  103%
c -  869.9   31541  1323504   3847475   20973   4456 77132  136   440   75  31%   1024   62  135  136   99%
c -  879.9   31541  1323504   3887635   29459   4456 77132  138   392   83  35%   1024   -3  137  137  100%
c -  889.5   31541  1323504   3922190   26777   4456 77132  138   387   82  36%   1024   -6  136  137   99%
c -  899.4   31541  1323504   3958629   22280   4456 77132  137   359   79  38%   1024  -24  136  137   99%
c -  911.3   31541  1323504   3999837   30162   4456 77132  139   342   86  41%   1024  -21  139  137  101%
c -  921.2   31541  1323504   4034893   28115   4456 77132  138   326   85  42%   1024  -22  137  138  100%
c -  931.8   31541  1323504   4072780   26940   4456 77132  137   303   84  45%   1024  -30  138  138  100%
c -  944.0   31541  1323504   4112979   29470   4456 77132  137   287   87  48%   1024  -29  136  137   99%
c -  956.1   31541  1323504   4153430   28191   4456 77132  137   288   85  48%   1024  -17  137  137  100%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 28 basic ate = 2 trn 7% + 26 lrg 93% in 1 updates
c bcas: 12 count, 24752 added (386 skipped), 3797748 steps
c bkwd: tried 103675 clauses, 207187 lits, 2.00 lits/clause
c bkwd: checked 207102807 occs, 1997.62 occs/clause, 999.59 occs/lit
c bkwd: subsumed 6 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 300 large (0% self)
c blkd: 7 bces, 446440 removed, 72516222 resolutions, 233407808 steps
c blkd: 16557 blocking literals 11%, 6256 pure
c bump: 4247091 bumped seen, 1577507055 lits 371.4 on average
c card: 5 count, 0 units, 0 am1, 32577355 steps
c card: 1 rescheduled, 5 eliminated, 479 resolved, 63 subsumed
c card: 15 at-most-one constraints found, average size 3.33
c card: 15 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: 4 cces, 718 eliminated, 717 ate 100%, 1 abce 0%
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: 8246612 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 73 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 40 decompositions, 420 equivalent 1%
c deco: 3646090 decision-only clauses 86%, 51% reduction
c decs: 26006375 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 10 elims, 44123 eliminated 57%, 111 pure 0%
c elms: 12 rounds, 1.2 rounds/bve
c elms: 26144 small 59%, 11612 large 26%
c elms: 26178 tried small, 26144 succeeded 100%, 34 failed 0%
c elms: 3074 subsumed, 132495 strengthened, 931 blocked
c elms: 5827304 copies, 14787290 resolutions, 523652 ipos
c elms: 31550362 subchks, 18308906 strchks
c gaus: 4 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8893924 steps, 4446962 extr 50%, 0 elim 0%
c glue: 158.8 orig avg, 158.8 real avg, 10.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 76508 = 11813 simple 15% + 64571 trn 84% + 124 lrg 0%, 2341 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4247090 clauses, 169.9 length
c lrnd: 721594080 lits = 1395724746 orig - 674130666 removed 48%
c lrnd: 1362916 uips 32%, 1987160 flips 47%
c mins: 598450 mins 14%, 288 bin 0%, 766 size 0%
c mins: 47646665 poisoned searches, 22727067 hits, 48% hit rate
c mins: 170458591 used twice searches, 62027117 hits, 36% hit rate
c move: moved 435730, 433644 bin 100%, 2086 trn 0%
c otfs: 18994 driving 47%, 21735 restarting 53%
c otfs: str 40729, 39727 red 98%, 1002 irr 2%
c otfs: str 40729, 0 bin 0%, 22 trn 0%, 40707 lrg 100%
c otfs: sub 581, 581 red 100%, 0 irr 0%
c otfs: sub 581, 0 bin 0%, 0 trn 0%, 581 lrg 100%
c phas: 1 computed, 68545 set, 0 pos (0%), 68545 neg (100%)
c prbs: 3 basic, 66094 probed, 441 failed, 0 lifted
c prbs: 4 simple, 153275 probed, 0 failed, 0 eqs
c prbs: 3 treelook, 16 probed, 0 failed, 0 lifted
c prom: 1026 locked 0% out of 1833871 tried
c prps: 3390922264 props, 128 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 14 count, 3008 quat, 637 self1, 0 self2, 11 dup
c queu: 18 sorted, 26006375 next (519801 steps 0.02)
c queu: 1578218575 enq (1886760111 steps 1.20), 1577507404 deq 100%
c redc: 262 clauses 32%, 817 tried 0%, 33 sat 4%
c redc: 1774 lits 22%, 8206 tried 0%, 33 sat 0%
c redc: 75 times jump level reduced, 16.6 levels on average
c reds: 14 count, 304590.6 conflicts per reduce
c reds: 0 memlim 0%, 14 arith 100%
c reds: 395527 collected 82%, 86035 retired 18%
c rmbd: 9825 removed, 750 red 8%
c rsts: 4364 restarts 54%, 3755 skipped 46%
c rsts: 3755 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 18 count, 18 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 4247090 count (7550365 tried 1.8), 3715389 sub out of 4246277 (87.5%)
c swps: 11 count, 15 rounds, 7311 queries (487.4/round)
c swps: 7129 sat calls, 51 unsat (0.3% success rate)
c swps: 353007 decisions 49.5, 1817 conflicts 0.3
c swps; 312.9 avg class size, 184.1 avg environment size
c swps: 0 failed, 862 impls, 231 equivs
c swp0: 2431 type 0 queries, 279 unsat (11.5%), 2377 sat (97.8%)
c swp1: 4880 type 1 queries, 939 unsat (19.2%), 4703 sat (96.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: 60507215 calls to obtain time
c tops: 1555 fixed 2%, 0 its, 0.00 confs/it
c trds: 7 transitive reductions, 29 removed, 0 failed
c trds: 885 nodes, 20840 edges, 11655075 steps
c trim: 5850877 words, 22.3 MB
c trnr: 13 count, 1 bin, 7953 trn, 132525615 steps
c unhd: 6 count, 6 rounds, 20486517 steps
c unhd: 2 non-trivial sccs of average size 2.0
c unhd: 64 units, 64 bin, 0 trn, 0 lrg
c unhd: 7 failed, 7 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 19250 tauts, 7 bin 0%, 257 trn 1%, 2967 lrg 15%
c unhd: 19250 tauts, 16019 stamp 83%, 2322 red 12%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 179650 str, 64 bin 0%, 345 trn 0%, 179241 lrg 100%, 118292 red 66%
c vars: 31541 remaining 41% and 46098 removed 59% out of 77639
c vars: 1555 fixed 2%, 44123 eliminated 57%, 420 equivalent 1%
c vsts: 26352852490 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 7.9 search visits per propagation, 6106.9 per conflict
c wchs: 1318363272 pushed, 87520089 enlarged, 131 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        4249285        395527         86035      79714591      47244909       1908904
c 
c  0 0          3651   0         6   0         0   0  19204634  24   2486533   5      6152   0     0.1
c  1 5           128   0        16   0        89   0    155424   0    104025   0      1392   0     0.0
c  2 6           470   0        93   0       283   0   1385543   2    973107   2      2765   0     0.0
c  3 9          1497   0       744   0       565   1   7231021   9   5487821  12     66751   3     0.1
c  4 14         1809   0      1466   0       245   0    988185   1    749062   2     32567   2     0.2
c  5 21         1213   0       644   0       347   0   3874804   5   2467449   5     27664   1     0.1
c  6 30         3919   0      3050   1       514   1   6208029   8<  3384669   7     27847   1     0.5
c  7 41         2279   0      1492   0       434   1   5756720   7   3449384   7<    18272   1     0.6
c  8 54        22024   1     15319   4      5036   6  14228442  18  11553402  24    201947  11     6.3
c  9 69        78729   2     59564  15      5292   6   4487024   6   3067196   6    440720  23<   17.1
c 10 86        11261   0      6690   2<     1423   2   5554395   7   4788885  10    325142  17     3.6
c 11 126     3960954  93<   304924  77     71004  83< 10362492  13   8539955  18    739079  39   512.0
c 12 230      161351   4      1519   0       803   1    277878   0    193421   0     18606   1    73.0
c 
c avg                 11.0          10.5          10.5           5.7           7.2           9.4
c std                  0.6           1.1           1.4           3.9           3.1           2.1
c 
c  239.298  24% bump
c   39.869   4% block
c   27.440   3% elim
c   17.779   2% probe
c   16.984   2% decide
c   13.338   1% sweep
c    5.844   1% unhide
c 
c   12.870 < 1% rest (below)
c 
c    4.584   0% bca
c    3.939   0% cce
c    2.182   0% quatres
c    1.123   0% gauss
c    0.523   0% ternres
c    0.297   0% card
c    0.221   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    3.478   0% preprocessing     3%
c  125.033  13% inprocessing     97%
c ==================================
c  128.511  13% simplifying
c  870.345  87% search
c ==================================
c  998.857 100% all
c 
c       4264268 conflicts,        4269.1 confs/sec
c            61 ternaries,       69906.0 confs/ternary
c            53 binaries,        80457.9 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            14 reductions,          0.0 redus/sec, 304590.6 confs/reduction
c          4364 restarts,            4.4 rests/sec,    977.1 confs/restart
c      26006375 decisions,       26036.1 decis/sec,      6.1 decis/conflict
c    3390922264 propagations,  3394801.1 props/sec,    130.4 props/decision
c 
c 998.9 seconds, 1050.8 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
