c launch: /data/cnf/sc2014/app/rbcl_xits_08_UNSAT.cnf.bz2
c host: atom30
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/rbcl_xits_08_UNSAT.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/rbcl_xits_08_UNSAT.cnf.bz2
c no embedded options
c found 'p cnf 1278 68055' header
c read 1278 variables, 68055 clauses, 202155 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=5
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 1278 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] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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    1278    68055         0       0      0     0    0     0    4   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 469 at-most-one constraints of average size 3.0
c [card-1] found 283 at-most-two constraints of average size 4.8
c [card-1] using previous limit 2000000 for elimination
c [card-1] 751 out of 752 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 67 variables
c [simpleprobe-1] all 1211 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 67 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 67 variables, found 0 hbrs, 0 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-6] 0 units, 0 failed, 6338 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1144 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 335 variables 29% in round 1 in 932292 steps
c [elim-1-1] backward subsumption/strengthening limit 932200
c [elim-1-1-1] backward checking 869 touched variables 76%
c [elim-1-1-1] incomplete backward checking 822 remain 95%
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 932241 steps
c [elim-1-1] fully rescheduled 809 variables 71%
c [elim-1-2] no variable eliminated in round 2 in 819318 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 335 = 29% variables out of 1144 scheduled
c [phase-count-1] 63813 negative 100.0% of 63836 except 23 0.0%
c [phase-count-1] 56682 positive 88.8% of 63836 except 7154 11.2%
c [phase-count-1] less non-negative clauses 23 than limit 6300 (10.0%)
c [phase-count-1] non-pos/non-neg = 7154/23 = 311.04 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 809 negative 100%
c [sort-queue-1] sorted 809 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 809 (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 469 variables 36.7% (809 remain 63%)
c [simplification-1] removed 4219 irredundant clauses 6.2% (63836 remain 94%)
c [simplification-1] maximum reduction of 37% = max (37%, 6%)
c [simplification-1] large reduction 37% >= 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 [simpleprobe-2] all 809 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 488 variables remain 60% (321 retained 40%)
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 1618 literals 100%
c [treelook-1] scheduling used 250854 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 311664 steps
c [treelook-1] 1583 literals remain 98%
c [treelook-1] 809 variables remain to probed next time 100%
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 631 sched 78%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-0] fully completed probing
c [block-1] scheduling all variables this time
c [block-1] scheduled 809 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 372 blocked clauses
c [block-1] 372 < 1/100 * 63836 = 638 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] completed large round (ATE)
c [cce-1-1] allowing another 127 steps for small clauses
c [cce-1-1] scheduling 63274 clauses = 1651 binary + 61623 ternary
c [cce-1-1] tried to eliminate 3031 small clauses 5%
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 0 covered clauses in round 1
c [cce-1] eliminated 0 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 809 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 5 variables 1% in round 1 in 11123812 steps
c [elim-2-1] backward subsumption/strengthening limit 8876188
c [elim-2-1-1] backward checking 213 touched variables 26%
c [elim-2-1-1] incomplete backward checking 170 remain 80%
c [elim-2-1] subsumed 0 and strengthened 10 clauses in 8877223 steps
c [elim-2] incomplete 45 not tried 6% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 5 = 1% variables out of 809 scheduled
c [elim-2] 5 < 1/100 * 809 = 8 considered unsuccessful
c [bca-1] limit of 10000000 steps and 125970 added (scaled 2)
c [bca-1] 1004 out of 1610 literals actually usable 62%
c [bca-1] added 4 blocked clauses in 3789 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 191 pos 23.8% + 613 neg 76.2% = 804 sched 100.0% ret 0
c [sweep-1-1] 1181408 steps 22 queries 58.18 avg class size
c [sweep-1-1] 1301 decisions 21 SAT calls 148.95 avg env size
c [sweep-1-1] 424 variables remain 53% (380 retained 47%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 21 queries)
c [sort-queue-2] sorted 188 enqueued variables after 1001 conflicts
c [score-dist-2] active 616 (77%), one 0 (0%), zero 188 (23%)
c [score-dist-2] max exp 814, different 128 (16%)
c [score-dist-2] median active exp 792, avg 768.2
c [simplification-2] removed 5 variables 0.6% (804 remain 63%)
c [simplification-2] removed 1101 irredundant clauses 1.7% (62735 remain 92%)
c [simplification-2] maximum reduction of 2% = max (1%, 2%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 6666
c [simplification-2] penalized conflict interval 6666 = 1 * 6666
c [simplification-2] hard conflict limit 17667 (soft 7667 + delta 10000)
c [simplification-2] new conflict limit 7667 (hard 17667)
c 
c [simplification-3] limit 7667 conflicts (hard 17667) hit after 7667 conflicts
c [quatres-1] found 0 quaternary clauses 0% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 804 free variables schedulable
c [ternres-1] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 201 at-most-one constraints of average size 4.3
c [card-2] found 255 at-most-two constraints of average size 4.7
c [card-2] using previous limit 1000000 for elimination
c [card-2] 456 out of 456 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 71 at-most-one constraints, 71 used 100%
c [card-2] exported 1006 binary clauses, 14.2 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 7 xors of average arity 3.0
c [gauss-1] connected 21 occurrences of 15 variables (average 1.4)
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-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-7] 0 units, 0 failed, 357 tauts, 0 hbrs, 1203 literals
c [transred-1] limit 462107 with penalty 0 = 0 + 0
c [transred-1] removed 184 transitive binary clauses
c [bca-2] limit of 10000000 steps and 125972 added (scaled 2)
c [bca-2] 712 out of 1610 literals actually usable 44%
c [bca-2] added 0 blocked clauses in 9181 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 68 pos 16.0% + 356 neg 84.0% = 424 sched 52.7% ret 380
c [sweep-2-1] 1085495 steps 14 queries 57.57 avg class size
c [sweep-2-1] 800 decisions 13 SAT calls 177.69 avg env size
c [sweep-2-1] 310 variables remain 39% (494 retained 61%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 13 queries)
c [sort-queue-3] sorted 105 enqueued variables after 7667 conflicts
c [score-dist-3] active 699 (87%), one 38 (5%), zero 67 (8%)
c [score-dist-3] max exp 593, different 147 (25%)
c [score-dist-3] median active exp 574, avg 531.5
c [simplification-3] removed 0 variables 0.0% (804 remain 63%)
c [simplification-3] removed 0 irredundant clauses 0.0% (62735 remain 92%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 26666
c [simplification-3] penalized conflict interval 26666 = 1 * 26666
c [simplification-3] hard conflict limit 47666 (soft 34333 + delta 13333)
c [simplification-3] new conflict limit 34333 (hard 47666)
c 
c [simplification-4] limit 34333 conflicts (hard 47666) hit after 34334 conflicts
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1126 literals 70%
c [treelook-2] scheduling used 150403 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 151944 steps
c [treelook-2] 1113 literals remain 69%
c [treelook-2] 769 variables remain to probed next time 96%
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 151 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 804 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 0 blocked clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 164 clauses out of 463 (35%) of length 10
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 164 large clauses in 9822898 steps
c [cce-2-1] allowing another 4911449 steps for small clauses
c [cce-2-1] scheduling 61937 clauses = 1573 binary + 60364 ternary
c [cce-2-1] tried to eliminate 938 small clauses 2%
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 164 covered clauses in round 1
c [cce-2] eliminated 164 covered clauses in TOTAL during 1 rounds
c [cce-2] 164 < 1/100 * 62735 = 627 considered unsuccessful
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 804 variables 100%
c [elim-3] limit of 22898166 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 179 not tried 22% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 16 = 2% variables out of 804 scheduled
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 88 pos 28.9% + 217 neg 71.1% = 305 sched 38.7% ret 483
c [sweep-3-1] 1230685 steps 6 queries 84.33 avg class size
c [sweep-3-1] 448 decisions 5 SAT calls 221.00 avg env size
c [sweep-3-1] 291 variables remain 37% (497 retained 63%)
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, 5 queries)
c [sort-queue-4] sorted 113 enqueued variables after 34334 conflicts
c [score-dist-4] active 675 (86%), one 94 (12%), zero 19 (2%)
c [score-dist-4] max exp 607, different 151 (25%)
c [score-dist-4] median active exp 592, avg 534.7
c [simplification-4] removed 16 variables 2.0% (788 remain 62%)
c [simplification-4] removed 188 irredundant clauses 0.3% (62547 remain 92%)
c [simplification-4] maximum reduction of 2% = max (2%, 0%)
c [simplification-4] geometric conflict interval increment 8888 = 26666 / 3
c [simplification-4] new conflict interval 35554
c [simplification-4] penalized conflict interval 35554 = 1 * 35554
c [simplification-4] hard conflict limit 87665 (soft 69888 + delta 17777)
c [simplification-4] new conflict limit 69888 (hard 87665)
c 
c [simplification-5] limit 69888 conflicts (hard 87665) hit after 69890 conflicts
c [quatres-2] found 0 quaternary clauses 0% in total
c [ternres-2] limit 2145840 with penalty 1 = 1 + 0
c [ternres-2] all 788 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 486 variables remain 62% (302 retained 38%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 2 xors of average arity 3.0
c [gauss-2] connected 6 occurrences of 6 variables (average 1.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 [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 117 transitive binary clauses
c [elim-4] 179 variables 23% will be scheduled this time
c [elim-4] scheduled 179 variables 23%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1716672500 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 2 variables 0% in round 1 in 55961224 steps
c [elim-4-1] backward subsumption/strengthening limit 55961200
c [elim-4-1-1] backward checking 374 touched variables 47%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 18 clauses in 31806311 steps
c [elim-4-1] rescheduled 72 variables 9% by backward subsumption
c [elim-4-2] eliminated 1 variables 0% in round 2 in 1162 steps
c [elim-4-2] backward subsumption/strengthening limit 1100
c [elim-4-2-1] backward checking 9 touched variables 1%
c [elim-4-2-1] incomplete backward checking 8 remain 89%
c [elim-4-2] subsumed 0 and strengthened 1 clauses in 1620 steps
c [elim-4-2] rescheduled 8 variables 1% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 321 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 3 = 2% variables out of 179 scheduled
c [elim-4] 3 < 1/100 * 179 = 1 considered unsuccessful
c [bca-3] limit of 10000000 steps and 125588 added (scaled 2)
c [bca-3] 655 out of 1572 literals actually usable 42%
c [bca-3] added 1 blocked clauses in 33549 steps
c [sweep-4] limit 1287504 penalty 0 = 0 + 0
c [sweep-4-1] 105 pos 36.1% + 186 neg 63.9% = 291 sched 37.1% ret 494
c [sweep-4-1] 1430678 steps 9 queries 61.33 avg class size
c [sweep-4-1] 515 decisions 8 SAT calls 157.00 avg env size
c [sweep-4-1] 258 variables remain 33% (527 retained 67%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 8 queries)
c [sort-queue-5] sorted 319 enqueued variables after 69890 conflicts
c [score-dist-5] active 466 (59%), one 311 (40%), zero 8 (1%)
c [score-dist-5] max exp 978, different 91 (9%)
c [score-dist-5] median active exp 971, avg 903.6
c [simplification-5] removed 3 variables 0.4% (785 remain 61%)
c [simplification-5] removed 4 irredundant clauses 0.0% (62543 remain 92%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 35554
c [simplification-5] new conflict interval 71108
c [simplification-5] penalized conflict interval 71108 = 1 * 71108
c [simplification-5] hard conflict limit 176552 (soft 140998 + delta 35554)
c [simplification-5] new conflict limit 140998 (hard 176552)
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 -   17.0     785    62543     92295   22423      7   344   15    24   11  61%    770   -3   15   18   85%
c -   22.8     785    62543    128858   24800      7   344   12    18   16  66%    878   -6   12   16   76%
c -   28.1     785    62543    162850   25668      7   344   12    16   16  74%    937   -5   15   15  105%
c 
c [simplification-6] limit 140998 conflicts (hard 176552) hit after 169557 conflicts
c [card-3] limit 1751377 penalty 2 = 2 + 0
c [card-3] found 199 at-most-one constraints of average size 4.2
c [card-3] found 231 at-most-two constraints of average size 4.7
c [card-3] using previous limit 1751377 for elimination
c [card-3] 429 out of 430 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] generated 90 at-most-one constraints, 90 used 100%
c [card-3] exported 1054 binary clauses, 11.7 per/constraint
c [basicprobe-2] limit 35027548 penalty 1 = 1 + 0
c [basicprobe-2-0] 628 sched 80%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-0] fully completed probing
c [bate-1] eliminated 79 asymmetric tautologies during probing
c [unhide-3] limit 700550 with penalty 2 = 2 + 0
c [unhide-3-9] 0 units, 0 failed, 820 tauts, 0 hbrs, 7153 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 184 transitive binary clauses
c [bca-4] limit of 10000000 steps and 125292 added (scaled 2)
c [bca-4] 652 out of 1572 literals actually usable 41%
c [bca-4] added 0 blocked clauses in 33178 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 42033050 penalty 0 = 0 + 0
c [sweep-5-1] 91 pos 35.3% + 167 neg 64.7% = 258 sched 32.9% ret 527
c [sweep-5-1] 5834170 steps 57 queries 9.16 avg class size
c [sweep-5-1] 2910 decisions 54 SAT calls 105.35 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 236 pos 30.1% + 549 neg 69.9% = 785 sched 100.0% ret 0
c [sweep-5-2] 7544148 steps 66 queries 20.23 avg class size
c [sweep-5-2] 3777 decisions 65 SAT calls 142.85 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-3] 236 pos 30.1% + 549 neg 69.9% = 785 sched 100.0% ret 0
c [sweep-5-3] 8131009 steps 90 queries 14.29 avg class size
c [sweep-5-3] 4818 decisions 87 SAT calls 130.66 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 210 queries)
c [sort-queue-6] sorted 93 enqueued variables after 169557 conflicts
c [score-dist-6] active 692 (88%), one 89 (11%), zero 4 (1%)
c [score-dist-6] max exp 710, different 165 (23%)
c [score-dist-6] median active exp 688, avg 625.3
c [simplification-6] removed 0 variables 0.0% (785 remain 61%)
c [simplification-6] removed 148 irredundant clauses 0.2% (62395 remain 92%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 71108
c [simplification-6] new conflict interval 142216
c [simplification-6] penalized conflict interval 142216 = 1 * 142216
c [simplification-6] hard conflict limit 382881 (soft 311773 + delta 71108)
c [simplification-6] new conflict limit 311773 (hard 382881)
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 -   34.7     785    62395    194354   24967     31   584   42    48   17  88%    970   18   42   23  180%
c -   42.9     785    62395    232303   27004     31   584   32    36   18  89%    994    2   31   28  109%
c -   51.6     785    62395    268286   27086     31   584   29    32   18  90%   1007   -3   25   29   84%
c -   61.5     785    62395    304274   27319     31   584   22    28   28  80%   1014   -6   19   28   69%
c 
c [simplification-7] limit 311773 conflicts (hard 382881) hit after 320342 conflicts
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 157 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 785 variables 100%
c [block-3] limit of 67666996 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 17 blocked clauses
c [block-3] 17 < 1/100 * 62395 = 623 considered unsuccessful
c [cce-3] limit of 33833498 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1881 clauses out of 2862 (66%) of length 10
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 1881 large clauses in 33833608 steps
c [cce-3-1] allowing another 16916804 steps for small clauses
c [cce-3-1] scheduling 58216 clauses = 1281 binary + 56935 ternary
c [cce-3-1] tried to eliminate 918 small clauses 2%
c [cce-3-1] eliminated 4 binary clauses 0%
c [cce-3-1] eliminated 41 ternary clauses 0%
c [cce-3-1] eliminated 45 small clauses 0%
c [cce-3-1] eliminated 45 small clauses in 33833504 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1926 covered clauses in round 1
c [cce-3] eliminated 1926 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 785 variables 100%
c [elim-5] limit of 270667987 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 2 variables 0% in round 1 in 86871580 steps
c [elim-5-1] backward subsumption/strengthening limit 86871500
c [elim-5-1-1] backward checking 18 touched variables 2%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 1573222 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 2 = 0% variables out of 785 scheduled
c [elim-5] 2 < 1/100 * 785 = 7 considered unsuccessful
c [sort-queue-7] sorted 384 enqueued variables after 320342 conflicts
c [score-dist-7] active 399 (51%), one 380 (49%), zero 4 (1%)
c [score-dist-7] max exp 829, different 115 (14%)
c [score-dist-7] median active exp 823, avg 753.7
c [simplification-7] removed 2 variables 0.3% (783 remain 61%)
c [simplification-7] removed 1950 irredundant clauses 3.1% (60445 remain 89%)
c [simplification-7] maximum reduction of 3% = max (0%, 3%)
c [simplification-7] geometric conflict interval increment 35554 = 142216 / 4
c [simplification-7] new conflict interval 177770
c [simplification-7] penalized conflict interval 177770 = 1 * 177770
c [simplification-7] hard conflict limit 586997 (soft 498112 + delta 88885)
c [simplification-7] new conflict limit 498112 (hard 586997)
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 -   74.5     783    60445    340156   27298     79   433   34    41   18  83%   1018    5   26   30   88%
c -   86.9     783    60445    381947   27915     79   433   36    39   30  91%   1021    1   34   33  105%
c -   99.5     783    60445    422150   27446     79   433   39    44   29  90%   1022    4   36   34  104%
c -  108.8     783    60445    465286   28393     79   433   30    33   30  90%   1023   -5   26   33   79%
c -  118.7     783    60445    510013   29343     79   433   29    34   30  85%   1024   -2   29   31   94%
c -  130.6     783    60445    557312   29733     79   433   23    25   30  93%   1024   -7   24   28   87%
c 
c [simplification-8] limit 498112 conflicts (hard 586997) hit after 586997 conflicts
c [quatres-3] found 6 quaternary clauses 0% in total
c [ternres-3] limit 13019958 with penalty 2 = 2 + 0
c [ternres-3] 482 schedulable variables 62%
c [ternres-3] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2603991 penalty 2 = 2 + 0
c [gauss-3] extracted 4 xors of average arity 3.0
c [gauss-3] connected 12 occurrences of 12 variables (average 1.0)
c [gauss-3] limit 2603991 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 471 schedulable variables 60%
c [simpleprobe-3] limit 100000000 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 119 transitive binary clauses
c [bca-5] limit of 10000000 steps and 121392 added (scaled 2)
c [bca-5] 881 out of 1568 literals actually usable 56%
c [bca-5] added 3 blocked clauses in 55922 steps
c [sweep-6] limit 7811975 penalty 1 = 1 + 0
c [sweep-6-1] 187 pos 23.9% + 596 neg 76.1% = 783 sched 100.0% ret 0
c [sweep-6-1] 7895264 steps 45 queries 25.87 avg class size
c [sweep-6-1] 2753 decisions 44 SAT calls 181.11 avg env size
c [sweep-6-1] 101 variables remain 13% (682 retained 87%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 44 queries)
c [sort-queue-8] sorted 234 enqueued variables after 586997 conflicts
c [score-dist-8] active 549 (70%), one 230 (29%), zero 4 (1%)
c [score-dist-8] max exp 959, different 104 (11%)
c [score-dist-8] median active exp 942, avg 904.3
c [simplification-8] removed 0 variables 0.0% (783 remain 61%)
c [simplification-8] removed 0 irredundant clauses 0.0% (60445 remain 89%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 177770
c [simplification-8] new conflict interval 355540
c [simplification-8] penalized conflict interval 355540 = 1 * 355540
c [simplification-8] hard conflict limit 1120307 (soft 942537 + delta 177770)
c [simplification-8] new conflict limit 942537 (hard 1120307)
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 -  140.0     783    60445    598200   29950     80   317   14    35   13  39%   1024    5   13   22   60%
c -  151.0     783    60445    636648   29742     80   317   15    36   18  43%   1024    3   13   19   71%
c -  159.1     783    60445    677659   30037     80   317   14    25   18  57%   1024   -7   10   16   62%
c -  164.4     783    60445    724432   30325     82   317   11    16   18  72%   1024   -9   12   14   83%
c -  170.5     783    60445    773657   32837     84   317   12    16   17  74%   1024   -4   11   13   85%
c -  176.2     783    60445    820095   33890     86   317   38    47   12  82%   1024   23   40   19  208%
c -  185.8     783    60445    865016   33967     86   317   37    44   21  85%   1024    9   35   29  122%
c -  195.9     783    60445    912219   34932     86   317   28    31   21  91%   1024   -5   28   30   92%
c 
c [simplification-9] limit 942537 conflicts (hard 1120307) hit after 942538 conflicts
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 72 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 2147814905 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 45 clauses out of 392 (11%) of length 24
c [cce-4-1] eliminated 22 clauses out of 261 (8%) of length 17
c [cce-4-1] eliminated 1 clauses out of 981 (0%) of length 10
c [cce-4-1] eliminated 23 clauses out of 457 (5%) of length 9
c [cce-4-1] eliminated 1 clauses out of 12 (8%) of length 7
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 92 large clauses in 40136152 steps
c [cce-4-1] allowing another 20068076 steps for small clauses
c [cce-4-1] scheduling 58166 clauses = 1272 binary + 56894 ternary
c [cce-4-1] tried to eliminate 58166 small clauses 100%
c [cce-4-1] eliminated 50 ternary clauses 0%
c [cce-4-1] eliminated 50 small clauses 0%
c [cce-4-1] eliminated 50 small clauses in 782569521 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 142 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 19977052 steps for small clauses
c [cce-4-2] scheduling 58116 clauses = 1272 binary + 56844 ternary
c [cce-4-2] tried to eliminate 58116 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 142 covered clauses in TOTAL during 2 rounds
c [cce-4] 142 < 1/100 * 60445 = 604 considered unsuccessful
c [bca-6] limit of 10000000 steps and 121110 added (scaled 2)
c [bca-6] 679 out of 1568 literals actually usable 43%
c [bca-6] added 0 blocked clauses in 61010 steps
c [sort-queue-9] sorted 388 enqueued variables after 942538 conflicts
c [score-dist-9] active 395 (50%), one 388 (50%), zero 0 (0%)
c [score-dist-9] max exp 912, different 103 (11%)
c [score-dist-9] median active exp 906, avg 785.6
c [simplification-9] removed 0 variables 0.0% (783 remain 61%)
c [simplification-9] removed 142 irredundant clauses 0.2% (60303 remain 89%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 355540
c [simplification-9] new conflict interval 711080
c [simplification-9] penalized conflict interval 711080 = 1 * 711080
c [simplification-9] hard conflict limit 2009158 (soft 1653618 + delta 355540)
c [simplification-9] new conflict limit 1653618 (hard 2009158)
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 -  222.6     783    60303    959030   34872    136   245   33    37   21  89%   1024    2   39   30  127%
c -  235.6     783    60303   1008976   35773    136   245   31    37   21  84%   1024    1   29   31   91%
c -  251.1     783    60303   1061976   35016    136   245   28    31   34  90%   1024   -4   30   31   98%
c -  266.9     783    60303   1114925   34786    136   245   28    31   33  90%   1024   -2   28   30   93%
c -  283.9     783    60303   1171342   36248    136   245   28    37   33  77%   1024    5   27   27  100%
c -  298.0     783    60303   1222149   37010    136   245   32    37   34  87%   1024    3   29   29   99%
c -  309.6     783    60303   1273939   37473    136   245   23    30   34  78%   1024   -3   22   28   81%
c -  323.9     783    60303   1323065   37234    136   245   21    24   34  86%   1024  -10   18   26   71%
c -  337.0     783    60303   1378843   38312    136   245   23    27   34  87%   1024   -3   25   24  103%
c -  350.0     783    60303   1437584   39210    136   245   26    30   34  88%   1024   -0   25   26   95%
c -  367.1     783    60303   1491182   40159    136   245   17    27   34  64%   1024   -2   22   23   96%
c -  386.9     783    60303   1545822   39695    136   245   28    31   60  88%   1024   -1   25   27   92%
c -  407.4     783    60303   1604538   40818    136   245   32    36   23  87%   1024    4   27   28   97%
c -  427.1     783    60303   1663724   40869    136   245   22    24   22  93%   1024   -6   20   26   78%
c 
c [simplification-10] limit 1653618 conflicts (hard 2009158) hit after 1674905 conflicts
c [card-4] limit 11015661 penalty 3 = 3 + 0
c [card-4] found 199 at-most-one constraints of average size 4.2
c [card-4] found 241 at-most-two constraints of average size 4.7
c [card-4] using previous limit 11015661 for elimination
c [card-4] 436 out of 440 constraints (99%) meet size limits
c [card-4] no units found
c [card-4] generated 71 at-most-one constraints, 71 used 100%
c [card-4] exported 873 binary clauses, 12.3 per/constraint
c [unhide-4] limit 2500000 with penalty 3 = 3 + 0
c [unhide-4-13] 0 units, 0 failed, 733 tauts, 0 hbrs, 23850 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 108 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 783 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 5 variables 1% in round 1 in 121563401 steps
c [elim-6-1] backward subsumption/strengthening limit 78436599
c [elim-6-1-1] backward checking 435 touched variables 56%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 18117710 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 5 = 1% variables out of 783 scheduled
c [elim-6] 5 < 1/100 * 783 = 7 considered unsuccessful
c [sort-queue-10] sorted 218 enqueued variables after 1674905 conflicts
c [score-dist-10] active 560 (72%), one 218 (28%), zero 0 (0%)
c [score-dist-10] max exp 720, different 128 (18%)
c [score-dist-10] median active exp 709, avg 657.2
c [simplification-10] removed 5 variables 0.6% (778 remain 61%)
c [simplification-10] removed 299 irredundant clauses 0.5% (60004 remain 88%)
c [simplification-10] maximum reduction of 1% = max (1%, 0%)
c [simplification-10] geometric conflict interval increment 355540 = 711080 / 2
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] hard conflict limit 3174905 (soft 2674905 + delta 500000)
c [simplification-10] new conflict limit 2674905 (hard 3174905)
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 -  445.6     778    60004   1772824   41989    110   291   15    24   14  64%   1024   -4   17   18   95%
c -  453.3     778    60004   1829914   44462    110   291   22    32   14  69%   1024    7   31   16  195%
c -  461.7     778    60004   1885189   46217    111   291   18    30   22  59%   1024    3   19   19  102%
c -  472.1     778    60004   1939432   43676    111   291   21    24   23  87%   1024  -10   21   25   85%
c -  482.7     778    60004   1999856   45207    111   291   18    34   22  54%   1024   -0   15   21   72%
c -  491.9     778    60004   2060368   45375    111   291   16    23   21  69%   1024   -6   14   18   77%
c -  501.4     778    60004   2120121   46550    111   291   13    24   21  53%   1024   -2   12   16   77%
c -  510.9     778    60004   2183719   48102    113   291   23    29   14  81%   1024    5   27   15  177%
c -  524.1     778    60004   2246864   49821    113   291   15    23   23  68%   1024   -2   12   19   66%
c -  537.1     778    60004   2307193   50260    114   291   22    26   16  84%   1024    4   23   17  137%
c -  548.2     778    60004   2370772   48838    115   291   19    27   23  71%   1024    6   35   15  235%
c -  558.3     778    60004   2435753   49523    116   291   11    16   23  73%   1024   -7   11   15   73%
c -  568.2     778    60004   2501657   50747    117   291   17    26   24  65%   1024   -4   15   21   72%
c -  580.4     778    60004   2567790   52184    117   291   14    21   15  65%   1024   -6   14   18   79%
c -  591.6     778    60004   2635344   53685    119   291   17    26   23  66%   1024    2   29   15  188%
c 
c [simplification-11] limit 2674905 conflicts (hard 3174905) hit after 2697398 conflicts
c [treelook-3] limit 7014673 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 1498 literals 96%
c [treelook-3] scheduling used 470607 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 7014673 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 2274026 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 1 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 56 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 778 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 16 blocked clauses
c [block-4] 16 < 1/100 * 60004 = 600 considered unsuccessful
c [bca-7] limit of 10000000 steps and 120480 added (scaled 2)
c [bca-7] 482 out of 1558 literals actually usable 31%
c [bca-7] added 0 blocked clauses in 107544 steps
c [sweep-7] limit 21044019 penalty 2 = 2 + 0
c [sweep-7-1] 25 pos 24.8% + 76 neg 75.2% = 101 sched 13.0% ret 677
c [sweep-7-1] 6754272 steps 32 queries 7.78 avg class size
c [sweep-7-1] 2123 decisions 31 SAT calls 154.55 avg env size
c [sweep-7-1] fully completed sweeping round
c [sweep-7-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7-2] 202 pos 26.0% + 576 neg 74.0% = 778 sched 100.0% ret 0
c [sweep-7-2] 10983394 steps 78 queries 18.49 avg class size
c [sweep-7-2] 4040 decisions 76 SAT calls 129.11 avg env size
c [sweep-7-2] fully completed sweeping round
c [sweep-7-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7-3] 202 pos 26.0% + 576 neg 74.0% = 778 sched 100.0% ret 0
c [sweep-7-3] 3692680 steps 16 queries 80.56 avg class size
c [sweep-7-3] 1151 decisions 15 SAT calls 201.07 avg env size
c [sweep-7-3] 575 variables remain 74% (203 retained 26%)
c [sweep-7-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] removed 0 vars in TOTAL (3 rounds, 123 queries)
c [sort-queue-11] sorted 90 enqueued variables after 2697398 conflicts
c [score-dist-11] active 688 (88%), one 90 (12%), zero 0 (0%)
c [score-dist-11] max exp 748, different 161 (21%)
c [score-dist-11] median active exp 728, avg 658.9
c [simplification-11] removed 0 variables 0.0% (778 remain 61%)
c [simplification-11] removed 16 irredundant clauses 0.0% (59988 remain 88%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] hard conflict limit 4197398 (soft 3697398 + delta 500000)
c [simplification-11] new conflict limit 3697398 (hard 4197398)
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 -  603.1     778    59988   2698616   54215    137   236   14    28   16  51%   1024    4   14   16   88%
c -  614.2     778    59988   2766867   55660    140   236   19    23   24  84%   1024   -0   22   15  153%
c i  620.0     777    59988   2801966   81806    158   241   11    12   29  88%   1024   -9    8   15   54%
c -  625.8     777    59988   2837765   57195    158   241   30    37   22  82% -24732    9   23   21  106%
c -  636.3     777    59988   2902129   56227    158   241   14    21   21  65%  -8622   -6   11   19   58%
c -  649.3     777    59988   2973457   56754    164   241   21    31   21  68%  -2224    7   32   16  199%
c -  660.3     777    59988   3044276   55929    173   241   12    18   21  68%    -78   -5   12   16   75%
c -  672.6     777    59988   3118075   58453    178   241   14    21   35  66%    666   -3   15   16   96%
c -  685.0     777    59988   3193846   61013    180   241   24    32   36  74%    911    4   16   20   78%
c -  698.1     777    59988   3269604   61890    181   241   14    20   22  70%    989   -5   14   17   86%
c -  711.0     777    59988   3343160   62267    182   241   17    25   22  68%   1012    2   18   16  114%
c -  724.1     777    59988   3415557   62869    183   241   18    31   23  58%   1020    1   20   21   92%
c -  738.4     777    59988   3488198   63634    183   241   30    38   25  80%   1023    7   28   22  126%
c -  753.4     777    59988   3564751   64603    183   241   28    34   26  81%   1024    4   22   24   90%
c -  767.0     777    59988   3640368   64777    183   241   16    29   25  55%   1024   -1   16   21   73%
c 
c [simplification-12] limit 3697398 conflicts (hard 4197398) hit after 3700865 conflicts
c [quatres-4] found 227 quaternary clauses 1% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [ternres-4] limit 25000000 with penalty 3 = 3 + 0
c [ternres-4] all 777 free variables schedulable
c [ternres-4] 91 ternary resolvents (0 bin, 91 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] extracted 18 xors of average arity 3.0
c [gauss-4] connected 54 occurrences of 21 variables (average 2.6)
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 26 transitive binary clauses
c [cce-5] limit of 485664359 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 16
c [cce-5-1] eliminated 7 clauses out of 404 (2%) of length 10
c [cce-5-1] eliminated 107 clauses out of 2916 (4%) of length 9
c [cce-5-1] eliminated 11 clauses out of 11 (100%) of length 7
c [cce-5-1] eliminated 8 clauses out of 8 (100%) of length 6
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 134 large clauses in 67964848 steps
c [cce-5-1] allowing another 33982424 steps for small clauses
c [cce-5-1] scheduling 1421 clauses = 1254 binary + 167 ternary
c [cce-5-1] tried to eliminate 1421 small clauses 100%
c [cce-5-1] eliminated 246 binary clauses 20%
c [cce-5-1] eliminated 246 small clauses 17%
c [cce-5-1] eliminated 246 small clauses in 36029654 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 380 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 33315958 steps for small clauses
c [cce-5-2] scheduling 1175 clauses = 1008 binary + 167 ternary
c [cce-5-2] tried to eliminate 1175 small clauses 100%
c [cce-5-2] eliminated 7 binary clauses 1%
c [cce-5-2] eliminated 7 small clauses 1%
c [cce-5-2] eliminated 7 small clauses in 34601595 steps
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 7 covered clauses in round 2
c [cce-5-3] completed large round (ACCE)
c [cce-5-3] allowing another 33331689 steps for small clauses
c [cce-5-3] scheduling 1168 clauses = 1001 binary + 167 ternary
c [cce-5-3] tried to eliminate 1168 small clauses 100%
c [cce-5-3] completed small round (ACCE)
c [cce-5-3] eliminated 0 covered clauses in round 3
c [cce-5] eliminated 387 covered clauses in TOTAL during 3 rounds
c [cce-5] 387 < 1/100 * 59845 = 598 considered unsuccessful
c [sort-queue-12] sorted 120 enqueued variables after 3700865 conflicts
c [score-dist-12] active 657 (85%), one 120 (15%), zero 0 (0%)
c [score-dist-12] max exp 590, different 136 (23%)
c [score-dist-12] median active exp 579, avg 530.8
c [simplification-12] removed 0 variables 0.0% (777 remain 61%)
c [simplification-12] removed 530 irredundant clauses 0.9% (59458 remain 87%)
c [simplification-12] maximum reduction of 1% = max (0%, 1%)
c [simplification-12] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-12] conflict interval soft limit 1000000 reached
c [simplification-12] new conflict interval 1000000
c [simplification-12] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-12] hard conflict limit 5200865 (soft 4700865 + delta 500000)
c [simplification-12] new conflict limit 4700865 (hard 5200865)
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 -  785.2     777    59458   3716276   64750    213   461   15    23   17  67%   1024   -3   14   17   83%
c -  801.2     777    59458   3796540   65720    213   461   14    19   26  73%   1024   -5   13   17   73%
c -  817.1     777    59458   3876234   66384    214   461   23    27   18  85%   1024   -1   19   21   92%
c -  835.7     777    59458   3955776   67809    214   461   29    33   28  88%   1024    3   27   25  108%
c -  854.3     777    59458   4034566   68353    214   461   22    27   29  83%   1024   -0   25   23  109%
c -  875.0     777    59458   4111731   67935    214   461   16    24   47  67%   1024   -4   13   20   66%
c -  895.6     777    59458   4192790   67815    217   461   14    20   46  70%   1024   -6   11   17   66%
c -  913.1     777    59458   4276742   69570    227   461   14    20   46  68%   1024   -3   13   16   83%
c -  932.1     777    59458   4361621   71075    234   461   16    25   27  62%   1024    2   16   15  103%
c -  951.1     777    59458   4446188   72636    240   461   14    22   18  65%   1024   -2   15   16   94%
c -  968.6     777    59458   4531147   73181    241   461   16    23   28  68%   1024   -2   15   17   92%
c -  986.5     777    59458   4616667   74128    244   461   13    19   26  69%   1024   -3   13   15   87%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 79 basic ate = 79 trn 100% + 0 lrg 0% in 1 updates
c bcas: 7 count, 8 added (35 skipped), 304173 steps
c bkwd: tried 102887 clauses, 205745 lits, 2.00 lits/clause
c bkwd: checked 59300183 occs, 576.36 occs/clause, 288.22 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 29 large (0% self)
c blkd: 4 bces, 405 removed, 885500 resolutions, 2704610 steps
c blkd: 433 blocking literals 17%, 0 pure
c bump: 4652546 bumped seen, 283041121 lits 60.8 on average
c card: 4 count, 0 units, 2933 am1, 25173686 steps
c card: 619 rescheduled, 1426 eliminated, 271430 resolved, 5392 subsumed
c card: 1068 at-most-one constraints found, average size 3.71
c card: 1068 at-most-one constraints used 100%, average size 3.71
c card: 1010 at-most-two constraints found, average size 4.73
c card: 1004 at-most-two constraints used 99%, average size 4.73
c cces: 5 cces, 2619 eliminated, 2248 ate 86%, 371 abce 14%
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: 270210 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 48 gcs, 0 rescored clauses, 2447 rescored vars
c dcps: 27 decompositions, 134 equivalent 10%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 6274374 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 366 eliminated 29%, 0 pure 0%
c elms: 12 rounds, 2.0 rounds/bve
c elms: 338 small 92%, 28 large 8%
c elms: 1144 tried small, 338 succeeded 30%, 806 failed 70%
c elms: 1398 subsumed, 28 strengthened, 24 blocked
c elms: 684313 copies, 670476 resolutions, 17445 ipos
c elms: 6152937 subchks, 2298176 strchks
c gaus: 4 extractions, 31 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 23754492 steps, 11877246 extr 50%, 230 elim 0%
c glue: 20.9 orig avg, 20.9 real avg, 4.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1 = 0 simple 0% + 1 trn 100% + 0 lrg 0%, 0 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4652546 clauses, 34.3 length
c lrnd: 159754954 lits = 215656476 orig - 55901522 removed 26%
c lrnd: 996719 uips 21%, 3346663 flips 72%
c mins: 4594065 mins 99%, 0 bin 0%, 58481 size 1%
c mins: 116640666 poisoned searches, 27717778 hits, 24% hit rate
c mins: 299343892 used twice searches, 76042689 hits, 25% hit rate
c move: moved 3938, 498 bin 13%, 3440 trn 87%
c otfs: 35220 driving 36%, 62026 restarting 64%
c otfs: str 97246, 97225 red 100%, 21 irr 0%
c otfs: str 97246, 0 bin 0%, 1 trn 0%, 97245 lrg 100%
c otfs: sub 326, 326 red 100%, 0 irr 0%
c otfs: sub 326, 0 bin 0%, 0 trn 0%, 326 lrg 100%
c phas: 1 computed, 809 set, 0 pos (0%), 809 neg (100%)
c prbs: 2 basic, 2518 probed, 0 failed, 0 lifted
c prbs: 3 simple, 4593 probed, 0 failed, 187 eqs
c prbs: 3 treelook, 1546 probed, 0 failed, 0 lifted
c prom: 484169 locked 17% out of 2832497 tried
c prps: 292719706 props, 47 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 4 count, 0 quat, 1 self1, 0 self2, 0 dup
c queu: 12 sorted, 6274374 next (1806307 steps 0.29)
c queu: 284320605 enq (286294018 steps 1.01), 283041121 deq 100%
c redc: 5234 clauses 3%, 164075 tried 4%, 0 sat 0%
c redc: 11546 lits 0%, 2598965 tried 1%, 0 sat 0%
c redc: 521 times jump level reduced, 1.5 levels on average
c reds: 76 count, 61608.4 conflicts per reduce
c reds: 0 memlim 0%, 76 arith 100%
c reds: 3325065 collected 92%, 281827 retired 8%
c rmbd: 4 removed, 4 red 100%
c rsts: 8004 restarts 78%, 2321 skipped 22%
c rsts: 2321 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 12 count, 12 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 4652546 count (4063170 tried 0.9), 841928 sub out of 4652448 (18.1%)
c swps: 7 count, 11 rounds, 424 queries (38.5/round)
c swps: 419 sat calls, 0 unsat (13.2% success rate)
c swps: 24636 decisions 58.8, 5529 conflicts 13.2
c swps; 24.6 avg class size, 142.5 avg environment size
c swps: 0 failed, 0 impls, 0 equivs
c swp0: 136 type 0 queries, 16 unsat (11.8%), 136 sat (100.0%)
c swp1: 288 type 1 queries, 54 unsat (18.8%), 288 sat (100.0%)
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: 21858988 calls to obtain time
c tops: 1 fixed 0%, 1 its, 4682237.00 confs/it
c trds: 10 transitive reductions, 1174 removed, 0 failed
c trds: 15599 nodes, 16530 edges, 287483 steps
c trim: 6128590 words, 23.4 MB
c trnr: 4 count, 0 bin, 91 trn, 20122635 steps
c unhd: 4 count, 13 rounds, 4083108 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 8248 tauts, 616 bin 7%, 6556 trn 79%, 0 lrg 0%
c unhd: 8248 tauts, 1076 stamp 13%, 5010 red 61%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 32206 str, 0 bin 0%, 0 trn 0%, 32206 lrg 100%, 32069 red 100%
c vars: 777 remaining 61% and 501 removed 39% out of 1278
c vars: 1 fixed 0%, 366 eliminated 29%, 134 equivalent 10%
c vsts: 51293435861 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 175.3 search visits per propagation, 10942.6 per conflict
c wchs: 19066701651 pushed, 1412214 enlarged, 108 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        4652448       3325065        281827      40418729      19728519       3027442
c 
c  0 0         52461   1     31203   1         0   0   3368737   8    798790   4    172459   6     1.2
c  1 5         56970   1     36835   1     10751   4   1532401   4    581465   3     93651   3     0.5
c  2 6        415232   9    298049   9     55627  20  13993863  35   4669913  24    520992  17     2.7
c  3 9        809566  17    616144  19     62193  22   6361499  16<  3420534  17    554205  18     3.7
c  4 14      1135006  24<   815915  25<    63536  23<  6962832  17   4272807  22<   715352  24<    5.0
c  5 21      1198965  26    844866  25     55081  20   5805148  14   3999173  20    672496  22     8.0
c  6 30       770220  17    545071  16     26891  10   2025394   5   1671049   8    262593   9     7.8
c  7 41       199967   4    129770   4      7105   3    347251   1    296886   2     33735   1     3.7
c  8 54        13958   0      7177   0       637   0     21445   0     17776   0      1944   0     0.5
c  9 69          103   0        35   0         6   0       159   0       126   0        15   0     0.0
c 
c avg                  4.3           4.3           3.7           3.0           3.5           3.6
c std                  1.4           1.4           1.5           1.6           1.6           1.6
c 
c   18.807   2% cce
c   17.626   2% bump
c    3.510   0% decide
c 
c    7.392 < 1% rest (below)
c 
c    3.388   0% elim
c    2.287   0% sweep
c    1.899   0% card
c    1.292   0% unhide
c    0.537   0% probe
c    0.371   0% rescore
c    0.303   0% gauss
c    0.239   0% bca
c    0.236   0% block
c    0.161   0% ternres
c    0.062   0% transred
c    0.005   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.515   0% preprocessing     2%
c   29.597   3% inprocessing     98%
c ==================================
c   30.111   3% simplifying
c  969.930  97% search
c ==================================
c 1000.042 100% all
c 
c       4682237 conflicts,        4682.0 confs/sec
c            91 ternaries,       51453.2 confs/ternary
c             5 binaries,       936447.4 confs/binary
c             1 iterations,    4682237.0 confs/iteration
c 
c            76 reductions,          0.1 redus/sec,  61608.4 confs/reduction
c          8004 restarts,            8.0 rests/sec,    585.0 confs/restart
c       6274374 decisions,        6274.1 decis/sec,      1.3 decis/conflict
c     292719706 propagations,   292707.5 props/sec,     46.7 props/decision
c 
c 1000.0 seconds, 99.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
