c launch: /data/cnf/sc2014/app/atco_enc1_opt2_05_4.cnf.bz2
c host: atom04
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_enc1_opt2_05_4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc1_opt2_05_4.cnf.bz2
c no embedded options
c found 'p cnf 14636 386163' header
c read 14636 variables, 386163 clauses, 1652800 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=4
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 14409 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   14409   371044         0       0      0     0    0     0   23   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 3123 at-most-one constraints of average size 3.0
c [card-1] found 64 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 3186 out of 3187 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1111 variables
c [simpleprobe-1] all 13525 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 258 variables
c [simpleprobe-1] 11193 variables remain 84% (2074 retained 16%)
c [simpleprobe-1] removed 258 variables, found 1943 hbrs, 8 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 54 units, 20 failed, 5914 tauts, 0 hbrs, 58 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 13195 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 3538 variables 27% in round 1 in 15295870 steps
c [elim-1-1] backward subsumption/strengthening limit 4704130
c [elim-1-1-1] backward checking 9353 touched variables 71%
c [elim-1-1-1] incomplete backward checking 8888 remain 95%
c [elim-1-1] subsumed 148 and strengthened 0 clauses in 4705085 steps
c [elim-1] incomplete 23 not tried 0% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 3538 = 27% variables out of 13195 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 321821 negative 93.0% of 345904 except 24083 7.0%
c [phase-count-1] 326580 positive 94.4% of 345904 except 19324 5.6%
c [phase-1] phase bias: 4898 positive 51%, 4759 negative 49%
c [sort-queue-1] sorted 9657 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 9657 (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 4507 variables 31.8% (9657 remain 67%)
c [simplification-1] removed 25140 irredundant clauses 6.8% (345904 remain 93%)
c [simplification-1] maximum reduction of 32% = max (32%, 7%)
c [simplification-1] large reduction 32% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 12 variables
c [simpleprobe-2] 8197 schedulable variables 85%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 1 variables
c [simpleprobe-2] 8247 variables remain 86% (1397 retained 14%)
c [simpleprobe-2] removed 1 variables, found 180 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 7266 literals 38%
c [treelook-1] scheduling used 300689 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 305177 steps
c [treelook-1] 7215 literals remain 37%
c [treelook-1] 6193 variables remain to probed next time 64%
c [decomp-5] removed 8 variables
c [treelook-1] removed 8 variables, found 131 hbrs
c [basicprobe-1] limit 2766928 based on 345866 irredundant clauses
c [basicprobe-1-0] 877 probes remain 9% after last round
c [basicprobe-1-0] 12 units = 12 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 14 variables, found 3940 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 1273 tauts, 0 hbrs, 1981 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 9622 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 2451 not tried 25% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 97 = 1% variables out of 9622 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 320327 negative 93.0% of 344355 except 24028 7.0%
c [phase-count-2] 325167 positive 94.4% of 344355 except 19188 5.6%
c [phase-2] phase bias: 3 positive 30%, 7 negative 70%
c [sort-queue-2] sorted 7979 enqueued variables after 1000 conflicts
c [score-dist-2] active 1546 (16%), one 0 (0%), zero 7979 (84%)
c [score-dist-2] max exp 509, different 12 (2%)
c [score-dist-2] median active exp 502, avg 503.0
c [simplification-2] removed 132 variables 1.4% (9525 remain 66%)
c [simplification-2] removed 1540 irredundant clauses 0.4% (344355 remain 93%)
c [simplification-2] maximum reduction of 1% = max (1%, 0%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 10000
c [simplification-2] penalized conflict interval 10000 = 1 * 10000
c [simplification-2] hard conflict limit 21000 (soft 11000 + delta 10000)
c [simplification-2] new conflict limit 11000 (hard 21000)
c 
c [simplification-3] limit 11000 conflicts (hard 21000) hit after 11000 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1179 at-most-one constraints of average size 3.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1179 out of 1179 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 139 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 6531 literals 35%
c [treelook-2] scheduling used 301152 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 503660 steps
c [treelook-2] 6449 literals remain 34%
c [treelook-2] 4046 variables remain to probed next time 43%
c [treelook-2] removed 7 variables, found 142 hbrs
c [elim-3] 2341 variables 25% will be scheduled this time
c [elim-3] scheduled 2341 variables 25%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 1422 not tried 15% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 2341 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 318432 negative 92.6% of 343808 except 25376 7.4%
c [phase-count-3] 323885 positive 94.2% of 343808 except 19923 5.8%
c [phase-3] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-3] sorted 7481 enqueued variables after 11000 conflicts
c [score-dist-3] active 1898 (20%), one 0 (0%), zero 7481 (80%)
c [score-dist-3] max exp 510, different 52 (10%)
c [score-dist-3] median active exp 499, avg 490.0
c [simplification-3] removed 146 variables 1.5% (9379 remain 65%)
c [simplification-3] removed 541 irredundant clauses 0.2% (343808 remain 93%)
c [simplification-3] maximum reduction of 2% = max (2%, 0%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 16666
c [simplification-3] penalized conflict interval 16666 = 1 * 16666
c [simplification-3] hard conflict limit 37666 (soft 27666 + delta 10000)
c [simplification-3] new conflict limit 27666 (hard 37666)
c 
c [simplification-4] limit 27666 conflicts (hard 37666) hit after 27666 conflicts
c [decomp-8] removed 6 variables
c [basicprobe-2] limit 9819440 penalty 0 = 0 + 0
c [basicprobe-2-0] 830 sched 9%, 18 failed, 3 lifted, 3340 hbrs
c [decomp-9] removed 163 variables
c [basicprobe-2-1] 1415 sched 15%, 10 failed, 0 lifted, 738 hbrs
c [decomp-10] removed 18 variables
c [basicprobe-2-2] 1353 probes remain 15% after last round
c [basicprobe-2-2] 31 units = 28 failed (90%) + 3 lifted (10%)
c [basicprobe-2-2] removed 181 variables, found 4078 hbrs
c [unhide-3] limit 196388 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 1738 tauts, 0 hbrs, 41621 literals
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 9192 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 785555260 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 81 variables 1% in round 1 in 648994203 steps
c [elim-4-1] backward subsumption/strengthening limit 136561057
c [elim-4-1-1] backward checking 1590 touched variables 17%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 199 and strengthened 18 clauses in 18197080 steps
c [elim-4-1] rescheduled 172 variables 2% by backward subsumption
c [elim-4-2] eliminated 1 variables 0% in round 2 in 4952734 steps
c [elim-4-2] backward subsumption/strengthening limit 4952700
c [elim-4-2-1] backward checking 10 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 1 and strengthened 0 clauses in 407160 steps
c [elim-4-2] rescheduled 6 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 2320967 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 82 = 1% variables out of 9192 scheduled
c [elim-4] 82 < 1/100 * 9192 = 91 considered unsuccessful
c [phase-count-4] 314419 negative 92.2% of 340934 except 26515 7.8%
c [phase-count-4] 322246 positive 94.5% of 340934 except 18688 5.5%
c [phase-4] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-4] sorted 6317 enqueued variables after 27666 conflicts
c [score-dist-4] active 2793 (31%), one 0 (0%), zero 6317 (69%)
c [score-dist-4] max exp 508, different 84 (17%)
c [score-dist-4] median active exp 496, avg 483.9
c [simplification-4] removed 269 variables 2.9% (9110 remain 63%)
c [simplification-4] removed 2870 irredundant clauses 0.8% (340934 remain 92%)
c [simplification-4] maximum reduction of 3% = max (3%, 1%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 21666
c [simplification-4] penalized conflict interval 21666 = 1 * 21666
c [simplification-4] hard conflict limit 60165 (soft 49332 + delta 10833)
c [simplification-4] new conflict limit 49332 (hard 60165)
c 
c [simplification-5] limit 49332 conflicts (hard 60165) hit after 49333 conflicts
c [quatres-1] found 62193 quaternary clauses 27% in total
c [quatres-1-1] removed 2 duplicate quaternary clauses
c [quatres-1-2] added 7 single-self-subsuming ternary resolvents
c [quatres-1-2] added 4 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 22612650 with penalty 0 = 0 + 0
c [ternres-1] all 9110 free variables schedulable
c [ternres-1] 1123 ternary resolvents (3 bin, 1120 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 89 xors of average arity 3.0
c [gauss-1] connected 263 occurrences of 242 variables (average 1.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 7 variables
c [simpleprobe-3] 7793 schedulable variables 86%
c [simpleprobe-3] limit 18090121 penalty 0 = 0 + 0
c [decomp-12] removed 5 variables
c [simpleprobe-3] 7452 variables remain 82% (1646 retained 18%)
c [simpleprobe-3] removed 5 variables, found 767 hbrs, 0 units
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 1780 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 9098 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 1178 blocked clauses
c [block-1] 1178 < 1/100 * 340364 = 3403 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 149 clauses out of 2981 (5%) of length 12
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 149 large clauses in 30000608 steps
c [cce-1-1] allowing another 15000304 steps for small clauses
c [cce-1-1] scheduling 106727 clauses = 18337 binary + 88390 ternary
c [cce-1-1] tried to eliminate 1082 small clauses 1%
c [cce-1-1] eliminated 3 binary clauses 0%
c [cce-1-1] eliminated 61 ternary clauses 0%
c [cce-1-1] eliminated 64 small clauses 0%
c [cce-1-1] eliminated 64 small clauses in 30000050 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 213 covered clauses in round 1
c [cce-1] eliminated 213 covered clauses in TOTAL during 1 rounds
c [cce-1] 213 < 1/100 * 339186 = 3391 considered unsuccessful
c [bca-1] limit of 10000000 steps and 678446 added (scaled 2)
c [bca-1] 14225 out of 18192 literals actually usable 78%
c [bca-1] added 46 blocked clauses in 73269 steps
c [sweep-1] limit 1356759 penalty 0 = 0 + 0
c [sweep-1-1] 5315 pos 58.4% + 3780 neg 41.6% = 9095 sched 100.0% ret 0
c [sweep-1-1] 1437864 steps 29 queries 1270.38 avg class size
c [sweep-1-1] 1467 decisions 29 SAT calls 121.59 avg env size
c [sweep-1-1] 8903 variables remain 98% (192 retained 2%)
c [decomp-13] removed 2 variables
c [sweep-1-1] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 2 vars in TOTAL (1 rounds, 28 queries)
c [phase-count-5] 312640 negative 92.2% of 338971 except 26331 7.8%
c [phase-count-5] 320346 positive 94.5% of 338971 except 18625 5.5%
c [phase-5] phase bias: 1 positive 50%, 1 negative 50%
c [sort-queue-5] sorted 5788 enqueued variables after 49333 conflicts
c [score-dist-5] active 3305 (36%), one 0 (0%), zero 5788 (64%)
c [score-dist-5] max exp 510, different 97 (19%)
c [score-dist-5] median active exp 496, avg 482.7
c [simplification-5] removed 17 variables 0.2% (9093 remain 63%)
c [simplification-5] removed 1960 irredundant clauses 0.6% (338971 remain 91%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 10833 = 21666 / 2
c [simplification-5] new conflict interval 32499
c [simplification-5] penalized conflict interval 32499 = 1 * 32499
c [simplification-5] hard conflict limit 98081 (soft 81832 + delta 16249)
c [simplification-5] new conflict limit 81832 (hard 98081)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   25.2    9093   338971     62374   23459   2487  5046   15    52   28  28%    622   13   13   12  108%
c 
c [simplification-6] limit 81832 conflicts (hard 98081) hit after 81832 conflicts
c [quatres-2] found 62215 quaternary clauses 27% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [quatres-2-2] added 4 quaternary resolvents
c [ternres-2] limit 7155085 with penalty 0 = 0 + 0
c [ternres-2] all 9093 free variables schedulable
c [ternres-2] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-2] 5069 variables remain 56% (4024 retained 44%)
c [card-3] limit 894385 penalty 2 = 2 + 0
c [card-3] found 793 at-most-one constraints of average size 3.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 894385 for elimination
c [card-3] 793 out of 793 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-14] removed 2 variables
c [treelook-3] limit 715508 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 13356 literals 73%
c [treelook-3] scheduling used 716388 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 715508 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 779409 steps
c [treelook-3] 13337 literals remain 73%
c [treelook-3] 3833 variables remain to probed next time 42%
c [treelook-3] removed 0 variables, found 148 hbrs
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 738 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 9091 variables 100%
c [elim-5] limit of 71550854 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 789 not tried 9% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 74 = 1% variables out of 9091 scheduled
c [elim-5] 74 < 1/100 * 9091 = 90 considered unsuccessful
c [bca-2] limit of 10000000 steps and 677929 added (scaled 2)
c [bca-2] 14159 out of 18036 literals actually usable 79%
c [bca-2] added 37 blocked clauses in 66605 steps
c [sweep-2] limit 2146525 penalty 0 = 0 + 0
c [sweep-2-1] 5305 pos 60.1% + 3520 neg 39.9% = 8825 sched 97.9% ret 192
c [sweep-2-1] 2165629 steps 60 queries 987.43 avg class size
c [sweep-2-1] 2715 decisions 66 SAT calls 108.24 avg env size
c [sweep-2-1] 8200 variables remain 91% (817 retained 9%)
c [decomp-16] removed 11 variables
c [sweep-2-1] removed 11 vars (0 failed, 8 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 11 vars in TOTAL (1 rounds, 59 queries)
c [phase-count-6] 312361 negative 92.2% of 338699 except 26338 7.8%
c [phase-count-6] 320062 positive 94.5% of 338699 except 18637 5.5%
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-6] sorted 5447 enqueued variables after 81832 conflicts
c [score-dist-6] active 3559 (40%), one 0 (0%), zero 5447 (60%)
c [score-dist-6] max exp 509, different 145 (28%)
c [score-dist-6] median active exp 502, avg 470.0
c [simplification-6] removed 87 variables 1.0% (9006 remain 63%)
c [simplification-6] removed 272 irredundant clauses 0.1% (338699 remain 91%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 16249 = 32499 / 2
c [simplification-6] new conflict interval 48748
c [simplification-6] penalized conflict interval 48748 = 1 * 48748
c [simplification-6] hard conflict limit 154954 (soft 130580 + delta 24374)
c [simplification-6] new conflict limit 130580 (hard 154954)
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 -   37.1    9006   338699    106435   28262   2538  4534   20    81   27  25%    819   34   22   13  164%
c 
c [simplification-7] limit 130580 conflicts (hard 154954) hit after 133374 conflicts
c [quatres-3] found 62310 quaternary clauses 26% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-2] added 10 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1 quaternary resolvents
c [ternres-3] limit 13315417 with penalty 0 = 0 + 0
c [ternres-3] 5026 schedulable variables 56%
c [ternres-3] 71 ternary resolvents (0 bin, 71 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1331541 penalty 1 = 1 + 0
c [gauss-2] extracted 64 xors of average arity 3.0
c [gauss-2] connected 192 occurrences of 168 variables (average 1.1)
c [gauss-2] limit 1331541 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 2 variables
c [basicprobe-3] limit 66577085 penalty 0 = 0 + 0
c [basicprobe-3-0] 1311 sched 15%, 10 failed, 0 lifted, 614 hbrs
c [decomp-18] removed 16 variables
c [basicprobe-3-1] 1367 sched 15%, 10 failed, 0 lifted, 113 hbrs
c [decomp-19] removed 10 variables
c [basicprobe-3-2] 1367 sched 15%, 10 failed, 0 lifted, 4 hbrs
c [decomp-20] removed 10 variables
c [basicprobe-3-3] 1367 sched 15%, 2 failed, 0 lifted, 53 hbrs
c [decomp-21] removed 2 variables
c [basicprobe-3-4] 1367 sched 15%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-3-5] 1367 sched 15%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-5] fully completed probing
c [basicprobe-3-5] 32 units = 32 failed (100%) + 0 lifted (0%)
c [basicprobe-3-5] removed 38 variables, found 790 hbrs
c [bate-1] eliminated 32 asymmetric tautologies during probing
c [unhide-4] limit 665770 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 1078 tauts, 0 hbrs, 43475 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 374 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 8966 variables 100%
c [block-2] limit of 66577085 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 4 blocked clauses
c [block-2] 4 < 1/100 * 338252 = 3382 considered unsuccessful
c [cce-2] limit of 33288542 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 13
c [cce-2-1] eliminated 99 clauses out of 2579 (4%) of length 12
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 100 large clauses in 33288570 steps
c [cce-2-1] allowing another 16644285 steps for small clauses
c [cce-2-1] scheduling 105610 clauses = 18048 binary + 87562 ternary
c [cce-2-1] tried to eliminate 1232 small clauses 1%
c [cce-2-1] eliminated 5 binary clauses 0%
c [cce-2-1] eliminated 50 ternary clauses 0%
c [cce-2-1] eliminated 55 small clauses 0%
c [cce-2-1] eliminated 55 small clauses in 33288565 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 155 covered clauses in round 1
c [cce-2] eliminated 155 covered clauses in TOTAL during 1 rounds
c [cce-2] 155 < 1/100 * 338248 = 3382 considered unsuccessful
c [bca-3] limit of 10000000 steps and 676727 added (scaled 2)
c [bca-3] 13649 out of 17932 literals actually usable 76%
c [bca-3] added 11 blocked clauses in 82919 steps
c [sweep-3] limit 3994625 penalty 0 = 0 + 0
c [sweep-3-1] 4967 pos 60.9% + 3191 neg 39.1% = 8158 sched 91.0% ret 807
c [sweep-3-1] 4057432 steps 67 queries 725.39 avg class size
c [sweep-3-1] 2964 decisions 66 SAT calls 132.12 avg env size
c [sweep-3-1] 7360 variables remain 82% (1605 retained 18%)
c [decomp-23] removed 10 variables
c [sweep-3-1] removed 10 vars (0 failed, 10 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 10 vars in TOTAL (1 rounds, 66 queries)
c [sort-queue-7] sorted 5176 enqueued variables after 133374 conflicts
c [score-dist-7] active 3779 (42%), one 62 (1%), zero 5114 (57%)
c [score-dist-7] max exp 510, different 197 (39%)
c [score-dist-7] median active exp 500, avg 447.0
c [simplification-7] removed 51 variables 0.6% (8955 remain 62%)
c [simplification-7] removed 612 irredundant clauses 0.2% (338087 remain 91%)
c [simplification-7] maximum reduction of 1% = max (1%, 0%)
c [simplification-7] geometric conflict interval increment 24374 = 48748 / 2
c [simplification-7] new conflict interval 73122
c [simplification-7] penalized conflict interval 73122 = 1 * 73122
c [simplification-7] hard conflict limit 243057 (soft 206496 + delta 36561)
c [simplification-7] new conflict limit 206496 (hard 243057)
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 -   52.1    8955   338087    144555   34260   2694  3939   16    68   28  23%    909   21    9   14   67%
c -   62.8    8955   338087    180135   36527   2737  3950   16    54   29  29%    957    4   20   14  142%
c 
c [simplification-8] limit 206496 conflicts (hard 243057) hit after 210048 conflicts
c [quatres-4] found 62353 quaternary clauses 26% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-2] added 3 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1 quaternary resolvents
c [ternres-4] limit 26347325 with penalty 0 = 0 + 0
c [ternres-4] all 8955 free variables schedulable
c [ternres-4] 56 ternary resolvents (2 bin, 54 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-24] removed 3 variables
c [simpleprobe-4] 7334 schedulable variables 82%
c [simpleprobe-4] limit 105389303 penalty 0 = 0 + 0
c [decomp-25] removed 4 variables
c [simpleprobe-4] 4267 variables remain 48% (4681 retained 52%)
c [simpleprobe-4] removed 4 variables, found 2528 hbrs, 0 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1530 transitive binary clauses
c [bca-4] limit of 10000000 steps and 676535 added (scaled 2)
c [bca-4] 13389 out of 17898 literals actually usable 75%
c [bca-4] added 1 blocked clauses in 94210 steps
c [sweep-4] limit 7904197 penalty 0 = 0 + 0
c [sweep-4-1] 4512 pos 61.4% + 2841 neg 38.6% = 7353 sched 82.2% ret 1595
c [sweep-4-1] 7926539 steps 140 queries 260.08 avg class size
c [sweep-4-1] 6622 decisions 147 SAT calls 111.29 avg env size
c [sweep-4-1] 5746 variables remain 64% (3196 retained 36%)
c [decomp-26] removed 12 variables
c [sweep-4-1] removed 12 vars (0 failed, 8 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 12 vars in TOTAL (1 rounds, 139 queries)
c [sort-queue-8] sorted 4981 enqueued variables after 210048 conflicts
c [score-dist-8] active 3955 (44%), one 242 (3%), zero 4739 (53%)
c [score-dist-8] max exp 509, different 215 (42%)
c [score-dist-8] median active exp 502, avg 455.9
c [simplification-8] removed 19 variables 0.2% (8936 remain 62%)
c [simplification-8] removed 162 irredundant clauses 0.0% (337925 remain 91%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 73122
c [simplification-8] new conflict interval 146244
c [simplification-8] penalized conflict interval 146244 = 1 * 146244
c [simplification-8] hard conflict limit 429414 (soft 356292 + delta 73122)
c [simplification-8] new conflict limit 356292 (hard 429414)
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 -   77.3    8936   337925    216076   39464   2902  5176   17    53   29  32%    986    4   16   15  111%
c -   89.7    8936   337925    251744   41858   2929  5181   17    42   30  41%   1002   -2   32   15  213%
c -  104.7    8936   337925    287700   43559   2947  5191   17    38   30  44%   1011   -7   10   17   57%
c -  116.8    8936   337925    323367   45709   2950  5193   16    29   30  55%   1017  -12   16   16  101%
c -  130.6    8936   337925    359455   47032   2953  5194   15    21   50  73%   1020  -14   16   16   98%
c -  146.7    8936   337925    399751   47374   2953  5194   14    17   50  80%   1022  -10   12   15   78%
c 
c [simplification-9] limit 356292 conflicts (hard 429414) hit after 413127 conflicts
c [quatres-5] found 62453 quaternary clauses 25% in total
c [quatres-5-2] added 9 single-self-subsuming ternary resolvents
c [quatres-5-2] added 10 quaternary resolvents
c [ternres-5] limit 67376960 with penalty 0 = 0 + 0
c [ternres-5] all 8936 free variables schedulable
c [ternres-5] 120 ternary resolvents (2 bin, 118 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-27] removed 1 variables
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 805 transitive binary clauses
c [elim-6] 776 variables 9% will be scheduled this time
c [elim-6] scheduled 776 variables 9%
c [elim-6] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 586 not tried 7% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 776 scheduled
c [bca-5] limit of 10000000 steps and 675653 added (scaled 2)
c [bca-5] 13441 out of 17872 literals actually usable 75%
c [bca-5] added 9 blocked clauses in 88025 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 202130880 penalty 0 = 0 + 0
c [sweep-5-1] 3663 pos 63.8% + 2082 neg 36.2% = 5745 sched 64.3% ret 3190
c [sweep-5-1] 41053303 steps 1725 queries 30.33 avg class size
c [sweep-5-1] 54527 decisions 1662 SAT calls 89.27 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-28] removed 109 variables
c [sweep-5-1] removed 109 vars (0 failed, 119 eqs, 15 impls)
c [sweep-5-2] 5225 pos 59.2% + 3601 neg 40.8% = 8826 sched 100.0% ret 0
c [sweep-5-2] 44725870 steps 1860 queries 25.53 avg class size
c [sweep-5-2] 57465 decisions 1832 SAT calls 88.36 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-29] removed 57 variables
c [sweep-5-2] removed 57 vars (0 failed, 92 eqs, 9 impls)
c [sweep-5-3] 5187 pos 59.2% + 3582 neg 40.8% = 8769 sched 100.0% ret 0
c [sweep-5-3] 43455404 steps 1841 queries 36.22 avg class size
c [sweep-5-3] 54756 decisions 1813 SAT calls 86.73 avg env size
c [sweep-5-3] fully completed sweeping round
c [decomp-30] removed 30 variables
c [sweep-5-3] removed 30 vars (0 failed, 64 eqs, 4 impls)
c [sweep-5] removed 196 vars in TOTAL (3 rounds, 5423 queries)
c [sort-queue-9] sorted 4020 enqueued variables after 413127 conflicts
c [score-dist-9] active 4719 (54%), one 505 (6%), zero 3515 (40%)
c [score-dist-9] max exp 511, different 106 (21%)
c [score-dist-9] median active exp 505, avg 496.2
c [simplification-9] removed 197 variables 2.2% (8739 remain 61%)
c [simplification-9] removed 527 irredundant clauses 0.2% (337398 remain 91%)
c [simplification-9] maximum reduction of 2% = max (2%, 0%)
c [simplification-9] geometric conflict interval increment 48748 = 146244 / 3
c [simplification-9] new conflict interval 194992
c [simplification-9] penalized conflict interval 194992 = 1 * 194992
c [simplification-9] hard conflict limit 705615 (soft 608119 + delta 97496)
c [simplification-9] new conflict limit 608119 (hard 705615)
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 -  169.3    8739   337398    435492   49136   3313  6325   21    51   30  40%   1023   20   18   17  109%
c -  182.9    8739   337398    474599   52761   3317  6325   15    19   31  75%   1023   -9   14   16   87%
c -  196.8    8739   337398    511549   54096   3318  6325   13    17   32  77%   1024   -7   13   15   85%
c -  212.2    8739   337398    548467   53608   3319  6325   13    17   32  73%   1024   -4   13   14   93%
c -  228.6    8739   337398    586826   54932   3320  6326   38    59   51  65%   1024   37   44   16  267%
c -  242.0    8739   337398    624476   56057   3320  6326   15    18   52  82%   1024   -4   14   16   90%
c -  255.5    8739   337398    661708   56613   3320  6326   15    17   52  84%   1024   -3   15   15   97%
c -  269.7    8739   337398    699617   57018   3320  6326   13    16   52  81%   1024   -2   15   14  106%
c 
c [simplification-10] limit 608119 conflicts (hard 705615) hit after 705615 conflicts
c [quatres-6] found 62902 quaternary clauses 25% in total
c [quatres-6-1] removed 32 duplicate quaternary clauses
c [quatres-6-1] added 2 double-self-subsuming ternary resolvents
c [quatres-6-2] added 18 single-self-subsuming ternary resolvents
c [quatres-6-2] added 19 quaternary resolvents
c [ternres-6] limit 132185876 with penalty 0 = 0 + 0
c [ternres-6] all 8739 free variables schedulable
c [ternres-6] 127 ternary resolvents (4 bin, 123 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 8261617 penalty 3 = 3 + 0
c [card-4] found 1036 at-most-one constraints of average size 3.2
c [card-4] found 24 at-most-two constraints of average size 4.0
c [card-4] using previous limit 8261617 for elimination
c [card-4] 1059 out of 1060 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 6609293 penalty 2 = 2 + 0
c [gauss-3] extracted 324 xors of average arity 3.0
c [gauss-3] connected 959 occurrences of 543 variables (average 1.8)
c [gauss-3] limit 6609293 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-4] limit 6609293 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 15661 literals 90%
c [treelook-4] scheduling used 919390 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 6609293 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 6695576 steps
c [treelook-4] 14978 literals remain 86%
c [treelook-4] 3606 variables remain to probed next time 41%
c [decomp-32] removed 4 variables
c [treelook-4] removed 4 variables, found 596 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1506 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 8735 variables 100%
c [block-3] limit of 200000000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 17 blocked clauses
c [block-3] 17 < 1/100 * 336875 = 3368 considered unsuccessful
c [cce-3] limit of 165232345 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1369 clauses out of 2480 (55%) of length 12
c [cce-3-1] eliminated 430 clauses out of 505 (85%) of length 11
c [cce-3-1] eliminated 101 clauses out of 475 (21%) of length 10
c [cce-3-1] eliminated 165 clauses out of 1562 (11%) of length 9
c [cce-3-1] eliminated 5 clauses out of 3158 (0%) of length 8
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2070 large clauses in 165232388 steps
c [cce-3-1] allowing another 82616194 steps for small clauses
c [cce-3-1] scheduling 104390 clauses = 17520 binary + 86870 ternary
c [cce-3-1] tried to eliminate 6128 small clauses 6%
c [cce-3-1] eliminated 99 binary clauses 1%
c [cce-3-1] eliminated 877 ternary clauses 1%
c [cce-3-1] eliminated 976 small clauses 1%
c [cce-3-1] eliminated 976 small clauses in 165232398 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 3046 covered clauses in round 1
c [cce-3] eliminated 3046 covered clauses in TOTAL during 1 rounds
c [cce-3] 3046 < 1/100 * 336858 = 3368 considered unsuccessful
c [bca-6] limit of 10000000 steps and 668176 added (scaled 2)
c [bca-6] 12213 out of 17472 literals actually usable 70%
c [bca-6] added 38 blocked clauses in 89266 steps
c [sweep-6] limit 39655762 penalty 0 = 0 + 0
c [sweep-6-1] 5100 pos 58.4% + 3635 neg 41.6% = 8735 sched 100.0% ret 0
c [sweep-6-1] 39731342 steps 1566 queries 28.73 avg class size
c [sweep-6-1] 49506 decisions 1558 SAT calls 87.15 avg env size
c [sweep-6-1] 532 variables remain 6% (8203 retained 94%)
c [decomp-33] removed 41 variables
c [sweep-6-1] removed 41 vars (0 failed, 62 eqs, 6 impls)
c [sweep-6] removed 41 vars in TOTAL (1 rounds, 1565 queries)
c [sort-queue-10] sorted 4909 enqueued variables after 705615 conflicts
c [score-dist-10] active 3785 (44%), one 1608 (18%), zero 3301 (38%)
c [score-dist-10] max exp 510, different 135 (26%)
c [score-dist-10] median active exp 504, avg 471.8
c [simplification-10] removed 45 variables 0.5% (8694 remain 60%)
c [simplification-10] removed 3608 irredundant clauses 1.1% (333790 remain 90%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 97496 = 194992 / 2
c [simplification-10] new conflict interval 292488
c [simplification-10] penalized conflict interval 292488 = 1 * 292488
c [simplification-10] hard conflict limit 1144347 (soft 998103 + delta 146244)
c [simplification-10] new conflict limit 998103 (hard 1144347)
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 -  290.2    8694   333790    738601   57759   4361  6048   15    29   32  52%   1024    0   14   18   75%
c -  305.1    8694   333790    779348   60686   4369  6048   13    18   33  71%   1024   -7   12   16   77%
c -  320.1    8694   333790    818830   61685   4371  6049   22    39   32  56%   1024   15   30   16  191%
c -  338.0    8694   333790    861095   60829   4381  6059   24    54   50  45%   1024   20   30   19  153%
c -  356.0    8694   333790    904775   63790   4395  6059   17    24   51  69%   1024  -10   19   20   98%
c -  372.4    8694   333790    947525   64850   4397  6060   15    25   51  59%   1024   -9   14   19   77%
c -  388.5    8694   333790    989645   65879   4399  6060   15    21   53  73%   1024   -8   15   17   86%
c -  404.1    8694   333790   1031863   66691   4399  6060   13    18   52  73%   1024   -7   13   15   84%
c 
c [simplification-11] limit 998103 conflicts (hard 1144347) hit after 1050925 conflicts
c [quatres-7] found 62796 quaternary clauses 24% in total
c [quatres-7-1] removed 14 duplicate quaternary clauses
c [quatres-7-2] added 16 single-self-subsuming ternary resolvents
c [quatres-7-2] added 16 quaternary resolvents
c [ternres-7] limit 200000000 with penalty 0 = 0 + 0
c [ternres-7] all 8694 free variables schedulable
c [ternres-7] 36 ternary resolvents (3 bin, 33 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-34] removed 1 variables
c [basicprobe-4] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 1317 sched 15%, 0 failed, 0 lifted, 467 hbrs
c [basicprobe-4-1] 1317 sched 15%, 0 failed, 0 lifted, 51 hbrs
c [basicprobe-4-2] 1317 sched 15%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-4-3] 1317 sched 15%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-3] fully completed probing
c [basicprobe-4-3] removed 0 variables, found 529 hbrs
c [bate-2] eliminated 10 asymmetric tautologies during probing
c [unhide-5] limit 2500000 with penalty 3 = 3 + 0
c [unhide-5-5] 0 units, 0 failed, 799 tauts, 0 hbrs, 141511 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 744 transitive binary clauses
c [bca-7] limit of 10000000 steps and 666317 added (scaled 2)
c [bca-7] 11770 out of 17388 literals actually usable 68%
c [bca-7] added 2 blocked clauses in 110555 steps
c [sweep-7] limit 64317253 penalty 0 = 0 + 0
c [sweep-7-1] 408 pos 77.0% + 122 neg 23.0% = 530 sched 6.1% ret 8163
c [sweep-7-1] 7703482 steps 346 queries 9.83 avg class size
c [sweep-7-1] 9574 decisions 338 SAT calls 88.37 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-38] removed 13 variables
c [sweep-7-1] removed 13 vars (0 failed, 19 eqs, 0 impls)
c [sweep-7-2] 5091 pos 58.7% + 3589 neg 41.3% = 8680 sched 100.0% ret 0
c [sweep-7-2] 53262921 steps 1810 queries 27.79 avg class size
c [sweep-7-2] 56818 decisions 1813 SAT calls 88.85 avg env size
c [sweep-7-2] fully completed sweeping round
c [decomp-39] removed 46 variables
c [sweep-7-2] removed 46 vars (0 failed, 75 eqs, 7 impls)
c [sweep-7-3] 5057 pos 58.6% + 3577 neg 41.4% = 8634 sched 100.0% ret 0
c [sweep-7-3] 3888893 steps 98 queries 532.85 avg class size
c [sweep-7-3] 3724 decisions 98 SAT calls 101.06 avg env size
c [sweep-7-3] 7396 variables remain 86% (1238 retained 14%)
c [decomp-40] removed 2 variables
c [sweep-7-3] removed 2 vars (0 failed, 2 eqs, 0 impls)
c [sweep-7] removed 61 vars in TOTAL (3 rounds, 2251 queries)
c [sort-queue-11] sorted 4427 enqueued variables after 1050925 conflicts
c [score-dist-11] active 4205 (49%), one 1441 (17%), zero 2986 (35%)
c [score-dist-11] max exp 510, different 123 (24%)
c [score-dist-11] median active exp 504, avg 494.1
c [simplification-11] removed 62 variables 0.7% (8632 remain 60%)
c [simplification-11] removed 934 irredundant clauses 0.3% (332856 remain 90%)
c [simplification-11] maximum reduction of 1% = max (1%, 0%)
c [simplification-11] geometric conflict interval increment 146244 = 292488 / 2
c [simplification-11] new conflict interval 438732
c [simplification-11] penalized conflict interval 438732 = 1 * 438732
c [simplification-11] hard conflict limit 1709023 (soft 1489657 + delta 219366)
c [simplification-11] new conflict limit 1489657 (hard 1709023)
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 -  427.3    8632   332856   1073867   67172   4499  6107   18    34   32  53%   1024    8   13   16   80%
c -  447.1    8632   332856   1119991   68955   4499  6111   14    19   53  74%   1024  -10   15   17   86%
c -  466.5    8632   332856   1164113   70542   4500  6111   14    17   55  82%   1024   -7   13   16   84%
c -  486.9    8632   332856   1209024   70115   4502  6113   19    41   53  46%   1024   17   19   16  118%
c -  504.6    8632   332856   1256035   71132   4503  6115   17    23   54  76%   1024   -5   17   18   92%
c -  520.9    8632   332856   1302935   72408   4503  6115   17    25   54  67%   1024   -4   15   19   82%
c -  542.4    8632   332856   1351848   72747   4506  6116   19    32   53  58%   1024    0   21   20  106%
c -  566.6    8632   332856   1403152   74688   4513  6118   17    28   53  61%   1024   -4   17   19   89%
c -  592.6    8632   332856   1456009   76664   4514  6120   15    23   53  66%   1024   -8   14   19   75%
c -  610.8    8632   332856   1504865   78360   4514  6120   15    20   55  75%   1024   -7   15   18   81%
c 
c [simplification-12] limit 1489657 conflicts (hard 1709023) hit after 1525355 conflicts
c [quatres-8] found 62657 quaternary clauses 24% in total
c [quatres-8-1] removed 22 duplicate quaternary clauses
c [quatres-8-2] added 14 single-self-subsuming ternary resolvents
c [quatres-8-2] added 17 quaternary resolvents
c [ternres-8] limit 200000000 with penalty 0 = 0 + 0
c [ternres-8] all 8632 free variables schedulable
c [ternres-8] 56 ternary resolvents (0 bin, 56 trn)
c [ternres-8] fully completed ternary resolution
c [simpleprobe-5] 4057 schedulable variables 47%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-42] removed 1 variables
c [simpleprobe-5] 3835 variables remain 44% (4796 retained 56%)
c [simpleprobe-5] removed 1 variables, found 2879 hbrs, 0 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1964 transitive binary clauses
c [bca-8] limit of 10000000 steps and 664166 added (scaled 2)
c [bca-8] 11302 out of 17264 literals actually usable 65%
c [bca-8] added 4 blocked clauses in 122152 steps
c [sweep-8] limit 99188801 penalty 0 = 0 + 0
c [sweep-8-1] 4454 pos 60.2% + 2940 neg 39.8% = 7394 sched 85.7% ret 1237
c [sweep-8-1] 43033520 steps 1709 queries 21.17 avg class size
c [sweep-8-1] 52259 decisions 1693 SAT calls 87.45 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-43] removed 26 variables
c [sweep-8-1] removed 26 vars (0 failed, 55 eqs, 3 impls)
c [sweep-8-2] 5065 pos 58.9% + 3540 neg 41.1% = 8605 sched 100.0% ret 0
c [sweep-8-2] 45765367 steps 1802 queries 34.15 avg class size
c [sweep-8-2] 54676 decisions 1790 SAT calls 87.58 avg env size
c [sweep-8-2] fully completed sweeping round
c [decomp-44] removed 26 variables
c [sweep-8-2] removed 26 vars (0 failed, 57 eqs, 2 impls)
c [sweep-8-3] 5045 pos 58.8% + 3534 neg 41.2% = 8579 sched 100.0% ret 0
c [sweep-8-3] 10451217 steps 270 queries 162.98 avg class size
c [sweep-8-3] 9223 decisions 276 SAT calls 100.33 avg env size
c [sweep-8-3] 5243 variables remain 61% (3336 retained 39%)
c [decomp-45] removed 11 variables
c [sweep-8-3] removed 11 vars (0 failed, 16 eqs, 2 impls)
c [sweep-8] removed 63 vars in TOTAL (3 rounds, 3778 queries)
c [sort-queue-12] sorted 4075 enqueued variables after 1525355 conflicts
c [score-dist-12] active 4493 (52%), one 1333 (16%), zero 2742 (32%)
c [score-dist-12] max exp 511, different 125 (24%)
c [score-dist-12] median active exp 505, avg 494.1
c [simplification-12] removed 64 variables 0.7% (8568 remain 59%)
c [simplification-12] removed 1078 irredundant clauses 0.3% (331778 remain 89%)
c [simplification-12] maximum reduction of 1% = max (1%, 0%)
c [simplification-12] geometric conflict interval increment 219366 = 438732 / 2
c [simplification-12] new conflict interval 658098
c [simplification-12] penalized conflict interval 658098 = 1 * 658098
c [simplification-12] hard conflict limit 2512502 (soft 2183453 + delta 329049)
c [simplification-12] new conflict limit 2183453 (hard 2512502)
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 -  635.3    8568   331778   1550927   79209   4656  7791   15    23   35  62%   1024   -3   15   17   91%
c -  658.5    8568   331778   1601027   80341   4656  7791   15    21   36  71%   1024   -3   16   16   98%
c -  680.4    8568   331778   1652673   81887   4660  7791   14    20   35  71%   1024   -4   14   16   93%
c -  705.2    8568   331778   1705440   82059   4660  7791   15    26   56  58%   1024   -1   15   17   90%
c -  729.7    8568   331778   1759826   84115   4661  7792   21    35   56  60%   1024    8   20   18  111%
c -  753.4    8568   331778   1813064   85636   4662  7792   25    40   56  62%   1024   10   31   20  155%
c -  779.5    8568   331778   1867899   86076   4662  7792   20    33   56  60%   1024    2   20   20  101%
c -  814.4    8568   331778   1925891   86437   4663  7792   28    43   56  66%   1024   10   33   23  144%
c -  854.3    8568   331778   1986666   87587   4663  7792   24    29   57  83%   1024   -5   27   24  109%
c -  887.0    8568   331778   2047525   87740   4664  7792   21    27   57  78%   1024   -3   18   23   82%
c -  916.3    8568   331778   2105931   88803   4665  7792   29    41   57  70%   1024    9   29   23  127%
c -  953.1    8568   331778   2171287   89740   4665  7792   21    27   57  79%   1024   -2   21   22   98%
c 
c [simplification-13] limit 2183453 conflicts (hard 2512502) hit after 2188399 conflicts
c [quatres-9] found 61987 quaternary clauses 23% in total
c [quatres-9-1] removed 18 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 24 single-self-subsuming ternary resolvents
c [quatres-9-2] added 32 quaternary resolvents
c [ternres-9] limit 200000000 with penalty 0 = 0 + 0
c [ternres-9] all 8568 free variables schedulable
c [ternres-9] 72 ternary resolvents (0 bin, 72 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-5] limit 50000000 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 15783 literals 92%
c [treelook-5] scheduling used 1014588 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 50000000 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 50000034 steps
c [treelook-5] 10207 literals remain 60%
c [treelook-5] 3178 variables remain to probed next time 37%
c [decomp-47] removed 23 variables
c [treelook-5] removed 24 variables, found 2847 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 2153 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 8544 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 732 not tried 9% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 106 = 1% variables out of 8544 scheduled
c [bca-9] limit of 10000000 steps and 640020 added (scaled 2)
c [bca-9] 10844 out of 16878 literals actually usable 64%
c [bca-9] added 2 blocked clauses in 108490 steps
c [sweep-9] limit 156658425 penalty 0 = 0 + 0
c [sweep-9-1] 3280 pos 63.4% + 1896 neg 36.6% = 5176 sched 61.3% ret 3262
c [sweep-9-1] 40368465 steps 1544 queries 21.31 avg class size
c [sweep-9-1] 47601 decisions 1568 SAT calls 87.82 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-48] removed 35 variables
c [sweep-9-1] removed 35 vars (0 failed, 43 eqs, 0 impls)
c [sweep-9-2] 4965 pos 59.1% + 3438 neg 40.9% = 8403 sched 100.0% ret 0
c [sweep-9-2] 45386617 steps 1748 queries 26.48 avg class size
c [sweep-9-2] 51626 decisions 1760 SAT calls 86.24 avg env size
c [sweep-9-2] fully completed sweeping round
c [decomp-49] removed 32 variables
c [sweep-9-2] removed 32 vars (0 failed, 49 eqs, 4 impls)
c [sweep-9-3] 4939 pos 59.0% + 3432 neg 41.0% = 8371 sched 100.0% ret 0
c [sweep-9-3] 45393868 steps 1736 queries 28.91 avg class size
c [sweep-9-3] 51775 decisions 1742 SAT calls 88.16 avg env size
c [sweep-9-3] fully completed sweeping round
c [decomp-50] removed 26 variables
c [sweep-9-3] removed 26 vars (0 failed, 47 eqs, 4 impls)
c [sweep-9] removed 93 vars in TOTAL (3 rounds, 5025 queries)
c [sort-queue-13] sorted 3853 enqueued variables after 2188399 conflicts
c [score-dist-13] active 4492 (54%), one 1416 (17%), zero 2437 (29%)
c [score-dist-13] max exp 512, different 96 (19%)
c [score-dist-13] median active exp 505, avg 499.7
c [simplification-13] removed 223 variables 2.6% (8345 remain 58%)
c [simplification-13] removed 12067 irredundant clauses 3.6% (319711 remain 86%)
c [simplification-13] maximum reduction of 4% = max (3%, 4%)
c [simplification-13] geometric conflict interval increment 131619 = 658098 / 5
c [simplification-13] new conflict interval 789717
c [simplification-13] penalized conflict interval 789717 = 1 * 789717
c [simplification-13] hard conflict limit 3372974 (soft 2978116 + delta 394858)
c [simplification-13] new conflict limit 2978116 (hard 3372974)
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 42 basic ate = 37 trn 88% + 5 lrg 12% in 2 updates
c bcas: 9 count, 150 added (256 skipped), 835491 steps
c bkwd: tried 37637 clauses, 74923 lits, 1.99 lits/clause
c bkwd: checked 12230216 occs, 324.95 occs/clause, 163.24 occs/lit
c bkwd: subsumed 0 binary, 19 ternary, 329 large
c bkwd: strengthened 0 binary, 4 ternary (100% self), 14 large (0% self)
c blkd: 3 bces, 1199 removed, 4568503 resolutions, 15064435 steps
c blkd: 1278 blocking literals 4%, 4 pure
c bump: 2264756 bumped seen, 259734488 lits 114.7 on average
c card: 4 count, 0 units, 0 am1, 19783292 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 16196 subsumed
c card: 6131 at-most-one constraints found, average size 3.10
c card: 6131 at-most-one constraints used 100%, average size 3.10
c card: 88 at-most-two constraints found, average size 4.00
c card: 86 at-most-two constraints used 98%, average size 4.00
c cces: 3 cces, 3414 eliminated, 2719 ate 80%, 695 abce 20%
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: 2038963 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 58 gcs, 0 rescored clauses, 8735 rescored vars
c dcps: 50 decompositions, 1750 equivalent 12%
c deco: 529 decision-only clauses 0%, 47% reduction
c decs: 4699736 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 7 elims, 3901 eliminated 27%, 575 pure 15%
c elms: 10 rounds, 1.4 rounds/bve
c elms: 2503 small 64%, 819 large 21%
c elms: 3129 tried small, 2503 succeeded 80%, 626 failed 20%
c elms: 15029 subsumed, 1477 strengthened, 68 blocked
c elms: 3321349 copies, 3858207 resolutions, 49540 ipos
c elms: 7189944 subchks, 1992668 strchks
c gaus: 3 extractions, 477 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 19907208 steps, 9953604 extr 50%, 19991 elim 0%
c glue: 17.9 orig avg, 17.9 real avg, 3.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 26001 = 8297 simple 32% + 15716 trn 60% + 1988 lrg 8%, 895 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2264756 clauses, 57.8 length
c lrnd: 130792488 lits = 202647632 orig - 71855144 removed 35%
c lrnd: 667761 uips 29%, 1373811 flips 61%
c mins: 2255389 mins 100%, 800 bin 0%, 8037 size 0%
c mins: 266583115 poisoned searches, 61361488 hits, 23% hit rate
c mins: 405399916 used twice searches, 24855905 hits, 6% hit rate
c move: moved 3653, 136 bin 4%, 3517 trn 96%
c otfs: 7357 driving 32%, 15850 restarting 68%
c otfs: str 23207, 23127 red 100%, 80 irr 0%
c otfs: str 23207, 0 bin 0%, 252 trn 1%, 22955 lrg 99%
c otfs: sub 450, 428 red 95%, 22 irr 5%
c otfs: sub 450, 0 bin 0%, 41 trn 9%, 409 lrg 91%
c phas: 6 computed, 9670 set, 4902 pos (51%), 4768 neg (49%)
c prbs: 4 basic, 32992 probed, 72 failed, 3 lifted
c prbs: 5 simple, 37201 probed, 8 failed, 255 eqs
c prbs: 5 treelook, 6371 probed, 3 failed, 0 lifted
c prom: 438798 locked 10% out of 4393146 tried
c prps: 1275663120 props, 269 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 9 count, 104 quat, 102 self1, 3 self2, 2266 dup
c queu: 13 sorted, 4699736 next (298109 steps 0.06)
c queu: 289299636 enq (341816491 steps 1.18), 259734488 deq 90%
c redc: 25924 clauses 15%, 167716 tried 7%, 0 sat 0%
c redc: 40782 lits 2%, 2325375 tried 1%, 0 sat 0%
c redc: 857 times jump level reduced, 5.3 levels on average
c reds: 48 count, 46735.8 conflicts per reduce
c reds: 0 memlim 0%, 48 arith 100%
c reds: 1764110 collected 92%, 149611 retired 8%
c rmbd: 900 removed, 104 red 12%
c rsts: 18006 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: 13 count, 13 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 2264756 count (3739670 tried 1.7), 182827 sub out of 2260832 (8.1%)
c swps: 9 count, 17 rounds, 18334 queries (1078.5/round)
c swps: 18251 sat calls, 643 unsat (1.6% success rate)
c swps: 567298 decisions 31.1, 28796 conflicts 1.6
c swps; 42.0 avg class size, 88.5 avg environment size
c swps: 0 failed, 57 impls, 726 equivs
c swp0: 6105 type 0 queries, 2810 unsat (46.0%), 5904 sat (96.7%)
c swp1: 12229 type 1 queries, 6500 unsat (53.2%), 11704 sat (95.7%)
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: 13946719 calls to obtain time
c tops: 640 fixed 4%, 0 its, 0.00 confs/it
c trds: 9 transitive reductions, 11594 removed, 0 failed
c trds: 157340 nodes, 196389 edges, 6711054 steps
c trim: 1497420 words, 5.7 MB
c trnr: 9 count, 14 bin, 1649 trn, 168730565 steps
c unhd: 5 count, 5 rounds, 16447223 steps
c unhd: 256 non-trivial sccs of average size 2.0
c unhd: 54 units, 54 bin, 0 trn, 0 lrg
c unhd: 20 failed, 18 stamp, 0 lits, 0 bin, 2 trn, 0 lrg
c unhd: 10802 tauts, 386 bin 4%, 2931 trn 27%, 1779 lrg 16%
c unhd: 10802 tauts, 5706 stamp 53%, 4203 red 39%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 228646 str, 54 bin 0%, 141 trn 0%, 228451 lrg 100%, 227376 red 99%
c vars: 8345 remaining 57% and 6291 removed 43% out of 14636
c vars: 640 fixed 4%, 3901 eliminated 27%, 1750 equivalent 12%
c vsts: 54365183572 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 42.7 search visits per propagation, 23998.1 per conflict
c wchs: 10577704065 pushed, 16043457 enlarged, 121 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2260936       1764110        149611      60376489      22408000       1327306
c 
c  0 0         63552   3     11172   1         0   0  27284087  45   6324689  28    285292  21     2.2
c  1 5         55939   2     27969   2     18368  12   6779666  11<  2544380  11    153366  12     0.6
c  2 6        246642  11    166461   9     50551  34  14479182  24   6477757  29<   420566  32<    2.3
c  3 9        487878  22    420223  24     31670  21<  7565248  13   4157412  19    296811  22     7.8
c  4 14       739908  33<   648150  37<    21045  14   2771753   5   1857569   8    111935   8    10.6
c  5 21       413637  18    299880  17     13611   9    968326   2    693988   3     37783   3     7.4
c  6 30       153737   7    114313   6      7688   5    326781   1    223940   1     13163   1     3.4
c  7 41        66842   3     51888   3      4056   3    136103   0     88568   0      5582   0     1.4
c  8 54        23109   1     17441   1      1613   1     44841   0     28366   0      1955   0     0.8
c  9 69         6878   0      4902   0       605   0     14132   0      8194   0       598   0     0.4
c 10 86         2455   0      1534   0       324   0      5610   0      2797   0       235   0     0.3
c 11 126         359   0       177   0        80   0       760   0       340   0        20   0     0.1
c 
c avg                  3.9           3.9           3.1           1.3           1.8           2.0
c std                  1.5           1.3           1.7           1.4           1.5           1.5
c 
c   34.852   3% bump
c   20.583   2% sweep
c   11.129   1% elim
c    9.595   1% probe
c    4.703   0% rescore
c    2.815   0% quatres
c 
c   11.930 < 1% rest (below)
c 
c    2.808   0% cce
c    2.682   0% decide
c    1.709   0% unhide
c    1.202   0% bca
c    0.990   0% ternres
c    0.986   0% block
c    0.780   0% transred
c    0.485   0% gauss
c    0.287   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.372   0% preprocessing     2%
c   55.160   6% inprocessing     98%
c ==================================
c   56.532   6% simplifying
c  943.188  94% search
c ==================================
c  999.720 100% all
c 
c       2243317 conflicts,        2243.9 confs/sec
c           586 ternaries,        3828.2 confs/ternary
c           358 binaries,         6266.2 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            48 reductions,          0.0 redus/sec,  46735.8 confs/reduction
c         18006 restarts,           18.0 rests/sec,    124.6 confs/restart
c       4699736 decisions,        4701.1 decis/sec,      2.1 decis/conflict
c    1275663120 propagations,  1276020.8 props/sec,    271.4 props/decision
c 
c 999.7 seconds, 82.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
