c launch: /data/cnf/sc2014/app/q_query_3_L100_coli.sat.cnf.bz2
c host: atom24
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/q_query_3_L100_coli.sat.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/q_query_3_L100_coli.sat.cnf.bz2
c no embedded options
c found 'p cnf 315617 1522583' header
c read 315617 variables, 1522583 clauses, 4407119 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=6
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 272603 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] AVG (--score=6)
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  272603  1433869         0       0      0     0    0     0  102   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 2537 at-most-one constraints of average size 4.1
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 2537 out of 2537 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 108788 variables
c [simpleprobe-1] all 206829 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 19466 variables
c [simpleprobe-1] 169250 variables remain 90% (18113 retained 10%)
c [simpleprobe-1] removed 19466 variables, found 0 hbrs, 135 units
c [unhide-1] limit 59602 based on 953644 irredundant clauses
c [unhide-1-1] 35 units, 117 failed, 251 tauts, 0 hbrs, 361 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 187099 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 116784 not tried 62% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 70325 = 38% variables out of 187099 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 721521 negative 96.9% of 744235 except 22714 3.1%
c [phase-count-1] 576711 positive 77.5% of 744235 except 167524 22.5%
c [phase-count-1] less non-negative clauses 22714 than limit 74400 (10.0%)
c [phase-count-1] non-pos/non-neg = 167524/22714 = 7.38 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 116774 negative 100%
c [sort-queue-1] sorted 116774 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 116774 (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 130246 variables 52.7% (116774 remain 43%)
c [simplification-1] removed 689634 irredundant clauses 48.1% (744235 remain 52%)
c [simplification-1] maximum reduction of 53% = max (53%, 48%)
c [simplification-1] large reduction 53% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    3.7  116773   744235         1       0      0     0    0     0   41   0%      0    0    0    0    0%
c i    4.1  116487   744235       284     100     88    91    0     3   60   8%      1    3    2    0 12271%
c i    4.1  116411   744235       286     100     89    91    0     3   60   8%      1    3    2    0 12201%
c i    4.1  116410   744235       339     142     94    92    0     4   60   8%      1    4    2    0 12359%
c i    4.1  116408   744235       453     240    103    94    0     6   60   8%      1    6    4    0 12544%
c i    4.1  116407   744235       454     240    103    94    0     6   60   8%      1    6    4    0 12495%
c i    4.1  116066   744235       470     253    103    96    0     6   60   9%      1    6    4    0 12870%
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [decomp-3] removed 5594 variables
c [simpleprobe-2] 100706 schedulable variables 91%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 35 variables
c [simpleprobe-2] 100740 variables remain 91% (10405 retained 9%)
c [simpleprobe-2] removed 35 variables, found 2417 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 30370 literals 14%
c [treelook-1] scheduling used 300375 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 383371 steps
c [treelook-1] 30326 literals remain 14%
c [treelook-1] 29630 variables remain to probed next time 27%
c [decomp-5] removed 8 variables
c [treelook-1] removed 8 variables, found 2410 hbrs
c [basicprobe-1] limit 5245792 based on 655724 irredundant clauses
c [basicprobe-1-0] 49358 probes remain 45% after last round
c [basicprobe-1-0] 112 units = 100 failed (89%) + 12 lifted (11%)
c [basicprobe-1-0] removed 368 variables, found 70483 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 57 units, 66 failed, 3805 tauts, 0 hbrs, 3913 literals
c [elim-2] 110439 variables 100% will be scheduled this time
c [elim-2] scheduled 110439 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 14876 not tried 13% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 67220 = 61% variables out of 110439 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 413009 negative 97.9% of 421975 except 8966 2.1%
c [phase-count-2] 305076 positive 72.3% of 421975 except 116899 27.7%
c [phase-count-2] less non-negative clauses 8966 than limit 42100 (10.0%)
c [phase-count-2] non-pos/non-neg = 116899/8966 = 13.04 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 4075 negative 100%
c [sort-queue-2] sorted 39324 enqueued variables after 509 conflicts
c [score-dist-2] active 3895 (9%), one 0 (0%), zero 39324 (91%)
c [score-dist-2] max exp 510, different 10 (2%)
c [score-dist-2] median active exp 510, avg 509.6
c [simplification-2] removed 72847 variables 62.8% (43219 remain 16%)
c [simplification-2] removed 322260 irredundant clauses 43.3% (421975 remain 29%)
c [simplification-2] maximum reduction of 63% = max (63%, 43%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1025 (hard 11000)
c [simplification-2] new binary interval 1000
c 
c [simplification-3] limit 1025 conflicts (hard 11000) hit after 1025 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1922 at-most-one constraints of average size 3.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1922 out of 1922 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 104 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 9384 literals 11%
c [treelook-2] scheduling used 300019 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 460272 steps
c [treelook-2] 9355 literals remain 11%
c [treelook-2] 4703 variables remain to probed next time 11%
c [treelook-2] removed 0 variables, found 1289 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 5 failed, 5181 tauts, 0 hbrs, 4360 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 43113 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 2627 not tried 6% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1493 = 3% variables out of 43113 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 401070 negative 97.9% of 409615 except 8545 2.1%
c [phase-count-3] 298857 positive 73.0% of 409615 except 110758 27.0%
c [phase-count-3] less non-negative clauses 8545 than limit 40900 (10.0%)
c [phase-count-3] non-pos/non-neg = 110758/8545 = 12.96 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 3947 negative 100%
c [sort-queue-3] sorted 37088 enqueued variables after 1025 conflicts
c [score-dist-3] active 4532 (11%), one 0 (0%), zero 37088 (89%)
c [score-dist-3] max exp 511, different 11 (2%)
c [score-dist-3] median active exp 510, avg 510.0
c [simplification-3] removed 1599 variables 3.7% (41620 remain 15%)
c [simplification-3] removed 12352 irredundant clauses 2.9% (409615 remain 29%)
c [simplification-3] maximum reduction of 4% = max (4%, 3%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 4000
c [simplification-3] penalized conflict interval 4000 = 1 * 4000
c [simplification-3] hard conflict limit 15025 (soft 5025 + delta 10000)
c [simplification-3] new conflict limit 5025 (hard 15025)
c 
c [simplification-4] limit 5025 conflicts (hard 15025) hit after 5025 conflicts
c [decomp-8] removed 2 variables
c [basicprobe-2] limit 3336540 penalty 0 = 0 + 0
c [basicprobe-2-0] 18156 probes remain 44% after last round
c [basicprobe-2-0] removed 0 variables, found 32746 hbrs
c [unhide-4] limit 133461 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 2661 tauts, 0 hbrs, 5088 literals
c [elim-4] 2626 variables 6% will be scheduled this time
c [elim-4] scheduled 2626 variables 6%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 289198264 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 2626 scheduled
c [phase-count-4] 385673 negative 97.8% of 394210 except 8537 2.2%
c [phase-count-4] 282818 positive 71.7% of 394210 except 111392 28.3%
c [phase-count-4] less non-negative clauses 8537 than limit 39400 (10.0%)
c [phase-count-4] non-pos/non-neg = 111392/8537 = 13.05 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 3900 negative 100%
c [sort-queue-4] sorted 35122 enqueued variables after 5025 conflicts
c [score-dist-4] active 6496 (16%), one 0 (0%), zero 35122 (84%)
c [score-dist-4] max exp 514, different 12 (2%)
c [score-dist-4] median active exp 513, avg 513.0
c [simplification-4] removed 2 variables 0.0% (41618 remain 15%)
c [simplification-4] removed 15335 irredundant clauses 3.7% (394210 remain 27%)
c [simplification-4] maximum reduction of 4% = max (0%, 4%)
c [simplification-4] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-4] new conflict interval 8000
c [simplification-4] penalized conflict interval 8000 = 1 * 8000
c [simplification-4] hard conflict limit 23025 (soft 13025 + delta 10000)
c [simplification-4] new conflict limit 13025 (hard 23025)
c 
c [simplification-5] limit 13025 conflicts (hard 23025) hit after 13025 conflicts
c [quatres-1] found 15396 quaternary clauses 31% in total
c [quatres-1-1] added 6 double-self-subsuming ternary resolvents
c [quatres-1-2] added 67 single-self-subsuming ternary resolvents
c [quatres-1-2] added 2902 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 41618 free variables schedulable
c [ternres-1] 3572 ternary resolvents (1 bin, 3571 trn)
c [ternres-1] 30056 variables remain 72% (11562 retained 28%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 51 xors of average arity 3.0
c [gauss-1] connected 151 occurrences of 59 variables (average 2.6)
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-9] removed 2 variables
c [simpleprobe-3] 37301 schedulable variables 90%
c [simpleprobe-3] limit 7706113 penalty 0 = 0 + 0
c [simpleprobe-3] 32985 variables remain 79% (8631 retained 21%)
c [simpleprobe-3] removed 0 variables, found 1557 hbrs, 0 units
c [transred-1] limit 1926528 with penalty 0 = 0 + 0
c [transred-1] removed 560 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 41616 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 12169 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 20 clauses out of 21 (95%) of length 12
c [cce-1-1] eliminated 3 clauses out of 133 (2%) of length 11
c [cce-1-1] eliminated 2 clauses out of 13 (15%) of length 10
c [cce-1-1] eliminated 5 clauses out of 198 (3%) of length 9
c [cce-1-1] eliminated 502 clauses out of 673 (75%) of length 8
c [cce-1-1] eliminated 675 clauses out of 3254 (21%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1207 large clauses in 30000172 steps
c [cce-1-1] allowing another 15000086 steps for small clauses
c [cce-1-1] scheduling 209687 clauses = 35962 binary + 173725 ternary
c [cce-1-1] tried to eliminate 5545 small clauses 3%
c [cce-1-1] eliminated 303 binary clauses 1%
c [cce-1-1] eliminated 4016 ternary clauses 2%
c [cce-1-1] eliminated 4319 small clauses 2%
c [cce-1-1] eliminated 4319 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 5526 covered clauses in round 1
c [cce-1] eliminated 5526 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 753130 added (scaled 2)
c [bca-1] 73849 out of 83234 literals actually usable 89%
c [bca-1] added 0 blocked clauses in 173753 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 9474 pos 22.8% + 32142 neg 77.2% = 41616 sched 100.0% ret 0
c [sweep-1-1] 1053026 steps 18 queries 9621.61 avg class size
c [sweep-1-1] 611 decisions 17 SAT calls 315.71 avg env size
c [sweep-1-1] 41518 variables remain 100% (98 retained 0%)
c [decomp-11] removed 3 variables
c [sweep-1-1] removed 3 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 3 vars in TOTAL (1 rounds, 17 queries)
c [phase-count-5] 367796 negative 97.7% of 376307 except 8511 2.3%
c [phase-count-5] 269628 positive 71.7% of 376307 except 106679 28.3%
c [phase-count-5] less non-negative clauses 8511 than limit 37600 (10.0%)
c [phase-count-5] non-pos/non-neg = 106679/8511 = 12.53 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 3756 negative 100%
c [sort-queue-5] sorted 34154 enqueued variables after 13025 conflicts
c [score-dist-5] active 7459 (18%), one 0 (0%), zero 34154 (82%)
c [score-dist-5] max exp 515, different 11 (2%)
c [score-dist-5] median active exp 515, avg 514.3
c [simplification-5] removed 5 variables 0.0% (41613 remain 15%)
c [simplification-5] removed 17903 irredundant clauses 4.5% (376307 remain 26%)
c [simplification-5] maximum reduction of 5% = max (0%, 5%)
c [simplification-5] large reduction 5% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 25025 (soft 15025 + delta 10000)
c [simplification-5] new conflict limit 15025 (hard 25025)
c 
c [simplification-6] limit 15025 conflicts (hard 25025) hit after 15025 conflicts
c [quatres-2] found 18315 quaternary clauses 35% in total
c [quatres-2-1] added 3 double-self-subsuming ternary resolvents
c [quatres-2-2] added 16 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2258 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 30052 schedulable variables 72%
c [ternres-2] 876 ternary resolvents (6 bin, 870 trn)
c [ternres-2] 28075 variables remain 67% (13538 retained 33%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 187 at-most-one constraints of average size 3.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 187 out of 187 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-5] limit 231984 with penalty 1 = 1 + 0
c [unhide-5-5] 0 units, 5 failed, 3351 tauts, 0 hbrs, 8453 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 522 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 41608 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 13 blocked clauses
c [block-2] 13 < 1/100 * 373822 = 3738 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 55 clauses out of 2578 (2%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 55 large clauses in 30000025 steps
c [cce-2-1] allowing another 15000012 steps for small clauses
c [cce-2-1] scheduling 203630 clauses = 35008 binary + 168622 ternary
c [cce-2-1] tried to eliminate 6015 small clauses 3%
c [cce-2-1] eliminated 281 binary clauses 1%
c [cce-2-1] eliminated 4136 ternary clauses 2%
c [cce-2-1] eliminated 4417 small clauses 2%
c [cce-2-1] eliminated 4417 small clauses in 30000051 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 4472 covered clauses in round 1
c [cce-2] eliminated 4472 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 41608 variables 100%
c [elim-5] limit of 23198488 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 1600 not tried 4% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 265 = 1% variables out of 41608 scheduled
c [elim-5] 265 < 1/100 * 41608 = 416 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 9814 pos 23.8% + 31440 neg 76.2% = 41254 sched 99.8% ret 89
c [sweep-2-1] 1015950 steps 11 queries 12616.18 avg class size
c [sweep-2-1] 224 decisions 10 SAT calls 68.70 avg env size
c [sweep-2-1] 41224 variables remain 100% (118 retained 0%)
c [decomp-13] removed 6 variables
c [sweep-2-1] removed 6 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 6 vars in TOTAL (1 rounds, 10 queries)
c [phase-count-6] 359124 negative 97.7% of 367675 except 8551 2.3%
c [phase-count-6] 262290 positive 71.3% of 367675 except 105385 28.7%
c [phase-count-6] less non-negative clauses 8551 than limit 36700 (10.0%)
c [phase-count-6] non-pos/non-neg = 105385/8551 = 12.32 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 3712 negative 100%
c [sort-queue-6] sorted 33904 enqueued variables after 15025 conflicts
c [score-dist-6] active 7433 (18%), one 0 (0%), zero 33904 (82%)
c [score-dist-6] max exp 515, different 11 (2%)
c [score-dist-6] median active exp 515, avg 514.4
c [simplification-6] removed 276 variables 0.7% (41337 remain 15%)
c [simplification-6] removed 8632 irredundant clauses 2.3% (367675 remain 26%)
c [simplification-6] maximum reduction of 2% = max (1%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 14666
c [simplification-6] penalized conflict interval 14666 = 1 * 14666
c [simplification-6] hard conflict limit 39691 (soft 29691 + delta 10000)
c [simplification-6] new conflict limit 29691 (hard 39691)
c 
c [simplification-7] limit 29691 conflicts (hard 39691) hit after 29691 conflicts
c [quatres-3] found 20998 quaternary clauses 37% in total
c [quatres-3-1] added 4 double-self-subsuming ternary resolvents
c [quatres-3-2] added 84 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1209 quaternary resolvents
c [ternres-3] limit 5195624 with penalty 0 = 0 + 0
c [ternres-3] 27869 schedulable variables 67%
c [ternres-3] 1490 ternary resolvents (7 bin, 1483 trn)
c [ternres-3] 24762 variables remain 60% (16575 retained 40%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 75 xors of average arity 3.0
c [gauss-2] connected 225 occurrences of 113 variables (average 2.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 1 variables
c [treelook-3] limit 259781 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 8903 literals 11%
c [treelook-3] scheduling used 259845 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 259781 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 311423 steps
c [treelook-3] 8889 literals remain 11%
c [treelook-3] 2333 variables remain to probed next time 6%
c [treelook-3] removed 0 variables, found 1072 hbrs
c [unhide-6] limit 1039124 with penalty 0 = 0 + 0
c [unhide-6-6] 2 units, 10 failed, 2004 tauts, 0 hbrs, 15938 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 610 transitive binary clauses
c [transred-3] found 1 units
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 35 clauses out of 42 (83%) of length 12
c [cce-3-1] eliminated 52 clauses out of 192 (27%) of length 11
c [cce-3-1] eliminated 12 clauses out of 111 (11%) of length 10
c [cce-3-1] eliminated 6 clauses out of 213 (3%) of length 9
c [cce-3-1] eliminated 4 clauses out of 177 (2%) of length 8
c [cce-3-1] eliminated 39 clauses out of 2472 (2%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 148 large clauses in 30000163 steps
c [cce-3-1] allowing another 15000081 steps for small clauses
c [cce-3-1] scheduling 161010 clauses = 35132 binary + 125878 ternary
c [cce-3-1] tried to eliminate 2719 small clauses 2%
c [cce-3-1] eliminated 220 binary clauses 1%
c [cce-3-1] eliminated 834 ternary clauses 1%
c [cce-3-1] eliminated 1054 small clauses 1%
c [cce-3-1] eliminated 1174 small clauses in 30000044 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1322 covered clauses in round 1
c [cce-3] eliminated 1322 covered clauses in TOTAL during 1 rounds
c [cce-3] 1322 < 1/100 * 367516 = 3675 considered unsuccessful
c [bca-2] limit of 10000000 steps and 732888 added (scaled 2)
c [bca-2] 66885 out of 82652 literals actually usable 81%
c [bca-2] added 85 blocked clauses in 172626 steps
c [sweep-3] limit 1558687 penalty 0 = 0 + 0
c [sweep-3-1] 17127 pos 41.6% + 24080 neg 58.4% = 41207 sched 99.7% ret 118
c [sweep-3-1] 1591042 steps 21 queries 9844.19 avg class size
c [sweep-3-1] 773 decisions 19 SAT calls 198.26 avg env size
c [sweep-3-1] 41011 variables remain 99% (314 retained 1%)
c [decomp-16] removed 17 variables
c [sweep-3-1] removed 17 vars (0 failed, 1 eqs, 2 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 17 vars in TOTAL (1 rounds, 20 queries)
c [phase-count-7] 357563 negative 97.7% of 366073 except 8510 2.3%
c [phase-count-7] 260781 positive 71.2% of 366073 except 105292 28.8%
c [phase-count-7] less non-negative clauses 8510 than limit 36600 (10.0%)
c [phase-count-7] non-pos/non-neg = 105292/8510 = 12.37 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 3174 negative 100%
c [sort-queue-7] sorted 26731 enqueued variables after 29691 conflicts
c [score-dist-7] active 14577 (35%), one 0 (0%), zero 26731 (65%)
c [score-dist-7] max exp 516, different 12 (2%)
c [score-dist-7] median active exp 515, avg 515.3
c [simplification-7] removed 29 variables 0.1% (41308 remain 15%)
c [simplification-7] removed 1592 irredundant clauses 0.4% (366073 remain 26%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20000
c [simplification-7] new conflict interval 34666
c [simplification-7] penalized conflict interval 34666 = 1 * 34666
c [simplification-7] hard conflict limit 81690 (soft 64357 + delta 17333)
c [simplification-7] new conflict limit 64357 (hard 81690)
c 
c [simplification-8] limit of 2867 ternary hit after 2867 ternaries
c [quatres-4] found 23207 quaternary clauses 36% in total
c [quatres-4-1] removed 4 duplicate quaternary clauses
c [quatres-4-1] added 8 double-self-subsuming ternary resolvents
c [quatres-4-2] added 125 single-self-subsuming ternary resolvents
c [quatres-4-2] added 736 quaternary resolvents
c [ternres-4] limit 10223639 with penalty 0 = 0 + 0
c [ternres-4] 24740 schedulable variables 60%
c [ternres-4] 2651 ternary resolvents (12 bin, 2639 trn)
c [ternres-4] 18582 variables remain 45% (22726 retained 55%)
c [unhide-7] limit 2044727 with penalty 0 = 0 + 0
c [unhide-7-8] 3 units, 15 failed, 3770 tauts, 0 hbrs, 47620 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 462 transitive binary clauses
c [transred-4] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 41293 variables 100%
c [block-3] limit of 51118196 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 81 blocked clauses
c [block-3] 81 < 1/100 * 364078 = 3640 considered unsuccessful
c [bca-3] limit of 10000000 steps and 728476 added (scaled 2)
c [bca-3] 63454 out of 82588 literals actually usable 77%
c [bca-3] added 66 blocked clauses in 189693 steps
c [sweep-4] limit 3067091 penalty 0 = 0 + 0
c [sweep-4-1] 17389 pos 42.4% + 23591 neg 57.6% = 40980 sched 99.2% ret 313
c [sweep-4-1] 3915984 steps 46 queries 9696.41 avg class size
c [sweep-4-1] 1113 decisions 39 SAT calls 102.44 avg env size
c [sweep-4-1] 40705 variables remain 99% (588 retained 1%)
c [decomp-18] removed 27 variables
c [sweep-4-1] removed 27 vars (0 failed, 8 eqs, 15 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 27 vars in TOTAL (1 rounds, 45 queries)
c [phase-count-8] 355345 negative 97.7% of 363867 except 8522 2.3%
c [phase-count-8] 258288 positive 71.0% of 363867 except 105579 29.0%
c [phase-count-8] less non-negative clauses 8522 than limit 36300 (10.0%)
c [phase-count-8] non-pos/non-neg = 105579/8522 = 12.39 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 3009 negative 100%
c [sort-queue-8] sorted 24157 enqueued variables after 57089 conflicts
c [score-dist-8] active 17109 (41%), one 0 (0%), zero 24157 (59%)
c [score-dist-8] max exp 517, different 11 (2%)
c [score-dist-8] median active exp 516, avg 515.9
c [simplification-8] removed 42 variables 0.1% (41266 remain 15%)
c [simplification-8] removed 2205 irredundant clauses 0.6% (363867 remain 25%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] forced so keeping old conflict interval 34666
c [simplification-8] conflict limit remains at 64357 (hard 81690)
c [simplification-8] new ternary interval 10000
c 
c [simplification-9] limit 64357 conflicts (hard 81690) hit after 64357 conflicts
c [quatres-5] found 23791 quaternary clauses 36% in total
c [quatres-5-1] removed 39 duplicate quaternary clauses
c [quatres-5-1] added 4 double-self-subsuming ternary resolvents
c [quatres-5-2] added 93 single-self-subsuming ternary resolvents
c [quatres-5-2] added 294 quaternary resolvents
c [ternres-5] limit 11538751 with penalty 0 = 0 + 0
c [ternres-5] 18556 schedulable variables 45%
c [ternres-5] 2540 ternary resolvents (10 bin, 2530 trn)
c [ternres-5] 14395 variables remain 35% (26871 retained 65%)
c [basicprobe-3] limit 28846879 penalty 1 = 1 + 0
c [basicprobe-3-0] 13770 probes remain 33% after last round
c [basicprobe-3-0] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 15 variables, found 91470 hbrs
c [bate-1] eliminated 13 asymmetric tautologies during probing
c [unhide-8] limit 2307750 with penalty 0 = 0 + 0
c [unhide-8-10] 12 units, 29 failed, 16841 tauts, 0 hbrs, 28129 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 513 transitive binary clauses
c [transred-5] found 2 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 288468790 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 2 clauses out of 150 (1%) of length 10
c [cce-4-1] eliminated 1 clauses out of 166 (1%) of length 8
c [cce-4-1] eliminated 617 clauses out of 2387 (26%) of length 7
c [cce-4-1] eliminated 5415 clauses out of 14329 (38%) of length 6
c [cce-4-1] eliminated 2777 clauses out of 11644 (24%) of length 5
c [cce-4-1] eliminated 3122 clauses out of 13520 (23%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 11934 large clauses in 262674428 steps
c [cce-4-1] allowing another 131337214 steps for small clauses
c [cce-4-1] scheduling 157424 clauses = 38582 binary + 118842 ternary
c [cce-4-1] tried to eliminate 30556 small clauses 19%
c [cce-4-1] eliminated 1602 binary clauses 4%
c [cce-4-1] eliminated 4306 ternary clauses 4%
c [cce-4-1] eliminated 5908 small clauses 4%
c [cce-4-1] eliminated 5999 small clauses in 288468793 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 17933 covered clauses in round 1
c [cce-4] eliminated 17933 covered clauses in TOTAL during 1 rounds
c [elim-6] 1597 variables 4% will be scheduled this time
c [elim-6] scheduled 1597 variables 4%
c [elim-6] limit of 57693758 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 901 not tried 2% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 5 = 0% variables out of 1597 scheduled
c [elim-6] 5 < 1/100 * 1597 = 15 considered unsuccessful
c [bca-4] limit of 10000000 steps and 686315 added (scaled 2)
c [bca-4] 63160 out of 82416 literals actually usable 77%
c [bca-4] added 115 blocked clauses in 193761 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 34616250 penalty 0 = 0 + 0
c [sweep-5-1] 17734 pos 43.6% + 22899 neg 56.4% = 40633 sched 98.6% ret 574
c [sweep-5-1] 34667122 steps 305 queries 2013.83 avg class size
c [sweep-5-1] 6314 decisions 267 SAT calls 96.18 avg env size
c [sweep-5-1] 34446 variables remain 84% (6754 retained 16%)
c [decomp-20] removed 86 variables
c [sweep-5-1] removed 86 vars (0 failed, 44 eqs, 85 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 86 vars in TOTAL (1 rounds, 304 queries)
c [phase-count-9] 334480 negative 97.6% of 342608 except 8128 2.4%
c [phase-count-9] 238800 positive 69.7% of 342608 except 103808 30.3%
c [phase-count-9] less non-negative clauses 8128 than limit 34200 (10.0%)
c [phase-count-9] non-pos/non-neg = 103808/8128 = 12.77 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 2650 negative 100%
c [sort-queue-9] sorted 20993 enqueued variables after 64357 conflicts
c [score-dist-9] active 20128 (49%), one 0 (0%), zero 20993 (51%)
c [score-dist-9] max exp 517, different 11 (2%)
c [score-dist-9] median active exp 517, avg 516.1
c [simplification-9] removed 145 variables 0.4% (41121 remain 15%)
c [simplification-9] removed 21257 irredundant clauses 5.8% (342608 remain 24%)
c [simplification-9] maximum reduction of 6% = max (0%, 6%)
c [simplification-9] large reduction 6% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 76357 (soft 66357 + delta 10000)
c [simplification-9] new conflict limit 66357 (hard 76357)
c 
c [simplification-10] limit 66357 conflicts (hard 76357) hit after 66357 conflicts
c [quatres-6] found 20700 quaternary clauses 39% in total
c [quatres-6-1] removed 101 duplicate quaternary clauses
c [quatres-6-1] added 6 double-self-subsuming ternary resolvents
c [quatres-6-2] added 64 single-self-subsuming ternary resolvents
c [quatres-6-2] added 400 quaternary resolvents
c [ternres-6] limit 11990206 with penalty 0 = 0 + 0
c [ternres-6] 14333 schedulable variables 35%
c [ternres-6] 3866 ternary resolvents (30 bin, 3836 trn)
c [ternres-6] 9021 variables remain 22% (32100 retained 78%)
c [card-4] limit 749387 penalty 3 = 3 + 0
c [card-4] found 182 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 749387 for elimination
c [card-4] 182 out of 182 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 599510 penalty 2 = 2 + 0
c [gauss-3] extracted 58 xors of average arity 2.9
c [gauss-3] connected 171 occurrences of 80 variables (average 2.1)
c [gauss-3] limit 599510 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-9] limit 2398041 with penalty 0 = 0 + 0
c [unhide-9-12] 4 units, 41 failed, 9673 tauts, 0 hbrs, 13244 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 541 transitive binary clauses
c [cce-5] limit of 59951034 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 223 (0%) of length 9
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1 large clauses in 59951169 steps
c [cce-5-1] allowing another 29975584 steps for small clauses
c [cce-5-1] scheduling 151523 clauses = 37961 binary + 113562 ternary
c [cce-5-1] tried to eliminate 4741 small clauses 3%
c [cce-5-1] eliminated 235 binary clauses 1%
c [cce-5-1] eliminated 993 ternary clauses 1%
c [cce-5-1] eliminated 1228 small clauses 1%
c [cce-5-1] eliminated 1343 small clauses in 59951041 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1344 covered clauses in round 1
c [cce-5] eliminated 1344 covered clauses in TOTAL during 1 rounds
c [cce-5] 1344 < 1/100 * 341423 = 3414 considered unsuccessful
c [bca-5] limit of 10000000 steps and 680791 added (scaled 2)
c [bca-5] 62779 out of 82182 literals actually usable 76%
c [bca-5] added 117 blocked clauses in 194186 steps
c [sweep-6] limit 3597062 penalty 0 = 0 + 0
c [sweep-6-1] 15392 pos 44.8% + 18992 neg 55.2% = 34384 sched 83.7% ret 6706
c [sweep-6-1] 3732921 steps 61 queries 7743.18 avg class size
c [sweep-6-1] 728 decisions 48 SAT calls 59.77 avg env size
c [sweep-6-1] 34150 variables remain 83% (6939 retained 17%)
c [decomp-22] removed 27 variables
c [sweep-6-1] removed 27 vars (0 failed, 13 eqs, 29 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 27 vars in TOTAL (1 rounds, 60 queries)
c [phase-count-10] 331923 negative 97.6% of 340031 except 8108 2.4%
c [phase-count-10] 236676 positive 69.6% of 340031 except 103355 30.4%
c [phase-count-10] less non-negative clauses 8108 than limit 34000 (10.0%)
c [phase-count-10] non-pos/non-neg = 103355/8108 = 12.75 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 2519 negative 100%
c [sort-queue-10] sorted 20907 enqueued variables after 66357 conflicts
c [score-dist-10] active 20156 (49%), one 0 (0%), zero 20907 (51%)
c [score-dist-10] max exp 518, different 12 (2%)
c [score-dist-10] median active exp 517, avg 516.2
c [simplification-10] removed 58 variables 0.1% (41063 remain 15%)
c [simplification-10] removed 2577 irredundant clauses 0.8% (340031 remain 24%)
c [simplification-10] maximum reduction of 1% = max (0%, 1%)
c [simplification-10] geometric conflict interval increment 17333 = 34666 / 2
c [simplification-10] new conflict interval 51999
c [simplification-10] penalized conflict interval 51999 = 1 * 51999
c [simplification-10] hard conflict limit 144355 (soft 118356 + delta 25999)
c [simplification-10] new conflict limit 118356 (hard 144355)
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 -   63.1   41063   340031     77457   35942  35188 109434    8    18   47  46%    703    3    8    5  160%
c i   67.4   41062   340031     88422   46233  35345 109475    8    19   49  43%    752    3    7    6  124%
c i   76.2   40984   340030    107388   64211  35577 109559    9    20   52  43%   -225    2    5    6   86%
c i   80.2   40843   340030    119728   75656  35750 109613    7    13   55  51%   -260   -5    4    7   67%
c -   82.9   40843   340030    125487   47603  35816 109637    8    20   49  40%   -330    2    9    7  140%
c 
c [simplification-11] limit 118356 conflicts (hard 144355) hit after 143853 conflicts
c [quatres-7] found 17002 quaternary clauses 40% in total
c [quatres-7-1] removed 42 duplicate quaternary clauses
c [quatres-7-1] added 3 double-self-subsuming ternary resolvents
c [quatres-7-2] added 94 single-self-subsuming ternary resolvents
c [quatres-7-2] added 674 quaternary resolvents
c [ternres-7] limit 29650992 with penalty 0 = 0 + 0
c [ternres-7] 8959 schedulable variables 22%
c [ternres-7] 7370 ternary resolvents (73 bin, 7297 trn)
c [ternres-7] 942 variables remain 2% (39901 retained 98%)
c [decomp-23] removed 299 variables
c [simpleprobe-4] 32286 schedulable variables 79%
c [simpleprobe-4] limit 59301985 penalty 1 = 1 + 0
c [decomp-24] removed 35 variables
c [simpleprobe-4] 7392 variables remain 18% (33337 retained 82%)
c [simpleprobe-4] removed 35 variables, found 12081 hbrs, 9 units
c [unhide-10] limit 5930198 with penalty 0 = 0 + 0
c [unhide-10-16] 8 units, 60 failed, 29552 tauts, 0 hbrs, 136481 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 421 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 40615 variables 100%
c [block-4] limit of 74127481 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 430 blocked clauses
c [block-4] 430 < 1/100 * 324201 = 3242 considered unsuccessful
c [bca-6] limit of 10000000 steps and 647877 added (scaled 2)
c [bca-6] 64992 out of 81196 literals actually usable 80%
c [bca-6] added 324 blocked clauses in 183114 steps
c [sweep-7] limit 8895297 penalty 0 = 0 + 0
c [sweep-7-1] 13928 pos 41.3% + 19835 neg 58.7% = 33763 sched 83.2% ret 6834
c [sweep-7-1] 9985851 steps 161 queries 4521.42 avg class size
c [sweep-7-1] 1932 decisions 132 SAT calls 56.36 avg env size
c [sweep-7-1] 33039 variables remain 81% (7555 retained 19%)
c [decomp-25] removed 95 variables
c [sweep-7-1] removed 95 vars (0 failed, 43 eqs, 75 impls)
c [sweep-7] removed 95 vars in TOTAL (1 rounds, 160 queries)
c [phase-count-11] 315685 negative 97.6% of 323460 except 7775 2.4%
c [phase-count-11] 217915 positive 67.4% of 323460 except 105545 32.6%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 355 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 19279 enqueued variables after 143853 conflicts
c [score-dist-11] active 21223 (52%), one 0 (0%), zero 19279 (48%)
c [score-dist-11] max exp 519, different 13 (2%)
c [score-dist-11] median active exp 517, avg 517.0
c [simplification-11] removed 341 variables 0.8% (40502 remain 15%)
c [simplification-11] removed 16570 irredundant clauses 4.9% (323460 remain 23%)
c [simplification-11] maximum reduction of 5% = max (1%, 5%)
c [simplification-11] large reduction 5% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 155853 (soft 145853 + delta 10000)
c [simplification-11] new conflict limit 145853 (hard 155853)
c 
c [simplification-12] limit 145853 conflicts (hard 155853) hit after 145853 conflicts
c [quatres-8] found 19375 quaternary clauses 40% in total
c [quatres-8-1] removed 182 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 365 single-self-subsuming ternary resolvents
c [quatres-8-2] added 255 quaternary resolvents
c [ternres-8] limit 30149515 with penalty 0 = 0 + 0
c [ternres-8] 936 schedulable variables 2%
c [ternres-8] 7307 ternary resolvents (116 bin, 7191 trn)
c [ternres-8] 123 variables remain 0% (40379 retained 100%)
c [unhide-11] limit 6029903 with penalty 0 = 0 + 0
c [unhide-11-20] 2 units, 54 failed, 12579 tauts, 0 hbrs, 40905 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 467 transitive binary clauses
c [cce-6] limit of 75373789 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 2 clauses out of 204 (1%) of length 9
c [cce-6-1] eliminated 3 clauses out of 1012 (0%) of length 7
c [cce-6-1] eliminated 1 clauses out of 6009 (0%) of length 6
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 6 large clauses in 75373860 steps
c [cce-6-1] allowing another 37686930 steps for small clauses
c [cce-6-1] scheduling 198122 clauses = 43770 binary + 154352 ternary
c [cce-6-1] tried to eliminate 7721 small clauses 4%
c [cce-6-1] eliminated 290 binary clauses 1%
c [cce-6-1] eliminated 4317 ternary clauses 3%
c [cce-6-1] eliminated 4607 small clauses 2%
c [cce-6-1] eliminated 4780 small clauses in 75373887 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 4786 covered clauses in round 1
c [cce-6] eliminated 4786 covered clauses in TOTAL during 1 rounds
c [bca-7] limit of 10000000 steps and 633543 added (scaled 2)
c [bca-7] 64940 out of 80814 literals actually usable 80%
c [bca-7] added 285 blocked clauses in 184228 steps
c [sweep-8] limit 9044854 penalty 0 = 0 + 0
c [sweep-8-1] 15142 pos 46.0% + 17764 neg 54.0% = 32906 sched 81.4% ret 7500
c [sweep-8-1] 9281765 steps 121 queries 4336.90 avg class size
c [sweep-8-1] 1611 decisions 95 SAT calls 81.09 avg env size
c [sweep-8-1] 32436 variables remain 80% (7969 retained 20%)
c [decomp-27] removed 72 variables
c [sweep-8-1] removed 72 vars (0 failed, 29 eqs, 53 impls)
c [sweep-8] removed 72 vars in TOTAL (1 rounds, 120 queries)
c [phase-count-12] 308513 negative 97.6% of 316241 except 7728 2.4%
c [phase-count-12] 211422 positive 66.9% of 316241 except 104819 33.1%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 28 positive 82%, 6 negative 18%
c [sort-queue-12] sorted 19122 enqueued variables after 145853 conflicts
c [score-dist-12] active 21212 (53%), one 0 (0%), zero 19122 (47%)
c [score-dist-12] max exp 519, different 13 (2%)
c [score-dist-12] median active exp 517, avg 517.1
c [simplification-12] removed 168 variables 0.4% (40334 remain 15%)
c [simplification-12] removed 7219 irredundant clauses 2.2% (316241 remain 22%)
c [simplification-12] maximum reduction of 2% = max (0%, 2%)
c [simplification-12] geometric conflict interval increment 17333 = 51999 / 3
c [simplification-12] new conflict interval 69332
c [simplification-12] penalized conflict interval 69332 = 1 * 69332
c [simplification-12] hard conflict limit 249851 (soft 215185 + delta 34666)
c [simplification-12] new conflict limit 215185 (hard 249851)
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  103.5   40333   316241    153917   60011  50446 101817    8    21   50  39%    146    2    9    7  121%
c i  104.6   40300   316241    155942   61962  50467 101835    8    22   51  39%   -279    2    8    7  116%
c i  109.6   40299   316241    165876   71548  50568 101869    9    24   53  38%   -188    4    9    8  126%
c -  112.8   40299   316241    171824   42618  50633 101908    9    25   47  37%   -226    5   10    8  124%
c i  114.5   40298   316241    176422   47098  50657 101922    9    26   49  34%   -142    5    9    8  121%
c i  115.2   40297   316241    178445   49019  50663 101924    9    22   50  39%   -245    1    8    8  104%
c i  115.4   40294   316241    179139   49687  50666 101924    9    23   50  38%   -259    2   10    8  124%
c i  120.7   40292   316241    193907   63650  50734 101966    9    22   53  39%    -31    1    8    8  103%
c -  128.9   40292   316241    212276   48768  50818 102018   10    22   48  44%     50    1   10    8  126%
c 
c [simplification-13] limit 215185 conflicts (hard 249851) hit after 215186 conflicts
c [quatres-9] found 19182 quaternary clauses 37% in total
c [quatres-9-1] removed 107 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 123 single-self-subsuming ternary resolvents
c [quatres-9-2] added 154 quaternary resolvents
c [ternres-9] limit 44039424 with penalty 0 = 0 + 0
c [ternres-9] 122 schedulable variables 0%
c [ternres-9] 5912 ternary resolvents (71 bin, 5841 trn)
c [ternres-9] 2 variables remain 0% (40290 retained 100%)
c [decomp-28] removed 71 variables
c [unhide-12] limit 8807884 with penalty 0 = 0 + 0
c [unhide-12-26] 49 units, 184 failed, 19707 tauts, 0 hbrs, 113162 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 364 transitive binary clauses
c [cce-7] limit of 220197121 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 55 clauses out of 885 (6%) of length 7
c [cce-7-1] eliminated 120 clauses out of 5609 (2%) of length 6
c [cce-7-1] eliminated 313 clauses out of 8910 (4%) of length 5
c [cce-7-1] eliminated 521 clauses out of 8537 (6%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 1009 large clauses in 204220609 steps
c [cce-7-1] allowing another 102110304 steps for small clauses
c [cce-7-1] scheduling 190117 clauses = 47056 binary + 143061 ternary
c [cce-7-1] tried to eliminate 21945 small clauses 12%
c [cce-7-1] eliminated 1316 binary clauses 3%
c [cce-7-1] eliminated 13656 ternary clauses 10%
c [cce-7-1] eliminated 14972 small clauses 8%
c [cce-7-1] eliminated 15136 small clauses in 220197122 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 16145 covered clauses in round 1
c [cce-7] eliminated 16145 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 40069 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 311 not tried 1% in round 1
c [gc-84] reconnected 90010 binary clauses (produced 0 empty 25 units)
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 5725 = 14% variables out of 40069 scheduled
c [bca-8] limit of 10000000 steps and 543208 added (scaled 2)
c [bca-8] 57022 out of 68690 literals actually usable 83%
c [bca-8] added 322 blocked clauses in 152029 steps
c [sweep-9] limit 13211827 penalty 0 = 0 + 0
c [sweep-9-1] 13052 pos 47.4% + 14495 neg 52.6% = 27547 sched 80.2% ret 6797
c [sweep-9-1] 13245523 steps 218 queries 2655.07 avg class size
c [sweep-9-1] 2023 decisions 195 SAT calls 54.22 avg env size
c [sweep-9-1] 26124 variables remain 76% (8112 retained 24%)
c [decomp-29] removed 202 variables
c [sweep-9-1] removed 202 vars (0 failed, 27 eqs, 61 impls)
c [sweep-9] removed 202 vars in TOTAL (1 rounds, 217 queries)
c [phase-count-13] 263853 negative 97.8% of 269902 except 6049 2.2%
c [phase-count-13] 174823 positive 64.8% of 269902 except 95079 35.2%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 13 positive 22%, 46 negative 78%
c [sort-queue-13] sorted 15468 enqueued variables after 215186 conflicts
c [score-dist-13] active 18674 (55%), one 0 (0%), zero 15468 (45%)
c [score-dist-13] max exp 519, different 13 (2%)
c [score-dist-13] median active exp 519, avg 517.5
c [simplification-13] removed 6150 variables 15.3% (34142 remain 13%)
c [simplification-13] removed 46339 irredundant clauses 14.7% (269902 remain 19%)
c [simplification-13] maximum reduction of 15% = max (15%, 15%)
c [simplification-13] large reduction 15% >= 5% limit
c [simplification-13] next conflict interval 2151 = min (215186/100, 69332)
c [simplification-13] penalized conflict interval 2151 = 1 * 2151
c [simplification-13] hard conflict limit 227337 (soft 217337 + delta 10000)
c [simplification-13] new conflict limit 217337 (hard 227337)
c 
c [simplification-14] limit 217337 conflicts (hard 227337) hit after 217338 conflicts
c [quatres-10] found 13533 quaternary clauses 31% in total
c [quatres-10-1] removed 11 duplicate quaternary clauses
c [quatres-10-1] added 9 double-self-subsuming ternary resolvents
c [quatres-10-2] added 375 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1780 quaternary resolvents
c [ternres-10] limit 44242235 with penalty 0 = 0 + 0
c [ternres-10] 2 schedulable variables 0%
c [ternres-10] 4965 ternary resolvents (48 bin, 4917 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1106055 penalty 3 = 3 + 0
c [gauss-4] extracted 123 xors of average arity 3.0
c [gauss-4] connected 369 occurrences of 87 variables (average 4.2)
c [gauss-4] limit 1106055 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-30] removed 6 variables
c [treelook-4] limit 1106055 penalty 2 = 2 + 0 boost 1
c [treelook-4] scheduled 18989 literals 28%
c [treelook-4] scheduling used 983790 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1106055 penalty 2 = 2 + 0 boost 1
c [treelook-4] used 1147673 steps
c [treelook-4] 18924 literals remain 28%
c [treelook-4] 1783 variables remain to probed next time 5%
c [decomp-31] removed 7 variables
c [treelook-4] removed 13 variables, found 3762 hbrs
c [unhide-13] limit 8848447 with penalty 0 = 0 + 0
c [unhide-13-34] 11 units, 75 failed, 20848 tauts, 0 hbrs, 31686 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 443 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 2212111770 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 5 (20%) of length 12
c [cce-8-1] eliminated 7 clauses out of 33 (21%) of length 11
c [cce-8-1] eliminated 14 clauses out of 152 (9%) of length 10
c [cce-8-1] eliminated 21 clauses out of 172 (12%) of length 9
c [cce-8-1] eliminated 20 clauses out of 52 (38%) of length 8
c [cce-8-1] eliminated 51 clauses out of 828 (6%) of length 7
c [cce-8-1] eliminated 453 clauses out of 5052 (9%) of length 6
c [cce-8-1] eliminated 540 clauses out of 8460 (6%) of length 5
c [cce-8-1] eliminated 553 clauses out of 4812 (11%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 1660 large clauses in 196220365 steps
c [cce-8-1] allowing another 98110182 steps for small clauses
c [cce-8-1] scheduling 106824 clauses = 30566 binary + 76258 ternary
c [cce-8-1] tried to eliminate 106824 small clauses 100%
c [cce-8-1] eliminated 3648 binary clauses 12%
c [cce-8-1] eliminated 6398 ternary clauses 8%
c [cce-8-1] eliminated 10046 small clauses 9%
c [cce-8-1] eliminated 10053 small clauses in 700941121 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] completed small and large (ATE)
c [cce-8-1] eliminated 11713 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 53668465 steps for small clauses
c [cce-8-2] scheduling 96834 clauses = 26918 binary + 69916 ternary
c [cce-8-2] tried to eliminate 96834 small clauses 100%
c [cce-8-2] eliminated 33 ternary clauses 0%
c [cce-8-2] eliminated 33 small clauses 0%
c [cce-8-2] eliminated 33 small clauses in 393057757 steps
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 33 covered clauses in round 2
c [cce-8-3] completed large round (ATE)
c [cce-8-3] allowing another 53661873 steps for small clauses
c [cce-8-3] scheduling 96801 clauses = 26918 binary + 69883 ternary
c [cce-8-3] tried to eliminate 96801 small clauses 100%
c [cce-8-3] completed small round (ATE)
c [cce-8-3] eliminated 0 covered clauses in round 3
c [cce-8] eliminated 11746 covered clauses in TOTAL during 3 rounds
c [bca-9] limit of 10000000 steps and 459875 added (scaled 2)
c [bca-9] 49563 out of 61072 literals actually usable 81%
c [bca-9] added 122 blocked clauses in 135420 steps
c [sweep-10] limit 13272670 penalty 0 = 0 + 0
c [sweep-10-1] 12804 pos 55.5% + 10269 neg 44.5% = 23073 sched 75.6% ret 7462
c [sweep-10-1] 13287716 steps 203 queries 2776.46 avg class size
c [sweep-10-1] 1725 decisions 187 SAT calls 45.66 avg env size
c [sweep-10-1] 21771 variables remain 71% (8764 retained 29%)
c [decomp-32] removed 64 variables
c [sweep-10-1] removed 64 vars (0 failed, 23 eqs, 38 impls)
c [sweep-10] removed 64 vars in TOTAL (1 rounds, 202 queries)
c [phase-count-14] 223136 negative 97.3% of 229251 except 6115 2.7%
c [phase-count-14] 146319 positive 63.8% of 229251 except 82932 36.2%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 14258 enqueued variables after 217338 conflicts
c [score-dist-14] active 16213 (53%), one 0 (0%), zero 14258 (47%)
c [score-dist-14] max exp 519, different 13 (2%)
c [score-dist-14] median active exp 519, avg 517.7
c [simplification-14] removed 3671 variables 10.8% (30471 remain 11%)
c [simplification-14] removed 40651 irredundant clauses 15.1% (229251 remain 16%)
c [simplification-14] maximum reduction of 15% = max (11%, 15%)
c [simplification-14] large reduction 15% >= 5% limit
c [simplification-14] next conflict interval 2173 = min (217338/100, 69332)
c [simplification-14] penalized conflict interval 2173 = 1 * 2173
c [simplification-14] hard conflict limit 229511 (soft 219511 + delta 10000)
c [simplification-14] new conflict limit 219511 (hard 229511)
c 
c [simplification-15] limit 219511 conflicts (hard 229511) hit after 219511 conflicts
c [quatres-11] found 10662 quaternary clauses 29% in total
c [quatres-11-1] removed 1 duplicate quaternary clauses
c [quatres-11-1] added 4 double-self-subsuming ternary resolvents
c [quatres-11-2] added 86 single-self-subsuming ternary resolvents
c [quatres-11-2] added 188 quaternary resolvents
c [ternres-11] limit 44457746 with penalty 0 = 0 + 0
c [ternres-11] all 30471 free variables schedulable
c [ternres-11] 2547 ternary resolvents (34 bin, 2513 trn)
c [ternres-11] 3186 variables remain 10% (27285 retained 90%)
c [card-5] limit 1389304 penalty 4 = 4 + 0
c [card-5] found 259 at-most-one constraints of average size 3.5
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1389304 for elimination
c [card-5] 259 out of 259 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-33] removed 4 variables
c [basicprobe-4] limit 222288731 penalty 0 = 0 + 0
c [basicprobe-4-0] 7743 sched 26%, 134 failed, 8 lifted, 92538 hbrs
c [decomp-34] removed 720 variables
c [basicprobe-4-1] 1335 probes remain 5% after last round
c [basicprobe-4-1] 200 units = 191 failed (96%) + 9 lifted (4%)
c [basicprobe-4-1] removed 889 variables, found 97700 hbrs
c [bate-2] eliminated 33 asymmetric tautologies during probing
c [unhide-14] limit 8891549 with penalty 0 = 0 + 0
c [unhide-14-42] 3 units, 10 failed, 51572 tauts, 0 hbrs, 42234 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 760 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 29568 variables 100%
c [block-5] limit of 55572182 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 934 blocked clauses
c [block-5] 934 < 1/100 * 221375 = 2213 considered unsuccessful
c [cce-9] limit of 222288731 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 110 (1%) of length 10
c [cce-9-1] eliminated 6 clauses out of 4006 (0%) of length 6
c [cce-9-1] eliminated 139 clauses out of 7862 (2%) of length 5
c [cce-9-1] eliminated 191 clauses out of 3715 (5%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 337 large clauses in 171378956 steps
c [cce-9-1] allowing another 85689478 steps for small clauses
c [cce-9-1] scheduling 140357 clauses = 31259 binary + 109098 ternary
c [cce-9-1] tried to eliminate 21705 small clauses 15%
c [cce-9-1] eliminated 336 binary clauses 1%
c [cce-9-1] eliminated 12397 ternary clauses 11%
c [cce-9-1] eliminated 12733 small clauses 9%
c [cce-9-1] eliminated 12733 small clauses in 222288795 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 13070 covered clauses in round 1
c [cce-9] eliminated 13070 covered clauses in TOTAL during 1 rounds
c [elim-8] 310 variables 1% will be scheduled this time
c [elim-8] scheduled 310 variables 1%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 34314697 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 310 scheduled
c [bca-10] limit of 10000000 steps and 415844 added (scaled 2)
c [bca-10] 48192 out of 59100 literals actually usable 82%
c [bca-10] added 231 blocked clauses in 132735 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 133373230 penalty 0 = 0 + 0
c [sweep-11-1] 12700 pos 60.1% + 8437 neg 39.9% = 21137 sched 71.5% ret 8412
c [sweep-11-1] 133377187 steps 2086 queries 655.88 avg class size
c [sweep-11-1] 15261 decisions 1906 SAT calls 24.88 avg env size
c [sweep-11-1] 7611 variables remain 26% (21903 retained 74%)
c [decomp-35] removed 346 variables
c [sweep-11-1] removed 346 vars (0 failed, 215 eqs, 384 impls)
c [sweep-11] removed 346 vars in TOTAL (1 rounds, 2085 queries)
c [phase-count-15] 200931 negative 97.2% of 206774 except 5843 2.8%
c [phase-count-15] 125239 positive 60.6% of 206774 except 81535 39.4%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 13835 enqueued variables after 219511 conflicts
c [score-dist-15] active 15368 (53%), one 0 (0%), zero 13835 (47%)
c [score-dist-15] max exp 519, different 12 (2%)
c [score-dist-15] median active exp 519, avg 518.2
c [simplification-15] removed 1268 variables 4.2% (29203 remain 11%)
c [simplification-15] removed 22477 irredundant clauses 9.8% (206774 remain 14%)
c [simplification-15] maximum reduction of 10% = max (4%, 10%)
c [simplification-15] large reduction 10% >= 5% limit
c [simplification-15] next conflict interval 2195 = min (219511/100, 69332)
c [simplification-15] penalized conflict interval 2195 = 1 * 2195
c [simplification-15] hard conflict limit 231706 (soft 221706 + delta 10000)
c [simplification-15] new conflict limit 221706 (hard 231706)
c 
c [simplification-16] limit 221706 conflicts (hard 231706) hit after 221706 conflicts
c [quatres-12] found 9582 quaternary clauses 27% in total
c [quatres-12-1] removed 15 duplicate quaternary clauses
c [quatres-12-1] added 3 double-self-subsuming ternary resolvents
c [quatres-12-2] added 59 single-self-subsuming ternary resolvents
c [quatres-12-2] added 73 quaternary resolvents
c [ternres-12] limit 44791147 with penalty 0 = 0 + 0
c [ternres-12] 2929 schedulable variables 10%
c [ternres-12] 4723 ternary resolvents (55 bin, 4668 trn)
c [ternres-12] 210 variables remain 1% (28993 retained 99%)
c [decomp-36] removed 24 variables
c [simpleprobe-5] 3812 schedulable variables 13%
c [simpleprobe-5] limit 179164589 penalty 0 = 0 + 0
c [decomp-37] removed 294 variables
c [simpleprobe-5] 916 variables remain 3% (27969 retained 97%)
c [simpleprobe-5] removed 294 variables, found 43883 hbrs, 58 units
c [unhide-15] limit 8958229 with penalty 0 = 0 + 0
c [unhide-15-50] 1 units, 11 failed, 70589 tauts, 0 hbrs, 35144 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 625 transitive binary clauses
c [cce-10] limit of 223955736 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 2 clauses out of 780 (0%) of length 7
c [cce-10-1] eliminated 9 clauses out of 3720 (0%) of length 6
c [cce-10-1] eliminated 32 clauses out of 7807 (0%) of length 5
c [cce-10-1] eliminated 25 clauses out of 3430 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 68 large clauses in 148463377 steps
c [cce-10-1] allowing another 74231688 steps for small clauses
c [cce-10-1] scheduling 92809 clauses = 30684 binary + 62125 ternary
c [cce-10-1] tried to eliminate 25919 small clauses 28%
c [cce-10-1] eliminated 349 binary clauses 1%
c [cce-10-1] eliminated 145 ternary clauses 0%
c [cce-10-1] eliminated 494 small clauses 1%
c [cce-10-1] eliminated 500 small clauses in 223955736 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 568 covered clauses in round 1
c [cce-10] eliminated 568 covered clauses in TOTAL during 1 rounds
c [cce-10] 568 < 1/100 * 204434 = 2044 considered unsuccessful
c [bca-11] limit of 10000000 steps and 409065 added (scaled 2)
c [bca-11] 46733 out of 57756 literals actually usable 81%
c [bca-11] added 159 blocked clauses in 131739 steps
c [sweep-12] limit 13437344 penalty 0 = 0 + 0
c [sweep-12-1] 4928 pos 65.5% + 2596 neg 34.5% = 7524 sched 26.1% ret 21353
c [sweep-12-1] 13437753 steps 310 queries 2055.13 avg class size
c [sweep-12-1] 1868 decisions 292 SAT calls 19.78 avg env size
c [sweep-12-1] 6874 variables remain 24% (22003 retained 76%)
c [decomp-38] removed 48 variables
c [sweep-12-1] removed 48 vars (0 failed, 26 eqs, 46 impls)
c [sweep-12] removed 48 vars in TOTAL (1 rounds, 309 queries)
c [phase-count-16] 198028 negative 97.2% of 203766 except 5738 2.8%
c [phase-count-16] 122746 positive 60.2% of 203766 except 81020 39.8%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-16] sorted 13612 enqueued variables after 221706 conflicts
c [score-dist-16] active 15217 (53%), one 0 (0%), zero 13612 (47%)
c [score-dist-16] max exp 519, different 11 (2%)
c [score-dist-16] median active exp 519, avg 518.2
c [simplification-16] removed 374 variables 1.3% (28829 remain 11%)
c [simplification-16] removed 3008 irredundant clauses 1.5% (203766 remain 14%)
c [simplification-16] maximum reduction of 1% = max (1%, 1%)
c [simplification-16] geometric conflict interval increment 34666 = 69332 / 2
c [simplification-16] new conflict interval 103998
c [simplification-16] penalized conflict interval 103998 = 1 * 103998
c [simplification-16] hard conflict limit 377703 (soft 325704 + delta 51999)
c [simplification-16] new conflict limit 325704 (hard 377703)
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  195.3   28828   203766    231429   47460  66903 103402    7    12   42  54%    297   -9    5    8   67%
c -  204.2   28483   203763    263514   47350  67063 103437    9    21   41  42%    213    0    9    8  109%
c -  214.8   28483   203763    299565   51855  67091 103456    8    14   41  57%    556   -6    8    8   97%
c i  222.8   28482   203763    327593   78333  67158 103475    7    13   48  55%    719   -5    6    8   71%
c i  224.3   28479   203763    331369   81754  67190 103483    7    14   48  48%   -667   -4    5    8   63%
c i  224.3   25263   203763    331391   81767  67192 103486    6    14   48  48%   -668   -4    5    8   61%
c i  224.3   24289   203763    331392   81767  67192 103486    6    14   48  48%   -668   -4    5    8   61%
c i  224.3   24232   203763    331394   81767  67192 103487    6    14   48  48%   -668   -4    5    8   60%
c 0  224.3   21517   203763    331394   81767  67192 103487    6    14   48  48%   -668   -4    5    8   60%
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 UNSATISFIABLE
c
c bate: 46 basic ate = 38 trn 83% + 8 lrg 17% in 2 updates
c bcas: 11 count, 1826 added (7641 skipped), 1843284 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, 13627 removed, 6090190 resolutions, 17252999 steps
c blkd: 13215 blocking literals 2%, 37 pure
c bump: 332593 bumped seen, 21686111 lits 65.2 on average
c card: 5 count, 0 units, 0 am1, 53976753 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 17351 subsumed
c card: 5087 at-most-one constraints found, average size 3.77
c card: 5087 at-most-one constraints used 100%, average size 3.77
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 10 cces, 76236 eliminated, 69287 ate 91%, 6949 abce 9%
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: 5929702 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 125 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 38 decompositions, 65560 equivalent 21%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1001929 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 139077 eliminated 44%, 510 pure 0%
c elms: 8 rounds, 1.0 rounds/bve
c elms: 137004 small 99%, 1526 large 1%
c elms: 220769 tried small, 137004 succeeded 62%, 83765 failed 38%
c elms: 13587 subsumed, 34849 strengthened, 89 blocked
c elms: 5123590 copies, 5461474 resolutions, 4450077 ipos
c elms: 10691708 subchks, 3280716 strchks
c gaus: 4 extractions, 307 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 9422996 steps, 4711498 extr 50%, 5051 elim 0%
c glue: 7.9 orig avg, 7.9 real avg, 2.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 460359 = 59938 simple 13% + 400411 trn 87% + 10 lrg 0%, 18148 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 332593 clauses, 27.5 length
c lrnd: 9157755 lits = 14103503 orig - 4945748 removed 35%
c lrnd: 77889 uips 23%, 204962 flips 62%
c mins: 321726 mins 97%, 927 bin 0%, 9940 size 3%
c mins: 22138122 poisoned searches, 3856437 hits, 17% hit rate
c mins: 32016505 used twice searches, 1055339 hits, 3% hit rate
c move: moved 80769, 16652 bin 21%, 64117 trn 79%
c otfs: 1876 driving 29%, 4558 restarting 71%
c otfs: str 6434, 5735 red 89%, 699 irr 11%
c otfs: str 6434, 0 bin 0%, 284 trn 4%, 6150 lrg 96%
c otfs: sub 285, 165 red 58%, 120 irr 42%
c otfs: sub 285, 0 bin 0%, 53 trn 19%, 232 lrg 81%
c phas: 16 computed, 147964 set, 396 pos (0%), 147568 neg (100%)
c prbs: 4 basic, 37163 probed, 298 failed, 21 lifted
c prbs: 5 simple, 244924 probed, 202 failed, 20164 eqs
c prbs: 4 treelook, 149 probed, 6 failed, 0 lifted
c prom: 71805 locked 14% out of 506563 tried
c prps: 294986179 props, 282 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 12 count, 10923 quat, 1551 self1, 52 self2, 812 dup
c queu: 16 sorted, 1001929 next (52353 steps 0.05)
c queu: 22486456 enq (337140312 steps 14.99), 21686111 deq 96%
c redc: 22469 clauses 21%, 106164 tried 32%, 57 sat 0%
c redc: 35850 lits 3%, 1353140 tried 10%, 58 sat 0%
c redc: 543 times jump level reduced, 2.1 levels on average
c reds: 6 count, 55232.3 conflicts per reduce
c reds: 0 memlim 0%, 6 arith 100%
c reds: 157507 collected 79%, 42894 retired 21%
c rmbd: 84653 removed, 82288 red 97%
c rsts: 16527 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 16 count, 14 confs 88%, 0 vars 0%
c simp: 0 its 0%, 1 bin 6%, 1 trns 6%
c subl: 332593 count (160179 tried 0.5), 10252 sub out of 325677 (3.1%)
c swps: 12 count, 12 rounds, 3549 queries (295.8/round)
c swps: 3207 sat calls, 110 unsat (1.0% success rate)
c swps: 34183 decisions 10.7, 3075 conflicts 1.0
c swps; 1817.9 avg class size, 40.5 avg environment size
c swps: 0 failed, 788 impls, 429 equivs
c swp0: 1180 type 0 queries, 95 unsat (8.1%), 1162 sat (98.5%)
c swp1: 2369 type 1 queries, 1066 unsat (45.0%), 1958 sat (82.7%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 2669366 calls to obtain time
c tops: 89463 fixed 28%, 23 its, 14408.43 confs/it
c trds: 12 transitive reductions, 6288 removed, 5 failed
c trds: 104995 nodes, 81307 edges, 23947414 steps
c trim: 176206 words, 0.7 MB
c trnr: 12 count, 463 bin, 47356 trn, 300279286 steps
c unhd: 15 count, 50 rounds, 73694893 steps
c unhd: 2899 non-trivial sccs of average size 2.7
c unhd: 187 units, 180 bin, 4 trn, 3 lrg
c unhd: 682 failed, 592 stamp, 0 lits, 9 bin, 50 trn, 3 lrg
c unhd: 252384 tauts, 4211 bin 2%, 25577 trn 10%, 5892 lrg 2%
c unhd: 252384 tauts, 216704 stamp 86%, 222771 red 88%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 526718 str, 180 bin 0%, 31978 trn 6%, 494560 lrg 94%, 489552 red 93%
c vars: 21517 remaining 7% and 294100 removed 93% out of 315617
c vars: 89463 fixed 28%, 139077 eliminated 44%, 65560 equivalent 21%
c vsts: 6337811097 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 21.2 search visits per propagation, 18037.3 per conflict
c wchs: 560755825 pushed, 24818548 enlarged, 179 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         336600        157507         42894       8150697       2287038        154356
c 
c  0 0         62703  19      6948   4         0   0   6023731  74<  1268762  55     58402  38     1.2
c  1 5         35558  11     14748   9      4004   9    763567   9    296387  13<    22165  14<    0.8
c  2 6        112788  34<    61248  39<    14294  33    972795  12    487144  21     47342  31     2.9
c  3 9         97757  29     58398  37     16995  40<   340623   4    203882   9     22985  15     2.9
c  4 14        24982   7     14671   9      6556  15     45800   1     28559   1      3188   2     0.9
c  5 21         2635   1      1400   1       980   2      3921   0      2162   0       256   0     0.1
c  6 30          173   0        92   0        63   0       252   0       139   0        18   0     0.0
c  7 41            4   0         2   0         2   0         8   0         3   0         0   0     0.0
c 
c avg                  2.0           2.4           2.7           0.5           0.9           1.3
c std                  1.2           1.0           0.9           0.9           1.1           1.2
c 
c   47.843  21% cce
c   11.901   5% unhide
c   11.814   5% probe
c   10.166   5% elim
c    9.539   4% sweep
c    6.450   3% bump
c    2.807   1% ternres
c    2.328   1% transred
c    1.382   1% block
c    1.302   1% bca
c 
c    2.650 < 1% rest (below)
c 
c    1.195   1% quatres
c    0.614   0% decide
c    0.489   0% gauss
c    0.351   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    3.694   2% preprocessing     3%
c  103.658  46% inprocessing     97%
c ==================================
c  107.352  48% simplifying
c  116.968  52% search
c ==================================
c  224.325 100% all
c 
c        331394 conflicts,        1477.3 confs/sec
c          4861 ternaries,          68.2 confs/ternary
c          1201 binaries,          275.9 confs/binary
c            23 iterations,      14408.4 confs/iteration
c 
c             6 reductions,          0.0 redus/sec,  55232.3 confs/reduction
c         16527 restarts,           73.7 rests/sec,     20.1 confs/restart
c       1001929 decisions,        4466.4 decis/sec,      3.0 decis/conflict
c     294986179 propagations,  1314996.3 props/sec,    294.4 props/decision
c 
c 224.3 seconds, 140.5 MB
c launch: done
