c launch: /data/cnf/sc2014/app/atco_enc2_opt1_15_100.cnf.bz2
c host: atom14
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_enc2_opt1_15_100.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc2_opt1_15_100.cnf.bz2
c no embedded options
c found 'p cnf 58752 580963' header
c read 58752 variables, 580963 clauses, 2227755 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=5
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 58373 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] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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   58373   558586         0       0      0     0    0     0   27   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 11420 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 11420 out of 11420 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 10781 variables
c [simpleprobe-1] all 47971 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 2900 variables
c [simpleprobe-1] 30556 variables remain 68% (14515 retained 32%)
c [simpleprobe-1] removed 2900 variables, found 3980 hbrs, 519 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 1210 failed, 1684 tauts, 0 hbrs, 3101 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 43832 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 5768 not tried 13% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 18736 = 43% variables out of 43832 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 439760 negative 90.4% of 486343 except 46583 9.6%
c [phase-count-1] 443554 positive 91.2% of 486343 except 42789 8.8%
c [phase-1] phase bias: 11291 positive 45%, 13805 negative 55%
c [sort-queue-1] sorted 25096 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 25096 (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 32672 variables 56.6% (25096 remain 43%)
c [simplification-1] removed 72243 irredundant clauses 12.9% (486343 remain 87%)
c [simplification-1] maximum reduction of 57% = max (57%, 13%)
c [simplification-1] large reduction 57% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [decomp-3] removed 6 variables
c [simpleprobe-2] 17458 schedulable variables 70%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 17503 variables remain 70% (7587 retained 30%)
c [simpleprobe-2] removed 0 variables, found 96 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 10882 literals 22%
c [treelook-1] scheduling used 305267 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 479949 steps
c [treelook-1] 10862 literals remain 22%
c [treelook-1] 10111 variables remain to probed next time 40%
c [decomp-5] removed 3 variables
c [treelook-1] removed 3 variables, found 240 hbrs
c [basicprobe-1] limit 3890672 based on 486334 irredundant clauses
c [basicprobe-1-0] 4557 probes remain 18% after last round
c [basicprobe-1-0] 14 units = 14 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 20 variables, found 5477 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 1 failed, 1611 tauts, 0 hbrs, 443 literals
c [elim-2] 5759 variables 23% will be scheduled this time
c [elim-2] scheduled 5759 variables 23%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 3080 not tried 12% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 0 = 0% variables out of 5759 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 439047 negative 90.4% of 485645 except 46598 9.6%
c [phase-count-2] 443020 positive 91.2% of 485645 except 42625 8.8%
c [phase-2] phase bias: 5 positive 100%, 0 negative 0%
c [sort-queue-2] sorted 21156 enqueued variables after 687 conflicts
c [score-dist-2] active 3910 (16%), one 0 (0%), zero 21156 (84%)
c [score-dist-2] max exp 681, different 179 (26%)
c [score-dist-2] median active exp 631, avg 611.0
c [simplification-2] removed 30 variables 0.1% (25066 remain 43%)
c [simplification-2] removed 698 irredundant clauses 0.1% (485645 remain 87%)
c [simplification-2] maximum reduction of 0% = max (0%, 0%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1000 (hard 11000)
c [simplification-2] new binary interval 1000
c 
c [simplification-3] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 2306 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] 2306 out of 2306 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 188 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 11650 literals 23%
c [treelook-2] scheduling used 303235 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 301071 steps
c [treelook-2] 11643 literals remain 23%
c [treelook-2] 5877 variables remain to probed next time 24%
c [decomp-7] removed 1 variables
c [treelook-2] removed 1 variables, found 88 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 3117 tauts, 0 hbrs, 191 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 24877 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 5286 not tried 21% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1512 = 6% variables out of 24877 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 432564 negative 89.9% of 481164 except 48600 10.1%
c [phase-count-3] 438148 positive 91.1% of 481164 except 43016 8.9%
c [phase-3] phase bias: 8 positive 100%, 0 negative 0%
c [sort-queue-3] sorted 18930 enqueued variables after 1000 conflicts
c [score-dist-3] active 4435 (19%), one 0 (0%), zero 18930 (81%)
c [score-dist-3] max exp 763, different 256 (34%)
c [score-dist-3] median active exp 686, avg 667.1
c [simplification-3] removed 1701 variables 6.8% (23365 remain 40%)
c [simplification-3] removed 4481 irredundant clauses 0.9% (481164 remain 86%)
c [simplification-3] maximum reduction of 7% = max (7%, 1%)
c [simplification-3] large reduction 7% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-3] new conflict limit 3000 (hard 13000)
c 
c [simplification-4] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [decomp-8] removed 10 variables
c [basicprobe-2] limit 5411810 penalty 0 = 0 + 0
c [basicprobe-2-0] 4490 sched 19%, 18 failed, 0 lifted, 4292 hbrs
c [decomp-9] removed 86 variables
c [basicprobe-2-1] 7270 probes remain 31% after last round
c [basicprobe-2-1] 20 units = 20 failed (100%) + 0 lifted (0%)
c [basicprobe-2-1] removed 88 variables, found 4712 hbrs
c [elim-4] 2871 variables 12% will be scheduled this time
c [elim-4] scheduled 2871 variables 12%
c [elim-4] boosting limit by 20
c [elim-4] limit of 432944840 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 283 not tried 1% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 39 = 1% variables out of 2871 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 432672 negative 90.1% of 480159 except 47487 9.9%
c [phase-count-4] 438296 positive 91.3% of 480159 except 41863 8.7%
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-4] sorted 15448 enqueued variables after 3000 conflicts
c [score-dist-4] active 7780 (33%), one 4 (0%), zero 15444 (66%)
c [score-dist-4] max exp 781, different 639 (82%)
c [score-dist-4] median active exp 625, avg 546.2
c [simplification-4] removed 137 variables 0.6% (23228 remain 40%)
c [simplification-4] removed 1005 irredundant clauses 0.2% (480159 remain 86%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 10000
c [simplification-4] penalized conflict interval 10000 = 1 * 10000
c [simplification-4] hard conflict limit 23000 (soft 13000 + delta 10000)
c [simplification-4] new conflict limit 13000 (hard 23000)
c 
c [simplification-5] limit of 1593 ternary hit after 1593 ternaries
c [quatres-1] found 66671 quaternary clauses 26% in total
c [quatres-1-1] removed 4 duplicate quaternary clauses
c [quatres-1-2] added 69 single-self-subsuming ternary resolvents
c [quatres-1-2] added 38 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 23228 free variables schedulable
c [ternres-1] 2530 ternary resolvents (0 bin, 2530 trn)
c [ternres-1] 1653 variables remain 7% (21575 retained 93%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 250 xors of average arity 3.0
c [gauss-1] connected 740 occurrences of 689 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-10] removed 27 variables
c [unhide-4] limit 332390 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 7 failed, 1497 tauts, 0 hbrs, 4521 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 1417 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 23200 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 4898 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 148 clauses out of 152 (97%) of length 22
c [cce-1-1] eliminated 24 clauses out of 41 (59%) of length 21
c [cce-1-1] eliminated 9 clauses out of 46 (20%) of length 20
c [cce-1-1] eliminated 2 clauses out of 37 (5%) of length 19
c [cce-1-1] eliminated 7 clauses out of 126 (6%) of length 17
c [cce-1-1] eliminated 21 clauses out of 142 (15%) of length 15
c [cce-1-1] eliminated 56 clauses out of 324 (17%) of length 13
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 267 large clauses in 30000009 steps
c [cce-1-1] allowing another 15000004 steps for small clauses
c [cce-1-1] scheduling 214275 clauses = 46350 binary + 167925 ternary
c [cce-1-1] tried to eliminate 1179 small clauses 1%
c [cce-1-1] eliminated 37 binary clauses 0%
c [cce-1-1] eliminated 63 ternary clauses 0%
c [cce-1-1] eliminated 100 small clauses 0%
c [cce-1-1] eliminated 100 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 367 covered clauses in round 1
c [cce-1] eliminated 367 covered clauses in TOTAL during 1 rounds
c [cce-1] 367 < 1/100 * 474415 = 4744 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 23200 variables 100%
c [elim-5] limit of 66478145 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 1481 not tried 6% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 29 = 0% variables out of 23200 scheduled
c [elim-5] 29 < 1/100 * 23200 = 232 considered unsuccessful
c [bca-1] limit of 10000000 steps and 948196 added (scaled 2)
c [bca-1] 35324 out of 46344 literals actually usable 76%
c [bca-1] added 578 blocked clauses in 93375 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 9638 pos 41.6% + 13533 neg 58.4% = 23171 sched 100.0% ret 0
c [sweep-1-1] 1002952 steps 74 queries 3801.45 avg class size
c [sweep-1-1] 1983 decisions 66 SAT calls 77.15 avg env size
c [sweep-1-1] 22570 variables remain 97% (601 retained 3%)
c [decomp-11] removed 33 variables
c [sweep-1-1] removed 33 vars (0 failed, 11 eqs, 13 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 33 vars in TOTAL (1 rounds, 73 queries)
c [phase-count-5] 426545 negative 90.0% of 473845 except 47300 10.0%
c [phase-count-5] 432287 positive 91.2% of 473845 except 41558 8.8%
c [phase-5] phase bias: 4 positive 100%, 0 negative 0%
c [sort-queue-5] sorted 14962 enqueued variables after 8820 conflicts
c [score-dist-5] active 8176 (35%), one 2855 (12%), zero 12107 (52%)
c [score-dist-5] max exp 799, different 657 (82%)
c [score-dist-5] median active exp 670, avg 595.8
c [simplification-5] removed 90 variables 0.4% (23138 remain 40%)
c [simplification-5] removed 6314 irredundant clauses 1.3% (473845 remain 85%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] forced so keeping old conflict interval 10000
c [simplification-5] conflict limit remains at 13000 (hard 23000)
c [simplification-5] new ternary interval 10000
c 
c [simplification-6] limit 13000 conflicts (hard 23000) hit after 13000 conflicts
c [quatres-2] found 65674 quaternary clauses 26% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 3 single-self-subsuming ternary resolvents
c [quatres-2-2] added 28 quaternary resolvents
c [ternres-2] limit 4905308 with penalty 0 = 0 + 0
c [ternres-2] 1638 schedulable variables 7%
c [ternres-2] 3422 ternary resolvents (0 bin, 3422 trn)
c [ternres-2] 260 variables remain 1% (22878 retained 99%)
c [card-3] limit 613163 penalty 2 = 2 + 0
c [card-3] found 1791 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 613163 for elimination
c [card-3] 1791 out of 1791 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 30 variables
c [simpleprobe-3] 16101 schedulable variables 70%
c [simpleprobe-3] limit 9810616 penalty 1 = 1 + 0
c [decomp-13] removed 13 variables
c [simpleprobe-3] 16455 variables remain 71% (6640 retained 29%)
c [simpleprobe-3] removed 13 variables, found 986 hbrs, 0 units
c [unhide-5] limit 981061 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 1 failed, 986 tauts, 0 hbrs, 2941 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 954 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 23094 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 438 blocked clauses
c [block-2] 438 < 1/100 * 472596 = 4725 considered unsuccessful
c [bca-2] limit of 10000000 steps and 945099 added (scaled 2)
c [bca-2] 33633 out of 46190 literals actually usable 73%
c [bca-2] added 116 blocked clauses in 92254 steps
c [sweep-2] limit 1471592 penalty 0 = 0 + 0
c [sweep-2-1] 9381 pos 41.7% + 13122 neg 58.3% = 22503 sched 97.4% ret 591
c [sweep-2-1] 1490226 steps 71 queries 4156.86 avg class size
c [sweep-2-1] 2235 decisions 70 SAT calls 82.47 avg env size
c [sweep-2-1] 21948 variables remain 95% (1142 retained 5%)
c [decomp-14] removed 76 variables
c [sweep-2-1] removed 76 vars (0 failed, 5 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 76 vars in TOTAL (1 rounds, 70 queries)
c [phase-count-6] 424794 negative 90.0% of 472022 except 47228 10.0%
c [phase-count-6] 430566 positive 91.2% of 472022 except 41456 8.8%
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-6] sorted 14696 enqueued variables after 13000 conflicts
c [score-dist-6] active 8322 (36%), one 3221 (14%), zero 11475 (50%)
c [score-dist-6] max exp 893, different 709 (79%)
c [score-dist-6] median active exp 776, avg 686.2
c [simplification-6] removed 120 variables 0.5% (23018 remain 39%)
c [simplification-6] removed 1823 irredundant clauses 0.4% (472022 remain 85%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 20000
c [simplification-6] penalized conflict interval 20000 = 1 * 20000
c [simplification-6] hard conflict limit 43000 (soft 33000 + delta 10000)
c [simplification-6] new conflict limit 33000 (hard 43000)
c 
c [simplification-7] limit 33000 conflicts (hard 43000) hit after 33000 conflicts
c [quatres-3] found 65824 quaternary clauses 26% in total
c [quatres-3-2] added 17 single-self-subsuming ternary resolvents
c [quatres-3-2] added 39 quaternary resolvents
c [ternres-3] limit 12994175 with penalty 0 = 0 + 0
c [ternres-3] 255 schedulable variables 1%
c [ternres-3] 695 ternary resolvents (0 bin, 695 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1299417 penalty 1 = 1 + 0
c [gauss-2] extracted 155 xors of average arity 2.7
c [gauss-2] connected 426 occurrences of 397 variables (average 1.1)
c [gauss-2] limit 1299417 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [decomp-15] removed 194 variables
c [gauss-2] exported 0 unary, 1 binary and 0 ternary equations
c [treelook-3] limit 1299417 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 32870 literals 72%
c [treelook-3] scheduling used 1161150 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1299417 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 1325865 steps
c [treelook-3] 32746 literals remain 72%
c [treelook-3] 5458 variables remain to probed next time 24%
c [decomp-17] removed 6 variables
c [treelook-3] removed 6 variables, found 262 hbrs
c [unhide-6] limit 2598835 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 0 failed, 843 tauts, 0 hbrs, 35087 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 714 transitive binary clauses
c [cce-2] limit of 32485438 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 33 clauses out of 37 (89%) of length 22
c [cce-2-1] eliminated 1 clauses out of 18 (6%) of length 21
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 34 large clauses in 32485565 steps
c [cce-2-1] allowing another 16242782 steps for small clauses
c [cce-2-1] scheduling 54518 clauses = 44375 binary + 10143 ternary
c [cce-2-1] tried to eliminate 1482 small clauses 3%
c [cce-2-1] eliminated 173 binary clauses 0%
c [cce-2-1] eliminated 18 ternary clauses 0%
c [cce-2-1] eliminated 191 small clauses 0%
c [cce-2-1] eliminated 191 small clauses in 32485465 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 225 covered clauses in round 1
c [cce-2] eliminated 225 covered clauses in TOTAL during 1 rounds
c [cce-2] 225 < 1/100 * 471187 = 4711 considered unsuccessful
c [elim-6] 275 variables 1% will be scheduled this time
c [elim-6] scheduled 275 variables 1%
c [elim-6] limit of 129941753 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 165 not tried 1% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 275 scheduled
c [bca-3] limit of 10000000 steps and 942673 added (scaled 2)
c [bca-3] 30153 out of 45638 literals actually usable 66%
c [bca-3] added 530 blocked clauses in 102859 steps
c [sweep-3] limit 3898252 penalty 0 = 0 + 0
c [sweep-3-1] 9095 pos 41.9% + 12590 neg 58.1% = 21685 sched 95.0% ret 1133
c [sweep-3-1] 3967600 steps 184 queries 1462.27 avg class size
c [sweep-3-1] 6859 decisions 174 SAT calls 99.95 avg env size
c [sweep-3-1] 19819 variables remain 87% (2999 retained 13%)
c [decomp-18] removed 201 variables
c [sweep-3-1] removed 201 vars (0 failed, 28 eqs, 21 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 201 vars in TOTAL (1 rounds, 183 queries)
c [phase-count-7] 423282 negative 89.9% of 470884 except 47602 10.1%
c [phase-count-7] 429457 positive 91.2% of 470884 except 41427 8.8%
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-7] sorted 14920 enqueued variables after 33000 conflicts
c [score-dist-7] active 7697 (34%), one 4487 (20%), zero 10433 (46%)
c [score-dist-7] max exp 584, different 527 (90%)
c [score-dist-7] median active exp 482, avg 429.8
c [simplification-7] removed 401 variables 1.7% (22617 remain 39%)
c [simplification-7] removed 1138 irredundant clauses 0.2% (470884 remain 84%)
c [simplification-7] maximum reduction of 2% = max (2%, 0%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 26666
c [simplification-7] penalized conflict interval 26666 = 1 * 26666
c [simplification-7] hard conflict limit 72999 (soft 59666 + delta 13333)
c [simplification-7] new conflict limit 59666 (hard 72999)
c 
c [simplification-8] limit 59666 conflicts (hard 72999) hit after 59666 conflicts
c [quatres-4] found 66377 quaternary clauses 26% in total
c [quatres-4-1] removed 5 duplicate quaternary clauses
c [quatres-4-2] added 24 single-self-subsuming ternary resolvents
c [quatres-4-2] added 53 quaternary resolvents
c [ternres-4] limit 25396469 with penalty 0 = 0 + 0
c [ternres-4] all 22617 free variables schedulable
c [ternres-4] 531 ternary resolvents (0 bin, 531 trn)
c [ternres-4] 282 variables remain 1% (22335 retained 99%)
c [gauss-3] limit 5079293 penalty 0 = 0 + 0
c [gauss-3] extracted 564 xors of average arity 2.8
c [gauss-3] connected 1558 occurrences of 991 variables (average 1.6)
c [gauss-3] limit 5079293 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [decomp-19] removed 103 variables
c [gauss-3] exported 0 unary, 1 binary and 2 ternary equations
c [basicprobe-3] limit 126982348 penalty 0 = 0 + 0
c [basicprobe-3-0] 7122 sched 32%, 6 failed, 0 lifted, 7994 hbrs
c [decomp-21] removed 1001 variables
c [basicprobe-3-1] 9012 sched 42%, 3 failed, 0 lifted, 1687 hbrs
c [decomp-22] removed 81 variables
c [basicprobe-3-2] 9012 sched 42%, 3 failed, 0 lifted, 303 hbrs
c [decomp-23] removed 3 variables
c [basicprobe-3-3] 9012 sched 42%, 3 failed, 0 lifted, 196 hbrs
c [decomp-24] removed 3 variables
c [basicprobe-3-4] 9012 sched 42%, 2 failed, 0 lifted, 228 hbrs
c [decomp-25] removed 2 variables
c [basicprobe-3-5] 9012 sched 42%, 0 failed, 0 lifted, 71 hbrs
c [basicprobe-3-6] 9012 sched 42%, 0 failed, 0 lifted, 56 hbrs
c [basicprobe-3-7] 9012 sched 42%, 0 failed, 0 lifted, 65 hbrs
c [basicprobe-3-8] 9012 sched 42%, 0 failed, 0 lifted, 60 hbrs
c [basicprobe-3-8] round limit 8 hit
c [basicprobe-3-8] 17 units = 17 failed (100%) + 0 lifted (0%)
c [basicprobe-3-8] removed 1090 variables, found 10660 hbrs
c [bate-1] eliminated 985 asymmetric tautologies during probing
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 3141 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 21424 variables 100%
c [block-3] limit of 126982348 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 392 blocked clauses
c [block-3] 392 < 1/100 * 468476 = 4684 considered unsuccessful
c [bca-4] limit of 10000000 steps and 937280 added (scaled 2)
c [bca-4] 23743 out of 42850 literals actually usable 55%
c [bca-4] added 1592 blocked clauses in 114441 steps
c [sweep-4] limit 7618940 penalty 0 = 0 + 0
c [sweep-4-1] 7943 pos 42.9% + 10561 neg 57.1% = 18504 sched 86.4% ret 2920
c [sweep-4-1] 7640481 steps 315 queries 622.02 avg class size
c [sweep-4-1] 11943 decisions 289 SAT calls 107.43 avg env size
c [sweep-4-1] 14825 variables remain 69% (6599 retained 31%)
c [decomp-29] removed 37 variables
c [sweep-4-1] removed 37 vars (0 failed, 41 eqs, 38 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 37 vars in TOTAL (1 rounds, 314 queries)
c [sort-queue-8] sorted 12506 enqueued variables after 59666 conflicts
c [score-dist-8] active 8881 (42%), one 5152 (24%), zero 7354 (34%)
c [score-dist-8] max exp 544, different 521 (96%)
c [score-dist-8] median active exp 407, avg 373.4
c [simplification-8] removed 1230 variables 5.4% (21387 remain 37%)
c [simplification-8] removed 2815 irredundant clauses 0.6% (468069 remain 84%)
c [simplification-8] maximum reduction of 5% = max (5%, 1%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 71666 (soft 61666 + delta 10000)
c [simplification-8] new conflict limit 61666 (hard 71666)
c 
c [simplification-9] limit 61666 conflicts (hard 71666) hit after 61666 conflicts
c [quatres-5] found 66232 quaternary clauses 26% in total
c [quatres-5-1] removed 23 duplicate quaternary clauses
c [quatres-5-2] added 9 single-self-subsuming ternary resolvents
c [quatres-5-2] added 20 quaternary resolvents
c [ternres-5] limit 26336799 with penalty 0 = 0 + 0
c [ternres-5] 219 schedulable variables 1%
c [ternres-5] 200 ternary resolvents (0 bin, 200 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-4] limit 5267359 penalty 0 = 0 + 0
c [gauss-4] extracted 415 xors of average arity 2.7
c [gauss-4] connected 1124 occurrences of 837 variables (average 1.3)
c [gauss-4] limit 5267359 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-30] removed 3 variables
c [simpleprobe-4] 15141 schedulable variables 71%
c [simpleprobe-4] limit 105347196 penalty 0 = 0 + 0
c [decomp-31] removed 45 variables
c [simpleprobe-4] 12620 variables remain 59% (8719 retained 41%)
c [simpleprobe-4] removed 45 variables, found 3418 hbrs, 0 units
c [unhide-7] limit 2633679 with penalty 1 = 1 + 0
c [unhide-7-7] 0 units, 0 failed, 959 tauts, 0 hbrs, 55436 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 2275 transitive binary clauses
c [bca-5] limit of 10000000 steps and 932344 added (scaled 2)
c [bca-5] 23347 out of 42680 literals actually usable 55%
c [bca-5] added 30 blocked clauses in 114566 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 79010390 penalty 0 = 0 + 0
c [sweep-5-1] 6289 pos 42.5% + 8495 neg 57.5% = 14784 sched 69.3% ret 6555
c [sweep-5-1] 47457904 steps 3318 queries 57.07 avg class size
c [sweep-5-1] 94355 decisions 2856 SAT calls 80.84 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-32] removed 401 variables
c [sweep-5-1] removed 401 vars (0 failed, 482 eqs, 470 impls)
c [sweep-5-2] 9188 pos 43.9% + 11750 neg 56.1% = 20938 sched 100.0% ret 0
c [sweep-5-2] 31580407 steps 1657 queries 104.33 avg class size
c [sweep-5-2] 54153 decisions 1514 SAT calls 89.37 avg env size
c [sweep-5-2] 4965 variables remain 24% (15973 retained 76%)
c [decomp-33] removed 99 variables
c [sweep-5-2] removed 99 vars (0 failed, 165 eqs, 132 impls)
c [sweep-5] removed 500 vars in TOTAL (2 rounds, 4973 queries)
c [sort-queue-9] sorted 11009 enqueued variables after 61666 conflicts
c [score-dist-9] active 9830 (47%), one 4303 (21%), zero 6706 (32%)
c [score-dist-9] max exp 884, different 747 (84%)
c [score-dist-9] median active exp 536, avg 534.1
c [simplification-9] removed 548 variables 2.6% (20839 remain 36%)
c [simplification-9] removed 3000 irredundant clauses 0.6% (465069 remain 83%)
c [simplification-9] maximum reduction of 3% = max (3%, 1%)
c [simplification-9] geometric conflict interval increment 6666 = 26666 / 4
c [simplification-9] new conflict interval 33332
c [simplification-9] penalized conflict interval 33332 = 1 * 33332
c [simplification-9] hard conflict limit 111664 (soft 94998 + delta 16666)
c [simplification-9] new conflict limit 94998 (hard 111664)
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 -   99.7   20839   465069     65643    8262   6936 14630   14   244   38   6%    642   84   14    7  202%
c 
c [simplification-10] limit 94998 conflicts (hard 111664) hit after 94998 conflicts
c [quatres-6] found 66623 quaternary clauses 26% in total
c [quatres-6-1] removed 29 duplicate quaternary clauses
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 16 single-self-subsuming ternary resolvents
c [quatres-6-2] added 60 quaternary resolvents
c [ternres-6] limit 41818545 with penalty 0 = 0 + 0
c [ternres-6] all 20839 free variables schedulable
c [ternres-6] 190 ternary resolvents (0 bin, 190 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 2613659 penalty 3 = 3 + 0
c [card-4] found 3588 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2613659 for elimination
c [card-4] 3588 out of 3588 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 8363709 penalty 0 = 0 + 0
c [gauss-5] extracted 712 xors of average arity 2.6
c [gauss-5] connected 1868 occurrences of 1141 variables (average 1.6)
c [gauss-5] limit 8363709 penalty 0 = 0 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 4 ternary equations
c [decomp-34] removed 18 variables
c [treelook-4] limit 4181854 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 30957 literals 74%
c [treelook-4] scheduling used 1185454 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 4181854 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 4185184 steps
c [treelook-4] 30615 literals remain 74%
c [treelook-4] 4997 variables remain to probed next time 24%
c [decomp-35] removed 2 variables
c [treelook-4] removed 2 variables, found 1248 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 2694 transitive binary clauses
c [cce-3] limit of 52273182 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 124 (1%) of length 17
c [cce-3-1] eliminated 4 clauses out of 80 (5%) of length 16
c [cce-3-1] eliminated 1 clauses out of 123 (1%) of length 15
c [cce-3-1] eliminated 5 clauses out of 280 (2%) of length 14
c [cce-3-1] eliminated 4 clauses out of 260 (2%) of length 13
c [cce-3-1] eliminated 20 clauses out of 1626 (1%) of length 12
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 35 large clauses in 52273263 steps
c [cce-3-1] allowing another 26136631 steps for small clauses
c [cce-3-1] scheduling 50600 clauses = 39497 binary + 11103 ternary
c [cce-3-1] tried to eliminate 2418 small clauses 5%
c [cce-3-1] eliminated 352 binary clauses 1%
c [cce-3-1] eliminated 152 ternary clauses 1%
c [cce-3-1] eliminated 504 small clauses 1%
c [cce-3-1] eliminated 504 small clauses in 52273433 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 539 covered clauses in round 1
c [cce-3] eliminated 539 covered clauses in TOTAL during 1 rounds
c [cce-3] 539 < 1/100 * 464212 = 4642 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 20819 variables 100%
c [elim-7] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 799 not tried 4% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 405 = 2% variables out of 20819 scheduled
c [bca-6] limit of 10000000 steps and 910413 added (scaled 2)
c [bca-6] 22177 out of 40830 literals actually usable 54%
c [bca-6] added 1124 blocked clauses in 91642 steps
c [sweep-6] limit 12545563 penalty 0 = 0 + 0
c [sweep-6-1] 2196 pos 44.7% + 2716 neg 55.3% = 4912 sched 24.1% ret 15502
c [sweep-6-1] 12550977 steps 942 queries 90.33 avg class size
c [sweep-6-1] 26989 decisions 865 SAT calls 77.03 avg env size
c [sweep-6-1] 1908 variables remain 9% (18506 retained 91%)
c [decomp-36] removed 58 variables
c [sweep-6-1] removed 58 vars (0 failed, 86 eqs, 49 impls)
c [sweep-6] removed 58 vars in TOTAL (1 rounds, 941 queries)
c [sort-queue-10] sorted 10693 enqueued variables after 94998 conflicts
c [score-dist-10] active 9663 (47%), one 5316 (26%), zero 5377 (26%)
c [score-dist-10] max exp 627, different 589 (94%)
c [score-dist-10] median active exp 484, avg 433.9
c [simplification-10] removed 483 variables 2.3% (20356 remain 35%)
c [simplification-10] removed 10836 irredundant clauses 2.3% (454233 remain 81%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] geometric conflict interval increment 11110 = 33332 / 3
c [simplification-10] new conflict interval 44442
c [simplification-10] penalized conflict interval 44442 = 1 * 44442
c [simplification-10] hard conflict limit 161661 (soft 139440 + delta 22221)
c [simplification-10] new conflict limit 139440 (hard 161661)
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 -  167.0   20356   454233    122830   11703   6554 14487   15   235   37   6%    864   30   15   11  133%
c 
c [simplification-11] limit 139440 conflicts (hard 161661) hit after 139443 conflicts
c [quatres-7] found 65771 quaternary clauses 26% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 40 single-self-subsuming ternary resolvents
c [quatres-7-2] added 70 quaternary resolvents
c [ternres-7] limit 61602779 with penalty 0 = 0 + 0
c [ternres-7] all 20356 free variables schedulable
c [ternres-7] 280 ternary resolvents (0 bin, 280 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-6] limit 12320555 penalty 0 = 0 + 0
c [gauss-6] extracted 873 xors of average arity 2.5
c [gauss-6] connected 2202 occurrences of 935 variables (average 2.4)
c [gauss-6] limit 12320555 penalty 0 = 0 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 3 ternary equations
c [decomp-37] removed 12 variables
c [basicprobe-4] limit 308013899 penalty 0 = 0 + 0
c [basicprobe-4-0] 8684 sched 43%, 2 failed, 0 lifted, 2157 hbrs
c [decomp-38] removed 41 variables
c [basicprobe-4-1] 8683 sched 43%, 1 failed, 0 lifted, 371 hbrs
c [decomp-39] removed 2 variables
c [basicprobe-4-2] 8683 sched 43%, 0 failed, 0 lifted, 50 hbrs
c [basicprobe-4-3] 8683 sched 43%, 0 failed, 0 lifted, 33 hbrs
c [basicprobe-4-4] 8683 sched 43%, 0 failed, 0 lifted, 23 hbrs
c [basicprobe-4-5] 8683 sched 43%, 0 failed, 0 lifted, 23 hbrs
c [basicprobe-4-6] 8683 sched 43%, 0 failed, 0 lifted, 23 hbrs
c [basicprobe-4-7] 8683 sched 43%, 0 failed, 0 lifted, 23 hbrs
c [basicprobe-4-8] 8683 sched 43%, 0 failed, 0 lifted, 24 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-4-8] removed 43 variables, found 2727 hbrs
c [bate-2] eliminated 143 asymmetric tautologies during probing
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1684 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 20301 variables 100%
c [block-4] limit of 154006949 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 262 blocked clauses
c [block-4] 262 < 1/100 * 453705 = 4537 considered unsuccessful
c [bca-7] limit of 10000000 steps and 909371 added (scaled 2)
c [bca-7] 22751 out of 40604 literals actually usable 56%
c [bca-7] added 492 blocked clauses in 91411 steps
c [sweep-7] limit 18480833 penalty 0 = 0 + 0
c [sweep-7-1] 890 pos 46.9% + 1008 neg 53.1% = 1898 sched 9.3% ret 18403
c [sweep-7-1] 10428897 steps 1010 queries 36.31 avg class size
c [sweep-7-1] 32028 decisions 966 SAT calls 84.99 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-46] removed 31 variables
c [sweep-7-1] removed 31 vars (0 failed, 44 eqs, 50 impls)
c [sweep-7-2] 8895 pos 43.9% + 11375 neg 56.1% = 20270 sched 100.0% ret 0
c [sweep-7-2] 8185878 steps 339 queries 656.66 avg class size
c [sweep-7-2] 12985 decisions 334 SAT calls 95.03 avg env size
c [sweep-7-2] 14908 variables remain 74% (5362 retained 26%)
c [decomp-47] removed 13 variables
c [sweep-7-2] removed 13 vars (0 failed, 15 eqs, 13 impls)
c [sweep-7] removed 44 vars in TOTAL (2 rounds, 1347 queries)
c [sort-queue-11] sorted 10473 enqueued variables after 139443 conflicts
c [score-dist-11] active 9784 (48%), one 5486 (27%), zero 4987 (25%)
c [score-dist-11] max exp 867, different 721 (83%)
c [score-dist-11] median active exp 667, avg 594.9
c [simplification-11] removed 99 variables 0.5% (20257 remain 35%)
c [simplification-11] removed 796 irredundant clauses 0.2% (453437 remain 81%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 44442
c [simplification-11] new conflict interval 88884
c [simplification-11] penalized conflict interval 88884 = 1 * 88884
c [simplification-11] hard conflict limit 272769 (soft 228327 + delta 44442)
c [simplification-11] new conflict limit 228327 (hard 272769)
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 -  222.5   20257   453437    174304   14448   7082 16168   16   226   61   7%    951    3   16   13  118%
c -  256.0   20257   453437    225340   18878   7283 16217   17   247   39   7%    991   14   17   15  111%
c 
c [simplification-12] limit 228327 conflicts (hard 272769) hit after 239557 conflicts
c [quatres-8] found 66128 quaternary clauses 25% in total
c [quatres-8-1] removed 7 duplicate quaternary clauses
c [quatres-8-2] added 51 single-self-subsuming ternary resolvents
c [quatres-8-2] added 97 quaternary resolvents
c [ternres-8] limit 92703096 with penalty 0 = 0 + 0
c [ternres-8] all 20257 free variables schedulable
c [ternres-8] 178 ternary resolvents (1 bin, 177 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-7] limit 18540619 penalty 0 = 0 + 0
c [gauss-7] extracted 1232 xors of average arity 2.5
c [gauss-7] connected 3114 occurrences of 1077 variables (average 2.9)
c [gauss-7] limit 18540619 penalty 0 = 0 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-48] removed 7 variables
c [simpleprobe-5] 11909 schedulable variables 59%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-49] removed 93 variables
c [simpleprobe-5] 7059 variables remain 35% (13098 retained 65%)
c [simpleprobe-5] removed 93 variables, found 4152 hbrs, 0 units
c [unhide-8] limit 4635154 with penalty 2 = 2 + 0
c [unhide-8-9] 0 units, 0 failed, 4611 tauts, 0 hbrs, 30616 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1482 transitive binary clauses
c [elim-8] 165 variables 1% will be scheduled this time
c [elim-8] scheduled 165 variables 1%
c [elim-8] boosting limit by 20
c [elim-8] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 289250581 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 165 scheduled
c [bca-8] limit of 10000000 steps and 907997 added (scaled 2)
c [bca-8] 23590 out of 40316 literals actually usable 59%
c [bca-8] added 260 blocked clauses in 99942 steps
c [sweep-8] limit 27810928 penalty 0 = 0 + 0
c [sweep-8-1] 6349 pos 42.9% + 8460 neg 57.1% = 14809 sched 73.5% ret 5348
c [sweep-8-1] 27812855 steps 1896 queries 134.22 avg class size
c [sweep-8-1] 52711 decisions 1833 SAT calls 69.64 avg env size
c [sweep-8-1] 3139 variables remain 16% (17018 retained 84%)
c [decomp-50] removed 78 variables
c [sweep-8-1] removed 78 vars (0 failed, 97 eqs, 58 impls)
c [sweep-8] removed 78 vars in TOTAL (1 rounds, 1895 queries)
c [sort-queue-12] sorted 11080 enqueued variables after 239557 conflicts
c [score-dist-12] active 8999 (45%), one 6523 (32%), zero 4557 (23%)
c [score-dist-12] max exp 773, different 624 (81%)
c [score-dist-12] median active exp 510, avg 484.2
c [simplification-12] removed 178 variables 0.9% (20079 remain 34%)
c [simplification-12] removed 815 irredundant clauses 0.2% (452622 remain 81%)
c [simplification-12] maximum reduction of 1% = max (1%, 0%)
c [simplification-12] geometric conflict interval increment 44442 = 88884 / 2
c [simplification-12] new conflict interval 133326
c [simplification-12] penalized conflict interval 133326 = 1 * 133326
c [simplification-12] hard conflict limit 439546 (soft 372883 + delta 66663)
c [simplification-12] new conflict limit 372883 (hard 439546)
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 -  284.9   20079   452622    273922   26766   7340 15058   17   182   38  10%   1008  -40   19   16  117%
c -  302.9   20079   452622    316433   30414   7390 15075   18   183   63  10%   1016  -36   21   17  124%
c -  315.5   20079   452622    357016   34930   7437 15083   18   212   63   8%   1020    1   18   18  105%
c 
c [simplification-13] limit 372883 conflicts (hard 439546) hit after 372911 conflicts
c [quatres-9] found 66416 quaternary clauses 25% in total
c [quatres-9-1] removed 30 duplicate quaternary clauses
c [quatres-9-2] added 24 single-self-subsuming ternary resolvents
c [quatres-9-2] added 65 quaternary resolvents
c [ternres-9] limit 118448503 with penalty 0 = 0 + 0
c [ternres-9] all 20079 free variables schedulable
c [ternres-9] 90 ternary resolvents (0 bin, 90 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-8] limit 23689700 penalty 0 = 0 + 0
c [gauss-8] extracted 856 xors of average arity 2.7
c [gauss-8] connected 2336 occurrences of 896 variables (average 2.6)
c [gauss-8] limit 23689700 penalty 0 = 0 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 4 ternary equations
c [decomp-51] removed 1 variables
c [treelook-5] limit 11844850 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 30106 literals 75%
c [treelook-5] scheduling used 1205846 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 11844850 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 11860576 steps
c [treelook-5] 29157 literals remain 73%
c [treelook-5] 4755 variables remain to probed next time 24%
c [decomp-52] removed 5 variables
c [treelook-5] removed 5 variables, found 1845 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1313 transitive binary clauses
c [bca-9] limit of 10000000 steps and 907551 added (scaled 2)
c [bca-9] 22227 out of 40148 literals actually usable 55%
c [bca-9] added 21 blocked clauses in 113175 steps
c [sweep-9] limit 35534551 penalty 0 = 0 + 0
c [sweep-9-1] 1391 pos 44.5% + 1736 neg 55.5% = 3127 sched 15.6% ret 16946
c [sweep-9-1] 17972880 steps 1393 queries 26.96 avg class size
c [sweep-9-1] 47385 decisions 1358 SAT calls 86.86 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-53] removed 27 variables
c [sweep-9-1] removed 27 vars (0 failed, 42 eqs, 34 impls)
c [sweep-9-2] 8805 pos 43.9% + 11241 neg 56.1% = 20046 sched 100.0% ret 0
c [sweep-9-2] 17564113 steps 831 queries 293.62 avg class size
c [sweep-9-2] 28882 decisions 819 SAT calls 87.72 avg env size
c [sweep-9-2] 9562 variables remain 48% (10484 retained 52%)
c [decomp-54] removed 33 variables
c [sweep-9-2] removed 33 vars (0 failed, 46 eqs, 26 impls)
c [sweep-9] removed 60 vars in TOTAL (2 rounds, 2222 queries)
c [sort-queue-13] sorted 12652 enqueued variables after 372911 conflicts
c [score-dist-13] active 7361 (37%), one 8289 (41%), zero 4363 (22%)
c [score-dist-13] max exp 505, different 396 (78%)
c [score-dist-13] median active exp 237, avg 240.8
c [simplification-13] removed 66 variables 0.3% (20013 remain 34%)
c [simplification-13] removed 279 irredundant clauses 0.1% (452343 remain 81%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 133326
c [simplification-13] new conflict interval 266652
c [simplification-13] penalized conflict interval 266652 = 1 * 266652
c [simplification-13] hard conflict limit 772889 (soft 639563 + delta 133326)
c [simplification-13] new conflict limit 639563 (hard 772889)
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 -  333.4   20013   452343    394545   34489   7604 16073   18   139   40  13%   1021  -79   17   18   95%
c -  342.8   20013   452343    434352   38484   7626 16081   20   229   40   9%   1023   29   20   19  109%
c -  354.5   20013   452343    471542   37931   7663 16084   21    88   40  23%   1023 -103   21   19  110%
c -  364.0   20013   452343    511115   40508   7683 16089   20   219   65   9%   1024   36   20   19  103%
c -  372.9   20013   452343    549342   41332   7699 16091   21   193   65  11%   1024   16   20   20  102%
c -  384.6   20013   452343    588333   40477   7724 16094   21   246   65   9%   1024   48   23   20  115%
c -  395.5   20013   452343    629935   42331   7740 16100   19   147   65  13%   1024  -44   19   20   92%
c 
c [simplification-14] limit 639563 conflicts (hard 772889) hit after 660710 conflicts
c [quatres-10] found 66564 quaternary clauses 25% in total
c [quatres-10-1] removed 2 duplicate quaternary clauses
c [quatres-10-1] added 2 double-self-subsuming ternary resolvents
c [quatres-10-2] added 23 single-self-subsuming ternary resolvents
c [quatres-10-2] added 32 quaternary resolvents
c [ternres-10] limit 161333657 with penalty 0 = 0 + 0
c [ternres-10] all 20013 free variables schedulable
c [ternres-10] 57 ternary resolvents (1 bin, 56 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-9] limit 32266731 penalty 0 = 0 + 0
c [gauss-9] extracted 939 xors of average arity 2.7
c [gauss-9] connected 2541 occurrences of 900 variables (average 2.8)
c [gauss-9] limit 32266731 penalty 0 = 0 + 0
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-55] removed 1 variables
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 8570 sched 43%, 0 failed, 0 lifted, 470 hbrs
c [decomp-56] removed 3 variables
c [basicprobe-5-1] 8570 sched 43%, 0 failed, 0 lifted, 40 hbrs
c [basicprobe-5-2] 8570 sched 43%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-5-3] 8570 sched 43%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-5-4] 8570 sched 43%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-5-5] 8570 sched 43%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-5-6] 8570 sched 43%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-5-7] 8570 sched 43%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-5-8] 8570 sched 43%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-5-8] round limit 8 hit
c [basicprobe-5-8] removed 3 variables, found 556 hbrs
c [bate-3] eliminated 84 asymmetric tautologies during probing
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 943 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 1008335356 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 4 clauses out of 412 (1%) of length 21
c [cce-4-1] eliminated 18 clauses out of 543 (3%) of length 19
c [cce-4-1] eliminated 69 clauses out of 356 (19%) of length 17
c [cce-4-1] eliminated 148 clauses out of 1057 (14%) of length 15
c [cce-4-1] eliminated 1 clauses out of 221 (0%) of length 14
c [cce-4-1] eliminated 195 clauses out of 1669 (12%) of length 13
c [cce-4-1] eliminated 77 clauses out of 2003 (4%) of length 12
c [cce-4-1] eliminated 252 clauses out of 1056 (24%) of length 11
c [cce-4-1] eliminated 35 clauses out of 1519 (2%) of length 10
c [cce-4-1] eliminated 1521 clauses out of 7855 (19%) of length 9
c [cce-4-1] eliminated 364 clauses out of 7832 (5%) of length 8
c [cce-4-1] eliminated 428 clauses out of 14913 (3%) of length 7
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 3112 large clauses in 1008335750 steps
c [cce-4-1] allowing another 504167875 steps for small clauses
c [cce-4-1] scheduling 48286 clauses = 37037 binary + 11249 ternary
c [cce-4-1] tried to eliminate 46058 small clauses 95%
c [cce-4-1] eliminated 2680 binary clauses 7%
c [cce-4-1] eliminated 687 ternary clauses 6%
c [cce-4-1] eliminated 3367 small clauses 7%
c [cce-4-1] eliminated 3367 small clauses in 1008335832 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 6479 covered clauses in round 1
c [cce-4] eliminated 6479 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 893903 added (scaled 2)
c [bca-10] 23427 out of 40020 literals actually usable 59%
c [bca-10] added 68 blocked clauses in 139913 steps
c [sweep-10] limit 48400097 penalty 0 = 0 + 0
c [sweep-10-1] 4136 pos 43.3% + 5422 neg 56.7% = 9558 sched 47.8% ret 10451
c [sweep-10-1] 38647036 steps 2828 queries 70.12 avg class size
c [sweep-10-1] 81710 decisions 2755 SAT calls 75.15 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-64] removed 53 variables
c [sweep-10-1] removed 53 vars (0 failed, 105 eqs, 44 impls)
c [sweep-10-2] 8808 pos 44.1% + 11148 neg 55.9% = 19956 sched 100.0% ret 0
c [sweep-10-2] 9755195 steps 418 queries 514.29 avg class size
c [sweep-10-2] 14205 decisions 426 SAT calls 86.42 avg env size
c [sweep-10-2] 13940 variables remain 70% (6016 retained 30%)
c [decomp-65] removed 15 variables
c [sweep-10-2] removed 15 vars (0 failed, 21 eqs, 11 impls)
c [sweep-10] removed 68 vars in TOTAL (2 rounds, 3244 queries)
c [sort-queue-14] sorted 14173 enqueued variables after 660710 conflicts
c [score-dist-14] active 5768 (29%), one 10069 (50%), zero 4104 (21%)
c [score-dist-14] max exp 922, different 414 (45%)
c [score-dist-14] median active exp 488, avg 601.7
c [simplification-14] removed 72 variables 0.4% (19941 remain 34%)
c [simplification-14] removed 6834 irredundant clauses 1.5% (445509 remain 80%)
c [simplification-14] maximum reduction of 2% = max (0%, 2%)
c [simplification-14] geometric conflict interval increment 88884 = 266652 / 3
c [simplification-14] new conflict interval 355536
c [simplification-14] penalized conflict interval 355536 = 1 * 355536
c [simplification-14] hard conflict limit 1194014 (soft 1016246 + delta 177768)
c [simplification-14] new conflict limit 1016246 (hard 1194014)
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 -  424.0   19941   445509    670777   46355   8522 18803   18   185   41  10%   1024   28   21   20  107%
c -  435.5   19941   445509    709564   43367   8550 18807   20   206   41  10%   1024   29   20   20  101%
c -  444.0   19941   445509    752720   46604   8570 18810   20   217   41   9%   1024   48   21   20  106%
c -  454.3   19941   445509    794203   46406   8587 18812   18   129   41  14%   1024  -49   17   20   87%
c -  461.1   19941   445509    837007   50175   8589 18812   19   247   68   8%   1024   85   20   20   99%
c -  472.6   19941   445509    877595   47302   8617 18817   21   257   67   8%   1024   68   24   20  117%
c -  487.3   19941   445509    922783   46297   8645 18820   21   230   67   9%   1024   28   20   20   99%
c -  496.9   19941   445509    970544   52139   8656 18823   19   120   67  16%   1024  -42   16   20   80%
c -  504.7   19941   445509   1013873   52937   8662 18824   21   173   67  12%   1024   18   21   21  102%
c 
c [simplification-15] limit 1016246 conflicts (hard 1194014) hit after 1016247 conflicts
c [quatres-11] found 66658 quaternary clauses 25% in total
c [quatres-11-1] removed 6 duplicate quaternary clauses
c [quatres-11-2] added 24 single-self-subsuming ternary resolvents
c [quatres-11-2] added 24 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 19941 free variables schedulable
c [ternres-11] 65 ternary resolvents (0 bin, 65 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 6634082 penalty 4 = 4 + 0
c [card-5] found 3461 at-most-one constraints of average size 3.1
c [card-5] found 69 at-most-two constraints of average size 4.0
c [card-5] using previous limit 6634082 for elimination
c [card-5] 3530 out of 3530 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-10] limit 42458127 penalty 0 = 0 + 0
c [gauss-10] extracted 915 xors of average arity 2.7
c [gauss-10] connected 2445 occurrences of 894 variables (average 2.7)
c [gauss-10] limit 42458127 penalty 0 = 0 + 0
c [gauss-10] fully completed
c [gauss-10] exported 0 unary, 0 binary and 1 ternary equations
c [simpleprobe-6] 6952 schedulable variables 35%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-67] removed 29 variables
c [simpleprobe-6] 5947 variables remain 30% (13965 retained 70%)
c [simpleprobe-6] removed 29 variables, found 4077 hbrs, 0 units
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 2872 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 19912 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 209 blocked clauses
c [block-5] 209 < 1/100 * 445123 = 4451 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 19911 variables 100%
c [elim-9] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 725 not tried 4% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 51 = 0% variables out of 19911 scheduled
c [elim-9] 51 < 1/100 * 19911 = 199 considered unsuccessful
c [bca-11] limit of 10000000 steps and 886745 added (scaled 2)
c [bca-11] 22558 out of 39722 literals actually usable 57%
c [bca-11] added 37 blocked clauses in 120613 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 636871900 penalty 0 = 0 + 0
c [sweep-11-1] 6009 pos 43.3% + 7867 neg 56.7% = 13876 sched 69.9% ret 5984
c [sweep-11-1] 44497658 steps 3206 queries 70.63 avg class size
c [sweep-11-1] 92240 decisions 3140 SAT calls 72.22 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-68] removed 52 variables
c [sweep-11-1] removed 52 vars (0 failed, 98 eqs, 48 impls)
c [sweep-11-2] 8759 pos 44.2% + 11049 neg 55.8% = 19808 sched 100.0% ret 0
c [sweep-11-2] 51365816 steps 3396 queries 68.10 avg class size
c [sweep-11-2] 98805 decisions 3340 SAT calls 72.99 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-69] removed 63 variables
c [sweep-11-2] removed 63 vars (0 failed, 126 eqs, 52 impls)
c [sweep-11-3] 8742 pos 44.3% + 11003 neg 55.7% = 19745 sched 100.0% ret 0
c [sweep-11-3] 51424198 steps 3400 queries 66.76 avg class size
c [sweep-11-3] 97159 decisions 3331 SAT calls 72.62 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-70] removed 52 variables
c [sweep-11-3] removed 52 vars (0 failed, 118 eqs, 52 impls)
c [sweep-11] removed 167 vars in TOTAL (3 rounds, 9999 queries)
c [sort-queue-15] sorted 15223 enqueued variables after 1016247 conflicts
c [score-dist-15] active 4470 (23%), one 11467 (58%), zero 3756 (19%)
c [score-dist-15] max exp 570, different 378 (66%)
c [score-dist-15] median active exp 360, avg 343.6
c [simplification-15] removed 248 variables 1.2% (19693 remain 34%)
c [simplification-15] removed 3595 irredundant clauses 0.8% (441914 remain 79%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 177768 = 355536 / 2
c [simplification-15] new conflict interval 533304
c [simplification-15] penalized conflict interval 533304 = 1 * 533304
c [simplification-15] hard conflict limit 1816203 (soft 1549551 + delta 266652)
c [simplification-15] new conflict limit 1549551 (hard 1816203)
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 -  531.6   19693   441914   1056718   48503   8622 20663   22   234   40   9%   1024   52   22   21  104%
c -  546.4   19693   441914   1107500   51920   8643 20666   21   265   40   8%   1024   59   20   21   94%
c -  559.9   19693   441914   1156312   53979   8665 20670   21   199   66  11%   1024   -8   23   21  108%
c -  571.7   19693   441914   1204491   55121   8678 20671   21   188   66  11%   1024   -6   23   21  108%
c -  581.1   19693   441914   1252877   57730   8684 20671   21    91   66  23%   1024  -75   21   21  102%
c -  588.0   19693   441914   1300016   60469   8689 20672   21    91   66  23%   1024  -45   21   21  100%
c -  599.6   19693   441914   1345814   57553   8707 20675   21   169   66  12%   1024   18   19   21   94%
c -  610.4   19693   441914   1396171   59475   8724 20677   21   155   66  14%   1024   -3   22   21  105%
c -  623.7   19693   441914   1445902   59261   8739 20681   21   211   66  10%   1024   42   20   21   94%
c -  634.1   19693   441914   1497338   61998   8746 20682   18   190   66  10%   1024   22   17   21   83%
c -  644.9   19693   441914   1547615   62532   8758 20684   19   164   42  12%   1024   -6   18   20   87%
c 
c [simplification-16] limit 1549551 conflicts (hard 1816203) hit after 1555729 conflicts
c [quatres-12] found 66869 quaternary clauses 25% in total
c [quatres-12-1] removed 20 duplicate quaternary clauses
c [quatres-12-1] added 2 double-self-subsuming ternary resolvents
c [quatres-12-2] added 54 single-self-subsuming ternary resolvents
c [quatres-12-2] added 31 quaternary resolvents
c [ternres-12] limit 200000000 with penalty 0 = 0 + 0
c [ternres-12] all 19693 free variables schedulable
c [ternres-12] 81 ternary resolvents (0 bin, 81 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-11] limit 50000000 penalty 0 = 0 + 0
c [gauss-11] extracted 926 xors of average arity 2.7
c [gauss-11] connected 2526 occurrences of 907 variables (average 2.8)
c [gauss-11] limit 50000000 penalty 0 = 0 + 0
c [gauss-11] fully completed
c [gauss-11] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-6] limit 29142623 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 29755 literals 76%
c [treelook-6] scheduling used 1238853 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 29142623 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 29155296 steps
c [treelook-6] 27182 literals remain 69%
c [treelook-6] 4643 variables remain to probed next time 24%
c [decomp-72] removed 1 variables
c [treelook-6] removed 2 variables, found 2098 hbrs
c [unhide-9] limit 2500000 with penalty 3 = 3 + 0
c [unhide-9-10] 0 units, 0 failed, 440 tauts, 0 hbrs, 25349 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 2115 transitive binary clauses
c [cce-5] limit of 364282799 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 3 clauses out of 6 (50%) of length 28
c [cce-5-1] eliminated 2 clauses out of 909 (0%) of length 15
c [cce-5-1] eliminated 2 clauses out of 217 (1%) of length 14
c [cce-5-1] eliminated 6 clauses out of 1471 (0%) of length 13
c [cce-5-1] eliminated 78 clauses out of 1923 (4%) of length 12
c [cce-5-1] eliminated 60 clauses out of 810 (7%) of length 11
c [cce-5-1] eliminated 31 clauses out of 1490 (2%) of length 10
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 182 large clauses in 364282857 steps
c [cce-5-1] allowing another 182141428 steps for small clauses
c [cce-5-1] scheduling 187024 clauses = 33688 binary + 153336 ternary
c [cce-5-1] tried to eliminate 17286 small clauses 9%
c [cce-5-1] eliminated 213 binary clauses 1%
c [cce-5-1] eliminated 2067 ternary clauses 1%
c [cce-5-1] eliminated 2280 small clauses 1%
c [cce-5-1] eliminated 2280 small clauses in 364282811 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2462 covered clauses in round 1
c [cce-5] eliminated 2462 covered clauses in TOTAL during 1 rounds
c [cce-5] 2462 < 1/100 * 441137 = 4411 considered unsuccessful
c [bca-12] limit of 10000000 steps and 880274 added (scaled 2)
c [bca-12] 21951 out of 39384 literals actually usable 56%
c [bca-12] added 489 blocked clauses in 134262 steps
c [sweep-12] limit 87427871 penalty 0 = 0 + 0
c [sweep-12-1] 8596 pos 43.7% + 11095 neg 56.3% = 19691 sched 100.0% ret 0
c [sweep-12-1] 56857420 steps 3286 queries 63.65 avg class size
c [sweep-12-1] 97318 decisions 3224 SAT calls 73.24 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-73] removed 35 variables
c [sweep-12-1] removed 35 vars (0 failed, 104 eqs, 25 impls)
c [sweep-12-2] 8583 pos 43.7% + 11073 neg 56.3% = 19656 sched 100.0% ret 0
c [sweep-12-2] 30571532 steps 1540 queries 122.47 avg class size
c [sweep-12-2] 46791 decisions 1518 SAT calls 75.61 avg env size
c [sweep-12-2] 5568 variables remain 28% (14088 retained 72%)
c [decomp-74] removed 27 variables
c [sweep-12-2] removed 27 vars (0 failed, 63 eqs, 19 impls)
c [sweep-12] removed 62 vars in TOTAL (2 rounds, 4824 queries)
c [sort-queue-16] sorted 11910 enqueued variables after 1555729 conflicts
c [score-dist-16] active 7719 (39%), one 8378 (43%), zero 3532 (18%)
c [score-dist-16] max exp 877, different 592 (67%)
c [score-dist-16] median active exp 492, avg 480.3
c [simplification-16] removed 64 variables 0.3% (19629 remain 34%)
c [simplification-16] removed 3241 irredundant clauses 0.7% (438673 remain 79%)
c [simplification-16] maximum reduction of 1% = max (0%, 1%)
c [simplification-16] geometric conflict interval increment 266652 = 533304 / 2
c [simplification-16] new conflict interval 799956
c [simplification-16] penalized conflict interval 799956 = 1 * 799956
c [simplification-16] hard conflict limit 2755663 (soft 2355685 + delta 399978)
c [simplification-16] new conflict limit 2355685 (hard 2755663)
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 1  664.9   19629   438673   1579545   95048  10956 21278   22   174   53  13%   1024    3   21   20  102%
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 
s SATISFIABLE
c
c bate: 1212 basic ate = 87 trn 7% + 1125 lrg 93% in 3 updates
c bcas: 12 count, 5337 added (722 skipped), 1308453 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 5 bces, 6199 removed, 10397774 resolutions, 33341393 steps
c blkd: 7058 blocking literals 6%, 1 pure
c bump: 1585842 bumped seen, 112276705 lits 70.8 on average
c card: 5 count, 0 units, 0 am1, 27240538 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 51655 subsumed
c card: 22566 at-most-one constraints found, average size 3.04
c card: 22566 at-most-one constraints used 100%, average size 3.04
c card: 69 at-most-two constraints found, average size 4.00
c card: 69 at-most-two constraints used 100%, average size 4.00
c cces: 5 cces, 10072 eliminated, 8688 ate 86%, 1384 abce 14%
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: 2808718 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 86 gcs, 0 rescored clauses, 834 rescored vars
c dcps: 74 decompositions, 15015 equivalent 26%
c deco: 108 decision-only clauses 0%, 47% reduction
c decs: 13978587 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 9 elims, 20756 eliminated 35%, 467 pure 2%
c elms: 9 rounds, 1.0 rounds/bve
c elms: 13606 small 66%, 6682 large 32%
c elms: 20138 tried small, 13606 succeeded 68%, 6532 failed 32%
c elms: 13698 subsumed, 8776 strengthened, 6 blocked
c elms: 5563739 copies, 6294506 resolutions, 382886 ipos
c elms: 13739176 subchks, 3309059 strchks
c gaus: 11 extractions, 7837 extracted, 2.7 size, 3 max
c gaus: exported 0 units, 2 binary and 17 ternary equations
c gaus: 0 gc, 402583508 steps, 201291754 extr 50%, 660827 elim 0%
c glue: 19.1 orig avg, 19.1 real avg, 4.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 52271 = 16709 simple 32% + 33698 trn 64% + 1864 lrg 4%, 2114 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1585842 clauses, 39.9 length
c lrnd: 63301984 lits = 76162237 orig - 12860253 removed 17%
c lrnd: 650485 uips 41%, 816348 flips 51%
c mins: 1562450 mins 99%, 1546 bin 0%, 21706 size 1%
c mins: 72769958 poisoned searches, 12108483 hits, 17% hit rate
c mins: 134990412 used twice searches, 15865227 hits, 12% hit rate
c move: moved 11269, 4645 bin 41%, 6624 trn 59%
c otfs: 4511 driving 49%, 4768 restarting 51%
c otfs: str 9279, 8746 red 94%, 533 irr 6%
c otfs: str 9279, 0 bin 0%, 615 trn 7%, 8664 lrg 93%
c otfs: sub 33, 33 red 100%, 0 irr 0%
c otfs: sub 33, 0 bin 0%, 6 trn 18%, 27 lrg 82%
c phas: 7 computed, 25113 set, 11308 pos (45%), 13805 neg (55%)
c prbs: 5 basic, 491737 probed, 54 failed, 0 lifted
c prbs: 6 simple, 101736 probed, 519 failed, 2033 eqs
c prbs: 6 treelook, 4004 probed, 1 failed, 0 lifted
c prom: 140493 locked 18% out of 760875 tried
c prps: 1014230683 props, 71 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 12 count, 557 quat, 354 self1, 5 self2, 1180 dup
c queu: 16 sorted, 13978587 next (3235919 steps 0.23)
c queu: 117734333 enq (121137844 steps 1.03), 112276705 deq 95%
c redc: 8989 clauses 7%, 132533 tried 8%, 360 sat 0%
c redc: 16024 lits 1%, 1482951 tried 2%, 361 sat 0%
c redc: 554 times jump level reduced, 27.4 levels on average
c reds: 34 count, 46457.2 conflicts per reduce
c reds: 0 memlim 0%, 34 arith 100%
c reds: 1125949 collected 78%, 323944 retired 22%
c rmbd: 10884 removed, 2104 red 19%
c rsts: 24050 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 16 count, 14 confs 88%, 0 vars 0%
c simp: 0 its 0%, 1 bin 6%, 1 trns 6%
c subl: 1585842 count (1145042 tried 0.7), 23644 sub out of 1574448 (1.5%)
c swps: 12 count, 19 rounds, 30085 queries (1583.4/round)
c swps: 28878 sat calls, 491 unsat (0.4% success rate)
c swps: 900736 decisions 31.2, 10808 conflicts 0.4
c swps; 125.6 avg class size, 77.2 avg environment size
c swps: 0 failed, 1160 impls, 1697 equivs
c swp0: 10022 type 0 queries, 3045 unsat (30.4%), 9665 sat (96.4%)
c swp1: 20063 type 1 queries, 8083 unsat (40.3%), 18723 sat (93.3%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 31130876 calls to obtain time
c tops: 3352 fixed 6%, 0 its, 0.00 confs/it
c trds: 12 transitive reductions, 21604 removed, 0 failed
c trds: 437496 nodes, 545523 edges, 23920539 steps
c trim: 196173 words, 0.7 MB
c trnr: 12 count, 2 bin, 8317 trn, 249701843 steps
c unhd: 9 count, 10 rounds, 36088499 steps
c unhd: 562 non-trivial sccs of average size 2.0
c unhd: 1 units, 1 bin, 0 trn, 0 lrg
c unhd: 1219 failed, 1218 stamp, 0 lits, 1 bin, 0 trn, 0 lrg
c unhd: 15748 tauts, 1637 bin 10%, 1186 trn 8%, 665 lrg 4%
c unhd: 15748 tauts, 12260 stamp 78%, 10016 red 64%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 157685 str, 1 bin 0%, 4757 trn 3%, 152927 lrg 97%, 153576 red 97%
c vars: 19629 remaining 33% and 39123 removed 67% out of 58752
c vars: 3352 fixed 6%, 20756 eliminated 35%, 15015 equivalent 26%
c vsts: 30175392685 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 29.8 search visits per propagation, 18691.5 per conflict
c wchs: 4013791388 pushed, 67494768 enlarged, 178 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1575005       1125949        323944      25624979       6655835        443437
c 
c  0 0         34836   2      1949   0         0   0  12902093  50   2161596  32    115993  26     1.1
c  1 5         40098   3     13905   1     19614   6   2616645  10<   613699   9     43743  10     0.4
c  2 6        198306  13     79818   7     94327  29   5476276  21   1548238  23<   127691  29<    1.3
c  3 9        289993  18    197982  18     75825  23   2615488  10   1045414  16     88077  20     1.4
c  4 14       384312  24<   318575  28<    52500  16<  1083864   4    611651   9     41789   9     2.8
c  5 21       418930  27    362047  32     36097  11    643042   3    480625   7     18612   4     4.6
c  6 30       126802   8     98570   9     20502   6    179555   1    128804   2      4825   1     1.7
c  7 41        51469   3     35463   3     13737   4     69160   0     44331   1      1740   0     1.4
c  8 54        21640   1     13180   1      7559   2     27943   0     16051   0       706   0     0.8
c  9 69         6226   0      3309   0      2639   1      7981   0      4065   0       194   0     0.4
c 10 86         1983   0       988   0       925   0      2423   0      1151   0        59   0     0.1
c 11 126         322   0       144   0       167   0       405   0       170   0         5   0     0.0
c 12 230          88   0        19   0        52   0       104   0        40   0         3   0     0.0
c 
c avg                  4.0           4.3           3.5           1.2           1.9           2.0
c std                  1.6           1.3           1.8           1.5           1.8           1.6
c 
c   23.623   4% sweep
c   20.966   3% probe
c   18.742   3% cce
c   16.182   2% elim
c    9.087   1% bump
c    8.725   1% decide
c    4.485   1% gauss
c    3.313   0% quatres
c    3.031   0% unhide
c    2.828   0% transred
c 
c    7.537 < 1% rest (below)
c 
c    2.417   0% block
c    1.970   0% bca
c    1.771   0% ternres
c    1.001   0% rescore
c    0.379   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    2.051   0% preprocessing     2%
c  102.742  15% inprocessing     98%
c ==================================
c  104.794  16% simplifying
c  560.064  84% search
c ==================================
c  664.862 100% all
c 
c       1579545 conflicts,        2375.7 confs/sec
c          6233 ternaries,         253.4 confs/ternary
c          3159 binaries,          500.0 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            34 reductions,          0.1 redus/sec,  46457.2 confs/reduction
c         24050 restarts,           36.2 rests/sec,     65.7 confs/restart
c      13978587 decisions,       21024.8 decis/sec,      8.8 decis/conflict
c    1014230683 propagations,  1525474.9 props/sec,     72.6 props/decision
c 
c 664.9 seconds, 104.6 MB
c launch: done
