c launch: /data/cnf/sc2014/app/atco_enc2_opt2_05_4.cnf.bz2
c host: atom21
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/atco_enc2_opt2_05_4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc2_opt2_05_4.cnf.bz2
c no embedded options
c found 'p cnf 14636 386147' header
c read 14636 variables, 386147 clauses, 1652660 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=2
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 14409 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] VMTF (--score=2)
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   14409   371028         0       0      0     0    0     0   23   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 3123 at-most-one constraints of average size 3.0
c [card-1] found 64 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 3186 out of 3187 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1111 variables
c [simpleprobe-1] all 13525 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 257 variables
c [simpleprobe-1] 11195 variables remain 84% (2073 retained 16%)
c [simpleprobe-1] removed 257 variables, found 1950 hbrs, 7 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 59 units, 20 failed, 4789 tauts, 0 hbrs, 63 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 13190 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 3514 variables 27% in round 1 in 15312278 steps
c [elim-1-1] backward subsumption/strengthening limit 4687722
c [elim-1-1-1] backward checking 9376 touched variables 71%
c [elim-1-1-1] incomplete backward checking 9138 remain 97%
c [elim-1-1] subsumed 207 and strengthened 0 clauses in 4687803 steps
c [elim-1] incomplete 24 not tried 0% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 3514 = 27% variables out of 13190 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 322848 negative 93.1% of 346901 except 24053 6.9%
c [phase-count-1] 327524 positive 94.4% of 346901 except 19377 5.6%
c [phase-1] phase bias: 4873 positive 50%, 4803 negative 50%
c [sort-queue-1] sorted 9676 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 9676 (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 4488 variables 31.7% (9676 remain 67%)
c [simplification-1] removed 24127 irredundant clauses 6.5% (346901 remain 93%)
c [simplification-1] maximum reduction of 32% = max (32%, 7%)
c [simplification-1] large reduction 32% >= 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 [decomp-3] removed 19 variables
c [simpleprobe-2] 8210 schedulable variables 85%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 1 variables
c [simpleprobe-2] 7087 variables remain 73% (2569 retained 27%)
c [simpleprobe-2] removed 1 variables, found 199 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6747 literals 35%
c [treelook-1] scheduling used 300077 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 317219 steps
c [treelook-1] 6737 literals remain 35%
c [treelook-1] 5308 variables remain to probed next time 55%
c [treelook-1] removed 0 variables, found 117 hbrs
c [basicprobe-1] limit 2774888 based on 346861 irredundant clauses
c [basicprobe-1-0] 883 probes remain 9% after last round
c [basicprobe-1-0] 12 units = 12 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 14 variables, found 3732 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 1 failed, 1182 tauts, 0 hbrs, 1035 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 9637 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 2452 not tried 25% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 96 = 1% variables out of 9637 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 321272 negative 93.0% of 345277 except 24005 7.0%
c [phase-count-2] 326162 positive 94.5% of 345277 except 19115 5.5%
c [phase-2] phase bias: 0 positive 0%, 4 negative 100%
c [sort-queue-2] sorted 9541 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 1719 (18%), zero 7822 (82%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 135 variables 1.4% (9541 remain 66%)
c [simplification-2] removed 1617 irredundant clauses 0.5% (345277 remain 93%)
c [simplification-2] maximum reduction of 1% = max (1%, 0%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 10000
c [simplification-2] penalized conflict interval 10000 = 1 * 10000
c [simplification-2] hard conflict limit 21001 (soft 11001 + delta 10000)
c [simplification-2] new conflict limit 11001 (hard 21001)
c 
c [simplification-3] limit of 190 binary hit after 190 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1265 at-most-one constraints of average size 3.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1265 out of 1265 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 118 variables
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 1351 tauts, 0 hbrs, 3468 literals
c [elim-3] 2354 variables 25% will be scheduled this time
c [elim-3] scheduled 2354 variables 25%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 1429 not tried 15% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 2354 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 318195 negative 92.7% of 343375 except 25180 7.3%
c [phase-count-3] 323757 positive 94.3% of 343375 except 19618 5.7%
c [phase-3] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-3] sorted 9423 enqueued variables after 5778 conflicts
c [score-dist-3] active 0 (0%), one 2336 (25%), zero 7087 (75%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 118 variables 1.2% (9423 remain 65%)
c [simplification-3] removed 1892 irredundant clauses 0.5% (343375 remain 93%)
c [simplification-3] maximum reduction of 1% = max (1%, 1%)
c [simplification-3] forced so keeping old conflict interval 10000
c [simplification-3] conflict limit remains at 11001 (hard 21001)
c [simplification-3] new binary interval 1000
c 
c [simplification-4] limit 11001 conflicts (hard 21001) hit after 11001 conflicts
c [decomp-7] removed 6 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 3352 literals 18%
c [treelook-2] scheduling used 150525 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 160485 steps
c [treelook-2] 3345 literals remain 18%
c [treelook-2] 2480 variables remain to probed next time 26%
c [treelook-2] removed 0 variables, found 11 hbrs
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 9417 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 483 not tried 5% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 89 = 1% variables out of 9417 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 317554 negative 92.6% of 342759 except 25205 7.4%
c [phase-count-4] 324383 positive 94.6% of 342759 except 18376 5.4%
c [phase-4] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-4] sorted 9328 enqueued variables after 11001 conflicts
c [score-dist-4] active 0 (0%), one 2426 (26%), zero 6902 (74%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 95 variables 1.0% (9328 remain 65%)
c [simplification-4] removed 615 irredundant clauses 0.2% (342759 remain 92%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 20000
c [simplification-4] penalized conflict interval 20000 = 1 * 20000
c [simplification-4] hard conflict limit 41001 (soft 31001 + delta 10000)
c [simplification-4] new conflict limit 31001 (hard 41001)
c 
c [simplification-5] limit 31001 conflicts (hard 41001) hit after 31002 conflicts
c [quatres-1] found 62282 quaternary clauses 27% in total
c [quatres-1-2] added 10 single-self-subsuming ternary resolvents
c [quatres-1-2] added 6 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 9328 free variables schedulable
c [ternres-1] 1023 ternary resolvents (3 bin, 1020 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 134 xors of average arity 2.8
c [gauss-1] connected 381 occurrences of 299 variables (average 1.3)
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 [decomp-9] removed 17 variables
c [basicprobe-2] limit 7492495 penalty 0 = 0 + 0
c [basicprobe-2-0] 821 sched 9%, 18 failed, 2 lifted, 2949 hbrs
c [decomp-10] removed 159 variables
c [basicprobe-2-1] 522 probes remain 6% after last round
c [basicprobe-2-1] 25 units = 23 failed (92%) + 2 lifted (8%)
c [basicprobe-2-1] removed 164 variables, found 3387 hbrs
c [bate-1] eliminated 92 asymmetric tautologies during probing
c [unhide-4] limit 149849 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 10 failed, 1120 tauts, 0 hbrs, 38881 literals
c [transred-1] limit 1498499 with penalty 0 = 0 + 0
c [transred-1] removed 1339 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 9143 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 1182 blocked clauses
c [block-1] 1182 < 1/100 * 341532 = 3415 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 15
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 13
c [cce-1-1] eliminated 152 clauses out of 2904 (5%) of length 12
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 158 large clauses in 30000716 steps
c [cce-1-1] allowing another 15000358 steps for small clauses
c [cce-1-1] scheduling 103260 clauses = 18796 binary + 84464 ternary
c [cce-1-1] tried to eliminate 1031 small clauses 1%
c [cce-1-1] eliminated 2 binary clauses 0%
c [cce-1-1] eliminated 43 ternary clauses 0%
c [cce-1-1] eliminated 45 small clauses 0%
c [cce-1-1] eliminated 45 small clauses in 30000045 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 203 covered clauses in round 1
c [cce-1] eliminated 203 covered clauses in TOTAL during 1 rounds
c [cce-1] 203 < 1/100 * 340324 = 3403 considered unsuccessful
c [elim-5] 361 variables 4% will be scheduled this time
c [elim-5] scheduled 361 variables 4%
c [elim-5] limit of 29969981 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 334 not tried 4% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 0 = 0% variables out of 361 scheduled
c [bca-1] limit of 10000000 steps and 680740 added (scaled 2)
c [bca-1] 15341 out of 18288 literals actually usable 84%
c [bca-1] added 353 blocked clauses in 62625 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 5296 pos 57.9% + 3847 neg 42.1% = 9143 sched 100.0% ret 0
c [sweep-1-1] 1043672 steps 36 queries 1522.11 avg class size
c [sweep-1-1] 1250 decisions 34 SAT calls 81.03 avg env size
c [sweep-1-1] 8834 variables remain 97% (309 retained 3%)
c [decomp-11] removed 14 variables
c [sweep-1-1] removed 14 vars (0 failed, 1 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 14 vars in TOTAL (1 rounds, 35 queries)
c [phase-count-5] 313603 negative 92.2% of 340088 except 26485 7.8%
c [phase-count-5] 321210 positive 94.4% of 340088 except 18878 5.6%
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-5] sorted 9129 enqueued variables after 31002 conflicts
c [score-dist-5] active 0 (0%), one 2419 (26%), zero 6710 (74%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 199 variables 2.1% (9129 remain 63%)
c [simplification-5] removed 2671 irredundant clauses 0.8% (340088 remain 92%)
c [simplification-5] maximum reduction of 2% = max (2%, 1%)
c [simplification-5] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-5] new conflict interval 26666
c [simplification-5] penalized conflict interval 26666 = 1 * 26666
c [simplification-5] hard conflict limit 71001 (soft 57668 + delta 13333)
c [simplification-5] new conflict limit 57668 (hard 71001)
c 
c [simplification-6] limit 57668 conflicts (hard 71001) hit after 57668 conflicts
c [quatres-2] found 62287 quaternary clauses 26% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 10 single-self-subsuming ternary resolvents
c [quatres-2-2] added 3 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 9129 free variables schedulable
c [ternres-2] 18 ternary resolvents (0 bin, 18 trn)
c [ternres-2] 6767 variables remain 74% (2362 retained 26%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 593 at-most-one constraints of average size 3.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 593 out of 593 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 3 variables
c [simpleprobe-3] 6695 schedulable variables 73%
c [simpleprobe-3] limit 14474462 penalty 0 = 0 + 0
c [decomp-13] removed 5 variables
c [simpleprobe-3] 6821 variables remain 75% (2300 retained 25%)
c [simpleprobe-3] removed 5 variables, found 712 hbrs, 0 units
c [unhide-5] limit 723723 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 0 failed, 836 tauts, 0 hbrs, 30542 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 780 transitive binary clauses
c [bca-2] limit of 10000000 steps and 679286 added (scaled 2)
c [bca-2] 14685 out of 18244 literals actually usable 80%
c [bca-2] added 19 blocked clauses in 85443 steps
c [sweep-2] limit 1085584 penalty 0 = 0 + 0
c [sweep-2-1] 5185 pos 58.8% + 3628 neg 41.2% = 8813 sched 96.6% ret 308
c [sweep-2-1] 1115840 steps 12 queries 2502.67 avg class size
c [sweep-2-1] 501 decisions 11 SAT calls 141.64 avg env size
c [sweep-2-1] 8777 variables remain 96% (344 retained 4%)
c [decomp-14] removed 2 variables
c [sweep-2-1] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 2 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-6] 313090 negative 92.3% of 339301 except 26211 7.7%
c [phase-count-6] 320466 positive 94.4% of 339301 except 18835 5.6%
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-6] sorted 9119 enqueued variables after 57668 conflicts
c [score-dist-6] active 0 (0%), one 2904 (32%), zero 6215 (68%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 10 variables 0.1% (9119 remain 63%)
c [simplification-6] removed 787 irredundant clauses 0.2% (339301 remain 91%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 26666
c [simplification-6] new conflict interval 53332
c [simplification-6] penalized conflict interval 53332 = 1 * 53332
c [simplification-6] hard conflict limit 137666 (soft 111000 + delta 26666)
c [simplification-6] new conflict limit 111000 (hard 137666)
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 -   25.3    9119   339301     63507   19677   2541  4083    8    30   26  26%    629   11    7    5  139%
c 
c [simplification-7] limit 111000 conflicts (hard 137666) hit after 111001 conflicts
c [quatres-3] found 62749 quaternary clauses 26% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 21 single-self-subsuming ternary resolvents
c [quatres-3-2] added 11 quaternary resolvents
c [ternres-3] limit 12218483 with penalty 0 = 0 + 0
c [ternres-3] 6760 schedulable variables 74%
c [ternres-3] 117 ternary resolvents (0 bin, 117 trn)
c [ternres-3] 48 variables remain 1% (9071 retained 99%)
c [gauss-2] limit 1221848 penalty 1 = 1 + 0
c [gauss-2] extracted 81 xors of average arity 2.9
c [gauss-2] connected 235 occurrences of 207 variables (average 1.1)
c [gauss-2] limit 1221848 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 34 variables
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 335 transitive binary clauses
c [transred-3] found 27 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 9026 variables 100%
c [block-2] limit of 61092415 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 54 blocked clauses
c [block-2] 54 < 1/100 * 337880 = 3378 considered unsuccessful
c [cce-2] limit of 30546207 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 129 clauses out of 2457 (5%) of length 12
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 129 large clauses in 30546278 steps
c [cce-2-1] allowing another 15273139 steps for small clauses
c [cce-2-1] scheduling 25693 clauses = 18399 binary + 7294 ternary
c [cce-2-1] tried to eliminate 880 small clauses 3%
c [cce-2-1] eliminated 48 binary clauses 0%
c [cce-2-1] eliminated 11 ternary clauses 0%
c [cce-2-1] eliminated 59 small clauses 0%
c [cce-2-1] eliminated 59 small clauses in 30546262 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 188 covered clauses in round 1
c [cce-2] eliminated 188 covered clauses in TOTAL during 1 rounds
c [cce-2] 188 < 1/100 * 335665 = 3356 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 9025 variables 100%
c [elim-6] limit of 122184831 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 709 not tried 8% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 130 = 1% variables out of 9025 scheduled
c [bca-3] limit of 10000000 steps and 665746 added (scaled 2)
c [bca-3] 12880 out of 17792 literals actually usable 72%
c [bca-3] added 29 blocked clauses in 74391 steps
c [sweep-3] limit 3665544 penalty 0 = 0 + 0
c [sweep-3-1] 5079 pos 59.2% + 3494 neg 40.8% = 8573 sched 96.4% ret 322
c [sweep-3-1] 3781937 steps 73 queries 753.93 avg class size
c [sweep-3-1] 3286 decisions 71 SAT calls 105.70 avg env size
c [sweep-3-1] 7515 variables remain 84% (1380 retained 16%)
c [decomp-16] removed 12 variables
c [sweep-3-1] removed 12 vars (0 failed, 5 eqs, 3 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 12 vars in TOTAL (1 rounds, 72 queries)
c [phase-count-7] 306575 negative 92.2% of 332517 except 25942 7.8%
c [phase-count-7] 314227 positive 94.5% of 332517 except 18290 5.5%
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-7] sorted 8883 enqueued variables after 111001 conflicts
c [score-dist-7] active 0 (0%), one 3783 (43%), zero 5100 (57%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 236 variables 2.6% (8883 remain 62%)
c [simplification-7] removed 6784 irredundant clauses 2.0% (332517 remain 90%)
c [simplification-7] maximum reduction of 3% = max (3%, 2%)
c [simplification-7] geometric conflict interval increment 13333 = 53332 / 4
c [simplification-7] new conflict interval 66665
c [simplification-7] penalized conflict interval 66665 = 1 * 66665
c [simplification-7] hard conflict limit 210998 (soft 177666 + delta 33332)
c [simplification-7] new conflict limit 177666 (hard 210998)
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 -   65.0    8883   332517    131556   27128   2728  3751   10    49   26  20%    884   11   10    8  128%
c -   89.5    8883   332517    177316   34888   2928  3787    9    25   45  35%    954  -13    9    8  109%
c 
c [simplification-8] limit 177666 conflicts (hard 210998) hit after 211000 conflicts
c [quatres-4] found 62449 quaternary clauses 25% in total
c [quatres-4-1] removed 5 duplicate quaternary clauses
c [quatres-4-1] added 15 double-self-subsuming ternary resolvents
c [quatres-4-2] added 47 single-self-subsuming ternary resolvents
c [quatres-4-2] added 175 quaternary resolvents
c [ternres-4] limit 32479046 with penalty 0 = 0 + 0
c [ternres-4] 39 schedulable variables 0%
c [ternres-4] 6088 ternary resolvents (134 bin, 5954 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 13 variables
c [unhide-6] limit 3247904 with penalty 1 = 1 + 0
c [unhide-6-7] 4 units, 40 failed, 8020 tauts, 0 hbrs, 71667 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 255 transitive binary clauses
c [transred-4] found 8 units
c [elim-7] 284 variables 3% will be scheduled this time
c [elim-7] scheduled 284 variables 3%
c [elim-7] limit of 649580927 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] no variable eliminated in round 1 in 467112519 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 0 = 0% variables out of 284 scheduled
c [bca-4] limit of 10000000 steps and 645840 added (scaled 2)
c [bca-4] 13031 out of 17582 literals actually usable 74%
c [bca-4] added 35 blocked clauses in 94692 steps
c [sweep-4] limit 9743713 penalty 0 = 0 + 0
c [sweep-4-1] 4435 pos 59.6% + 3005 neg 40.4% = 7440 sched 84.6% ret 1350
c [sweep-4-1] 9966072 steps 139 queries 263.79 avg class size
c [sweep-4-1] 5586 decisions 143 SAT calls 98.89 avg env size
c [sweep-4-1] 5796 variables remain 66% (2988 retained 34%)
c [decomp-18] removed 40 variables
c [sweep-4-1] removed 40 vars (0 failed, 20 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 40 vars in TOTAL (1 rounds, 138 queries)
c [sort-queue-8] sorted 8750 enqueued variables after 211000 conflicts
c [score-dist-8] active 0 (0%), one 3991 (46%), zero 4759 (54%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 133 variables 1.5% (8750 remain 61%)
c [simplification-8] removed 9990 irredundant clauses 3.0% (322527 remain 87%)
c [simplification-8] maximum reduction of 3% = max (1%, 3%)
c [simplification-8] geometric conflict interval increment 16666 = 66665 / 4
c [simplification-8] new conflict interval 83331
c [simplification-8] penalized conflict interval 83331 = 1 * 83331
c [simplification-8] hard conflict limit 335996 (soft 294331 + delta 41665)
c [simplification-8] new conflict limit 294331 (hard 335996)
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 -  114.6    8750   322527    219789   43191   7016  3795    9    19   28  48%    988  -14    9    9  109%
c -  130.6    8750   322527    256991   47449   7067  3806    9    17   28  55%   1003  -11    9    9  106%
c -  146.4    8750   322527    294202   50970   7082  3809    9    15   28  56%   1012   -8    8    9   87%
c 
c [simplification-9] limit 294331 conflicts (hard 335996) hit after 324346 conflicts
c [quatres-5] found 61540 quaternary clauses 25% in total
c [quatres-5-1] removed 19 duplicate quaternary clauses
c [quatres-5-1] added 16 double-self-subsuming ternary resolvents
c [quatres-5-2] added 206 single-self-subsuming ternary resolvents
c [quatres-5-2] added 161 quaternary resolvents
c [ternres-5] limit 54593508 with penalty 0 = 0 + 0
c [ternres-5] all 8750 free variables schedulable
c [ternres-5] 4434 ternary resolvents (29 bin, 4405 trn)
c [ternres-5] 1 variables remain 0% (8749 retained 100%)
c [decomp-19] removed 1 variables
c [treelook-3] limit 1364837 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 11368 literals 65%
c [treelook-3] scheduling used 784454 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1364837 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 1383161 steps
c [treelook-3] 11340 literals remain 65%
c [treelook-3] 2077 variables remain to probed next time 24%
c [treelook-3] removed 2 variables, found 409 hbrs
c [unhide-7] limit 10918701 with penalty 0 = 0 + 0
c [unhide-7-10] 2 units, 19 failed, 5244 tauts, 0 hbrs, 38633 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 248 transitive binary clauses
c [transred-5] found 1 units
c [bca-5] limit of 10000000 steps and 637886 added (scaled 2)
c [bca-5] 12849 out of 17434 literals actually usable 74%
c [bca-5] added 29 blocked clauses in 106822 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 163780520 penalty 0 = 0 + 0
c [sweep-5-1] 3582 pos 62.1% + 2187 neg 37.9% = 5769 sched 66.2% ret 2947
c [sweep-5-1] 61934487 steps 1543 queries 24.17 avg class size
c [sweep-5-1] 44881 decisions 1452 SAT calls 87.62 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-21] removed 249 variables
c [sweep-5-1] removed 249 vars (0 failed, 181 eqs, 54 impls)
c [sweep-5-2] 4935 pos 58.3% + 3532 neg 41.7% = 8467 sched 100.0% ret 0
c [sweep-5-2] 71508724 steps 1626 queries 18.59 avg class size
c [sweep-5-2] 45114 decisions 1574 SAT calls 84.91 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-22] removed 107 variables
c [sweep-5-2] removed 107 vars (0 failed, 102 eqs, 32 impls)
c [sweep-5-3] 4857 pos 58.1% + 3503 neg 41.9% = 8360 sched 100.0% ret 0
c [sweep-5-3] 30358197 steps 511 queries 71.60 avg class size
c [sweep-5-3] 15178 decisions 511 SAT calls 86.13 avg env size
c [sweep-5-3] 3018 variables remain 36% (5333 retained 64%)
c [decomp-23] removed 38 variables
c [sweep-5-3] removed 38 vars (0 failed, 25 eqs, 8 impls)
c [sweep-5] removed 394 vars in TOTAL (3 rounds, 3677 queries)
c [sort-queue-9] sorted 8322 enqueued variables after 324346 conflicts
c [score-dist-9] active 0 (0%), one 4934 (59%), zero 3388 (41%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 428 variables 4.9% (8322 remain 58%)
c [simplification-9] removed 10379 irredundant clauses 3.2% (312148 remain 84%)
c [simplification-9] maximum reduction of 5% = max (5%, 3%)
c [simplification-9] large reduction 5% >= 5% limit
c [simplification-9] next conflict interval 3243 = min (324346/100, 83331)
c [simplification-9] penalized conflict interval 3243 = 1 * 3243
c [simplification-9] hard conflict limit 337589 (soft 327589 + delta 10000)
c [simplification-9] new conflict limit 327589 (hard 337589)
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 -  170.3    8322   312148    326121   51016   9185  8624   10    19   28  50%   1017   -2   11    9  120%
c 
c [simplification-10] limit 327589 conflicts (hard 337589) hit after 337589 conflicts
c [quatres-6] found 60814 quaternary clauses 26% in total
c [quatres-6-1] removed 71 duplicate quaternary clauses
c [quatres-6-1] added 34 double-self-subsuming ternary resolvents
c [quatres-6-2] added 350 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1285 quaternary resolvents
c [ternres-6] limit 57102948 with penalty 0 = 0 + 0
c [ternres-6] 1 schedulable variables 0%
c [ternres-6] 6749 ternary resolvents (434 bin, 6315 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 3568934 penalty 3 = 3 + 0
c [card-4] found 1156 at-most-one constraints of average size 3.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 3568934 for elimination
c [card-4] 1156 out of 1156 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 2855147 penalty 2 = 2 + 0
c [gauss-3] extracted 108 xors of average arity 3.0
c [gauss-3] connected 320 occurrences of 192 variables (average 1.7)
c [gauss-3] limit 2855147 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-24] removed 1 variables
c [basicprobe-3] limit 285514744 penalty 0 = 0 + 0
c [basicprobe-3-0] 554 sched 7%, 39 failed, 0 lifted, 1448 hbrs
c [decomp-25] removed 58 variables
c [basicprobe-3-1] 1354 sched 16%, 29 failed, 0 lifted, 1016 hbrs
c [decomp-26] removed 32 variables
c [basicprobe-3-2] 1356 sched 17%, 15 failed, 0 lifted, 323 hbrs
c [decomp-27] removed 21 variables
c [basicprobe-3-3] 1355 sched 17%, 4 failed, 0 lifted, 102 hbrs
c [decomp-28] removed 6 variables
c [basicprobe-3-4] 1353 sched 16%, 1 failed, 0 lifted, 26 hbrs
c [decomp-29] removed 1 variables
c [basicprobe-3-5] 1353 sched 16%, 1 failed, 0 lifted, 23 hbrs
c [decomp-30] removed 1 variables
c [basicprobe-3-6] 1353 sched 16%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-3-7] 1353 sched 16%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-3-8] 1353 sched 16%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-8] round limit 8 hit
c [basicprobe-3-8] 89 units = 89 failed (100%) + 0 lifted (0%)
c [basicprobe-3-8] removed 119 variables, found 2946 hbrs
c [bate-2] eliminated 1792 asymmetric tautologies during probing
c [unhide-8] limit 11420589 with penalty 0 = 0 + 0
c [unhide-8-14] 0 units, 0 failed, 19956 tauts, 0 hbrs, 18503 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 620 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 8202 variables 100%
c [block-3] limit of 142757372 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1075 blocked clauses
c [block-3] 1075 < 1/100 * 290130 = 2901 considered unsuccessful
c [cce-3] limit of 71378686 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 458 clauses out of 762 (60%) of length 12
c [cce-3-1] eliminated 499 clauses out of 537 (93%) of length 11
c [cce-3-1] eliminated 164 clauses out of 430 (38%) of length 10
c [cce-3-1] eliminated 562 clauses out of 1306 (43%) of length 9
c [cce-3-1] eliminated 115 clauses out of 1704 (7%) of length 8
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 1798 large clauses in 71378766 steps
c [cce-3-1] allowing another 35689383 steps for small clauses
c [cce-3-1] scheduling 86718 clauses = 16113 binary + 70605 ternary
c [cce-3-1] tried to eliminate 2625 small clauses 3%
c [cce-3-1] eliminated 53 binary clauses 0%
c [cce-3-1] eliminated 351 ternary clauses 0%
c [cce-3-1] eliminated 404 small clauses 0%
c [cce-3-1] eliminated 404 small clauses in 71378728 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 2202 covered clauses in round 1
c [cce-3] eliminated 2202 covered clauses in TOTAL during 1 rounds
c [cce-3] 2202 < 1/100 * 289055 = 2890 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 8152 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 138 variables 2% in round 1 in 894862583 steps
c [elim-8-1] backward subsumption/strengthening limit 894862500
c [elim-8-1-1] backward checking 1537 touched variables 19%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1206 and strengthened 549 clauses in 160861745 steps
c [elim-8-1] rescheduled 362 variables 4% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 70934482 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 138 = 2% variables out of 8152 scheduled
c [bca-6] limit of 10000000 steps and 540400 added (scaled 2)
c [bca-6] 10662 out of 16030 literals actually usable 67%
c [bca-6] added 112 blocked clauses in 74858 steps
c [sweep-6] limit 17130884 penalty 0 = 0 + 0
c [sweep-6-1] 1873 pos 63.9% + 1057 neg 36.1% = 2930 sched 36.6% ret 5084
c [sweep-6-1] 17132302 steps 682 queries 19.78 avg class size
c [sweep-6-1] 17831 decisions 680 SAT calls 78.50 avg env size
c [sweep-6-1] 832 variables remain 10% (7180 retained 90%)
c [decomp-33] removed 25 variables
c [sweep-6-1] removed 25 vars (0 failed, 19 eqs, 3 impls)
c [sweep-6] removed 25 vars in TOTAL (1 rounds, 681 queries)
c [sort-queue-10] sorted 7989 enqueued variables after 337589 conflicts
c [score-dist-10] active 0 (0%), one 4861 (61%), zero 3128 (39%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 333 variables 4.0% (7989 remain 55%)
c [simplification-10] removed 42354 irredundant clauses 13.6% (269794 remain 73%)
c [simplification-10] maximum reduction of 14% = max (4%, 14%)
c [simplification-10] large reduction 14% >= 5% limit
c [simplification-10] next conflict interval 3375 = min (337589/100, 83331)
c [simplification-10] penalized conflict interval 3375 = 1 * 3375
c [simplification-10] hard conflict limit 350964 (soft 340964 + delta 10000)
c [simplification-10] new conflict limit 340964 (hard 350964)
c 
c [simplification-11] limit 340964 conflicts (hard 350964) hit after 350965 conflicts
c [quatres-7] found 56110 quaternary clauses 27% in total
c [quatres-7-1] removed 60 duplicate quaternary clauses
c [quatres-7-1] added 8 double-self-subsuming ternary resolvents
c [quatres-7-2] added 98 single-self-subsuming ternary resolvents
c [quatres-7-2] added 489 quaternary resolvents
c [ternres-7] limit 59297449 with penalty 0 = 0 + 0
c [ternres-7] all 7989 free variables schedulable
c [ternres-7] 4107 ternary resolvents (126 bin, 3981 trn)
c [ternres-7] fully completed ternary resolution
c [simpleprobe-4] 5960 schedulable variables 75%
c [simpleprobe-4] limit 200000000 penalty 0 = 0 + 0
c [decomp-35] removed 1 variables
c [simpleprobe-4] 3367 variables remain 42% (4621 retained 58%)
c [simpleprobe-4] removed 1 variables, found 3604 hbrs, 0 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 2023 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 7988 variables 100%
c [elim-9] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 11 not tried 0% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 95 = 1% variables out of 7988 scheduled
c [bca-7] limit of 10000000 steps and 535924 added (scaled 2)
c [bca-7] 10262 out of 15788 literals actually usable 65%
c [bca-7] added 65 blocked clauses in 86580 steps
c [sweep-7] limit 17789234 penalty 0 = 0 + 0
c [sweep-7-1] 592 pos 73.1% + 218 neg 26.9% = 810 sched 10.3% ret 7083
c [sweep-7-1] 9155687 steps 468 queries 9.99 avg class size
c [sweep-7-1] 13279 decisions 462 SAT calls 87.03 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-36] removed 17 variables
c [sweep-7-1] removed 17 vars (0 failed, 10 eqs, 2 impls)
c [sweep-7-2] 4548 pos 57.7% + 3328 neg 42.3% = 7876 sched 100.0% ret 0
c [sweep-7-2] 8729889 steps 188 queries 204.97 avg class size
c [sweep-7-2] 4987 decisions 189 SAT calls 78.31 avg env size
c [sweep-7-2] 5424 variables remain 69% (2452 retained 31%)
c [decomp-37] removed 14 variables
c [sweep-7-2] removed 14 vars (0 failed, 16 eqs, 11 impls)
c [sweep-7] removed 31 vars in TOTAL (2 rounds, 654 queries)
c [sort-queue-11] sorted 7862 enqueued variables after 350965 conflicts
c [score-dist-11] active 0 (0%), one 4891 (62%), zero 2971 (38%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 127 variables 1.6% (7862 remain 55%)
c [simplification-11] removed 2337 irredundant clauses 0.9% (267457 remain 72%)
c [simplification-11] maximum reduction of 2% = max (2%, 1%)
c [simplification-11] geometric conflict interval increment 27777 = 83331 / 3
c [simplification-11] new conflict interval 111108
c [simplification-11] penalized conflict interval 111108 = 1 * 111108
c [simplification-11] hard conflict limit 517627 (soft 462073 + delta 55554)
c [simplification-11] new conflict limit 462073 (hard 517627)
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 -  218.9    7862   267457    373189   51749  15614  8461    9    14   25  62%   1021   -5   10    9  110%
c -  234.5    7862   267457    415387   55565  15630  8464    8    10   25  77%   1022   -6    9    9  101%
c -  250.8    7862   267457    455574   56620  15653  8467   10    17   25  57%   1023    2   10    9  110%
c 
c [simplification-12] limit 462073 conflicts (hard 517627) hit after 462073 conflicts
c [quatres-8] found 56484 quaternary clauses 27% in total
c [quatres-8-1] removed 33 duplicate quaternary clauses
c [quatres-8-1] added 5 double-self-subsuming ternary resolvents
c [quatres-8-2] added 89 single-self-subsuming ternary resolvents
c [quatres-8-2] added 305 quaternary resolvents
c [ternres-8] limit 79727994 with penalty 0 = 0 + 0
c [ternres-8] all 7862 free variables schedulable
c [ternres-8] 1415 ternary resolvents (59 bin, 1356 trn)
c [ternres-8] fully completed ternary resolution
c [unhide-9] limit 7972799 with penalty 1 = 1 + 0
c [unhide-9-17] 0 units, 1 failed, 7016 tauts, 0 hbrs, 14907 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 734 transitive binary clauses
c [elim-10] 10 variables 0% will be scheduled this time
c [elim-10] scheduled 10 variables 0%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] no variable eliminated in round 1 in 128134241 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 0 = 0% variables out of 10 scheduled
c [bca-8] limit of 10000000 steps and 527341 added (scaled 2)
c [bca-8] 10332 out of 15724 literals actually usable 66%
c [bca-8] added 45 blocked clauses in 84881 steps
c [sweep-8] limit 23918398 penalty 0 = 0 + 0
c [sweep-8-1] 3295 pos 60.8% + 2127 neg 39.2% = 5422 sched 69.0% ret 2439
c [sweep-8-1] 23943830 steps 557 queries 31.91 avg class size
c [sweep-8-1] 17536 decisions 572 SAT calls 79.89 avg env size
c [sweep-8-1] 2139 variables remain 27% (5722 retained 73%)
c [decomp-39] removed 33 variables
c [sweep-8-1] removed 33 vars (0 failed, 32 eqs, 12 impls)
c [sweep-8] removed 33 vars in TOTAL (1 rounds, 556 queries)
c [sort-queue-12] sorted 7828 enqueued variables after 462073 conflicts
c [score-dist-12] active 0 (0%), one 4970 (63%), zero 2858 (37%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 34 variables 0.4% (7828 remain 54%)
c [simplification-12] removed 4203 irredundant clauses 1.6% (263254 remain 71%)
c [simplification-12] maximum reduction of 2% = max (0%, 2%)
c [simplification-12] geometric conflict interval increment 37036 = 111108 / 3
c [simplification-12] new conflict interval 148144
c [simplification-12] penalized conflict interval 148144 = 1 * 148144
c [simplification-12] hard conflict limit 684289 (soft 610217 + delta 74072)
c [simplification-12] new conflict limit 610217 (hard 684289)
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 -  271.0    7828   263254    496946   60104  15050  6510    9    18   25  50%   1023    2   11    9  123%
c -  288.3    7828   263254    541257   62230  15063  6511   10    14   25  72%   1024   -1   11    9  124%
c i  298.7    7827   263254    570351   85250  15124  6520    7     9   29  81%   1024   -5    6    9   64%
c -  306.0    7800   263254    587160   65131  15126  6520   10    13   25  74%  -5981   -1   11    9  117%
c i  308.6    7799   263254    595210   71047  15152  6526    8    10   28  83%  -5171   -4    6    9   64%
c i  310.1    7682   263254    599994   74750  15171  6528    8     9   28  84%  -5098   -4    6    9   69%
c i  310.2    7577   263254    600019   74772  15171  6528    7     9   28  84%  -5098   -4    6    9   67%
c i  314.3    7564   263254    612184   83954  15209  6536    8     9   29  81%  -4126   -3    6    9   67%
c i  314.5    7534   263254    612527   84113  15230  6545    7     9   29  82%  -4153   -4    5    9   55%
c i  315.2    7384   263254    614424   85449  15254  6550    7     9   29  81%  -4122   -4    5    9   59%
c i  315.6    7350   263254    615400   86102  15268  6563    7     9   29  81%  -4078   -4    5    9   62%
c i  315.6    7216   263254    615433   86115  15273  6566    7     8   29  81%  -4076   -4    5    9   59%
c i  315.6    7186   263254    615541   86177  15282  6567    7     8   29  81%  -4071   -4    5    9   55%
c i  315.7    7165   263254    615617   86216  15294  6572    7     8   29  81%  -4068   -4    4    9   50%
c i  315.7    7119   263254    615636   86223  15296  6574    7     8   29  81%  -4067   -4    4    9   49%
c i  315.7    7063   263254    615684   86235  15302  6581    7     8   29  81%  -4064   -4    4    9   48%
c i  315.7    5740   263254    615685   86235  15302  6581    7     8   29  81%  -4064   -4    4    9   47%
c i  315.7    5718   263254    615686   86235  15302  6581    7     8   29  81%  -4064   -4    4    9   47%
c i  315.7    5656   263254    615688   86234  15302  6582    7     8   29  81%  -4064   -4    4    9   47%
c 0  315.7    5638   263254    615688   86234  15302  6582    7     8   29  81%  -4064   -4    4    9   47%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 1884 basic ate = 397 trn 21% + 1487 lrg 79% in 2 updates
c bcas: 8 count, 687 added (430 skipped), 670292 steps
c bkwd: tried 82385 clauses, 162808 lits, 1.98 lits/clause
c bkwd: checked 85735591 occs, 1040.67 occs/clause, 526.61 occs/lit
c bkwd: subsumed 0 binary, 449 ternary, 964 large
c bkwd: strengthened 0 binary, 202 ternary (100% self), 347 large (0% self)
c blkd: 3 bces, 2311 removed, 4370348 resolutions, 14338178 steps
c blkd: 1022 blocking literals 3%, 51 pure
c bump: 623231 bumped seen, 27907086 lits 44.8 on average
c card: 4 count, 0 units, 0 am1, 14643357 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 15776 subsumed
c card: 6137 at-most-one constraints found, average size 3.10
c card: 6137 at-most-one constraints used 100%, average size 3.10
c card: 64 at-most-two constraints found, average size 4.00
c card: 63 at-most-two constraints used 98%, average size 4.00
c cces: 3 cces, 2593 eliminated, 2339 ate 90%, 254 abce 10%
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: 2038807 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 70 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 39 decompositions, 1684 equivalent 12%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1864129 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 10 elims, 4113 eliminated 28%, 624 pure 15%
c elms: 12 rounds, 1.2 rounds/bve
c elms: 2478 small 60%, 960 large 23%
c elms: 3348 tried small, 2478 succeeded 74%, 870 failed 26%
c elms: 24352 subsumed, 3055 strengthened, 69 blocked
c elms: 5248386 copies, 6143828 resolutions, 63521 ipos
c elms: 16452386 subchks, 4448430 strchks
c gaus: 3 extractions, 323 extracted, 2.9 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12164548 steps, 6082274 extr 50%, 4112 elim 0%
c glue: 8.9 orig avg, 8.9 real avg, 2.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 25761 = 6465 simple 25% + 19101 trn 74% + 195 lrg 1%, 1431 sub 6%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 623231 clauses, 19.5 length
c lrnd: 12165628 lits = 18285230 orig - 6119602 removed 33%
c lrnd: 182533 uips 29%, 383517 flips 62%
c mins: 616592 mins 99%, 721 bin 0%, 5918 size 1%
c mins: 15286136 poisoned searches, 2682210 hits, 18% hit rate
c mins: 30231394 used twice searches, 2642102 hits, 9% hit rate
c move: moved 5239, 137 bin 3%, 5102 trn 97%
c otfs: 3711 driving 32%, 7856 restarting 68%
c otfs: str 11567, 11326 red 98%, 241 irr 2%
c otfs: str 11567, 0 bin 0%, 307 trn 3%, 11260 lrg 97%
c otfs: sub 157, 115 red 73%, 42 irr 27%
c otfs: sub 157, 0 bin 0%, 51 trn 32%, 106 lrg 68%
c phas: 7 computed, 9681 set, 4873 pos (50%), 4808 neg (50%)
c prbs: 3 basic, 27731 probed, 124 failed, 2 lifted
c prbs: 4 simple, 30072 probed, 8 failed, 250 eqs
c prbs: 3 treelook, 42 probed, 2 failed, 0 lifted
c prom: 141655 locked 11% out of 1237351 tried
c prps: 288506243 props, 151 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 8 count, 2435 quat, 831 self1, 79 self2, 1642 dup
c queu: 12 sorted, 1864129 next (19 steps 0.00)
c queu: 28027572 enq (28027547 steps 1.00), 27907086 deq 100%
c redc: 19900 clauses 11%, 175723 tried 29%, 2 sat 0%
c redc: 27202 lits 1%, 2273239 tried 12%, 2 sat 0%
c redc: 1121 times jump level reduced, 3.8 levels on average
c reds: 13 count, 47360.6 conflicts per reduce
c reds: 0 memlim 0%, 13 arith 100%
c reds: 364021 collected 83%, 75238 retired 17%
c rmbd: 2158 removed, 1096 red 51%
c rsts: 19321 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 12 count, 11 confs 92%, 0 vars 0%
c simp: 0 its 0%, 1 bin 8%, 0 trns 0%
c subl: 623231 count (198245 tried 0.3), 60974 sub out of 619701 (9.8%)
c swps: 8 count, 11 rounds, 5824 queries (529.5/round)
c swps: 5699 sat calls, 287 unsat (2.0% success rate)
c swps: 169429 decisions 29.7, 11254 conflicts 2.0
c swps; 61.0 avg class size, 85.1 avg environment size
c swps: 0 failed, 129 impls, 411 equivs
c swp0: 1938 type 0 queries, 962 unsat (49.6%), 1813 sat (93.6%)
c swp1: 3886 type 1 queries, 2250 unsat (57.9%), 3600 sat (92.6%)
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: 4974964 calls to obtain time
c tops: 3201 fixed 22%, 16 its, 38480.50 confs/it
c trds: 8 transitive reductions, 6334 removed, 36 failed
c trds: 136056 nodes, 169659 edges, 6556955 steps
c trim: 325560 words, 1.2 MB
c trnr: 8 count, 785 bin, 23166 trn, 316639530 steps
c unhd: 9 count, 17 rounds, 56506587 steps
c unhd: 262 non-trivial sccs of average size 2.0
c unhd: 65 units, 65 bin, 0 trn, 0 lrg
c unhd: 91 failed, 84 stamp, 0 lits, 2 bin, 5 trn, 0 lrg
c unhd: 49514 tauts, 798 bin 2%, 11979 trn 24%, 19274 lrg 39%
c unhd: 49514 tauts, 17463 stamp 35%, 19406 red 39%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 217699 str, 65 bin 0%, 1559 trn 1%, 216075 lrg 99%, 202882 red 93%
c vars: 5638 remaining 39% and 8998 removed 61% out of 14636
c vars: 3201 fixed 22%, 4113 eliminated 28%, 1684 equivalent 12%
c vsts: 11135238967 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 38.6 search visits per propagation, 17601.8 per conflict
c wchs: 4266632252 pushed, 12069421 enlarged, 121 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         622136        364021         75238      12708224       4646167        407456
c 
c  0 0         64166  10      7964   2         0   0   7339821  58   2091048  45    145891  36     1.7
c  1 5         54895   9     29951   8      7329  10   1937822  15<   803173  17<    73467  18<    0.5
c  2 6        205605  33<   132994  37     23685  31   2510277  20   1210322  26    131183  32     1.8
c  3 9        224592  36    150309  41<    27801  37<   787942   6    461025  10     49630  12     2.0
c  4 14        64907  10     39383  11     13313  18    121980   1     75265   2      6874   2     0.9
c  5 21         7029   1      3124   1      2663   4      9251   0      4887   0       391   0     0.2
c  6 30          819   0       263   0       394   1       976   0       384   0        17   0     0.0
c  7 41          107   0        31   0        45   0       137   0        57   0         2   0     0.0
c  8 54           15   0         2   0         8   0        17   0         6   0         1   0     0.0
c  9 69            1   0         0   0         0   0         1   0         0   0         0   0     0.0
c 
c avg                  2.3           2.5           2.8           0.8           1.1           1.3
c std                  1.1           0.9           1.0           1.0           1.1           1.1
c 
c   31.056  10% elim
c   10.085   3% sweep
c    6.519   2% probe
c    4.934   2% unhide
c    2.818   1% quatres
c    2.684   1% ternres
c    1.804   1% cce
c    1.185   0% bump
c    1.097   0% decide
c 
c    3.255 < 1% rest (below)
c 
c    1.052   0% block
c    0.897   0% bca
c    0.729   0% transred
c    0.409   0% gauss
c    0.168   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.366   0% preprocessing     2%
c   64.461  20% inprocessing     98%
c ==================================
c   65.827  21% simplifying
c  249.858  79% search
c ==================================
c  315.685 100% all
c 
c        615688 conflicts,        1950.3 confs/sec
c          1514 ternaries,         406.7 confs/ternary
c           681 binaries,          904.1 confs/binary
c            16 iterations,      38480.5 confs/iteration
c 
c            13 reductions,          0.0 redus/sec,  47360.6 confs/reduction
c         19321 restarts,           61.2 rests/sec,     31.9 confs/restart
c       1864129 decisions,        5905.0 decis/sec,      3.0 decis/conflict
c     288506243 propagations,   913904.9 props/sec,    154.8 props/decision
c 
c 315.7 seconds, 77.8 MB
c launch: done
