c launch: /data/cnf/sc2014/app/atco_enc2_opt2_05_9.cnf.bz2
c host: atom05
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 Wed Apr 29 14:26:58 CEST 2015
c compiled Fri May  1 18:19:30 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT
c Linux fmvx1 3.13.0-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/atco_enc2_opt2_05_9.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc2_opt2_05_9.cnf.bz2
c no embedded options
c found 'p cnf 14912 390488' header
c read 14912 variables, 390488 clauses, 1669846 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 14685 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   14685   375369         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 3099 at-most-one constraints of average size 3.0
c [card-1] found 87 at-most-two constraints of average size 4.9
c [card-1] using previous limit 2000000 for elimination
c [card-1] 3186 out of 3186 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1109 variables
c [simpleprobe-1] all 13803 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 233 variables
c [simpleprobe-1] 11401 variables remain 84% (2169 retained 16%)
c [simpleprobe-1] removed 233 variables, found 1704 hbrs, 15 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 9 units, 9 failed, 4197 tauts, 0 hbrs, 13 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 13547 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 3518 variables 26% in round 1 in 15581473 steps
c [elim-1-1] backward subsumption/strengthening limit 4418527
c [elim-1-1-1] backward checking 9323 touched variables 69%
c [elim-1-1-1] incomplete backward checking 8801 remain 94%
c [elim-1-1] subsumed 201 and strengthened 9 clauses in 4419004 steps
c [elim-1] incomplete 72 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 3518 = 26% variables out of 13547 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 326405 negative 92.8% of 351840 except 25435 7.2%
c [phase-count-1] 332098 positive 94.4% of 351840 except 19742 5.6%
c [phase-1] phase bias: 5086 positive 51%, 4943 negative 49%
c [sort-queue-1] sorted 10029 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 10029 (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 4411 variables 30.5% (10029 remain 68%)
c [simplification-1] removed 23529 irredundant clauses 6.3% (351840 remain 94%)
c [simplification-1] maximum reduction of 31% = max (31%, 6%)
c [simplification-1] large reduction 31% >= 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 11 variables
c [simpleprobe-2] 8457 schedulable variables 84%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 8492 variables remain 85% (1526 retained 15%)
c [simpleprobe-2] removed 0 variables, found 131 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 7996 literals 40%
c [treelook-1] scheduling used 305061 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 365749 steps
c [treelook-1] 7970 literals remain 40%
c [treelook-1] 6538 variables remain to probed next time 65%
c [decomp-5] removed 1 variables
c [treelook-1] removed 2 variables, found 51 hbrs
c [basicprobe-1] limit 2814400 based on 351800 irredundant clauses
c [basicprobe-1-0] 931 probes remain 9% after last round
c [basicprobe-1-0] 14 units = 14 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 16 variables, found 4060 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 18 failed, 1246 tauts, 0 hbrs, 1242 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 9998 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 2527 not tried 25% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 81 = 1% variables out of 9998 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 324881 negative 92.7% of 350279 except 25398 7.3%
c [phase-count-2] 330763 positive 94.4% of 350279 except 19516 5.6%
c [phase-2] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-2] sorted 7423 enqueued variables after 1000 conflicts
c [score-dist-2] active 2494 (25%), one 0 (0%), zero 7423 (75%)
c [score-dist-2] max exp 509, different 9 (2%)
c [score-dist-2] median active exp 505, avg 504.6
c [simplification-2] removed 112 variables 1.1% (9917 remain 68%)
c [simplification-2] removed 1543 irredundant clauses 0.4% (350279 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  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    3.9    9916   350277      5042    4395     51  3156   31    82   27  38%     61   78   50    3 1604%
c i    4.3    9915   350276      6803    6058     54  3162   37    97   27  38%     23   91   53    4 1242%
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 1376 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1376 out of 1376 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 137 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 7208 literals 37%
c [treelook-2] scheduling used 302294 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 486236 steps
c [treelook-2] 7192 literals remain 37%
c [treelook-2] 4758 variables remain to probed next time 49%
c [treelook-2] removed 3 variables, found 162 hbrs
c [unhide-3] limit 241711 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 1297 tauts, 0 hbrs, 29792 literals
c [elim-3] 2416 variables 25% will be scheduled this time
c [elim-3] scheduled 2416 variables 25%
c [elim-3] limit of 24171186 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 1323 not tried 14% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 2416 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 321892 negative 92.4% of 348330 except 26438 7.6%
c [phase-count-3] 328309 positive 94.3% of 348330 except 20021 5.7%
c [phase-3] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-3] sorted 7102 enqueued variables after 11000 conflicts
c [score-dist-3] active 2675 (27%), one 0 (0%), zero 7102 (73%)
c [score-dist-3] max exp 514, different 14 (3%)
c [score-dist-3] median active exp 506, avg 506.8
c [simplification-3] removed 138 variables 1.4% (9777 remain 67%)
c [simplification-3] removed 1946 irredundant clauses 0.6% (348330 remain 93%)
c [simplification-3] maximum reduction of 1% = max (1%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 20000
c [simplification-3] penalized conflict interval 20000 = 1 * 20000
c [simplification-3] hard conflict limit 41000 (soft 31000 + delta 10000)
c [simplification-3] new conflict limit 31000 (hard 41000)
c 
c [simplification-4] limit 31000 conflicts (hard 41000) hit after 31000 conflicts
c [decomp-8] removed 1 variables
c [basicprobe-2] limit 17710321 penalty 0 = 0 + 0
c [basicprobe-2-0] 866 sched 9%, 24 failed, 2 lifted, 3305 hbrs
c [decomp-9] removed 192 variables
c [basicprobe-2-1] 1508 sched 16%, 16 failed, 0 lifted, 320 hbrs
c [decomp-10] removed 25 variables
c [basicprobe-2-2] 1500 sched 16%, 7 failed, 0 lifted, 167 hbrs
c [decomp-11] removed 7 variables
c [basicprobe-2-3] 622 probes remain 7% after last round
c [basicprobe-2-3] 56 units = 54 failed (96%) + 2 lifted (4%)
c [basicprobe-2-3] removed 231 variables, found 3900 hbrs
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 9545 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1416825700 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 55 variables 1% in round 1 in 647893656 steps
c [elim-4-1] backward subsumption/strengthening limit 647893600
c [elim-4-1-1] backward checking 1370 touched variables 14%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 382 and strengthened 17 clauses in 15240056 steps
c [elim-4-1] rescheduled 250 variables 3% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 5093777 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 55 = 1% variables out of 9545 scheduled
c [elim-4] 55 < 1/100 * 9545 = 95 considered unsuccessful
c [phase-count-4] 318682 negative 91.9% of 346945 except 28263 8.1%
c [phase-count-4] 327512 positive 94.4% of 346945 except 19433 5.6%
c [phase-4] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-4] sorted 6915 enqueued variables after 31000 conflicts
c [score-dist-4] active 2575 (27%), one 0 (0%), zero 6915 (73%)
c [score-dist-4] max exp 516, different 16 (3%)
c [score-dist-4] median active exp 506, avg 507.8
c [simplification-4] removed 287 variables 2.9% (9490 remain 65%)
c [simplification-4] removed 1385 irredundant clauses 0.4% (346945 remain 92%)
c [simplification-4] maximum reduction of 3% = max (3%, 0%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 25000
c [simplification-4] penalized conflict interval 25000 = 1 * 25000
c [simplification-4] hard conflict limit 68500 (soft 56000 + delta 12500)
c [simplification-4] new conflict limit 56000 (hard 68500)
c 
c [simplification-5] limit 56000 conflicts (hard 68500) hit after 56002 conflicts
c [quatres-1] found 63376 quaternary clauses 27% in total
c [quatres-1-2] added 6 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 51664615 with penalty 0 = 0 + 0
c [ternres-1] all 9490 free variables schedulable
c [ternres-1] 1089 ternary resolvents (11 bin, 1078 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2066584 penalty 0 = 0 + 0
c [gauss-1] extracted 105 xors of average arity 2.9
c [gauss-1] connected 308 occurrences of 243 variables (average 1.3)
c [gauss-1] limit 2066584 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 10 variables
c [unhide-4] limit 516646 with penalty 2 = 1 + 1
c [unhide-4-4] 0 units, 1 failed, 1214 tauts, 0 hbrs, 242679 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 1175 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 9478 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 1033292370 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 1143 blocked clauses
c [block-1] 1143 < 1/100 * 346263 = 3462 considered unsuccessful
c [cce-1] limit of 51664618 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 15
c [cce-1-1] eliminated 232 clauses out of 2832 (8%) of length 12
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 233 large clauses in 51664645 steps
c [cce-1-1] allowing another 25832322 steps for small clauses
c [cce-1-1] scheduling 107578 clauses = 19419 binary + 88159 ternary
c [cce-1-1] tried to eliminate 1967 small clauses 2%
c [cce-1-1] eliminated 21 binary clauses 0%
c [cce-1-1] eliminated 102 ternary clauses 0%
c [cce-1-1] eliminated 123 small clauses 0%
c [cce-1-1] eliminated 123 small clauses in 51664638 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 356 covered clauses in round 1
c [cce-1] eliminated 356 covered clauses in TOTAL during 1 rounds
c [cce-1] 356 < 1/100 * 345105 = 3451 considered unsuccessful
c [bca-1] limit of 10000000 steps and 689998 added (scaled 2)
c [bca-1] 15646 out of 18952 literals actually usable 83%
c [bca-1] added 305 blocked clauses in 83007 steps
c [sweep-1] limit 3099877 penalty 0 = 0 + 0
c [sweep-1-1] 5528 pos 58.3% + 3947 neg 41.7% = 9475 sched 100.0% ret 0
c [sweep-1-1] 3109163 steps 110 queries 464.89 avg class size
c [sweep-1-1] 4697 decisions 113 SAT calls 109.96 avg env size
c [sweep-1-1] 7899 variables remain 83% (1576 retained 17%)
c [decomp-13] removed 5 variables
c [sweep-1-1] removed 5 vars (0 failed, 4 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 5 vars in TOTAL (1 rounds, 109 queries)
c [phase-count-5] 316804 negative 91.9% of 344749 except 27945 8.1%
c [phase-count-5] 325403 positive 94.4% of 344749 except 19346 5.6%
c [phase-5] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-5] sorted 6085 enqueued variables after 56002 conflicts
c [score-dist-5] active 3385 (36%), one 0 (0%), zero 6085 (64%)
c [score-dist-5] max exp 517, different 17 (3%)
c [score-dist-5] median active exp 510, avg 509.4
c [simplification-5] removed 20 variables 0.2% (9470 remain 64%)
c [simplification-5] removed 2194 irredundant clauses 0.6% (344749 remain 92%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 12500 = 25000 / 2
c [simplification-5] new conflict interval 37500
c [simplification-5] penalized conflict interval 37500 = 1 * 37500
c [simplification-5] hard conflict limit 112252 (soft 93502 + delta 18750)
c [simplification-5] new conflict limit 93502 (hard 112252)
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 -   36.5    9470   344749     60224   23391   2401  4067   57   150   33  38%    562   73   84   36  234%
c 
c [simplification-6] limit 93502 conflicts (hard 112252) hit after 93504 conflicts
c [quatres-2] found 63385 quaternary clauses 27% in total
c [quatres-2-1] added 2 double-self-subsuming ternary resolvents
c [quatres-2-2] added 8 single-self-subsuming ternary resolvents
c [ternres-2] limit 22313133 with penalty 0 = 0 + 0
c [ternres-2] all 9470 free variables schedulable
c [ternres-2] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 2789141 penalty 2 = 2 + 0
c [card-3] found 1201 at-most-one constraints of average size 3.0
c [card-3] found 37 at-most-two constraints of average size 6.1
c [card-3] using previous limit 2789141 for elimination
c [card-3] 1238 out of 1238 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-14] removed 4 variables
c [simpleprobe-3] 8033 schedulable variables 85%
c [simpleprobe-3] limit 44626267 penalty 1 = 1 + 0
c [decomp-15] removed 14 variables
c [simpleprobe-3] 6565 variables remain 69% (2887 retained 31%)
c [simpleprobe-3] removed 14 variables, found 1587 hbrs, 0 units
c [unhide-5] limit 2231313 with penalty 1 = 0 + 1
c [unhide-5-5] 0 units, 0 failed, 710 tauts, 0 hbrs, 142183 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 1147 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 9452 variables 100%
c [elim-5] limit of 223131339 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 644 not tried 7% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 78 = 1% variables out of 9452 scheduled
c [elim-5] 78 < 1/100 * 9452 = 94 considered unsuccessful
c [bca-2] limit of 10000000 steps and 688344 added (scaled 2)
c [bca-2] 15545 out of 18750 literals actually usable 83%
c [bca-2] added 120 blocked clauses in 53643 steps
c [sweep-2] limit 6693940 penalty 0 = 0 + 0
c [sweep-2-1] 4639 pos 59.3% + 3179 neg 40.7% = 7818 sched 83.4% ret 1556
c [sweep-2-1] 6700445 steps 225 queries 193.40 avg class size
c [sweep-2-1] 8469 decisions 235 SAT calls 97.31 avg env size
c [sweep-2-1] 5834 variables remain 62% (3540 retained 38%)
c [decomp-16] removed 23 variables
c [sweep-2-1] removed 23 vars (0 failed, 18 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 23 vars in TOTAL (1 rounds, 224 queries)
c [sort-queue-6] sorted 5469 enqueued variables after 93504 conflicts
c [score-dist-6] active 3882 (42%), one 0 (0%), zero 5469 (58%)
c [score-dist-6] max exp 517, different 17 (3%)
c [score-dist-6] median active exp 510, avg 509.6
c [simplification-6] removed 119 variables 1.3% (9351 remain 64%)
c [simplification-6] removed 911 irredundant clauses 0.3% (343838 remain 92%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 18750 = 37500 / 2
c [simplification-6] new conflict interval 56250
c [simplification-6] penalized conflict interval 56250 = 1 * 56250
c [simplification-6] hard conflict limit 177879 (soft 149754 + delta 28125)
c [simplification-6] new conflict limit 149754 (hard 177879)
c 
c [simplification-7] limit 149754 conflicts (hard 177879) hit after 149758 conflicts
c [quatres-3] found 63360 quaternary clauses 27% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-2] added 8 single-self-subsuming ternary resolvents
c [quatres-3-2] added 3 quaternary resolvents
c [ternres-3] limit 42157624 with penalty 0 = 0 + 0
c [ternres-3] all 9351 free variables schedulable
c [ternres-3] 70 ternary resolvents (0 bin, 70 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 4215762 penalty 1 = 1 + 0
c [gauss-2] extracted 198 xors of average arity 3.0
c [gauss-2] connected 594 occurrences of 306 variables (average 1.9)
c [gauss-2] limit 4215762 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 4215762 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 16550 literals 88%
c [treelook-3] scheduling used 895136 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 4215762 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 4222621 steps
c [treelook-3] 16326 literals remain 87%
c [treelook-3] 4444 variables remain to probed next time 48%
c [decomp-18] removed 8 variables
c [treelook-3] removed 14 variables, found 986 hbrs
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 881 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 9337 variables 100%
c [block-2] limit of 210788121 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 1 blocked clauses
c [block-2] 1 < 1/100 * 343597 = 3435 considered unsuccessful
c [cce-2] limit of 105394060 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 15
c [cce-2-1] eliminated 1218 clauses out of 2581 (47%) of length 12
c [cce-2-1] eliminated 312 clauses out of 427 (73%) of length 11
c [cce-2-1] eliminated 61 clauses out of 603 (10%) of length 10
c [cce-2-1] eliminated 3 clauses out of 1588 (0%) of length 9
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 1595 large clauses in 105394089 steps
c [cce-2-1] allowing another 52697044 steps for small clauses
c [cce-2-1] scheduling 106432 clauses = 18906 binary + 87526 ternary
c [cce-2-1] tried to eliminate 4394 small clauses 4%
c [cce-2-1] eliminated 32 binary clauses 0%
c [cce-2-1] eliminated 125 ternary clauses 0%
c [cce-2-1] eliminated 157 small clauses 0%
c [cce-2-1] eliminated 157 small clauses in 105394061 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1752 covered clauses in round 1
c [cce-2] eliminated 1752 covered clauses in TOTAL during 1 rounds
c [cce-2] 1752 < 1/100 * 343596 = 3435 considered unsuccessful
c [bca-3] limit of 10000000 steps and 684400 added (scaled 2)
c [bca-3] 14648 out of 18676 literals actually usable 78%
c [bca-3] added 48 blocked clauses in 79075 steps
c [sweep-3] limit 12647287 penalty 0 = 0 + 0
c [sweep-3-1] 3505 pos 60.3% + 2310 neg 39.7% = 5815 sched 62.3% ret 3522
c [sweep-3-1] 12658804 steps 577 queries 92.65 avg class size
c [sweep-3-1] 16922 decisions 556 SAT calls 92.17 avg env size
c [sweep-3-1] 2840 variables remain 30% (6497 retained 70%)
c [decomp-19] removed 23 variables
c [sweep-3-1] removed 23 vars (0 failed, 24 eqs, 12 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 23 vars in TOTAL (1 rounds, 576 queries)
c [sort-queue-7] sorted 4897 enqueued variables after 149758 conflicts
c [score-dist-7] active 4417 (47%), one 0 (0%), zero 4897 (53%)
c [score-dist-7] max exp 518, different 18 (3%)
c [score-dist-7] median active exp 510, avg 509.8
c [simplification-7] removed 37 variables 0.4% (9314 remain 63%)
c [simplification-7] removed 2005 irredundant clauses 0.6% (341833 remain 91%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 28125 = 56250 / 2
c [simplification-7] new conflict interval 84375
c [simplification-7] penalized conflict interval 84375 = 1 * 84375
c [simplification-7] hard conflict limit 276320 (soft 234133 + delta 42187)
c [simplification-7] new conflict limit 234133 (hard 276320)
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 -  105.6    9314   341833    167130   24555   2640  5178  155   179   33  87%    934   21  154  120  129%
c 
c [simplification-8] limit 234133 conflicts (hard 276320) hit after 248018 conflicts
c [quatres-4] found 63310 quaternary clauses 27% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [quatres-4-2] added 3 quaternary resolvents
c [ternres-4] limit 77924576 with penalty 0 = 0 + 0
c [ternres-4] all 9314 free variables schedulable
c [ternres-4] 11 ternary resolvents (1 bin, 10 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-20] removed 1 variables
c [basicprobe-3] limit 389622884 penalty 0 = 0 + 0
c [basicprobe-3-0] 619 sched 7%, 4 failed, 0 lifted, 346 hbrs
c [decomp-21] removed 4 variables
c [basicprobe-3-1] 1443 sched 16%, 0 failed, 0 lifted, 243 hbrs
c [basicprobe-3-2] 1443 sched 16%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-3-3] 1443 sched 16%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-3-4] 1443 sched 16%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-3-5] 1443 sched 16%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-5] fully completed probing
c [basicprobe-3-5] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-3-5] removed 4 variables, found 614 hbrs
c [bate-1] eliminated 105 asymmetric tautologies during probing
c [unhide-6] limit 3896228 with penalty 2 = 1 + 1
c [unhide-6-7] 0 units, 0 failed, 1470 tauts, 0 hbrs, 404956 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 299 transitive binary clauses
c [bca-4] limit of 10000000 steps and 683468 added (scaled 2)
c [bca-4] 14431 out of 18620 literals actually usable 78%
c [bca-4] added 22 blocked clauses in 77906 steps
c [sweep-4] limit 23377373 penalty 0 = 0 + 0
c [sweep-4-1] 1796 pos 63.3% + 1040 neg 36.7% = 2836 sched 30.5% ret 6473
c [sweep-4-1] 20488990 steps 1273 queries 17.54 avg class size
c [sweep-4-1] 39389 decisions 1218 SAT calls 92.89 avg env size
c [sweep-4-1] fully completed sweeping round
c [decomp-26] removed 38 variables
c [sweep-4-1] removed 38 vars (0 failed, 64 eqs, 18 impls)
c [sweep-4-2] 5398 pos 58.2% + 3873 neg 41.8% = 9271 sched 100.0% ret 0
c [sweep-4-2] 2901916 steps 75 queries 995.89 avg class size
c [sweep-4-2] 3298 decisions 78 SAT calls 121.95 avg env size
c [sweep-4-2] 8389 variables remain 90% (882 retained 10%)
c [decomp-27] removed 3 variables
c [sweep-4-2] removed 3 vars (0 failed, 3 eqs, 0 impls)
c [sweep-4] removed 41 vars in TOTAL (2 rounds, 1346 queries)
c [sort-queue-8] sorted 4513 enqueued variables after 248018 conflicts
c [score-dist-8] active 4755 (51%), one 0 (0%), zero 4513 (49%)
c [score-dist-8] max exp 519, different 19 (4%)
c [score-dist-8] median active exp 511, avg 510.1
c [simplification-8] removed 46 variables 0.5% (9268 remain 63%)
c [simplification-8] removed 494 irredundant clauses 0.1% (341339 remain 91%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 84375
c [simplification-8] new conflict interval 168750
c [simplification-8] penalized conflict interval 168750 = 1 * 168750
c [simplification-8] hard conflict limit 501143 (soft 416768 + delta 84375)
c [simplification-8] new conflict limit 416768 (hard 501143)
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 -  171.6    9268   341339    266864   25918   2716  5003  134   153   32  88%   1004   -9  134  137   98%
c -  203.8    9268   341339    328944   25072   2740  5004  112   149   32  75%   1016   -8  104  128   81%
c -  231.8    9268   341339    387269   25446   2792  5007  125   148   33  84%   1021   -3  125  121  103%
c 
c [simplification-9] limit 416768 conflicts (hard 501143) hit after 443715 conflicts
c [quatres-5] found 63309 quaternary clauses 27% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 5 single-self-subsuming ternary resolvents
c [quatres-5-2] added 2 quaternary resolvents
c [ternres-5] limit 130945982 with penalty 0 = 0 + 0
c [ternres-5] all 9268 free variables schedulable
c [ternres-5] 69 ternary resolvents (11 bin, 58 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-28] removed 1 variables
c [simpleprobe-4] 6429 schedulable variables 69%
c [simpleprobe-4] limit 200000000 penalty 0 = 0 + 0
c [decomp-29] removed 20 variables
c [simpleprobe-4] 4124 variables remain 45% (5123 retained 55%)
c [simpleprobe-4] removed 20 variables, found 3938 hbrs, 0 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 2089 transitive binary clauses
c [elim-6] 642 variables 7% will be scheduled this time
c [elim-6] scheduled 642 variables 7%
c [elim-6] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 454 not tried 5% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 642 scheduled
c [bca-5] limit of 10000000 steps and 681783 added (scaled 2)
c [bca-5] 14083 out of 18496 literals actually usable 76%
c [bca-5] added 18 blocked clauses in 82482 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 392837940 penalty 0 = 0 + 0
c [sweep-5-1] 4901 pos 58.5% + 3472 neg 41.5% = 8373 sched 90.5% ret 874
c [sweep-5-1] 36254166 steps 1859 queries 26.01 avg class size
c [sweep-5-1] 57488 decisions 1828 SAT calls 93.86 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-30] removed 30 variables
c [sweep-5-1] removed 30 vars (0 failed, 70 eqs, 8 impls)
c [sweep-5-2] 5358 pos 58.1% + 3859 neg 41.9% = 9217 sched 100.0% ret 0
c [sweep-5-2] 36386716 steps 1935 queries 31.28 avg class size
c [sweep-5-2] 59669 decisions 1916 SAT calls 92.20 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-31] removed 25 variables
c [sweep-5-2] removed 25 vars (0 failed, 69 eqs, 6 impls)
c [sweep-5-3] 5337 pos 58.1% + 3855 neg 41.9% = 9192 sched 100.0% ret 0
c [sweep-5-3] 39300573 steps 1888 queries 26.49 avg class size
c [sweep-5-3] 57642 decisions 1859 SAT calls 92.95 avg env size
c [sweep-5-3] fully completed sweeping round
c [decomp-32] removed 25 variables
c [sweep-5-3] removed 25 vars (0 failed, 67 eqs, 2 impls)
c [sweep-5] removed 80 vars in TOTAL (3 rounds, 5679 queries)
c [sort-queue-9] sorted 3611 enqueued variables after 443715 conflicts
c [score-dist-9] active 5556 (61%), one 0 (0%), zero 3611 (39%)
c [score-dist-9] max exp 520, different 20 (4%)
c [score-dist-9] median active exp 509, avg 509.8
c [simplification-9] removed 101 variables 1.1% (9167 remain 62%)
c [simplification-9] removed 841 irredundant clauses 0.2% (340498 remain 91%)
c [simplification-9] maximum reduction of 1% = max (1%, 0%)
c [simplification-9] geometric conflict interval increment 84375 = 168750 / 2
c [simplification-9] new conflict interval 253125
c [simplification-9] penalized conflict interval 253125 = 1 * 253125
c [simplification-9] hard conflict limit 823402 (soft 696840 + delta 126562)
c [simplification-9] new conflict limit 696840 (hard 823402)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  271.2    9167   340498    454259   26474   3078  7838  124   139   33  89%   1023   -6  131  120  109%
c -  328.0    9167   340498    571887   27401   3081  7839  116   122   34  95%   1024  -12  111  121   92%
c -  371.0    9167   340498    665228   28639   3088  7839  129   139   34  92%   1024    5  126  120  105%
c 
c [simplification-10] limit 696840 conflicts (hard 823402) hit after 712133 conflicts
c [quatres-6] found 63332 quaternary clauses 27% in total
c [quatres-6-1] removed 3 duplicate quaternary clauses
c [quatres-6-2] added 26 single-self-subsuming ternary resolvents
c [quatres-6-2] added 21 quaternary resolvents
c [ternres-6] limit 200000000 with penalty 0 = 0 + 0
c [ternres-6] all 9167 free variables schedulable
c [ternres-6] 82 ternary resolvents (10 bin, 72 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 12610154 penalty 3 = 3 + 0
c [card-4] found 1097 at-most-one constraints of average size 3.0
c [card-4] found 38 at-most-two constraints of average size 6.2
c [card-4] using previous limit 12610154 for elimination
c [card-4] 1134 out of 1135 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 10088123 penalty 2 = 2 + 0
c [gauss-3] extracted 546 xors of average arity 3.0
c [gauss-3] connected 1620 occurrences of 543 variables (average 3.0)
c [gauss-3] limit 10088123 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 20176247 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 16938 literals 92%
c [treelook-4] scheduling used 905693 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 20176247 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 20177671 steps
c [treelook-4] 15372 literals remain 84%
c [treelook-4] 4250 variables remain to probed next time 46%
c [decomp-34] removed 13 variables
c [treelook-4] removed 13 variables, found 1517 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 2239 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 9154 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 9 blocked clauses
c [block-3] 9 < 1/100 * 339730 = 3397 considered unsuccessful
c [cce-3] limit of 252203098 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 72 clauses out of 1359 (5%) of length 12
c [cce-3-1] eliminated 10 clauses out of 119 (8%) of length 11
c [cce-3-1] eliminated 117 clauses out of 1588 (7%) of length 9
c [cce-3-1] eliminated 289 clauses out of 3389 (9%) of length 8
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 488 large clauses in 252203467 steps
c [cce-3-1] allowing another 126101733 steps for small clauses
c [cce-3-1] scheduling 104841 clauses = 18420 binary + 86421 ternary
c [cce-3-1] tried to eliminate 10073 small clauses 10%
c [cce-3-1] eliminated 151 binary clauses 1%
c [cce-3-1] eliminated 1135 ternary clauses 1%
c [cce-3-1] eliminated 1286 small clauses 1%
c [cce-3-1] eliminated 1286 small clauses in 252203173 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1774 covered clauses in round 1
c [cce-3] eliminated 1774 covered clauses in TOTAL during 1 rounds
c [cce-3] 1774 < 1/100 * 339721 = 3397 considered unsuccessful
c [bca-6] limit of 10000000 steps and 676650 added (scaled 2)
c [bca-6] 13067 out of 18310 literals actually usable 71%
c [bca-6] added 23 blocked clauses in 70242 steps
c [sweep-6] limit 60528743 penalty 0 = 0 + 0
c [sweep-6-1] 5342 pos 58.4% + 3812 neg 41.6% = 9154 sched 100.0% ret 0
c [sweep-6-1] 38950515 steps 1921 queries 36.59 avg class size
c [sweep-6-1] 59593 decisions 1910 SAT calls 91.77 avg env size
c [sweep-6-1] fully completed sweeping round
c [decomp-35] removed 31 variables
c [sweep-6-1] removed 31 vars (0 failed, 56 eqs, 10 impls)
c [sweep-6-2] 5319 pos 58.3% + 3804 neg 41.7% = 9123 sched 100.0% ret 0
c [sweep-6-2] 21581896 steps 985 queries 57.17 avg class size
c [sweep-6-2] 31363 decisions 988 SAT calls 89.85 avg env size
c [sweep-6-2] 2173 variables remain 24% (6950 retained 76%)
c [decomp-36] removed 19 variables
c [sweep-6-2] removed 19 vars (0 failed, 38 eqs, 3 impls)
c [sweep-6] removed 50 vars in TOTAL (2 rounds, 2904 queries)
c [sort-queue-10] sorted 3317 enqueued variables after 712133 conflicts
c [score-dist-10] active 5787 (64%), one 0 (0%), zero 3317 (36%)
c [score-dist-10] max exp 521, different 21 (4%)
c [score-dist-10] median active exp 509, avg 509.9
c [simplification-10] removed 63 variables 0.7% (9104 remain 62%)
c [simplification-10] removed 2563 irredundant clauses 0.8% (337935 remain 90%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 126562 = 253125 / 2
c [simplification-10] new conflict interval 379687
c [simplification-10] penalized conflict interval 379687 = 1 * 379687
c [simplification-10] hard conflict limit 1281663 (soft 1091820 + delta 189843)
c [simplification-10] new conflict limit 1091820 (hard 1281663)
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 -  440.3    9104   337935    785265   28949   4327  7785  124   131   33  94%   1024   -3  114  123   93%
c -  521.8    9104   337935    940371   30173   4340  7785  100   132   34  76%   1024    3   62  119   52%
c -  589.1    9104   337935   1068927   30325   4356  7785  110   131   33  84%   1024   -1   98  119   83%
c 
c [simplification-11] limit 1091820 conflicts (hard 1281663) hit after 1118443 conflicts
c [quatres-7] found 63054 quaternary clauses 27% in total
c [quatres-7-1] removed 6 duplicate quaternary clauses
c [quatres-7-2] added 22 single-self-subsuming ternary resolvents
c [quatres-7-2] added 15 quaternary resolvents
c [ternres-7] limit 200000000 with penalty 0 = 0 + 0
c [ternres-7] all 9104 free variables schedulable
c [ternres-7] 75 ternary resolvents (6 bin, 69 trn)
c [ternres-7] fully completed ternary resolution
c [basicprobe-4] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 1348 sched 15%, 0 failed, 0 lifted, 182 hbrs
c [basicprobe-4-1] 1348 sched 15%, 0 failed, 0 lifted, 19 hbrs
c [basicprobe-4-2] 1348 sched 15%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-2] fully completed probing
c [basicprobe-4-2] removed 0 variables, found 201 hbrs
c [bate-2] eliminated 43 asymmetric tautologies during probing
c [unhide-7] limit 5000000 with penalty 2 = 2 + 0
c [unhide-7-9] 0 units, 0 failed, 2656 tauts, 0 hbrs, 182107 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 601 transitive binary clauses
c [bca-7] limit of 10000000 steps and 675194 added (scaled 2)
c [bca-7] 12846 out of 18210 literals actually usable 71%
c [bca-7] added 53 blocked clauses in 76377 steps
c [sweep-7] limit 98074279 penalty 0 = 0 + 0
c [sweep-7-1] 1429 pos 65.8% + 743 neg 34.2% = 2172 sched 23.9% ret 6932
c [sweep-7-1] 18885694 steps 943 queries 19.99 avg class size
c [sweep-7-1] 30686 decisions 945 SAT calls 92.43 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-40] removed 15 variables
c [sweep-7-1] removed 15 vars (0 failed, 22 eqs, 1 impls)
c [sweep-7-2] 5304 pos 58.4% + 3785 neg 41.6% = 9089 sched 100.0% ret 0
c [sweep-7-2] 40054951 steps 1926 queries 24.09 avg class size
c [sweep-7-2] 60067 decisions 1921 SAT calls 90.84 avg env size
c [sweep-7-2] fully completed sweeping round
c [decomp-41] removed 24 variables
c [sweep-7-2] removed 24 vars (0 failed, 53 eqs, 1 impls)
c [sweep-7-3] 5290 pos 58.4% + 3775 neg 41.6% = 9065 sched 100.0% ret 0
c [sweep-7-3] 39138271 steps 1899 queries 27.56 avg class size
c [sweep-7-3] 59054 decisions 1891 SAT calls 89.80 avg env size
c [sweep-7-3] 4 variables remain 0% (9061 retained 100%)
c [decomp-42] removed 23 variables
c [sweep-7-3] removed 23 vars (0 failed, 58 eqs, 6 impls)
c [sweep-7] removed 62 vars in TOTAL (3 rounds, 4765 queries)
c [sort-queue-11] sorted 2987 enqueued variables after 1118443 conflicts
c [score-dist-11] active 6055 (67%), one 0 (0%), zero 2987 (33%)
c [score-dist-11] max exp 521, different 21 (4%)
c [score-dist-11] median active exp 509, avg 510.2
c [simplification-11] removed 62 variables 0.7% (9042 remain 62%)
c [simplification-11] removed 727 irredundant clauses 0.2% (337208 remain 90%)
c [simplification-11] maximum reduction of 1% = max (1%, 0%)
c [simplification-11] geometric conflict interval increment 189843 = 379687 / 2
c [simplification-11] new conflict interval 569530
c [simplification-11] penalized conflict interval 569530 = 1 * 569530
c [simplification-11] hard conflict limit 1972738 (soft 1687973 + delta 284765)
c [simplification-11] new conflict limit 1687973 (hard 1972738)
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 -  632.1    9042   337208   1143369   32321   4388  5680   95   138   33  69%   1024    7   46  106   43%
c -  684.7    9042   337208   1254696   32978   4393  5680   72   139   32  51%   1024   13   91  103   89%
c -  718.5    9042   337208   1327376   33802   4398  5680  116   130   33  89%   1024   -1  106  103  103%
c -  757.2    9042   337208   1410125   33415   4405  5681  103   125   33  82%   1024   -6  105  107   98%
c -  801.4    9042   337208   1505355   35004   4409  5681   94   139   34  68%   1024   10   89  105   84%
c -  835.5    9042   337208   1582931   34345   4413  5681  109   134   34  81%   1024   -5  101  108   94%
c -  878.8    9042   337208   1676357   34633   4419  5682  109   125   34  87%   1024   -8  113  110  102%
c 
c [simplification-12] limit 1687973 conflicts (hard 1972738) hit after 1687975 conflicts
c [quatres-8] found 62970 quaternary clauses 27% in total
c [quatres-8-1] removed 13 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 40 single-self-subsuming ternary resolvents
c [quatres-8-2] added 23 quaternary resolvents
c [ternres-8] limit 200000000 with penalty 0 = 0 + 0
c [ternres-8] all 9042 free variables schedulable
c [ternres-8] 133 ternary resolvents (11 bin, 122 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-43] removed 1 variables
c [simpleprobe-5] 3963 schedulable variables 44%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-44] removed 6 variables
c [simpleprobe-5] 3532 variables remain 39% (5503 retained 61%)
c [simpleprobe-5] removed 6 variables, found 3015 hbrs, 0 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1960 transitive binary clauses
c [bca-8] limit of 10000000 steps and 673918 added (scaled 2)
c [bca-8] 12439 out of 18072 literals actually usable 69%
c [bca-8] added 44 blocked clauses in 67340 steps
c [sweep-8] limit 142797342 penalty 0 = 0 + 0
c [sweep-8-1] 2 pos 50.0% + 2 neg 50.0% = 4 sched 0.0% ret 9031
c [sweep-8-1] 7639 steps 3 queries 2.00 avg class size
c [sweep-8-1] 44 decisions 1 SAT calls 111.00 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-45] removed 2 variables
c [sweep-8-1] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8-2] 5259 pos 58.2% + 3774 neg 41.8% = 9033 sched 100.0% ret 0
c [sweep-8-2] 36791095 steps 1960 queries 21.46 avg class size
c [sweep-8-2] 58752 decisions 1957 SAT calls 87.61 avg env size
c [sweep-8-2] fully completed sweeping round
c [decomp-46] removed 31 variables
c [sweep-8-2] removed 31 vars (0 failed, 65 eqs, 3 impls)
c [sweep-8-3] 5239 pos 58.2% + 3763 neg 41.8% = 9002 sched 100.0% ret 0
c [sweep-8-3] 36926832 steps 1849 queries 32.15 avg class size
c [sweep-8-3] 57530 decisions 1831 SAT calls 90.15 avg env size
c [sweep-8-3] fully completed sweeping round
c [decomp-47] removed 21 variables
c [sweep-8-3] removed 21 vars (0 failed, 57 eqs, 2 impls)
c [sweep-8] removed 54 vars in TOTAL (3 rounds, 3809 queries)
c [sort-queue-12] sorted 2724 enqueued variables after 1687975 conflicts
c [score-dist-12] active 6257 (70%), one 0 (0%), zero 2724 (30%)
c [score-dist-12] max exp 522, different 22 (4%)
c [score-dist-12] median active exp 509, avg 510.3
c [simplification-12] removed 61 variables 0.7% (8981 remain 61%)
c [simplification-12] removed 651 irredundant clauses 0.2% (336557 remain 90%)
c [simplification-12] maximum reduction of 1% = max (1%, 0%)
c [simplification-12] geometric conflict interval increment 284765 = 569530 / 2
c [simplification-12] new conflict interval 854295
c [simplification-12] penalized conflict interval 854295 = 1 * 854295
c [simplification-12] hard conflict limit 2969417 (soft 2542270 + delta 427147)
c [simplification-12] new conflict limit 2542270 (hard 2969417)
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 -  933.1    8981   336557   1783007   36457   4640  7302  115   124   35  92%   1024   -3  119  109  109%
c -  989.2    8981   336557   1901481   37681   4652  7302  116   125   35  93%   1024   -1  110  109  100%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 148 basic ate = 82 trn 55% + 66 lrg 45% in 2 updates
c bcas: 8 count, 633 added (220 skipped), 590072 steps
c bkwd: tried 34294 clauses, 67996 lits, 1.98 lits/clause
c bkwd: checked 10333214 occs, 301.31 occs/clause, 151.97 occs/lit
c bkwd: subsumed 2 binary, 35 ternary, 546 large
c bkwd: strengthened 0 binary, 2 ternary (100% self), 24 large (0% self)
c blkd: 3 bces, 1153 removed, 4674533 resolutions, 15267451 steps
c blkd: 1390 blocking literals 5%, 3 pure
c bump: 1942359 bumped seen, 535851537 lits 275.9 on average
c card: 4 count, 0 units, 0 am1, 28639016 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 18524 subsumed
c card: 6773 at-most-one constraints found, average size 3.02
c card: 6773 at-most-one constraints used 100%, average size 3.02
c card: 162 at-most-two constraints found, average size 5.48
c card: 161 at-most-two constraints used 99%, average size 5.48
c cces: 3 cces, 3882 eliminated, 2917 ate 75%, 965 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: 2060334 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 55 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 47 decompositions, 1595 equivalent 11%
c deco: 1234373 decision-only clauses 64%, 50% reduction
c decs: 4658535 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 3735 eliminated 25%, 529 pure 14%
c elms: 8 rounds, 1.3 rounds/bve
c elms: 2459 small 66%, 744 large 20%
c elms: 2905 tried small, 2459 succeeded 85%, 446 failed 15%
c elms: 4393 subsumed, 1322 strengthened, 11 blocked
c elms: 2955891 copies, 3578137 resolutions, 43871 ipos
c elms: 6869008 subchks, 1801905 strchks
c gaus: 3 extractions, 849 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 32744662 steps, 16372331 extr 50%, 47607 elim 0%
c glue: 113.4 orig avg, 113.4 real avg, 9.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 25630 = 10375 simple 40% + 13585 trn 53% + 1670 lrg 7%, 848 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1942358 clauses, 130.7 length
c lrnd: 253796020 lits = 433553582 orig - 179757562 removed 41%
c lrnd: 478598 uips 25%, 1218641 flips 63%
c mins: 704435 mins 36%, 577 bin 0%, 2934 size 0%
c mins: 71085736 poisoned searches, 13367627 hits, 19% hit rate
c mins: 146200478 used twice searches, 44998492 hits, 31% hit rate
c move: moved 3993, 207 bin 5%, 3786 trn 95%
c otfs: 3407 driving 36%, 5970 restarting 64%
c otfs: str 9377, 9318 red 99%, 59 irr 1%
c otfs: str 9377, 0 bin 0%, 146 trn 2%, 9231 lrg 98%
c otfs: sub 133, 110 red 83%, 23 irr 17%
c otfs: sub 133, 0 bin 0%, 32 trn 24%, 101 lrg 76%
c phas: 5 computed, 10035 set, 5088 pos (51%), 4947 neg (49%)
c prbs: 4 basic, 35006 probed, 72 failed, 2 lifted
c prbs: 5 simple, 40260 probed, 15 failed, 247 eqs
c prbs: 4 treelook, 1807 probed, 4 failed, 0 lifted
c prom: 45221 locked 3% out of 1621062 tried
c prps: 1680793846 props, 358 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 8 count, 73 quat, 110 self1, 3 self2, 1399 dup
c queu: 12 sorted, 4658535 next (135702 steps 0.03)
c queu: 535931521 enq (729319382 steps 1.36), 535851537 deq 100%
c redc: 2543 clauses 12%, 21745 tried 1%, 2 sat 0%
c redc: 3891 lits 2%, 218068 tried 0%, 2 sat 0%
c redc: 152 times jump level reduced, 9.3 levels on average
c reds: 20 count, 96274.1 conflicts per reduce
c reds: 0 memlim 0%, 20 arith 100%
c reds: 595115 collected 89%, 73053 retired 11%
c rmbd: 1015 removed, 199 red 20%
c rsts: 9144 restarts 74%, 3176 skipped 26%
c rsts: 3176 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 12 count, 12 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 1942358 count (6236957 tried 3.2), 1195169 sub out of 1939182 (61.6%)
c swps: 8 count, 16 rounds, 19412 queries (1213.2/round)
c swps: 19247 sat calls, 504 unsat (1.1% success rate)
c swps: 604663 decisions 31.4, 20284 conflicts 1.1
c swps; 38.6 avg class size, 91.6 avg environment size
c swps: 0 failed, 75 impls, 668 equivs
c swp0: 6466 type 0 queries, 2979 unsat (46.1%), 6290 sat (97.3%)
c swp1: 12946 type 1 queries, 7011 unsat (54.2%), 12454 sat (96.2%)
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: 13202013 calls to obtain time
c tops: 601 fixed 4%, 2 its, 962741.00 confs/it
c trds: 8 transitive reductions, 10391 removed, 0 failed
c trds: 146268 nodes, 187064 edges, 5846571 steps
c trim: 27910708 words, 106.5 MB
c trnr: 8 count, 50 bin, 1485 trn, 146712198 steps
c unhd: 7 count, 9 rounds, 29207893 steps
c unhd: 292 non-trivial sccs of average size 2.0
c unhd: 9 units, 9 bin, 0 trn, 0 lrg
c unhd: 28 failed, 26 stamp, 0 lits, 0 bin, 2 trn, 0 lrg
c unhd: 12790 tauts, 775 bin 6%, 2741 trn 21%, 738 lrg 6%
c unhd: 12790 tauts, 8536 stamp 67%, 7719 red 60%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1002972 str, 9 bin 0%, 227 trn 0%, 1002736 lrg 100%, 1001963 red 100%
c vars: 8981 remaining 60% and 5931 removed 40% out of 14912
c vars: 601 fixed 4%, 3735 eliminated 25%, 1595 equivalent 11%
c vsts: 54572675242 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 32.4 search visits per propagation, 28121.8 per conflict
c wchs: 7103355658 pushed, 15589224 enlarged, 114 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1939255        595115         73053      83555509      29571617       1139600
c 
c  0 0         11814   1       232   0         0   0  15011346  18   2658286   9     64126   6     0.3
c  1 5          5172   0       536   0      2087   3   4862182   6   1108103   4     35523   3     0.1
c  2 6         14435   1      2610   0      5822   8   8019454  10   2261366   8    102582   9     0.4
c  3 9         20876   1      8143   1      5861   8  14885437  18   4311884  15    129924  11     0.7
c  4 14        25911   1     15891   3      4635   6   8038199  10<  2953438  10    104546   9     0.9
c  5 21        36428   2     26062   4      4141   6   8165502  10   3298972  11<   136909  12     1.2
c  6 30        57497   3     46617   8      3922   5   4283409   5   2077497   7     91747   8<    2.0
c  7 41        68824   4     58568  10      3810   5   4499883   5   1818014   6     64545   6     3.0
c  8 54        56815   3     47596   8      2980   4<  3302386   4   1582590   5     55399   5     3.9
c  9 69        65179   3     54021   9<     3068   4   3351581   4   1805497   6     81529   7     3.3
c 10 86       595503  31<   260414  44     20272  28   7795504   9   4676794  16    255246  22    34.1
c 11 126      980801  51     74425  13     16455  23   1340626   2   1019176   3     17524   2    44.2
c 
c avg                  9.8           8.7           7.6           4.1           5.4           5.8
c std                  2.0           2.1           3.3           3.2           3.3           3.3
c 
c   93.717   9% bump
c   17.143   2% sweep
c   11.530   1% elim
c    9.035   1% probe
c    6.508   1% unhide
c 
c   14.826 < 1% rest (below)
c 
c    4.891   0% cce
c    2.651   0% decide
c    2.208   0% quatres
c    1.334   0% bca
c    1.160   0% block
c    0.879   0% ternres
c    0.652   0% transred
c    0.652   0% gauss
c    0.397   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.377   0% preprocessing     2%
c   58.489   6% inprocessing     98%
c ==================================
c   59.866   6% simplifying
c  939.915  94% search
c ==================================
c  999.781 100% all
c 
c       1925482 conflicts,        1925.9 confs/sec
c           414 ternaries,        4650.9 confs/ternary
c           188 binaries,        10241.9 confs/binary
c             2 iterations,     962741.0 confs/iteration
c 
c            20 reductions,          0.0 redus/sec,  96274.1 confs/reduction
c          9144 restarts,            9.1 rests/sec,    210.6 confs/restart
c       4658535 decisions,        4659.6 decis/sec,      2.4 decis/conflict
c    1680793846 propagations,  1681161.5 props/sec,    360.8 props/decision
c 
c 999.8 seconds, 146.4 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
