c launch: /data/cnf/sc2014/app/atco_enc3_opt2_05_21.cnf.bz2
c host: atom32
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_enc3_opt2_05_21.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc3_opt2_05_21.cnf.bz2
c no embedded options
c found 'p cnf 1484061 5933456' header
c read 1484061 variables, 5933456 clauses, 14805254 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 1483680 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0 1483680  5933074         0       0      0     0    0     0  400   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1483268 based on 5933074 irredundant clauses
c [card-1] found 221 at-most-one constraints of average size 3.1
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1483268 for elimination
c [card-1] 221 out of 221 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 218367 variables
c [simpleprobe-1] all 1265694 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 10225566 based on 5112783 irredundant clauses
c [decomp-2] removed 2499 variables
c [simpleprobe-1] 1067219 variables remain 84% (195976 retained 16%)
c [simpleprobe-1] removed 2499 variables, found 11 hbrs, 18 units
c [unhide-1] limit 318927 based on 5102834 irredundant clauses
c [unhide-1-1] 3 units, 352 failed, 4399 tauts, 0 hbrs, 851 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1261329 variables 100%
c [elim-1] limit of 5042721 steps based on 5042721 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 1231734 not tried 98% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 29307 = 2% variables out of 1261329 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 5012531 negative 99.9% of 5015695 except 3164 0.1%
c [phase-count-1] 4988605 positive 99.5% of 5015695 except 27090 0.5%
c [phase-count-1] less non-negative clauses 3164 than limit 501500 (10.0%)
c [phase-count-1] non-pos/non-neg = 27090/3164 = 8.56 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 1232022 negative 100%
c [sort-queue-1] sorted 1232022 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1232022 (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 83102 variables 6.3% (1232022 remain 83%)
c [simplification-1] removed 917379 irredundant clauses 15.5% (5015695 remain 85%)
c [simplification-1] maximum reduction of 15% = max (6%, 15%)
c [simplification-1] large reduction 15% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   20.5 1232021  5015695       419     264     70    35    1    20  357   4%      1   20    7    0 14346%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 189 variables
c [simpleprobe-2] 1040657 schedulable variables 84%
c [simpleprobe-2] limit 10029840 based on 5014920 irredundant clauses
c [decomp-4] removed 103 variables
c [simpleprobe-2] 1040670 variables remain 84% (191060 retained 16%)
c [simpleprobe-2] removed 103 variables, found 307 hbrs, 0 units
c [treelook-1] limit 1253623 based on 5014493 irredundant clauses
c [treelook-1] scheduled 180452 literals 7%
c [treelook-1] scheduling used 1319028 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1253623 based on 5014493 irredundant clauses
c [treelook-1] used 1418927 steps
c [treelook-1] 180312 literals remain 7%
c [treelook-1] 179759 variables remain to probed next time 15%
c [decomp-5] removed 78 variables
c [treelook-1] removed 216 variables, found 393 hbrs
c [basicprobe-1] limit 40107168 based on 5013396 irredundant clauses
c [basicprobe-1-0] 1196 probes remain 0% after last round
c [basicprobe-1-0] 48 units = 48 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1636 variables, found 40794 hbrs
c [unhide-2] limit 313337 based on 5013396 irredundant clauses
c [unhide-2-2] 16 units, 346 failed, 22361 tauts, 0 hbrs, 897 literals
c [elim-2] 1226826 variables 100% will be scheduled this time
c [elim-2] scheduled 1226826 variables 100%
c [elim-2] limit of 28576504 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 1101308 not tried 90% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 125513 = 10% variables out of 1226826 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 4969562 negative 99.9% of 4972989 except 3427 0.1%
c [phase-count-2] 4943626 positive 99.4% of 4972989 except 29363 0.6%
c [phase-count-2] less non-negative clauses 3427 than limit 497200 (10.0%)
c [phase-count-2] non-pos/non-neg = 29363/3427 = 8.57 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 55982 negative 100%
c [sort-queue-2] sorted 1093697 enqueued variables after 1000 conflicts
c [score-dist-2] active 7905 (1%), one 0 (0%), zero 1093697 (99%)
c [score-dist-2] max exp 508, different 8 (2%)
c [score-dist-2] median active exp 503, avg 503.3
c [simplification-2] removed 130418 variables 10.6% (1101602 remain 74%)
c [simplification-2] removed 42706 irredundant clauses 0.9% (4972989 remain 84%)
c [simplification-2] maximum reduction of 11% = max (11%, 1%)
c [simplification-2] large reduction 11% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3001 conflicts
c [card-2] limit 1243247 based on 4972989 irredundant clauses
c [card-2] found 168 at-most-one constraints of average size 3.2
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1243247 for elimination
c [card-2] 168 out of 168 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 115 variables
c [treelook-2] limit 1243170 based on 4972681 irredundant clauses
c [treelook-2] scheduled 184455 literals 8%
c [treelook-2] scheduling used 1248141 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1243170 based on 4972681 irredundant clauses
c [treelook-2] used 1366910 steps
c [treelook-2] 183591 literals remain 8%
c [treelook-2] 13559 variables remain to probed next time 1%
c [decomp-7] removed 36 variables
c [treelook-2] removed 680 variables, found 602 hbrs
c [unhide-3] limit 310593 based on 4969497 irredundant clauses
c [unhide-3-3] 1 units, 149 failed, 15875 tauts, 0 hbrs, 2769 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1100315 variables 100%
c [elim-3] limit of 69658023 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 823753 not tried 75% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 275781 = 25% variables out of 1100315 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 4930628 negative 99.9% of 4934061 except 3433 0.1%
c [phase-count-3] 4905651 positive 99.4% of 4934061 except 28410 0.6%
c [phase-count-3] less non-negative clauses 3433 than limit 493400 (10.0%)
c [phase-count-3] non-pos/non-neg = 28410/3433 = 8.28 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 30852 negative 100%
c [sort-queue-3] sorted 815413 enqueued variables after 3001 conflicts
c [score-dist-3] active 9121 (1%), one 0 (0%), zero 815413 (99%)
c [score-dist-3] max exp 511, different 11 (2%)
c [score-dist-3] median active exp 504, avg 504.9
c [simplification-3] removed 277068 variables 25.2% (824534 remain 56%)
c [simplification-3] removed 38928 irredundant clauses 0.8% (4934061 remain 83%)
c [simplification-3] maximum reduction of 25% = max (25%, 1%)
c [simplification-3] large reduction 25% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15001 (soft 5001 + delta 10000)
c [simplification-3] new conflict limit 5001 (hard 15001)
c 
c [simplification-4] limit 5001 conflicts (hard 15001) hit after 5001 conflicts
c [decomp-8] removed 41 variables
c [basicprobe-2] limit 39471824 based on 4933978 irredundant clauses
c [basicprobe-2-0] 597 probes remain 0% after last round
c [basicprobe-2-0] 95 units = 95 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1064 variables, found 11263 hbrs
c [unhide-4] limit 308373 based on 4933978 irredundant clauses
c [unhide-4-4] 3 units, 1625 failed, 4575 tauts, 0 hbrs, 7024 literals
c [elim-4] 821689 variables 100% will be scheduled this time
c [elim-4] scheduled 821689 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 2364127485 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 1654 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 74208 = 9% variables out of 821689 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 4877751 negative 99.9% of 4881929 except 4178 0.1%
c [phase-count-4] 4852925 positive 99.4% of 4881929 except 29004 0.6%
c [phase-count-4] less non-negative clauses 4178 than limit 488100 (10.0%)
c [phase-count-4] non-pos/non-neg = 29004/4178 = 6.94 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 21200 negative 100%
c [sort-queue-4] sorted 740020 enqueued variables after 5001 conflicts
c [score-dist-4] active 8248 (1%), one 0 (0%), zero 740020 (99%)
c [score-dist-4] max exp 512, different 12 (2%)
c [score-dist-4] median active exp 505, avg 505.6
c [simplification-4] removed 76266 variables 9.2% (748268 remain 50%)
c [simplification-4] removed 52132 irredundant clauses 1.1% (4881929 remain 82%)
c [simplification-4] maximum reduction of 9% = max (9%, 1%)
c [simplification-4] large reduction 9% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 17001 (soft 7001 + delta 10000)
c [simplification-4] new conflict limit 7001 (hard 17001)
c 
c [simplification-5] limit 7001 conflicts (hard 17001) hit after 7001 conflicts
c [quatres-1] found 917794 quaternary clauses 100% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 13 single-self-subsuming ternary resolvents
c [quatres-1-2] added 69 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 40003422 with penalty 2 = 0 + 2
c [ternres-1] all 748268 free variables schedulable
c [ternres-1] 1270 ternary resolvents (0 bin, 1270 trn)
c [ternres-1] 711052 variables remain 95% (37216 retained 5%)
c [gauss-1] limit 2440964 based on 4881929 irredundant clauses
c [gauss-1] extracted 27 xors of average arity 2.0
c [gauss-1] connected 55 occurrences of 51 variables (average 1.1)
c [gauss-1] limit 2440964 based on 4881929 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 274 variables
c [simpleprobe-3] 632201 schedulable variables 85%
c [simpleprobe-3] limit 32002738 penalty 2 = 0 + 2
c [decomp-10] removed 4 variables
c [simpleprobe-3] 602739 variables remain 81% (145251 retained 19%)
c [simpleprobe-3] removed 4 variables, found 1175 hbrs, 0 units
c [unhide-5] limit 400034 with penalty 4 = 0 + 4
c [unhide-5-5] 0 units, 21 failed, 10675 tauts, 0 hbrs, 6930 literals
c [transred-1] limit 4870038 based on 4870038 irredundant clauses
c [transred-1] removed 3 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 747887 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 800068465 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 2500 blocked clauses
c [block-1] 2500 < 1/100 * 4870035 = 48700 considered unsuccessful
c [cce-1] limit of 40003423 steps penalty 2 = 0 + 2
c [cce-1-1] eliminated 1 clauses out of 20 (5%) of length 7
c [cce-1-1] eliminated 39 clauses out of 306 (13%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 40 large clauses in 40003423 steps
c [cce-1-1] allowing another 20001711 steps for small clauses
c [cce-1-1] scheduling 2131271 clauses = 1540704 binary + 590567 ternary
c [cce-1-1] tried to eliminate 117 small clauses 0%
c [cce-1-1] eliminated 2 binary clauses 0%
c [cce-1-1] eliminated 2 small clauses 0%
c [cce-1-1] eliminated 2 small clauses in 40003425 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 42 covered clauses in round 1
c [cce-1] eliminated 42 covered clauses in TOTAL during 1 rounds
c [cce-1] 42 < 1/100 * 4866892 = 48668 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 747887 variables 100%
c [elim-5] limit of 160013693 steps penalty 2 = 0 + 2
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 202069 not tried 27% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2028 = 0% variables out of 747887 scheduled
c [elim-5] 2028 < 1/100 * 747887 = 7478 considered unsuccessful
c [bca-1] limit of 10000000 steps and 9728838 added (scaled 2)
c [bca-1] 1489305 out of 1491720 literals actually usable 100%
c [bca-1] added 74 blocked clauses in 2982550 steps
c [sweep-1] limit 9728338 based on 4864169 irredundant clauses
c [sweep-1-1] 385193 pos 51.6% + 360666 neg 48.4% = 745859 sched 100.0% ret 0
c [sweep-1-1] 9916716 steps 40 queries 178829.73 avg class size
c [sweep-1-1] 395 decisions 35 SAT calls 49.23 avg env size
c [sweep-1-1] 745686 variables remain 100% (173 retained 0%)
c [decomp-11] removed 9 variables
c [sweep-1-1] removed 9 vars (0 failed, 4 eqs, 5 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 9 vars in TOTAL (1 rounds, 39 queries)
c [phase-count-5] 4859976 negative 99.9% of 4864167 except 4191 0.1%
c [phase-count-5] 4835589 positive 99.4% of 4864167 except 28578 0.6%
c [phase-count-5] less non-negative clauses 4191 than limit 486400 (10.0%)
c [phase-count-5] non-pos/non-neg = 28578/4191 = 6.82 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 19912 negative 100%
c [sort-queue-5] sorted 737683 enqueued variables after 7001 conflicts
c [score-dist-5] active 8167 (1%), one 0 (0%), zero 737683 (99%)
c [score-dist-5] max exp 513, different 13 (3%)
c [score-dist-5] median active exp 506, avg 506.1
c [simplification-5] removed 2418 variables 0.3% (745850 remain 50%)
c [simplification-5] removed 17762 irredundant clauses 0.4% (4864167 remain 82%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 20000
c [simplification-5] new conflict interval 20000
c [simplification-5] penalized conflict interval 20000 = 1 * 20000
c [simplification-5] hard conflict limit 37001 (soft 27001 + delta 10000)
c [simplification-5] new conflict limit 27001 (hard 37001)
c 
c [simplification-6] limit 27001 conflicts (hard 37001) hit after 27001 conflicts
c [quatres-2] found 916035 quaternary clauses 100% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 27 single-self-subsuming ternary resolvents
c [quatres-2-2] added 40 quaternary resolvents
c [ternres-2] limit 28854691 with penalty 2 = 0 + 2
c [ternres-2] 708761 schedulable variables 95%
c [ternres-2] 1103 ternary resolvents (0 bin, 1103 trn)
c [ternres-2] 681396 variables remain 91% (64454 retained 9%)
c [card-3] limit 3606836 penalty 4 = 2 + 2
c [card-3] found 443 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 3606836 for elimination
c [card-3] 443 out of 443 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [treelook-3] limit 2885469 penalty 2 = 0 + 2 boost 1
c [treelook-3] scheduled 285357 literals 19%
c [treelook-3] scheduling used 2885472 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 2885469 penalty 2 = 0 + 2 boost 1
c [treelook-3] used 2895924 steps
c [treelook-3] 281467 literals remain 19%
c [treelook-3] 6805 variables remain to probed next time 1%
c [decomp-13] removed 113 variables
c [treelook-3] removed 3582 variables, found 912 hbrs
c [unhide-6] limit 1250000 with penalty 4 = 0 + 4
c [unhide-6-6] 0 units, 26 failed, 1262 tauts, 0 hbrs, 93095 literals
c [transred-2] limit 4839267 based on 4839267 irredundant clauses
c [transred-2] removed 2 transitive binary clauses
c [bca-2] limit of 10000000 steps and 9670515 added (scaled 2)
c [bca-2] 1479510 out of 1482950 literals actually usable 100%
c [bca-2] added 38 blocked clauses in 2980764 steps
c [sweep-2] limit 9669978 based on 4834989 irredundant clauses
c [sweep-2-1] 388325 pos 52.4% + 352980 neg 47.6% = 741305 sched 100.0% ret 169
c [sweep-2-1] 9784128 steps 36 queries 173196.44 avg class size
c [sweep-2-1] 484 decisions 30 SAT calls 84.30 avg env size
c [sweep-2-1] 741181 variables remain 100% (293 retained 0%)
c [decomp-14] removed 14 variables
c [sweep-2-1] removed 14 vars (0 failed, 6 eqs, 8 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 14 vars in TOTAL (1 rounds, 35 queries)
c [phase-count-6] 4830734 negative 99.9% of 4834971 except 4237 0.1%
c [phase-count-6] 4806489 positive 99.4% of 4834971 except 28482 0.6%
c [phase-count-6] less non-negative clauses 4237 than limit 483400 (10.0%)
c [phase-count-6] non-pos/non-neg = 28482/4237 = 6.72 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 11492 negative 100%
c [sort-queue-6] sorted 732237 enqueued variables after 27001 conflicts
c [score-dist-6] active 9223 (1%), one 0 (0%), zero 732237 (99%)
c [score-dist-6] max exp 516, different 16 (3%)
c [score-dist-6] median active exp 508, avg 507.5
c [simplification-6] removed 4390 variables 0.6% (741460 remain 50%)
c [simplification-6] removed 29196 irredundant clauses 0.6% (4834971 remain 81%)
c [simplification-6] maximum reduction of 1% = max (1%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 30000
c [simplification-6] penalized conflict interval 30000 = 1 * 30000
c [simplification-6] hard conflict limit 72001 (soft 57001 + delta 15000)
c [simplification-6] new conflict limit 57001 (hard 72001)
c 
c [simplification-7] limit 57001 conflicts (hard 72001) hit after 57002 conflicts
c [quatres-3] found 907965 quaternary clauses 100% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-2] added 10 single-self-subsuming ternary resolvents
c [quatres-3-2] added 9 quaternary resolvents
c [ternres-3] limit 50000000 with penalty 2 = 0 + 2
c [ternres-3] 677386 schedulable variables 91%
c [ternres-3] 2362 ternary resolvents (0 bin, 2362 trn)
c [ternres-3] 628597 variables remain 85% (112863 retained 15%)
c [gauss-2] limit 5221278 penalty 3 = 1 + 2
c [gauss-2] extracted 6 xors of average arity 3.0
c [gauss-2] connected 18 occurrences of 7 variables (average 2.6)
c [gauss-2] limit 5221278 penalty 3 = 1 + 2
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 100000000 penalty 2 = 0 + 2
c [basicprobe-3-0] 825 sched 0%, 261 failed, 675 lifted, 7359 hbrs
c [decomp-16] removed 3812 variables
c [basicprobe-3-1] 842 probes remain 0% after last round
c [basicprobe-3-1] 1336 units = 444 failed (33%) + 892 lifted (67%)
c [basicprobe-3-1] removed 5112 variables, found 13058 hbrs
c [bate-1] eliminated 935 asymmetric tautologies during probing
c [unhide-7] limit 1250000 with penalty 4 = 0 + 4
c [unhide-7-7] 2 units, 100 failed, 6681 tauts, 0 hbrs, 317215 literals
c [transred-3] limit 4793908 based on 4793908 irredundant clauses
c [transred-3] removed 2 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 736036 variables 100%
c [block-2] limit of 100000000 steps penalty 3 = 1 + 2
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 378 blocked clauses
c [block-2] 378 < 1/100 * 4793907 = 47939 considered unsuccessful
c [cce-2] limit of 130531960 steps penalty 3 = 1 + 2
c [cce-2-1] eliminated 9 clauses out of 259 (3%) of length 6
c [cce-2-1] eliminated 774 clauses out of 1800 (43%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 783 large clauses in 130531966 steps
c [cce-2-1] allowing another 65265983 steps for small clauses
c [cce-2-1] scheduling 2096016 clauses = 1515564 binary + 580452 ternary
c [cce-2-1] tried to eliminate 450 small clauses 0%
c [cce-2-1] eliminated 10 binary clauses 0%
c [cce-2-1] eliminated 9 ternary clauses 0%
c [cce-2-1] eliminated 19 small clauses 0%
c [cce-2-1] eliminated 19 small clauses in 130531960 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 802 covered clauses in round 1
c [cce-2] eliminated 802 covered clauses in TOTAL during 1 rounds
c [cce-2] 802 < 1/100 * 4791609 = 47916 considered unsuccessful
c [elim-6] 1654 variables 0% will be scheduled this time
c [elim-6] scheduled 1654 variables 0%
c [elim-6] limit of 100000000 steps penalty 3 = 1 + 2
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 1554 not tried 0% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 1654 scheduled
c [bca-3] limit of 10000000 steps and 9582054 added (scaled 2)
c [bca-3] 1468170 out of 1472072 literals actually usable 100%
c [bca-3] added 1 blocked clauses in 2984118 steps
c [sweep-3] limit 15663835 penalty 2 = 0 + 2
c [sweep-3-1] 389202 pos 52.9% + 346548 neg 47.1% = 735750 sched 100.0% ret 285
c [sweep-3-1] 15690476 steps 53 queries 130729.11 avg class size
c [sweep-3-1] 390 decisions 41 SAT calls 54.54 avg env size
c [sweep-3-1] 735611 variables remain 100% (424 retained 0%)
c [decomp-17] removed 67 variables
c [sweep-3-1] removed 67 vars (0 failed, 11 eqs, 19 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 67 vars in TOTAL (1 rounds, 52 queries)
c [phase-count-7] 4786512 negative 99.9% of 4790594 except 4082 0.1%
c [phase-count-7] 4762687 positive 99.4% of 4790594 except 27907 0.6%
c [phase-count-7] less non-negative clauses 4082 than limit 479000 (10.0%)
c [phase-count-7] non-pos/non-neg = 27907/4082 = 6.84 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 8580 negative 100%
c [sort-queue-7] sorted 725785 enqueued variables after 57002 conflicts
c [score-dist-7] active 10183 (1%), one 0 (0%), zero 725785 (99%)
c [score-dist-7] max exp 517, different 17 (3%)
c [score-dist-7] median active exp 508, avg 507.8
c [simplification-7] removed 5492 variables 0.7% (735968 remain 50%)
c [simplification-7] removed 44377 irredundant clauses 0.9% (4790594 remain 81%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-7] new conflict interval 45000
c [simplification-7] penalized conflict interval 45000 = 1 * 45000
c [simplification-7] hard conflict limit 124502 (soft 102002 + delta 22500)
c [simplification-7] new conflict limit 102002 (hard 124502)
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 -  938.1  735968  4790594     63609   23371   5355 23193  255   308  397  83%    627  112  267  138  193%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 935 basic ate = 867 trn 93% + 68 lrg 7% in 1 updates
c bcas: 3 count, 113 added (310 skipped), 8947432 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 2 bces, 2878 removed, 30837960 resolutions, 90372346 steps
c blkd: 2635 blocking literals 0%, 1 pure
c bump: 71051 bumped seen, 28910263 lits 406.9 on average
c card: 3 count, 0 units, 0 am1, 12778548 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1051 subsumed
c card: 832 at-most-one constraints found, average size 3.08
c card: 832 at-most-one constraints used 100%, average size 3.08
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 2 cces, 844 eliminated, 844 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 20738710 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 40 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 17 decompositions, 50576 equivalent 3%
c deco: 9424 decision-only clauses 13%, 37% reduction
c decs: 2036268 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 506835 eliminated 34%, 0 pure 0%
c elms: 6 rounds, 1.0 rounds/bve
c elms: 506744 small 100%, 90 large 0%
c elms: 1778978 tried small, 506744 succeeded 28%, 1272234 failed 72%
c elms: 19330 subsumed, 6790 strengthened, 0 blocked
c elms: 39015536 copies, 29957418 resolutions, 107476168 ipos
c elms: 33000981 subchks, 7496366 strchks
c gaus: 2 extractions, 33 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 15324540 steps, 7662270 extr 50%, 119 elim 0%
c glue: 219.6 orig avg, 219.6 real avg, 10.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 69008 = 1493 simple 2% + 66994 trn 97% + 521 lrg 1%, 4390 sub 6%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 71051 clauses, 288.6 length
c lrnd: 20506764 lits = 22335515 orig - 1828751 removed 8%
c lrnd: 27685 uips 39%, 31307 flips 44%
c mins: 25040 mins 71%, 109 bin 0%, 718 size 2%
c mins: 1820066 poisoned searches, 196385 hits, 11% hit rate
c mins: 4464056 used twice searches, 2219773 hits, 50% hit rate
c move: moved 5979, 143 bin 2%, 5836 trn 98%
c otfs: 972 driving 25%, 2868 restarting 75%
c otfs: str 3840, 3701 red 96%, 139 irr 4%
c otfs: str 3840, 0 bin 0%, 116 trn 3%, 3724 lrg 97%
c otfs: sub 3, 3 red 100%, 0 irr 0%
c otfs: sub 3, 0 bin 0%, 2 trn 67%, 1 lrg 33%
c phas: 7 computed, 1380040 set, 0 pos (0%), 1380040 neg (100%)
c prbs: 3 basic, 6280 probed, 587 failed, 892 lifted
c prbs: 3 simple, 1228969 probed, 18 failed, 46 eqs
c prbs: 3 treelook, 536 probed, 31 failed, 0 lifted
c prom: 57 locked 0% out of 17062 tried
c prps: 2504666581 props, 1222 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 3 count, 118 quat, 50 self1, 0 self2, 13 dup
c queu: 7 sorted, 2036268 next (38963 steps 0.02)
c queu: 36471181 enq (44036960 steps 1.21), 28910263 deq 79%
c redc: 95 clauses 9%, 1046 tried 1%, 1 sat 0%
c redc: 117 lits 1%, 10399 tried 0%, 1 sat 0%
c redc: 8 times jump level reduced, 5.6 levels on average
c reds: 1 count, 71879.0 conflicts per reduce
c reds: 0 memlim 0%, 1 arith 100%
c reds: 25004 collected 92%, 2204 retired 8%
c rmbd: 58815 removed, 773 red 1%
c rsts: 5545 restarts 99%, 46 skipped 1%
c rsts: 46 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 7 count, 7 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 71051 count (189966 tried 2.7), 9519 sub out of 70390 (13.5%)
c swps: 3 count, 3 rounds, 126 queries (42.0/round)
c swps: 106 sat calls, 1 unsat (1.4% success rate)
c swps: 1269 decisions 12.0, 144 conflicts 1.4
c swps; 161245.3 avg class size, 61.2 avg environment size
c swps: 0 failed, 32 impls, 21 equivs
c swp0: 41 type 0 queries, 2 unsat (4.9%), 41 sat (100.0%)
c swp1: 85 type 1 queries, 71 unsat (83.5%), 64 sat (75.3%)
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: 4214755 calls to obtain time
c tops: 190682 fixed 13%, 1 its, 71879.00 confs/it
c trds: 3 transitive reductions, 7 removed, 0 failed
c trds: 1461 nodes, 1497 edges, 14532519 steps
c trim: 6813 words, 0.0 MB
c trnr: 3 count, 0 bin, 4735 trn, 118858113 steps
c unhd: 7 count, 7 rounds, 178123870 steps
c unhd: 50 non-trivial sccs of average size 6.0
c unhd: 25 units, 25 bin, 0 trn, 0 lrg
c unhd: 2619 failed, 2484 stamp, 0 lits, 2 bin, 117 trn, 0 lrg
c unhd: 65828 tauts, 102 bin 0%, 9391 trn 14%, 165 lrg 0%
c unhd: 65828 tauts, 56170 stamp 85%, 33029 red 50%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 428781 str, 25 bin 0%, 3091 trn 1%, 425665 lrg 99%, 423552 red 99%
c vars: 735968 remaining 50% and 748093 removed 50% out of 1484061
c vars: 190682 fixed 13%, 506835 eliminated 34%, 50576 equivalent 3%
c vsts: 24831799226 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 9.9 search visits per propagation, 343269.6 per conflict
c wchs: 897257856 pushed, 157379822 enlarged, 64 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          70508         25004          2204       2897858        831517         33437
c 
c  0 0           688   1         0   0         0   0    495610  17     95593  11      2452   7     0.0
c  1 5           203   0         0   0         6   0     86188   3     17557   2       428   1     0.0
c  2 6           720   1         1   0        30   1    175652   6     45687   5      1398   4     0.0
c  3 9          1667   2         5   0        68   3    410538  14     80581  10      3182  10     0.1
c  4 14         1343   2         0   0        40   2    363698  13     79145  10      2603   8     0.1
c  5 21         1078   2         1   0        33   1    246540   9<    65865   8      1331   4     0.1
c  6 30         1379   2         4   0        35   2    203142   7     66200   8<     1632   5     0.2
c  7 41         1484   2        38   0        38   2    159808   6     46275   6      1408   4     0.3
c  8 54         1641   2       102   0        40   2    144308   5     46156   6      1339   4<    0.4
c  9 69         1406   2       183   1        36   2    105040   4     35792   4      1195   4     0.4
c 10 86         3229   5       434   2        87   4    144673   5     56173   7      2093   6     1.4
c 11 126       13472  19<     4247  17       458  21<   199981   7     97601  12      4577  14     9.4
c 12 230       42198  60     19989  80<     1333  60    162680   6     98892  12      9799  29    45.0
c 
c avg                 10.6          11.7          10.7           5.0           6.3           7.8
c std                  2.6           0.6           2.5           3.7           4.0           4.1
c 
c  108.029  11% elim
c   27.891   3% probe
c   19.808   2% unhide
c   18.628   2% quatres
c   10.334   1% cce
c    9.177   1% block
c    9.111   1% sweep
c    6.270   1% bca
c 
c   14.554 < 1% rest (below)
c 
c    6.118   1% bump
c    3.144   0% gauss
c    1.724   0% transred
c    1.239   0% ternres
c    1.193   0% decide
c    1.135   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   13.371   1% preprocessing     5%
c  234.572  24% inprocessing     95%
c ==================================
c  247.943  25% simplifying
c  748.398  75% search
c ==================================
c  996.367 100% all
c 
c         71879 conflicts,          72.1 confs/sec
c           464 ternaries,         154.9 confs/ternary
c            97 binaries,          741.0 confs/binary
c             1 iterations,      71879.0 confs/iteration
c 
c             1 reductions,          0.0 redus/sec,  71879.0 confs/reduction
c          5545 restarts,            5.6 rests/sec,     13.0 confs/restart
c       2036268 decisions,        2043.7 decis/sec,     28.3 decis/conflict
c    2504666581 propagations,  2513799.9 props/sec,   1230.0 props/decision
c 
c 996.4 seconds, 591.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
