c launch: /data/cnf/sc2014/app/atco_enc3_opt1_03_53.cnf.bz2
c host: atom08
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_opt1_03_53.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc3_opt1_03_53.cnf.bz2
c no embedded options
c found 'p cnf 1296235 5156702' header
c read 1296235 variables, 5156702 clauses, 12869708 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 1254502 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 1254502  4931292         0       0      0     0    0     0  258   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1232823 based on 4931292 irredundant clauses
c [card-1] found 980 at-most-one constraints of average size 3.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1232823 for elimination
c [card-1] 980 out of 980 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 324478 variables
c [simpleprobe-1] all 971757 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 7806618 based on 3903309 irredundant clauses
c [decomp-2] removed 89 variables
c [simpleprobe-1] 787600 variables remain 81% (184068 retained 19%)
c [simpleprobe-1] removed 89 variables, found 275 hbrs, 7 units
c [unhide-1] limit 243938 based on 3903010 irredundant clauses
c [unhide-1-1] 5 units, 210 failed, 3875 tauts, 0 hbrs, 593 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 970387 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 943340 not tried 97% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 25941 = 3% variables out of 970387 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3822000 negative 99.9% of 3826922 except 4922 0.1%
c [phase-count-1] 3801621 positive 99.3% of 3826922 except 25301 0.7%
c [phase-count-1] less non-negative clauses 4922 than limit 382600 (10.0%)
c [phase-count-1] non-pos/non-neg = 25301/4922 = 5.14 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 944446 negative 100%
c [sort-queue-1] sorted 944446 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 944446 (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 69241 variables 6.8% (944446 remain 75%)
c [simplification-1] removed 1104370 irredundant clauses 22.4% (3826922 remain 78%)
c [simplification-1] maximum reduction of 22% = max (7%, 22%)
c [simplification-1] large reduction 22% >= 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 of 100 binary hit after 100 binaries
c [decomp-3] removed 204 variables
c [simpleprobe-2] 765247 schedulable variables 81%
c [simpleprobe-2] limit 7652740 based on 3826370 irredundant clauses
c [decomp-4] removed 84 variables
c [simpleprobe-2] 765310 variables remain 81% (178848 retained 19%)
c [simpleprobe-2] removed 84 variables, found 243 hbrs, 0 units
c [treelook-1] limit 956510 based on 3826040 irredundant clauses
c [treelook-1] scheduled 153702 literals 8%
c [treelook-1] scheduling used 1034885 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 956510 based on 3826040 irredundant clauses
c [treelook-1] used 1196062 steps
c [treelook-1] 153531 literals remain 8%
c [treelook-1] 110808 variables remain to probed next time 12%
c [decomp-5] removed 85 variables
c [treelook-1] removed 246 variables, found 898 hbrs
c [basicprobe-1] limit 30598384 based on 3824798 irredundant clauses
c [basicprobe-1-0] 8792 probes remain 1% after last round
c [basicprobe-1-0] 35 units = 35 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 883 variables, found 21120 hbrs
c [unhide-2] limit 239049 based on 3824798 irredundant clauses
c [unhide-2-2] 4 units, 914 failed, 8851 tauts, 0 hbrs, 3274 literals
c [elim-2] 937374 variables 100% will be scheduled this time
c [elim-2] scheduled 937374 variables 100%
c [elim-2] limit of 7037902 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 908701 not tried 97% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 28531 = 3% variables out of 937374 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 3784643 negative 99.9% of 3789749 except 5106 0.1%
c [phase-count-2] 3762845 positive 99.3% of 3789749 except 26904 0.7%
c [phase-count-2] less non-negative clauses 5106 than limit 378900 (10.0%)
c [phase-count-2] non-pos/non-neg = 26904/5106 = 5.27 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 311876 negative 100%
c [sort-queue-2] sorted 906701 enqueued variables after 587 conflicts
c [score-dist-2] active 3248 (0%), one 0 (0%), zero 906701 (100%)
c [score-dist-2] max exp 515, different 15 (3%)
c [score-dist-2] median active exp 511, avg 510.9
c [simplification-2] removed 34497 variables 3.7% (909949 remain 73%)
c [simplification-2] removed 37173 irredundant clauses 1.0% (3789749 remain 77%)
c [simplification-2] maximum reduction of 4% = max (4%, 1%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1000 (hard 11000)
c [simplification-2] new binary interval 1000
c 
c [simplification-3] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [card-2] limit 947437 based on 3789749 irredundant clauses
c [card-2] found 563 at-most-one constraints of average size 3.4
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 947437 for elimination
c [card-2] 563 out of 563 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 213 variables
c [treelook-2] limit 947318 based on 3789275 irredundant clauses
c [treelook-2] scheduled 162427 literals 9%
c [treelook-2] scheduling used 1085303 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 947318 based on 3789275 irredundant clauses
c [treelook-2] used 1338774 steps
c [treelook-2] 162265 literals remain 9%
c [treelook-2] 19648 variables remain to probed next time 2%
c [decomp-7] removed 9 variables
c [treelook-2] removed 154 variables, found 763 hbrs
c [unhide-3] limit 236777 based on 3788436 irredundant clauses
c [unhide-3-3] 3 units, 371 failed, 16911 tauts, 0 hbrs, 2750 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 908842 variables 100%
c [elim-3] limit of 12083474 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 859285 not tried 95% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 48291 = 5% variables out of 908842 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 3744738 negative 99.9% of 3749961 except 5223 0.1%
c [phase-count-3] 3724497 positive 99.3% of 3749961 except 25464 0.7%
c [phase-count-3] less non-negative clauses 5223 than limit 374900 (10.0%)
c [phase-count-3] non-pos/non-neg = 25464/5223 = 4.88 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 280309 negative 100%
c [sort-queue-3] sorted 855345 enqueued variables after 1000 conflicts
c [score-dist-3] active 5206 (1%), one 0 (0%), zero 855345 (99%)
c [score-dist-3] max exp 516, different 16 (3%)
c [score-dist-3] median active exp 511, avg 511.9
c [simplification-3] removed 49398 variables 5.4% (860551 remain 69%)
c [simplification-3] removed 39788 irredundant clauses 1.0% (3749961 remain 76%)
c [simplification-3] maximum reduction of 5% = max (5%, 1%)
c [simplification-3] large reduction 5% >= 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 13000 (soft 3000 + delta 10000)
c [simplification-3] new conflict limit 3000 (hard 13000)
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   43.1  860550  3749961      1141     639    142  8278    2    57  280   3%      7   56    7    0 6002%
c 
c [simplification-4] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [decomp-8] removed 83 variables
c [basicprobe-2] limit 29998560 based on 3749820 irredundant clauses
c [basicprobe-2-0] 4699 probes remain 1% after last round
c [basicprobe-2-0] 85 units = 71 failed (84%) + 14 lifted (16%)
c [basicprobe-2-0] removed 916 variables, found 16983 hbrs
c [unhide-4] limit 234363 based on 3749820 irredundant clauses
c [unhide-4-4] 6 units, 1072 failed, 8056 tauts, 0 hbrs, 11099 literals
c [elim-4] 854566 variables 100% will be scheduled this time
c [elim-4] scheduled 854566 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 827463175 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 2156 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 294455 = 34% variables out of 854566 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 3621082 negative 99.8% of 3628059 except 6977 0.2%
c [phase-count-4] 3603503 positive 99.3% of 3628059 except 24556 0.7%
c [phase-count-4] less non-negative clauses 6977 than limit 362800 (10.0%)
c [phase-count-4] non-pos/non-neg = 24556/6977 = 3.52 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 102053 negative 100%
c [sort-queue-4] sorted 553406 enqueued variables after 3000 conflicts
c [score-dist-4] active 8198 (1%), one 0 (0%), zero 553406 (99%)
c [score-dist-4] max exp 521, different 21 (4%)
c [score-dist-4] median active exp 514, avg 514.5
c [simplification-4] removed 298946 variables 34.7% (561604 remain 45%)
c [simplification-4] removed 121902 irredundant clauses 3.3% (3628059 remain 74%)
c [simplification-4] maximum reduction of 35% = max (35%, 3%)
c [simplification-4] large reduction 35% >= 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 15000 (soft 5000 + delta 10000)
c [simplification-4] new conflict limit 5000 (hard 15000)
c 
c [simplification-5] limit 5000 conflicts (hard 15000) hit after 5000 conflicts
c [quatres-1] found 640425 quaternary clauses 99% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 73 single-self-subsuming ternary resolvents
c [quatres-1-2] added 89 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 16525277 with penalty 2 = 0 + 2
c [ternres-1] all 561604 free variables schedulable
c [ternres-1] 2901 ternary resolvents (0 bin, 2901 trn)
c [ternres-1] 544061 variables remain 97% (17543 retained 3%)
c [gauss-1] limit 1814029 based on 3628059 irredundant clauses
c [gauss-1] extracted 286 xors of average arity 2.5
c [gauss-1] connected 726 occurrences of 669 variables (average 1.1)
c [gauss-1] limit 1814029 based on 3628059 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-9] removed 1068 variables
c [simpleprobe-3] 454446 schedulable variables 81%
c [simpleprobe-3] limit 13220222 penalty 2 = 0 + 2
c [decomp-10] removed 10 variables
c [simpleprobe-3] 454688 variables remain 81% (105838 retained 19%)
c [simpleprobe-3] removed 10 variables, found 540 hbrs, 0 units
c [unhide-5] limit 226600 based on 3625606 irredundant clauses
c [unhide-5-5] 25 units, 865 failed, 26542 tauts, 0 hbrs, 62598 literals
c [transred-1] limit 3594381 based on 3594381 irredundant clauses
c [transred-1] removed 6 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 557596 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 330505555 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 4769 blocked clauses
c [block-1] 4769 < 1/100 * 3594376 = 35943 considered unsuccessful
c [cce-1] limit of 16525277 steps penalty 2 = 0 + 2
c [cce-1-1] eliminated 1 clauses out of 33 (3%) of length 16
c [cce-1-1] eliminated 1 clauses out of 148 (1%) of length 14
c [cce-1-1] eliminated 57 clauses out of 293 (19%) of length 13
c [cce-1-1] eliminated 2 clauses out of 115 (2%) of length 11
c [cce-1-1] eliminated 28 clauses out of 150 (19%) of length 10
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 89 large clauses in 16525473 steps
c [cce-1-1] allowing another 8262736 steps for small clauses
c [cce-1-1] scheduling 2495607 clauses = 1161713 binary + 1333894 ternary
c [cce-1-1] tried to eliminate 64 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 16525281 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 91 covered clauses in round 1
c [cce-1] eliminated 91 covered clauses in TOTAL during 1 rounds
c [cce-1] 91 < 1/100 * 3572395 = 35723 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 557596 variables 100%
c [elim-5] limit of 66101111 steps penalty 2 = 0 + 2
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 345564 not tried 62% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 26209 = 5% variables out of 557596 scheduled
c [bca-1] limit of 10000000 steps and 7079132 added (scaled 2)
c [bca-1] 1060423 out of 1062776 literals actually usable 100%
c [bca-1] added 10152 blocked clauses in 2171875 steps
c [sweep-1] limit 7078632 based on 3539316 irredundant clauses
c [sweep-1-1] 239459 pos 45.1% + 291928 neg 54.9% = 531387 sched 100.0% ret 0
c [sweep-1-1] 7111238 steps 36 queries 121637.61 avg class size
c [sweep-1-1] 293 decisions 25 SAT calls 115.64 avg env size
c [sweep-1-1] 531348 variables remain 100% (39 retained 0%)
c [decomp-11] removed 97 variables
c [sweep-1-1] removed 97 vars (0 failed, 10 eqs, 9 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 97 vars in TOTAL (1 rounds, 35 queries)
c [phase-count-5] 3533697 negative 99.8% of 3539147 except 5450 0.2%
c [phase-count-5] 3519538 positive 99.4% of 3539147 except 19609 0.6%
c [phase-count-5] less non-negative clauses 5450 than limit 353900 (10.0%)
c [phase-count-5] non-pos/non-neg = 19609/5450 = 3.60 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 92296 negative 100%
c [sort-queue-5] sorted 522586 enqueued variables after 5000 conflicts
c [score-dist-5] active 8704 (2%), one 0 (0%), zero 522586 (98%)
c [score-dist-5] max exp 524, different 23 (4%)
c [score-dist-5] median active exp 515, avg 515.3
c [simplification-5] removed 30314 variables 5.4% (531290 remain 42%)
c [simplification-5] removed 88912 irredundant clauses 2.5% (3539147 remain 72%)
c [simplification-5] maximum reduction of 5% = max (5%, 2%)
c [simplification-5] large reduction 5% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 17000 (soft 7000 + delta 10000)
c [simplification-5] new conflict limit 7000 (hard 17000)
c 
c [simplification-6] limit 7000 conflicts (hard 17000) hit after 7000 conflicts
c [quatres-2] found 546287 quaternary clauses 98% in total
c [quatres-2-1] removed 3 duplicate quaternary clauses
c [quatres-2-2] added 115 single-self-subsuming ternary resolvents
c [quatres-2-2] added 70 quaternary resolvents
c [ternres-2] limit 14156504 based on 3539126 irredundant clauses
c [ternres-2] 514656 schedulable variables 97%
c [ternres-2] 9139 ternary resolvents (7 bin, 9132 trn)
c [ternres-2] 499880 variables remain 94% (31410 retained 6%)
c [card-3] limit 884781 based on 3539126 irredundant clauses
c [card-3] found 440 at-most-one constraints of average size 3.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 884781 for elimination
c [card-3] 440 out of 440 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 1769563 based on 3539126 irredundant clauses
c [gauss-2] extracted 125 xors of average arity 3.0
c [gauss-2] connected 374 occurrences of 368 variables (average 1.0)
c [gauss-2] limit 1769563 based on 3539126 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 1 variables
c [treelook-3] limit 884781 based on 3539126 irredundant clauses
c [treelook-3] scheduled 98249 literals 9%
c [treelook-3] scheduling used 950962 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 884781 based on 3539126 irredundant clauses
c [treelook-3] used 928234 steps
c [treelook-3] 98123 literals remain 9%
c [treelook-3] 7668 variables remain to probed next time 1%
c [decomp-13] removed 20 variables
c [treelook-3] removed 65 variables, found 289 hbrs
c [unhide-6] limit 269792 with penalty 4 = 0 + 4
c [unhide-6-6] 18 units, 1025 failed, 973 tauts, 0 hbrs, 60481 literals
c [transred-2] limit 3531610 based on 3531610 irredundant clauses
c [transred-2] removed 15 transitive binary clauses
c [elim-6] 1904 variables 0% will be scheduled this time
c [elim-6] scheduled 1904 variables 0%
c [elim-6] limit of 107916861 steps penalty 2 = 0 + 2
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 1725 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 1904 scheduled
c [bca-2] limit of 10000000 steps and 7004544 added (scaled 2)
c [bca-2] 1048969 out of 1052664 literals actually usable 100%
c [bca-2] added 116 blocked clauses in 2145629 steps
c [sweep-2] limit 6998968 based on 3499484 irredundant clauses
c [sweep-2-1] 270610 pos 51.4% + 255694 neg 48.6% = 526304 sched 100.0% ret 27
c [sweep-2-1] 7248743 steps 31 queries 101813.68 avg class size
c [sweep-2-1] 464 decisions 26 SAT calls 144.88 avg env size
c [sweep-2-1] 526240 variables remain 100% (91 retained 0%)
c [decomp-14] removed 264 variables
c [sweep-2-1] removed 264 vars (0 failed, 4 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 264 vars in TOTAL (1 rounds, 30 queries)
c [phase-count-6] 3493571 negative 99.8% of 3498877 except 5306 0.2%
c [phase-count-6] 3479206 positive 99.4% of 3498877 except 19671 0.6%
c [phase-count-6] less non-negative clauses 5306 than limit 349800 (10.0%)
c [phase-count-6] non-pos/non-neg = 19671/5306 = 3.71 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 14505 negative 100%
c [sort-queue-6] sorted 514844 enqueued variables after 7000 conflicts
c [score-dist-6] active 11223 (2%), one 0 (0%), zero 514844 (98%)
c [score-dist-6] max exp 525, different 24 (5%)
c [score-dist-6] median active exp 516, avg 516.6
c [simplification-6] removed 5223 variables 1.0% (526067 remain 42%)
c [simplification-6] removed 40270 irredundant clauses 1.1% (3498877 remain 71%)
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 10000
c [simplification-6] penalized conflict interval 10000 = 1 * 10000
c [simplification-6] hard conflict limit 27000 (soft 17000 + delta 10000)
c [simplification-6] new conflict limit 17000 (hard 27000)
c 
c [simplification-7] limit 17000 conflicts (hard 27000) hit after 17000 conflicts
c [quatres-3] found 493968 quaternary clauses 98% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 14 single-self-subsuming ternary resolvents
c [quatres-3-2] added 9 quaternary resolvents
c [ternres-3] limit 15221882 with penalty 2 = 0 + 2
c [ternres-3] 494978 schedulable variables 94%
c [ternres-3] 10017 ternary resolvents (1 bin, 10016 trn)
c [ternres-3] 477605 variables remain 91% (48462 retained 9%)
c [decomp-15] removed 1 variables
c [basicprobe-3] limit 76109411 penalty 2 = 0 + 2
c [basicprobe-3-0] 320 probes remain 0% after last round
c [basicprobe-3-0] 259 units = 236 failed (91%) + 23 lifted (9%)
c [basicprobe-3-0] removed 1072 variables, found 23284 hbrs
c [bate-1] eliminated 740 asymmetric tautologies during probing
c [unhide-7] limit 761094 with penalty 4 = 0 + 4
c [unhide-7-7] 75 units, 919 failed, 36859 tauts, 0 hbrs, 100640 literals
c [transred-3] limit 3459289 based on 3459289 irredundant clauses
c [transred-3] removed 6 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 519705 variables 100%
c [block-2] limit of 76109411 steps penalty 3 = 1 + 2
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 158 blocked clauses
c [block-2] 158 < 1/100 * 3459284 = 34592 considered unsuccessful
c [cce-2] limit of 38054705 steps penalty 3 = 1 + 2
c [cce-2-1] eliminated 34 clauses out of 562 (6%) of length 12
c [cce-2-1] eliminated 277 clauses out of 1249 (22%) of length 9
c [cce-2-1] eliminated 55 clauses out of 1503 (4%) of length 8
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 366 large clauses in 38054706 steps
c [cce-2-1] allowing another 19027353 steps for small clauses
c [cce-2-1] scheduling 1633495 clauses = 1108804 binary + 524691 ternary
c [cce-2-1] tried to eliminate 184 small clauses 0%
c [cce-2-1] eliminated 21 binary clauses 0%
c [cce-2-1] eliminated 2 ternary clauses 0%
c [cce-2-1] eliminated 23 small clauses 0%
c [cce-2-1] eliminated 23 small clauses in 38054705 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 389 covered clauses in round 1
c [cce-2] eliminated 389 covered clauses in TOTAL during 1 rounds
c [cce-2] 389 < 1/100 * 3427446 = 34274 considered unsuccessful
c [bca-3] limit of 10000000 steps and 6859748 added (scaled 2)
c [bca-3] 1034594 out of 1039410 literals actually usable 100%
c [bca-3] added 24 blocked clauses in 2120454 steps
c [sweep-3] limit 6854114 based on 3427057 irredundant clauses
c [sweep-3-1] 274594 pos 52.8% + 245027 neg 47.2% = 519621 sched 100.0% ret 83
c [sweep-3-1] 6903609 steps 30 queries 126246.60 avg class size
c [sweep-3-1] 273 decisions 23 SAT calls 149.48 avg env size
c [sweep-3-1] 519547 variables remain 100% (157 retained 0%)
c [decomp-16] removed 1417 variables
c [sweep-3-1] removed 1417 vars (0 failed, 6 eqs, 10 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1417 vars in TOTAL (1 rounds, 29 queries)
c [phase-count-7] 3421358 negative 99.9% of 3426309 except 4951 0.1%
c [phase-count-7] 3407390 positive 99.4% of 3426309 except 18919 0.6%
c [phase-count-7] less non-negative clauses 4951 than limit 342600 (10.0%)
c [phase-count-7] non-pos/non-neg = 18919/4951 = 3.82 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 9609 negative 100%
c [sort-queue-7] sorted 504833 enqueued variables after 17000 conflicts
c [score-dist-7] active 13454 (3%), one 0 (0%), zero 504833 (97%)
c [score-dist-7] max exp 528, different 26 (5%)
c [score-dist-7] median active exp 518, avg 518.0
c [simplification-7] removed 7780 variables 1.5% (518287 remain 41%)
c [simplification-7] removed 72568 irredundant clauses 2.1% (3426309 remain 69%)
c [simplification-7] maximum reduction of 2% = max (1%, 2%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 16666
c [simplification-7] penalized conflict interval 16666 = 1 * 16666
c [simplification-7] hard conflict limit 43666 (soft 33666 + delta 10000)
c [simplification-7] new conflict limit 33666 (hard 43666)
c 
c [simplification-8] limit 33666 conflicts (hard 43666) hit after 33668 conflicts
c [quatres-4] found 313365 quaternary clauses 98% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 10 single-self-subsuming ternary resolvents
c [quatres-4-2] added 7 quaternary resolvents
c [ternres-4] limit 29837180 with penalty 2 = 0 + 2
c [ternres-4] 470526 schedulable variables 91%
c [ternres-4] 80291 ternary resolvents (4 bin, 80287 trn)
c [ternres-4] 430240 variables remain 83% (88047 retained 17%)
c [gauss-3] limit 2983718 penalty 3 = 1 + 2
c [gauss-3] extracted 172 xors of average arity 3.0
c [gauss-3] connected 513 occurrences of 395 variables (average 1.3)
c [gauss-3] limit 2983718 penalty 3 = 1 + 2
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 63 variables
c [simpleprobe-4] 420254 schedulable variables 81%
c [simpleprobe-4] limit 50000000 penalty 2 = 0 + 2
c [decomp-18] removed 142 variables
c [simpleprobe-4] 420663 variables remain 81% (97419 retained 19%)
c [simpleprobe-4] removed 142 variables, found 953 hbrs, 1 units
c [unhide-8] limit 1250000 with penalty 4 = 0 + 4
c [unhide-8-8] 13 units, 960 failed, 3790 tauts, 0 hbrs, 233209 literals
c [transred-4] limit 3414899 based on 3414899 irredundant clauses
c [transred-4] removed 8 transitive binary clauses
c [transred-4] found 1 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 512792 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 1 + 2
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 351909 not tried 69% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 47872 = 9% variables out of 512792 scheduled
c [bca-4] limit of 10000000 steps and 6641010 added (scaled 2)
c [bca-4] 925062 out of 929842 literals actually usable 99%
c [bca-4] added 156 blocked clauses in 1913936 steps
c [sweep-4] limit 8951154 penalty 2 = 0 + 2
c [sweep-4-1] 246995 pos 53.1% + 217791 neg 46.9% = 464786 sched 100.0% ret 134
c [sweep-4-1] 9062394 steps 33 queries 104839.36 avg class size
c [sweep-4-1] 439 decisions 28 SAT calls 225.71 avg env size
c [sweep-4-1] 464650 variables remain 100% (270 retained 0%)
c [decomp-19] removed 137 variables
c [sweep-4-1] removed 137 vars (0 failed, 4 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 137 vars in TOTAL (1 rounds, 32 queries)
c [phase-count-8] 3311726 negative 99.8% of 3317196 except 5470 0.2%
c [phase-count-8] 3299691 positive 99.5% of 3317196 except 17505 0.5%
c [phase-count-8] less non-negative clauses 5470 than limit 331700 (10.0%)
c [phase-count-8] non-pos/non-neg = 17505/5470 = 3.20 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 6280 negative 100%
c [sort-queue-8] sorted 449809 enqueued variables after 33668 conflicts
c [score-dist-8] active 14974 (3%), one 0 (0%), zero 449809 (97%)
c [score-dist-8] max exp 530, different 27 (5%)
c [score-dist-8] median active exp 519, avg 519.2
c [simplification-8] removed 53504 variables 10.3% (464783 remain 37%)
c [simplification-8] removed 109113 irredundant clauses 3.2% (3317196 remain 67%)
c [simplification-8] maximum reduction of 10% = max (10%, 3%)
c [simplification-8] large reduction 10% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 45668 (soft 35668 + delta 10000)
c [simplification-8] new conflict limit 35668 (hard 45668)
c 
c [simplification-9] limit 35668 conflicts (hard 45668) hit after 35671 conflicts
c [quatres-5] found 266772 quaternary clauses 97% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 738 single-self-subsuming ternary resolvents
c [quatres-5-2] added 155 quaternary resolvents
c [ternres-5] limit 31869293 with penalty 2 = 0 + 2
c [ternres-5] 385878 schedulable variables 83%
c [ternres-5] 108838 ternary resolvents (73 bin, 108765 trn)
c [ternres-5] 335413 variables remain 72% (129370 retained 28%)
c [treelook-4] limit 3186929 penalty 2 = 0 + 2 boost 1
c [treelook-4] scheduled 169578 literals 18%
c [treelook-4] scheduling used 3186931 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 3186929 penalty 2 = 0 + 2 boost 1
c [treelook-4] used 3197500 steps
c [treelook-4] 169286 literals remain 18%
c [treelook-4] 4368 variables remain to probed next time 1%
c [decomp-21] removed 30 variables
c [treelook-4] removed 123 variables, found 1291 hbrs
c [unhide-9] limit 1250000 with penalty 4 = 0 + 4
c [unhide-9-9] 9 units, 362 failed, 57393 tauts, 0 hbrs, 48882 literals
c [transred-5] limit 3270941 based on 3270941 irredundant clauses
c [transred-5] removed 10 transitive binary clauses
c [elim-8] 1091 variables 0% will be scheduled this time
c [elim-8] scheduled 1091 variables 0%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 0 + 2
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 3572414384 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 25 = 2% variables out of 1091 scheduled
c [elim-8] 25 < 1/100 * 1091 = 10 considered unsuccessful
c [bca-5] limit of 10000000 steps and 6283618 added (scaled 2)
c [bca-5] 919115 out of 924136 literals actually usable 99%
c [bca-5] added 9 blocked clauses in 1902872 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 95607880 penalty 2 = 0 + 2
c [sweep-5-1] 246414 pos 53.4% + 215388 neg 46.6% = 461802 sched 99.9% ret 265
c [sweep-5-1] 95611603 steps 401 queries 20209.55 avg class size
c [sweep-5-1] 3243 decisions 328 SAT calls 86.60 avg env size
c [sweep-5-1] 457828 variables remain 99% (3635 retained 1%)
c [decomp-22] removed 2289 variables
c [sweep-5-1] removed 2289 vars (0 failed, 75 eqs, 77 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 2289 vars in TOTAL (1 rounds, 400 queries)
c [phase-count-9] 3125886 negative 99.8% of 3131005 except 5119 0.2%
c [phase-count-9] 3114796 positive 99.5% of 3131005 except 16209 0.5%
c [phase-count-9] less non-negative clauses 5119 than limit 313100 (10.0%)
c [phase-count-9] non-pos/non-neg = 16209/5119 = 3.17 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 5772 negative 100%
c [sort-queue-9] sorted 443898 enqueued variables after 35671 conflicts
c [score-dist-9] active 15880 (3%), one 0 (0%), zero 443898 (97%)
c [score-dist-9] max exp 530, different 27 (5%)
c [score-dist-9] median active exp 519, avg 519.3
c [simplification-9] removed 5005 variables 1.1% (459778 remain 37%)
c [simplification-9] removed 186191 irredundant clauses 5.6% (3131005 remain 63%)
c [simplification-9] maximum reduction of 6% = max (1%, 6%)
c [simplification-9] large reduction 6% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 47671 (soft 37671 + delta 10000)
c [simplification-9] new conflict limit 37671 (hard 47671)
c 
c [simplification-10] limit 37671 conflicts (hard 47671) hit after 37671 conflicts
c [quatres-6] found 209784 quaternary clauses 97% in total
c [quatres-6-2] added 297 single-self-subsuming ternary resolvents
c [quatres-6-2] added 14 quaternary resolvents
c [ternres-6] limit 33700152 with penalty 2 = 0 + 2
c [ternres-6] 331774 schedulable variables 72%
c [ternres-6] 171810 ternary resolvents (20 bin, 171790 trn)
c [ternres-6] 269918 variables remain 59% (189860 retained 41%)
c [card-4] limit 2106259 penalty 5 = 3 + 2
c [card-4] found 715 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2106259 for elimination
c [card-4] 715 out of 715 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [basicprobe-4] limit 100000000 penalty 2 = 0 + 2
c [basicprobe-4-0] 843 sched 0%, 396 failed, 18 lifted, 9758 hbrs
c [decomp-24] removed 2053 variables
c [basicprobe-4-1] 3783 probes remain 1% after last round
c [basicprobe-4-1] 660 units = 641 failed (97%) + 19 lifted (3%)
c [basicprobe-4-1] removed 4013 variables, found 24799 hbrs
c [bate-2] eliminated 450 asymmetric tautologies during probing
c [unhide-10] limit 1250000 with penalty 4 = 0 + 4
c [unhide-10-10] 28 units, 2252 failed, 9573 tauts, 0 hbrs, 64958 literals
c [transred-6] limit 3095021 based on 3095021 irredundant clauses
c [transred-6] removed 11 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 448370 variables 100%
c [block-3] limit of 50000000 steps penalty 4 = 2 + 2
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 144 blocked clauses
c [block-3] 144 < 1/100 * 3095011 = 30950 considered unsuccessful
c [cce-3] limit of 42125190 steps penalty 4 = 2 + 2
c [cce-3-1] eliminated 2 clauses out of 20 (10%) of length 18
c [cce-3-1] eliminated 1 clauses out of 24 (4%) of length 17
c [cce-3-1] eliminated 4 clauses out of 36 (11%) of length 16
c [cce-3-1] eliminated 4 clauses out of 46 (9%) of length 15
c [cce-3-1] eliminated 56 clauses out of 127 (44%) of length 14
c [cce-3-1] eliminated 54 clauses out of 514 (11%) of length 13
c [cce-3-1] eliminated 321 clauses out of 660 (49%) of length 12
c [cce-3-1] eliminated 85 clauses out of 144 (59%) of length 11
c [cce-3-1] eliminated 84 clauses out of 129 (65%) of length 10
c [cce-3-1] eliminated 279 clauses out of 1359 (21%) of length 9
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 890 large clauses in 42125566 steps
c [cce-3-1] allowing another 21062783 steps for small clauses
c [cce-3-1] scheduling 2282292 clauses = 1023711 binary + 1258581 ternary
c [cce-3-1] tried to eliminate 268 small clauses 0%
c [cce-3-1] eliminated 57 binary clauses 0%
c [cce-3-1] eliminated 2 ternary clauses 0%
c [cce-3-1] eliminated 59 small clauses 0%
c [cce-3-1] eliminated 59 small clauses in 42125194 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 949 covered clauses in round 1
c [cce-3] eliminated 949 covered clauses in TOTAL during 1 rounds
c [cce-3] 949 < 1/100 * 3045420 = 30454 considered unsuccessful
c [bca-6] limit of 10000000 steps and 6094670 added (scaled 2)
c [bca-6] 891748 out of 896742 literals actually usable 99%
c [bca-6] added 1064 blocked clauses in 1842523 steps
c [sweep-6] limit 10110045 penalty 2 = 0 + 2
c [sweep-6-1] 238855 pos 53.7% + 206333 neg 46.3% = 445188 sched 99.3% ret 3182
c [sweep-6-1] 10311628 steps 43 queries 102597.58 avg class size
c [sweep-6-1] 179 decisions 38 SAT calls 42.68 avg env size
c [sweep-6-1] 444973 variables remain 99% (3397 retained 1%)
c [decomp-25] removed 541 variables
c [sweep-6-1] removed 541 vars (0 failed, 4 eqs, 5 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 541 vars in TOTAL (1 rounds, 42 queries)
c [phase-count-10] 3038178 negative 99.8% of 3043172 except 4994 0.2%
c [phase-count-10] 3026485 positive 99.5% of 3043172 except 16687 0.5%
c [phase-count-10] less non-negative clauses 4994 than limit 304300 (10.0%)
c [phase-count-10] non-pos/non-neg = 16687/4994 = 3.34 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 5709 negative 100%
c [sort-queue-10] sorted 432016 enqueued variables after 37671 conflicts
c [score-dist-10] active 15813 (4%), one 0 (0%), zero 432016 (96%)
c [score-dist-10] max exp 531, different 28 (5%)
c [score-dist-10] median active exp 519, avg 519.4
c [simplification-10] removed 11949 variables 2.6% (447829 remain 36%)
c [simplification-10] removed 87833 irredundant clauses 2.8% (3043172 remain 62%)
c [simplification-10] maximum reduction of 3% = max (3%, 3%)
c [simplification-10] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-10] new conflict interval 21666
c [simplification-10] penalized conflict interval 21666 = 1 * 21666
c [simplification-10] hard conflict limit 70170 (soft 59337 + delta 10833)
c [simplification-10] new conflict limit 59337 (hard 70170)
c 
c [simplification-11] limit 59337 conflicts (hard 70170) hit after 59341 conflicts
c [quatres-7] found 162564 quaternary clauses 96% in total
c [quatres-7-2] added 949 single-self-subsuming ternary resolvents
c [quatres-7-2] added 7 quaternary resolvents
c [ternres-7] limit 50000000 with penalty 2 = 0 + 2
c [ternres-7] 262952 schedulable variables 59%
c [ternres-7] 251051 ternary resolvents (29 bin, 251022 trn)
c [ternres-7] 195047 variables remain 44% (252782 retained 56%)
c [gauss-4] limit 2791027 penalty 4 = 2 + 2
c [gauss-4] extracted 167 xors of average arity 3.0
c [gauss-4] connected 495 occurrences of 486 variables (average 1.0)
c [gauss-4] limit 2791027 penalty 4 = 2 + 2
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-26] removed 3 variables
c [simpleprobe-5] 363645 schedulable variables 81%
c [simpleprobe-5] limit 50000000 penalty 2 = 0 + 2
c [decomp-27] removed 135 variables
c [simpleprobe-5] 364019 variables remain 81% (83672 retained 19%)
c [simpleprobe-5] removed 135 variables, found 826 hbrs, 8 units
c [unhide-11] limit 1250000 with penalty 4 = 0 + 4
c [unhide-11-11] 41 units, 516 failed, 27301 tauts, 0 hbrs, 210173 literals
c [transred-7] limit 3017756 based on 3017756 irredundant clauses
c [transred-7] removed 14 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 444601 variables 100%
c [elim-9] limit of 200000000 steps penalty 2 = 1 + 1
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 154674 not tried 35% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 92145 = 21% variables out of 444601 scheduled
c [bca-7] limit of 10000000 steps and 5722172 added (scaled 2)
c [bca-7] 700904 out of 704914 literals actually usable 99%
c [bca-7] added 87 blocked clauses in 1447640 steps
c [sweep-7] limit 33492332 penalty 1 = 0 + 1
c [sweep-7-1] 183157 pos 52.4% + 166674 neg 47.6% = 349831 sched 99.3% ret 2625
c [sweep-7-1] 33704458 steps 163 queries 34155.08 avg class size
c [sweep-7-1] 1052 decisions 145 SAT calls 93.87 avg env size
c [sweep-7-1] 347540 variables remain 99% (3967 retained 1%)
c [decomp-28] removed 1043 variables
c [sweep-7-1] removed 1043 vars (0 failed, 19 eqs, 29 impls)
c [sweep-7] removed 1043 vars in TOTAL (1 rounds, 162 queries)
c [phase-count-11] 2843854 negative 99.8% of 2848555 except 4701 0.2%
c [phase-count-11] 2832042 positive 99.4% of 2848555 except 16513 0.6%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 1462 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 336175 enqueued variables after 59341 conflicts
c [score-dist-11] active 15238 (4%), one 0 (0%), zero 336175 (96%)
c [score-dist-11] max exp 532, different 29 (5%)
c [score-dist-11] median active exp 520, avg 520.2
c [simplification-11] removed 96416 variables 21.5% (351413 remain 28%)
c [simplification-11] removed 194617 irredundant clauses 6.4% (2848555 remain 58%)
c [simplification-11] maximum reduction of 22% = max (22%, 6%)
c [simplification-11] large reduction 22% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 71341 (soft 61341 + delta 10000)
c [simplification-11] new conflict limit 61341 (hard 71341)
c 
c [simplification-12] limit 61341 conflicts (hard 71341) hit after 61341 conflicts
c [quatres-8] found 234258 quaternary clauses 96% in total
c [quatres-8-1] removed 4 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 3730 single-self-subsuming ternary resolvents
c [quatres-8-2] added 3101 quaternary resolvents
c [ternres-8] limit 100000000 with penalty 1 = 0 + 1
c [ternres-8] 153109 schedulable variables 44%
c [ternres-8] 775042 ternary resolvents (129 bin, 774913 trn)
c [ternres-8] 25173 variables remain 7% (326240 retained 93%)
c [decomp-29] removed 3 variables
c [treelook-5] limit 11476893 penalty 1 = 0 + 1 boost 1
c [treelook-5] scheduled 108505 literals 15%
c [treelook-5] scheduling used 4137839 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 11476893 penalty 1 = 0 + 1 boost 1
c [treelook-5] used 11484372 steps
c [treelook-5] 106671 literals remain 15%
c [treelook-5] 2229 variables remain to probed next time 1%
c [decomp-30] removed 203 variables
c [treelook-5] removed 1567 variables, found 3286 hbrs
c [unhide-12] limit 2500000 with penalty 3 = 0 + 3
c [unhide-12-12] 7 units, 790 failed, 6833 tauts, 0 hbrs, 37031 literals
c [transred-8] limit 2817865 based on 2817865 irredundant clauses
c [transred-8] removed 84 transitive binary clauses
c [elim-10] 151805 variables 44% will be scheduled this time
c [elim-10] scheduled 151805 variables 44%
c [elim-10] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 822 not tried 0% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 10414 = 7% variables out of 151805 scheduled
c [bca-8] limit of 10000000 steps and 5328310 added (scaled 2)
c [bca-8] 663306 out of 673364 literals actually usable 99%
c [bca-8] added 10 blocked clauses in 1374685 steps
c [sweep-8] limit 34430681 penalty 1 = 0 + 1
c [sweep-8-1] 175459 pos 52.7% + 157546 neg 47.3% = 333005 sched 98.9% ret 3676
c [sweep-8-1] 34508128 steps 178 queries 32518.35 avg class size
c [sweep-8-1] 885 decisions 139 SAT calls 49.73 avg env size
c [sweep-8-1] 331623 variables remain 99% (4569 retained 1%)
c [decomp-31] removed 935 variables
c [sweep-8-1] removed 935 vars (0 failed, 43 eqs, 56 impls)
c [sweep-8] removed 935 vars in TOTAL (1 rounds, 177 queries)
c [phase-count-12] 2651626 negative 99.8% of 2656256 except 4630 0.2%
c [phase-count-12] 2640045 positive 99.4% of 2656256 except 16211 0.6%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 259 positive 56%, 207 negative 44%
c [sort-queue-12] sorted 319884 enqueued variables after 61341 conflicts
c [score-dist-12] active 15862 (5%), one 0 (0%), zero 319884 (95%)
c [score-dist-12] max exp 532, different 29 (5%)
c [score-dist-12] median active exp 520, avg 520.5
c [simplification-12] removed 15667 variables 4.5% (335746 remain 27%)
c [simplification-12] removed 192299 irredundant clauses 6.8% (2656256 remain 54%)
c [simplification-12] maximum reduction of 7% = max (4%, 7%)
c [simplification-12] large reduction 7% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 73341 (soft 63341 + delta 10000)
c [simplification-12] new conflict limit 63341 (hard 73341)
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 1190 basic ate = 950 trn 80% + 240 lrg 20% in 2 updates
c bcas: 8 count, 11618 added (796 skipped), 14919614 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: 3 bces, 5071 removed, 31300232 resolutions, 90379376 steps
c blkd: 5321 blocking literals 0%, 1 pure
c bump: 62886 bumped seen, 23506634 lits 373.8 on average
c card: 4 count, 0 units, 0 am1, 11592627 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 33212 subsumed
c card: 2698 at-most-one constraints found, average size 3.58
c card: 2698 at-most-one constraints used 100%, average size 3.58
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: 3 cces, 1429 eliminated, 1074 ate 75%, 355 abce 25%
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: 18026410 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 72 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 31 decompositions, 49149 equivalent 4%
c deco: 12868 decision-only clauses 20%, 38% reduction
c decs: 1699497 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 10 elims, 573764 eliminated 44%, 108 pure 0%
c elms: 10 rounds, 1.0 rounds/bve
c elms: 571027 small 100%, 2628 large 0%
c elms: 1547757 tried small, 571027 succeeded 37%, 976730 failed 63%
c elms: 275098 subsumed, 56147 strengthened, 74 blocked
c elms: 38383021 copies, 30763892 resolutions, 79970981 ipos
c elms: 43069951 subchks, 26718707 strchks
c gaus: 4 extractions, 750 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 0 binary and 1 ternary equations
c gaus: 0 gc, 18716872 steps, 9358436 extr 50%, 5223 elim 0%
c glue: 193.5 orig avg, 193.5 real avg, 9.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 106317 = 2837 simple 3% + 102302 trn 96% + 1178 lrg 1%, 17713 sub 17%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 62886 clauses, 246.7 length
c lrnd: 15516842 lits = 17926960 orig - 2410118 removed 13%
c lrnd: 25716 uips 41%, 29630 flips 47%
c mins: 24443 mins 64%, 253 bin 1%, 741 size 2%
c mins: 1129950 poisoned searches, 309508 hits, 27% hit rate
c mins: 3308549 used twice searches, 1806240 hits, 55% hit rate
c move: moved 43164, 725 bin 2%, 42439 trn 98%
c otfs: 474 driving 21%, 1752 restarting 79%
c otfs: str 2226, 2115 red 95%, 111 irr 5%
c otfs: str 2226, 0 bin 0%, 70 trn 3%, 2156 lrg 97%
c otfs: sub 8, 8 red 100%, 0 irr 0%
c otfs: sub 8, 0 bin 0%, 0 trn 0%, 8 lrg 100%
c phas: 12 computed, 1774783 set, 1721 pos (0%), 1773062 neg (100%)
c prbs: 4 basic, 30459 probed, 983 failed, 56 lifted
c prbs: 5 simple, 929320 probed, 16 failed, 201 eqs
c prbs: 5 treelook, 630 probed, 71 failed, 0 lifted
c prom: 0 locked 0% out of 33963 tried
c prps: 2066944268 props, 1198 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 8 count, 3452 quat, 5926 self1, 1 self2, 189 dup
c queu: 12 sorted, 1699497 next (54296 steps 0.03)
c queu: 31586812 enq (39711478 steps 1.26), 23506634 deq 74%
c redc: 236 clauses 10%, 2248 tried 4%, 102 sat 5%
c redc: 284 lits 1%, 23239 tried 0%, 102 sat 0%
c redc: 33 times jump level reduced, 13.7 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 101051 removed, 14810 red 15%
c rsts: 5129 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: 62886 count (188927 tried 3.0), 12274 sub out of 61808 (19.9%)
c swps: 8 count, 8 rounds, 907 queries (113.4/round)
c swps: 752 sat calls, 16 unsat (0.3% success rate)
c swps: 6828 decisions 9.1, 250 conflicts 0.3
c swps; 42616.9 avg class size, 89.1 avg environment size
c swps: 0 failed, 195 impls, 165 equivs
c swp0: 300 type 0 queries, 66 unsat (22.0%), 293 sat (97.7%)
c swp1: 607 type 1 queries, 477 unsat (78.6%), 449 sat (74.0%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 3524983 calls to obtain time
c tops: 337576 fixed 26%, 1 its, 63110.00 confs/it
c trds: 8 transitive reductions, 154 removed, 1 failed
c trds: 3954 nodes, 4431 edges, 26260047 steps
c trim: 11839 words, 0.0 MB
c trnr: 8 count, 263 bin, 1408826 trn, 291310293 steps
c unhd: 12 count, 12 rounds, 190106956 steps
c unhd: 605 non-trivial sccs of average size 3.1
c unhd: 234 units, 203 bin, 20 trn, 11 lrg
c unhd: 10256 failed, 9966 stamp, 0 lits, 54 bin, 229 trn, 11 lrg
c unhd: 206957 tauts, 615 bin 0%, 84762 trn 41%, 1229 lrg 1%
c unhd: 206957 tauts, 120351 stamp 58%, 78883 red 38%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 835688 str, 203 bin 0%, 24154 trn 3%, 811331 lrg 97%, 561096 red 67%
c vars: 335746 remaining 26% and 960489 removed 74% out of 1296235
c vars: 337576 fixed 26%, 573764 eliminated 44%, 49149 equivalent 4%
c vsts: 24184730282 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 11.7 search visits per propagation, 378073.1 per conflict
c wchs: 915453991 pushed, 186976941 enlarged, 115 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          65260             0             0       2807753        832876         28741
c 
c  0 0          4463   7         0   0<        0   0<   612718  22    146442  18      2954  10     0.1
c  1 5           492   1         0   0         0   0    119334   4     35388   4      1070   4     0.0
c  2 6          1431   2         0   0         0   0    279639  10     86650  10      3260  11     0.1
c  3 9          1803   3         0   0         0   0    377558  13     95168  11      3292  11     0.1
c  4 14         1685   3         0   0         0   0    266603   9<    64033   8      2063   7     0.1
c  5 21         1783   3         0   0         0   0    224086   8     57701   7<     1681   6     0.2
c  6 30         1831   3         0   0         0   0    225787   8     65755   8      1472   5<    0.2
c  7 41         1271   2         0   0         0   0    171353   6     38097   5       759   3     0.2
c  8 54         1133   2         0   0         0   0    145905   5     41935   5       892   3     0.2
c  9 69         1205   2         0   0         0   0     49890   2     21524   3       807   3     0.3
c 10 86         2483   4<        0   0         0   0     89972   3     39274   5      1628   6     0.9
c 11 126       12821  20         0   0         0   0    152521   5     83562  10      4089  14     8.3
c 12 230       32859  50         0   0         0   0     92387   3     57347   7      4774  17    29.0
c 
c avg                  9.6           0.0           0.0           4.2           5.1           6.3
c std                  3.8           0.0           0.0           3.5           4.0           4.3
c 
c  117.528  12% elim
c   33.420   3% probe
c   27.854   3% sweep
c   27.725   3% quatres
c   23.650   2% unhide
c   10.141   1% bca
c    9.056   1% block
c    7.103   1% cce
c    5.043   1% bump
c 
c   13.048 < 1% rest (below)
c 
c    4.102   0% gauss
c    3.996   0% ternres
c    3.218   0% transred
c    0.904   0% card
c    0.829   0% decide
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   10.340   1% preprocessing     3%
c  295.548  30% inprocessing     97%
c ==================================
c  305.887  31% simplifying
c  690.845  69% search
c ==================================
c  996.755 100% all
c 
c         63110 conflicts,          63.3 confs/sec
c           586 ternaries,         107.7 confs/ternary
c           291 binaries,          216.9 confs/binary
c             1 iterations,      63110.0 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          5129 restarts,            5.1 rests/sec,     12.3 confs/restart
c       1699497 decisions,        1705.0 decis/sec,     26.9 decis/conflict
c    2066944268 propagations,  2073672.4 props/sec,   1216.2 props/decision
c 
c 996.8 seconds, 461.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
