c launch: /data/cnf/sc2014/app/atco_enc3_opt2_05_21.cnf.bz2
c host: atom02
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=3
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] SUM (--score=3)
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   15.3 1232021  5015695       126      89     18     4    0     5  357   4%      0    5    2    0 20690%
c i   15.7 1232020  5015695       143     100     21     4    0     6  357   4%      0    6    3    0 20248%
c i   19.3 1232019  5015695       302     202     48    16    0    16  358   3%      0   16    5    0 15991%
c i   26.3 1232018  5015695       688     455    111    42    1    33  358   4%      1   33   11    0 11814%
c i   26.4 1232017  5015695       689     455    111    42    1    33  358   4%      1   33   11    0 11768%
c 
c [simplification-2] limit 1010 conflicts (hard 11000) hit after 1010 conflicts
c [decomp-3] removed 196 variables
c [simpleprobe-2] 1040650 schedulable variables 84%
c [simpleprobe-2] limit 10029758 based on 5014879 irredundant clauses
c [decomp-4] removed 101 variables
c [simpleprobe-2] 1040715 variables remain 84% (191010 retained 16%)
c [simpleprobe-2] removed 101 variables, found 425 hbrs, 0 units
c [treelook-1] limit 1253615 based on 5014461 irredundant clauses
c [treelook-1] scheduled 199829 literals 8%
c [treelook-1] scheduling used 1295991 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1253615 based on 5014461 irredundant clauses
c [treelook-1] used 1726086 steps
c [treelook-1] 199250 literals remain 8%
c [treelook-1] 198932 variables remain to probed next time 16%
c [decomp-5] removed 85 variables
c [treelook-1] removed 619 variables, found 749 hbrs
c [basicprobe-1] limit 40091600 based on 5011450 irredundant clauses
c [basicprobe-1-0] 1185 probes remain 0% after last round
c [basicprobe-1-0] 532 units = 266 failed (50%) + 266 lifted (50%)
c [basicprobe-1-0] removed 1459 variables, found 39946 hbrs
c [unhide-2] limit 313215 based on 5011450 irredundant clauses
c [unhide-2-2] 0 units, 87 failed, 21114 tauts, 0 hbrs, 1101 literals
c [elim-2] 1228673 variables 100% will be scheduled this time
c [elim-2] scheduled 1228673 variables 100%
c [elim-2] limit of 27628124 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 1107309 not tried 90% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 121358 = 10% variables out of 1228673 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 4980642 negative 99.9% of 4984022 except 3380 0.1%
c [phase-count-2] 4954686 positive 99.4% of 4984022 except 29336 0.6%
c [phase-count-2] less non-negative clauses 3380 than limit 498400 (10.0%)
c [phase-count-2] non-pos/non-neg = 29336/3380 = 8.68 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 190649 negative 100%
c [sort-queue-2] sorted 1099209 enqueued variables after 1010 conflicts
c [score-dist-2] active 8395 (1%), one 0 (0%), zero 1099209 (99%)
c [score-dist-2] max exp 517, different 15 (3%)
c [score-dist-2] median active exp 512, avg 511.9
c [simplification-2] removed 124409 variables 10.1% (1107604 remain 75%)
c [simplification-2] removed 31673 irredundant clauses 0.6% (4984022 remain 84%)
c [simplification-2] maximum reduction of 10% = max (10%, 1%)
c [simplification-2] large reduction 10% >= 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 13010 (soft 3010 + delta 10000)
c [simplification-2] new conflict limit 3010 (hard 13010)
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   60.2 1107603  4984022      1683    1234    161 13612    8    80  362  10%      6   79   32    1 5505%
c 
c [simplification-3] limit 3010 conflicts (hard 13010) hit after 3010 conflicts
c [card-2] limit 1246005 based on 4984022 irredundant clauses
c [card-2] found 172 at-most-one constraints of average size 3.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1246005 for elimination
c [card-2] 172 out of 172 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 156 variables
c [treelook-2] limit 1245904 based on 4983616 irredundant clauses
c [treelook-2] scheduled 196913 literals 9%
c [treelook-2] scheduling used 1245907 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1245904 based on 4983616 irredundant clauses
c [treelook-2] used 1454889 steps
c [treelook-2] 196696 literals remain 9%
c [treelook-2] 53042 variables remain to probed next time 5%
c [treelook-2] removed 199 variables, found 238 hbrs
c [unhide-3] limit 311401 based on 4982428 irredundant clauses
c [unhide-3-3] 2 units, 64 failed, 16030 tauts, 0 hbrs, 1722 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1106794 variables 100%
c [elim-3] limit of 79093845 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 795185 not tried 72% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 310596 = 28% variables out of 1106794 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 4942450 negative 99.9% of 4945891 except 3441 0.1%
c [phase-count-3] 4917410 positive 99.4% of 4945891 except 28481 0.6%
c [phase-count-3] less non-negative clauses 3441 than limit 494500 (10.0%)
c [phase-count-3] non-pos/non-neg = 28481/3441 = 8.28 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 26299 negative 100%
c [sort-queue-3] sorted 785365 enqueued variables after 3010 conflicts
c [score-dist-3] active 10833 (1%), one 0 (0%), zero 785365 (99%)
c [score-dist-3] max exp 521, different 19 (4%)
c [score-dist-3] median active exp 515, avg 514.6
c [simplification-3] removed 311405 variables 28.1% (796198 remain 54%)
c [simplification-3] removed 38131 irredundant clauses 0.8% (4945891 remain 83%)
c [simplification-3] maximum reduction of 28% = max (28%, 1%)
c [simplification-3] large reduction 28% >= 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 15010 (soft 5010 + delta 10000)
c [simplification-3] new conflict limit 5010 (hard 15010)
c 
c [simplification-4] limit 5010 conflicts (hard 15010) hit after 5010 conflicts
c [decomp-8] removed 37 variables
c [basicprobe-2] limit 39566536 based on 4945817 irredundant clauses
c [basicprobe-2-0] 613 probes remain 0% after last round
c [basicprobe-2-0] 401 units = 220 failed (55%) + 181 lifted (45%)
c [basicprobe-2-0] removed 1141 variables, found 10249 hbrs
c [unhide-4] limit 310007 with penalty 4 = 0 + 4
c [unhide-4-4] 0 units, 290 failed, 4038 tauts, 0 hbrs, 3416 literals
c [elim-4] 793582 variables 100% will be scheduled this time
c [elim-4] scheduled 793582 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 2480061610 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 1550 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 42887 = 5% variables out of 793582 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 4892484 negative 99.9% of 4896610 except 4126 0.1%
c [phase-count-4] 4867550 positive 99.4% of 4896610 except 29060 0.6%
c [phase-count-4] less non-negative clauses 4126 than limit 489600 (10.0%)
c [phase-count-4] non-pos/non-neg = 29060/4126 = 7.04 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 18834 negative 100%
c [sort-queue-4] sorted 743575 enqueued variables after 5010 conflicts
c [score-dist-4] active 8135 (1%), one 0 (0%), zero 743575 (99%)
c [score-dist-4] max exp 523, different 21 (4%)
c [score-dist-4] median active exp 515, avg 515.8
c [simplification-4] removed 44488 variables 5.6% (751710 remain 51%)
c [simplification-4] removed 49281 irredundant clauses 1.0% (4896610 remain 83%)
c [simplification-4] maximum reduction of 6% = max (6%, 1%)
c [simplification-4] large reduction 6% >= 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 17010 (soft 7010 + delta 10000)
c [simplification-4] new conflict limit 7010 (hard 17010)
c 
c [simplification-5] limit 7010 conflicts (hard 17010) hit after 7010 conflicts
c [quatres-1] found 918721 quaternary clauses 100% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 8 single-self-subsuming ternary resolvents
c [quatres-1-2] added 76 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 39569640 with penalty 2 = 0 + 2
c [ternres-1] all 751710 free variables schedulable
c [ternres-1] 1719 ternary resolvents (0 bin, 1719 trn)
c [ternres-1] 713504 variables remain 95% (38206 retained 5%)
c [gauss-1] limit 2448305 based on 4896610 irredundant clauses
c [gauss-1] extracted 21 xors of average arity 2.0
c [gauss-1] connected 42 occurrences of 40 variables (average 1.1)
c [gauss-1] limit 2448305 based on 4896610 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 251 variables
c [simpleprobe-3] 635224 schedulable variables 85%
c [simpleprobe-3] limit 31655712 penalty 2 = 0 + 2
c [decomp-10] removed 1 variables
c [simpleprobe-3] 635618 variables remain 85% (115840 retained 15%)
c [simpleprobe-3] removed 1 variables, found 1077 hbrs, 0 units
c [unhide-5] limit 395696 with penalty 4 = 0 + 4
c [unhide-5-5] 0 units, 74 failed, 10707 tauts, 0 hbrs, 6131 literals
c [transred-1] limit 4884615 based on 4884615 irredundant clauses
c [transred-1] removed 1 transitive binary clauses
c [transred-1] found 1 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 751220 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 791392822 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 2345 blocked clauses
c [block-1] 2345 < 1/100 * 4884614 = 48846 considered unsuccessful
c [cce-1] limit of 39569641 steps penalty 2 = 0 + 2
c [cce-1-1] eliminated 27 clauses out of 323 (8%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 27 large clauses in 39569644 steps
c [cce-1-1] allowing another 19784822 steps for small clauses
c [cce-1-1] scheduling 2016859 clauses = 1546920 binary + 469939 ternary
c [cce-1-1] tried to eliminate 122 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 39569644 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 29 covered clauses in round 1
c [cce-1] eliminated 29 covered clauses in TOTAL during 1 rounds
c [cce-1] 29 < 1/100 * 4880760 = 48807 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 751220 variables 100%
c [elim-5] limit of 158278564 steps penalty 2 = 0 + 2
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 206630 not tried 28% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2106 = 0% variables out of 751220 scheduled
c [elim-5] 2106 < 1/100 * 751220 = 7512 considered unsuccessful
c [bca-1] limit of 10000000 steps and 9756112 added (scaled 2)
c [bca-1] 1495798 out of 1498230 literals actually usable 100%
c [bca-1] added 49 blocked clauses in 2995572 steps
c [sweep-1] limit 9755612 based on 4877806 irredundant clauses
c [sweep-1-1] 396731 pos 53.0% + 352383 neg 47.0% = 749114 sched 100.0% ret 0
c [sweep-1-1] 9768202 steps 33 queries 205620.42 avg class size
c [sweep-1-1] 311 decisions 31 SAT calls 37.61 avg env size
c [sweep-1-1] 749007 variables remain 100% (107 retained 0%)
c [decomp-11] removed 8 variables
c [sweep-1-1] removed 8 vars (0 failed, 1 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 8 vars in TOTAL (1 rounds, 32 queries)
c [phase-count-5] 4873638 negative 99.9% of 4877790 except 4152 0.1%
c [phase-count-5] 4849055 positive 99.4% of 4877790 except 28735 0.6%
c [phase-count-5] less non-negative clauses 4152 than limit 487700 (10.0%)
c [phase-count-5] non-pos/non-neg = 28735/4152 = 6.92 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 12611 negative 100%
c [sort-queue-5] sorted 741194 enqueued variables after 7010 conflicts
c [score-dist-5] active 7912 (1%), one 0 (0%), zero 741194 (99%)
c [score-dist-5] max exp 525, different 23 (4%)
c [score-dist-5] median active exp 516, avg 516.5
c [simplification-5] removed 2604 variables 0.3% (749106 remain 50%)
c [simplification-5] removed 18820 irredundant clauses 0.4% (4877790 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 37010 (soft 27010 + delta 10000)
c [simplification-5] new conflict limit 27010 (hard 37010)
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  416.5  749105  4877790     16643   11505   1500 14177  149   402  386  37%    196  338  151   28  542%
c 
c [simplification-6] limit 27010 conflicts (hard 37010) hit after 27010 conflicts
c [quatres-2] found 917732 quaternary clauses 100% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-2] added 25 single-self-subsuming ternary resolvents
c [quatres-2-2] added 56 quaternary resolvents
c [ternres-2] limit 29461126 with penalty 2 = 0 + 2
c [ternres-2] 711022 schedulable variables 95%
c [ternres-2] 1075 ternary resolvents (0 bin, 1075 trn)
c [ternres-2] 686493 variables remain 92% (62612 retained 8%)
c [card-3] limit 3682640 penalty 4 = 2 + 2
c [card-3] found 444 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 3682640 for elimination
c [card-3] 444 out of 444 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 1 variables
c [treelook-3] limit 2946112 penalty 2 = 0 + 2 boost 1
c [treelook-3] scheduled 295555 literals 20%
c [treelook-3] scheduling used 3105079 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 2946112 penalty 2 = 0 + 2 boost 1
c [treelook-3] used 3005258 steps
c [treelook-3] 293419 literals remain 20%
c [treelook-3] 32171 variables remain to probed next time 4%
c [treelook-3] removed 4 variables, found 1582 hbrs
c [unhide-6] limit 1250000 with penalty 4 = 0 + 4
c [unhide-6-6] 0 units, 52 failed, 1813 tauts, 0 hbrs, 148767 literals
c [transred-2] limit 4877092 based on 4877092 irredundant clauses
c [transred-2] removed 0 transitive binary clauses
c [bca-2] limit of 10000000 steps and 9752378 added (scaled 2)
c [bca-2] 1493803 out of 1497822 literals actually usable 100%
c [bca-2] added 15 blocked clauses in 3010078 steps
c [sweep-2] limit 9751854 based on 4875927 irredundant clauses
c [sweep-2-1] 402408 pos 53.7% + 346395 neg 46.3% = 748803 sched 100.0% ret 107
c [sweep-2-1] 9805115 steps 29 queries 149645.86 avg class size
c [sweep-2-1] 549 decisions 23 SAT calls 115.96 avg env size
c [sweep-2-1] 748686 variables remain 100% (189 retained 0%)
c [decomp-14] removed 53 variables
c [sweep-2-1] removed 53 vars (0 failed, 5 eqs, 8 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 53 vars in TOTAL (1 rounds, 28 queries)
c [phase-count-6] 4871459 negative 99.9% of 4875652 except 4193 0.1%
c [phase-count-6] 4846985 positive 99.4% of 4875652 except 28667 0.6%
c [phase-count-6] less non-negative clauses 4193 than limit 487500 (10.0%)
c [phase-count-6] non-pos/non-neg = 28667/4193 = 6.84 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 4691 negative 100%
c [sort-queue-6] sorted 738488 enqueued variables after 27010 conflicts
c [score-dist-6] active 10369 (1%), one 0 (0%), zero 738488 (99%)
c [score-dist-6] max exp 529, different 27 (5%)
c [score-dist-6] median active exp 520, avg 519.7
c [simplification-6] removed 248 variables 0.0% (748857 remain 50%)
c [simplification-6] removed 2138 irredundant clauses 0.0% (4875652 remain 82%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 20000
c [simplification-6] new conflict interval 40000
c [simplification-6] penalized conflict interval 40000 = 1 * 40000
c [simplification-6] hard conflict limit 87010 (soft 67010 + delta 20000)
c [simplification-6] new conflict limit 67010 (hard 87010)
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 -  994.3  748857  4875652     60012   23734   2634 14034  259   418  383  62%    474  191  280  124  225%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 2 count, 64 added (156 skipped), 6005650 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: 1 bces, 2345 removed, 15608469 resolutions, 45809535 steps
c blkd: 2211 blocking literals 0%, 0 pure
c bump: 59405 bumped seen, 20931409 lits 352.4 on average
c card: 3 count, 0 units, 0 am1, 12958360 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 755 subsumed
c card: 837 at-most-one constraints found, average size 3.09
c card: 837 at-most-one constraints used 100%, average size 3.09
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: 1 cces, 29 eliminated, 29 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: 34 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 14 decompositions, 50314 equivalent 3%
c deco: 2866 decision-only clauses 5%, 36% reduction
c decs: 2003833 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 506253 eliminated 34%, 0 pure 0%
c elms: 5 rounds, 1.0 rounds/bve
c elms: 506165 small 100%, 88 large 0%
c elms: 1781036 tried small, 506165 succeeded 28%, 1274871 failed 72%
c elms: 19080 subsumed, 6643 strengthened, 0 blocked
c elms: 38998982 copies, 29833071 resolutions, 107291986 ipos
c elms: 35207866 subchks, 6955311 strchks
c gaus: 1 extractions, 21 extracted, 2.0 size, 2 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 4896610 steps, 2448305 extr 50%, 66 elim 0%
c glue: 198.5 orig avg, 198.5 real avg, 9.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 54986 = 1513 simple 3% + 52578 trn 96% + 895 lrg 2%, 4446 sub 8%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 59405 clauses, 267.4 length
c lrnd: 15886202 lits = 16643597 orig - 757395 removed 5%
c lrnd: 22647 uips 38%, 24592 flips 41%
c mins: 31099 mins 89%, 140 bin 0%, 905 size 3%
c mins: 2732788 poisoned searches, 280029 hits, 10% hit rate
c mins: 5046166 used twice searches, 1839417 hits, 36% hit rate
c move: moved 3100, 113 bin 4%, 2987 trn 96%
c otfs: 856 driving 27%, 2278 restarting 73%
c otfs: str 3134, 2992 red 95%, 142 irr 5%
c otfs: str 3134, 0 bin 0%, 116 trn 4%, 3018 lrg 96%
c otfs: sub 4, 4 red 100%, 0 irr 0%
c otfs: sub 4, 0 bin 0%, 1 trn 25%, 3 lrg 75%
c phas: 6 computed, 1485106 set, 0 pos (0%), 1485106 neg (100%)
c prbs: 2 basic, 2761 probed, 486 failed, 447 lifted
c prbs: 3 simple, 1245465 probed, 18 failed, 38 eqs
c prbs: 3 treelook, 2182 probed, 10 failed, 0 lifted
c prom: 1489 locked 8% out of 18558 tried
c prps: 2759277544 props, 1373 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 2 count, 132 quat, 33 self1, 0 self2, 13 dup
c queu: 6 sorted, 2003833 next (33149 steps 0.02)
c queu: 27755323 enq (35849500 steps 1.29), 20931409 deq 75%
c redc: 172 clauses 12%, 1441 tried 2%, 1 sat 0%
c redc: 238 lits 1%, 18982 tried 0%, 1 sat 0%
c redc: 13 times jump level reduced, 34.9 levels on average
c reds: 1 count, 60197.0 conflicts per reduce
c reds: 0 memlim 0%, 1 arith 100%
c reds: 25003 collected 92%, 2175 retired 8%
c rmbd: 57702 removed, 111 red 0%
c rsts: 4547 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: 6 count, 6 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 59405 count (141372 tried 2.4), 3841 sub out of 58736 (6.5%)
c swps: 2 count, 2 rounds, 60 queries (30.0/round)
c swps: 54 sat calls, 1 unsat (1.2% success rate)
c swps: 860 decisions 15.9, 64 conflicts 1.2
c swps; 185420.1 avg class size, 71.0 avg environment size
c swps: 0 failed, 9 impls, 6 equivs
c swp0: 19 type 0 queries, 2 unsat (10.5%), 19 sat (100.0%)
c swp1: 41 type 1 queries, 20 unsat (48.8%), 35 sat (85.4%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 4126573 calls to obtain time
c tops: 178637 fixed 12%, 7 its, 8599.57 confs/it
c trds: 2 transitive reductions, 1 removed, 1 failed
c trds: 995 nodes, 1002 edges, 9775608 steps
c trim: 11836 words, 0.0 MB
c trnr: 2 count, 0 bin, 2794 trn, 69030768 steps
c unhd: 6 count, 6 rounds, 150255560 steps
c unhd: 65 non-trivial sccs of average size 4.9
c unhd: 5 units, 5 bin, 0 trn, 0 lrg
c unhd: 919 failed, 809 stamp, 0 lits, 2 bin, 101 trn, 0 lrg
c unhd: 58101 tauts, 33 bin 0%, 5708 trn 10%, 64 lrg 0%
c unhd: 58101 tauts, 52296 stamp 90%, 29843 red 51%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 161988 str, 5 bin 0%, 3267 trn 2%, 158716 lrg 98%, 156340 red 97%
c vars: 748857 remaining 50% and 735204 removed 50% out of 1484061
c vars: 178637 fixed 12%, 506253 eliminated 34%, 50314 equivalent 3%
c vsts: 24318799608 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 8.8 search visits per propagation, 402757.5 per conflict
c wchs: 733448251 pushed, 135140404 enlarged, 54 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          58868         25003          2175       2384733        684935         26790
c 
c  0 0          1045   2         3   0         0   0    380325  16     75929  11      1954   7     0.1
c  1 5           560   1         7   0        23   1    106971   4     18824   3      1009   4     0.1
c  2 6          2306   4        29   0        68   3    164858   7     39792   6      3148  12     0.3
c  3 9          3482   6        37   0       139   6    339454  14     82343  12      3635  14     0.4
c  4 14         2679   5        34   0        98   5    323742  14     74786  11      2222   8     0.3
c  5 21         3409   6        40   0       138   6    217680   9<    61943   9      2028   8     0.6
c  6 30         2544   4        39   0        90   4    200523   8     59294   9<     1647   6<    0.5
c  7 41         2576   4        64   0        96   4    137058   6     46876   7      1487   6     0.5
c  8 54         2088   4       124   0        83   4    111784   5     37311   5       901   3     0.5
c  9 69         1590   3<      210   1        82   4<    88277   4     35600   5       907   3     0.5
c 10 86         2315   4       764   3       115   5     81491   3     31907   5       785   3     1.0
c 11 126        8772  15      4493  18       337  15    123320   5     57556   8      2023   8     6.7
c 12 230       25502  43     19159  77<      906  42    109250   5     62774   9      5044  19    45.9
c 
c avg                  9.1          11.6           9.2           4.7           5.8           6.1
c std                  3.6           0.9           3.4           3.5           3.8           4.1
c 
c  105.969  11% elim
c   21.765   2% probe
c   14.409   1% unhide
c   12.270   1% quatres
c    6.447   1% sweep
c    4.584   0% block
c    4.508   0% bump
c 
c   13.435 < 1% rest (below)
c 
c    4.201   0% bca
c    3.580   0% cce
c    1.443   0% gauss
c    1.176   0% decide
c    1.168   0% transred
c    1.132   0% card
c    0.735   0% ternres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   13.463   1% preprocessing     7%
c  192.717  19% inprocessing     93%
c ==================================
c  206.180  21% simplifying
c  790.057  79% search
c ==================================
c  996.265 100% all
c 
c         60197 conflicts,          60.4 confs/sec
c           486 ternaries,         123.9 confs/ternary
c           137 binaries,          439.4 confs/binary
c             7 iterations,       8599.6 confs/iteration
c 
c             1 reductions,          0.0 redus/sec,  60197.0 confs/reduction
c          4547 restarts,            4.6 rests/sec,     13.2 confs/restart
c       2003833 decisions,        2011.3 decis/sec,     33.3 decis/conflict
c    2759277544 propagations,  2769622.7 props/sec,   1377.0 props/decision
c 
c 996.3 seconds, 546.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
