c launch: /data/cnf/sc2014/app/AProVE09-06.cnf.bz2
c host: atom19
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/AProVE09-06.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/AProVE09-06.cnf.bz2
c no embedded options
c found 'p cnf 77262 263137' header
c read 77262 variables, 263137 clauses, 679549 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 77185 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   77185   262886         0       0      0     0    0     0   16   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] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 1104 variables
c [simpleprobe-1] all 76158 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 297 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 297 variables, found 12929 hbrs, 102 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 120 tauts, 0 hbrs, 13 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 75861 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 893 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 41942 = 55% variables out of 75861 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 189358 negative 99.1% of 191030 except 1672 0.9%
c [phase-count-1] 184954 positive 96.8% of 191030 except 6076 3.2%
c [phase-count-1] less non-negative clauses 1672 than limit 19100 (10.0%)
c [phase-count-1] non-pos/non-neg = 6076/1672 = 3.63 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 33919 negative 100%
c [sort-queue-1] sorted 33919 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 33919 (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 43266 variables 56.1% (33919 remain 44%)
c [simplification-1] removed 71856 irredundant clauses 27.3% (191030 remain 73%)
c [simplification-1] maximum reduction of 56% = max (56%, 27%)
c [simplification-1] large reduction 56% >= 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.4   33918   191030       234     193     25  2821    0     4   20   9%      0    4    4    0 17442%
c i    3.4   33825   191030       266     219     27  2822    0     4   20  10%      0    4    5    0 16889%
c i    3.4   33820   191030       280     229     28  2823    0     4   20  11%      0    4    5    0 16411%
c i    3.4   33818   191030       282     230     28  2823    0     4   20  11%      0    4    5    0 16326%
c i    3.4   33816   191030       285     231     28  2823    0     4   20  11%      0    4    5    0 16215%
c i    3.4   33814   191030       297     236     30  2825    0     4   20  11%      0    4    5    0 15732%
c i    3.4   33812   191030       299     237     30  2825    0     4   20  11%      0    4    5    0 15620%
c i    3.4   33810   191030       309     236     32  2827    0     4   20  11%      0    4    5    0 15287%
c i    3.5   33806   191030       615     486     68  2831    1     6   20  18%      1    6    9    0 11286%
c i    3.6   33795   191030       875     691     95  2837    2     7   20  23%      1    7    9    0 8266%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 158 variables
c [simpleprobe-2] all 33761 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 18 variables
c [simpleprobe-2] 20082 variables remain 60% (13661 retained 40%)
c [simpleprobe-2] removed 18 variables, found 714 hbrs, 10 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 25729 literals 38%
c [treelook-1] scheduling used 300006 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 313464 steps
c [treelook-1] 25454 literals remain 38%
c [treelook-1] 20662 variables remain to probed next time 61%
c [decomp-5] removed 3 variables
c [treelook-1] removed 5 variables, found 2060 hbrs
c [basicprobe-1] limit 1520720 based on 190090 irredundant clauses
c [basicprobe-1-0] 10803 probes remain 32% after last round
c [basicprobe-1-0] 34 units = 29 failed (85%) + 5 lifted (15%)
c [basicprobe-1-0] removed 41 variables, found 2140 hbrs
c [elim-2] 891 variables 3% will be scheduled this time
c [elim-2] scheduled 891 variables 3%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 1 variables 0% in round 1 in 2961227 steps
c [elim-2-1] backward subsumption/strengthening limit 2961200
c [elim-2-1-1] backward checking 726 touched variables 2%
c [elim-2-1-1] incomplete backward checking 734 remain 101%
c [elim-2-1] subsumed 2 and strengthened 47 clauses in 2961503 steps
c [elim-2-1] rescheduled 143 variables 0% by backward subsumption
c [elim-2-2] eliminated 9 variables 0% in round 2 in 119922 steps
c [elim-2-2] backward subsumption/strengthening limit 119900
c [elim-2-2-1] backward checking 801 touched variables 2%
c [elim-2-2-1] incomplete backward checking 797 remain 100%
c [elim-2-2] subsumed 0 and strengthened 0 clauses in 120114 steps
c [elim-2-2] fully rescheduled 33682 variables 100%
c [elim-2] incomplete 4390 not tried 13% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 777 = 87% variables out of 891 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 185335 negative 99.1% of 186950 except 1615 0.9%
c [phase-count-2] 180651 positive 96.6% of 186950 except 6299 3.4%
c [phase-count-2] less non-negative clauses 1615 than limit 18600 (10.0%)
c [phase-count-2] non-pos/non-neg = 6299/1615 = 3.90 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-2] sorted 29048 enqueued variables after 875 conflicts
c [score-dist-2] active 3872 (12%), one 0 (0%), zero 29048 (88%)
c [score-dist-2] max exp 510, different 10 (2%)
c [score-dist-2] median active exp 504, avg 504.1
c [simplification-2] removed 874 variables 2.6% (32920 remain 43%)
c [simplification-2] removed 4080 irredundant clauses 2.1% (186950 remain 71%)
c [simplification-2] maximum reduction of 3% = max (3%, 2%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1014 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c [simplification-3] limit 1014 conflicts (hard 11000) hit after 1015 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 307 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 307 out of 307 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 14 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 21523 literals 33%
c [treelook-2] scheduling used 300007 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 382194 steps
c [treelook-2] 21402 literals remain 33%
c [treelook-2] 13761 variables remain to probed next time 42%
c [treelook-2] removed 0 variables, found 3252 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 5 failed, 204 tauts, 0 hbrs, 1154 literals
c [elim-3] 4389 variables 13% will be scheduled this time
c [elim-3] scheduled 4389 variables 13%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 19 not tried 0% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 21 = 0% variables out of 4389 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 184742 negative 99.1% of 186350 except 1608 0.9%
c [phase-count-3] 179985 positive 96.6% of 186350 except 6365 3.4%
c [phase-count-3] less non-negative clauses 1608 than limit 18600 (10.0%)
c [phase-count-3] non-pos/non-neg = 6365/1608 = 3.96 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-3] sorted 28982 enqueued variables after 1015 conflicts
c [score-dist-3] active 3895 (12%), one 0 (0%), zero 28982 (88%)
c [score-dist-3] max exp 510, different 10 (2%)
c [score-dist-3] median active exp 504, avg 504.1
c [simplification-3] removed 43 variables 0.1% (32877 remain 43%)
c [simplification-3] removed 600 irredundant clauses 0.3% (186350 remain 71%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 20000
c [simplification-3] penalized conflict interval 20000 = 1 * 20000
c [simplification-3] hard conflict limit 31015 (soft 21015 + delta 10000)
c [simplification-3] new conflict limit 21015 (hard 31015)
c 
c [simplification-4] limit 21015 conflicts (hard 31015) hit after 21016 conflicts
c [basicprobe-2] limit 11651293 penalty 0 = 0 + 0
c [basicprobe-2-0] 13525 sched 41%, 1 failed, 0 lifted, 5848 hbrs
c [decomp-9] removed 2 variables
c [basicprobe-2-1] 21064 sched 64%, 0 failed, 0 lifted, 880 hbrs
c [decomp-10] removed 1 variables
c [basicprobe-2-2] 5420 probes remain 16% after last round
c [basicprobe-2-2] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-2-2] removed 3 variables, found 6923 hbrs
c [unhide-3] limit 466051 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 223 tauts, 0 hbrs, 9679 literals
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 32874 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 932103460 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 119 variables 0% in round 1 in 48006200 steps
c [elim-4-1] backward subsumption/strengthening limit 48006200
c [elim-4-1-1] backward checking 515 touched variables 2%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 5 and strengthened 19 clauses in 6281180 steps
c [elim-4-1] rescheduled 38 variables 0% by backward subsumption
c [elim-4-2] eliminated 2 variables 0% in round 2 in 3874377 steps
c [elim-4-2] backward subsumption/strengthening limit 3874300
c [elim-4-2-1] backward checking 15 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 356966 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 121 = 0% variables out of 32874 scheduled
c [elim-4] 121 < 1/100 * 32874 = 328 considered unsuccessful
c [sort-queue-4] sorted 18486 enqueued variables after 21016 conflicts
c [score-dist-4] active 14267 (44%), one 0 (0%), zero 18486 (56%)
c [score-dist-4] max exp 515, different 15 (3%)
c [score-dist-4] median active exp 507, avg 507.3
c [simplification-4] removed 124 variables 0.4% (32753 remain 42%)
c [simplification-4] removed 504 irredundant clauses 0.3% (185846 remain 71%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 40000
c [simplification-4] penalized conflict interval 40000 = 1 * 40000
c [simplification-4] hard conflict limit 81016 (soft 61016 + delta 20000)
c [simplification-4] new conflict limit 61016 (hard 81016)
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 -   55.1   32753   185846     58761   26825    843 12241   16    18   26  86%    594    8   16    8  194%
c 
c [simplification-5] limit 61016 conflicts (hard 81016) hit after 61018 conflicts
c [quatres-1] found 79284 quaternary clauses 94% in total
c [quatres-1-2] added 505 single-self-subsuming ternary resolvents
c [quatres-1-2] added 575 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 66489325 with penalty 0 = 0 + 0
c [ternres-1] all 32753 free variables schedulable
c [ternres-1] 23522 ternary resolvents (281 bin, 23241 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2659573 penalty 0 = 0 + 0
c [gauss-1] extracted 8536 xors of average arity 3.0
c [gauss-1] connected 25608 occurrences of 3479 variables (average 7.4)
c [gauss-1] limit 2659573 penalty 0 = 0 + 0
c [gauss-1] connected 5308 occurrences of 3479 variables (average 1.5)
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 19500 schedulable variables 60%
c [simpleprobe-3] limit 53191463 penalty 0 = 0 + 0
c [decomp-12] removed 1 variables
c [simpleprobe-3] 318 variables remain 1% (32434 retained 99%)
c [simpleprobe-3] removed 1 variables, found 8688 hbrs, 1 units
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 824 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 32752 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 1329786590 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 3593 blocked clauses
c [cce-1] limit of 66489329 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 5 clauses out of 185 (3%) of length 7
c [cce-1-1] eliminated 3 clauses out of 243 (1%) of length 6
c [cce-1-1] eliminated 31 clauses out of 1434 (2%) of length 5
c [cce-1-1] eliminated 2534 clauses out of 77893 (3%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 2573 large clauses in 38470629 steps
c [cce-1-1] allowing another 19235314 steps for small clauses
c [cce-1-1] scheduling 81227 clauses = 25786 binary + 55441 ternary
c [cce-1-1] tried to eliminate 59061 small clauses 73%
c [cce-1-1] eliminated 279 binary clauses 1%
c [cce-1-1] eliminated 1178 ternary clauses 2%
c [cce-1-1] eliminated 1457 small clauses 2%
c [cce-1-1] eliminated 1457 small clauses in 66489331 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 4030 covered clauses in round 1
c [cce-1] eliminated 4030 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 356922 added (scaled 2)
c [bca-1] 54492 out of 65506 literals actually usable 83%
c [bca-1] added 442 blocked clauses in 174275 steps
c [sweep-1] limit 3989359 penalty 0 = 0 + 0
c [sweep-1-1] 1698 pos 5.2% + 31054 neg 94.8% = 32752 sched 100.0% ret 0
c [sweep-1-1] 4069247 steps 158 queries 2036.37 avg class size
c [sweep-1-1] 2227 decisions 157 SAT calls 50.59 avg env size
c [sweep-1-1] 28586 variables remain 87% (4166 retained 13%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 157 queries)
c [sort-queue-5] sorted 14258 enqueued variables after 61018 conflicts
c [score-dist-5] active 18494 (56%), one 0 (0%), zero 14258 (44%)
c [score-dist-5] max exp 517, different 17 (3%)
c [score-dist-5] median active exp 509, avg 508.4
c [simplification-5] removed 1 variables 0.0% (32752 remain 42%)
c [simplification-5] removed 7635 irredundant clauses 4.1% (178211 remain 68%)
c [simplification-5] maximum reduction of 4% = max (0%, 4%)
c [simplification-5] geometric conflict interval increment 8000 = 40000 / 5
c [simplification-5] new conflict interval 48000
c [simplification-5] penalized conflict interval 48000 = 1 * 48000
c [simplification-5] hard conflict limit 133018 (soft 109018 + delta 24000)
c [simplification-5] new conflict limit 109018 (hard 133018)
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 -   91.6   32752   178211     87458   28600  27987 21889   18    28   29  66%    746   14   19   11  175%
c 
c [simplification-6] limit 109018 conflicts (hard 133018) hit after 109019 conflicts
c [quatres-2] found 76298 quaternary clauses 93% in total
c [quatres-2-1] added 4 double-self-subsuming ternary resolvents
c [quatres-2-2] added 183 single-self-subsuming ternary resolvents
c [quatres-2-2] added 136 quaternary resolvents
c [ternres-2] limit 31960348 with penalty 0 = 0 + 0
c [ternres-2] all 32752 free variables schedulable
c [ternres-2] 1584 ternary resolvents (80 bin, 1504 trn)
c [ternres-2] 25 variables remain 0% (32727 retained 100%)
c [card-3] limit 3995043 penalty 2 = 2 + 0
c [card-3] found 371 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 3995043 for elimination
c [card-3] 371 out of 371 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] generated 100 at-most-one constraints, 41 used 41%
c [card-3] exported 134 binary clauses, 3.3 per/constraint
c [unhide-4] limit 3196034 with penalty 1 = 1 + 0
c [unhide-4-6] 0 units, 0 failed, 7911 tauts, 0 hbrs, 113715 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 548 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 32752 variables 100%
c [block-2] limit of 319603484 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 21 blocked clauses
c [block-2] 21 < 1/100 * 177805 = 1778 considered unsuccessful
c [cce-2] limit of 159801742 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 383 clauses out of 73263 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 383 large clauses in 34741239 steps
c [cce-2-1] allowing another 17370619 steps for small clauses
c [cce-2-1] scheduling 80130 clauses = 26462 binary + 53668 ternary
c [cce-2-1] tried to eliminate 80130 small clauses 100%
c [cce-2-1] eliminated 411 binary clauses 2%
c [cce-2-1] eliminated 342 ternary clauses 1%
c [cce-2-1] eliminated 753 small clauses 1%
c [cce-2-1] eliminated 753 small clauses in 82983481 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] completed small and large (ATE)
c [cce-2-1] eliminated 1136 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 16802757 steps for small clauses
c [cce-2-2] scheduling 79377 clauses = 26051 binary + 53326 ternary
c [cce-2-2] tried to eliminate 75112 small clauses 95%
c [cce-2-2] incomplete small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 1136 covered clauses in TOTAL during 2 rounds
c [cce-2] 1136 < 1/100 * 177784 = 1777 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 32752 variables 100%
c [elim-5] limit of 319603484 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 2354 variables 7% in round 1 in 50984823 steps
c [elim-5-1] backward subsumption/strengthening limit 50984800
c [elim-5-1-1] backward checking 6622 touched variables 20%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 1 and strengthened 190 clauses in 18590014 steps
c [elim-5-1] rescheduled 441 variables 1% by backward subsumption
c [elim-5-2] eliminated 185 variables 1% in round 2 in 29418598 steps
c [elim-5-2] backward subsumption/strengthening limit 29418500
c [elim-5-2-1] backward checking 845 touched variables 3%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 1 and strengthened 1 clauses in 5505804 steps
c [elim-5-2] rescheduled 8 variables 0% by backward subsumption
c [elim-5-3] no variable eliminated in round 3 in 920621 steps
c [elim-5] fully completed in 3 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 2539 = 8% variables out of 32752 scheduled
c [bca-2] limit of 10000000 steps and 347923 added (scaled 2)
c [bca-2] 49232 out of 60428 literals actually usable 81%
c [bca-2] added 311 blocked clauses in 159667 steps
c [sweep-2] limit 9588104 penalty 0 = 0 + 0
c [sweep-2-1] 937 pos 3.5% + 25464 neg 96.5% = 26401 sched 87.4% ret 3812
c [sweep-2-1] 9763538 steps 680 queries 645.06 avg class size
c [sweep-2-1] 7027 decisions 679 SAT calls 28.21 avg env size
c [sweep-2-1] 16638 variables remain 55% (13575 retained 45%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 679 queries)
c [sort-queue-6] sorted 7481 enqueued variables after 109019 conflicts
c [score-dist-6] active 22732 (75%), one 0 (0%), zero 7481 (25%)
c [score-dist-6] max exp 518, different 18 (3%)
c [score-dist-6] median active exp 509, avg 508.8
c [simplification-6] removed 2539 variables 7.8% (30213 remain 39%)
c [simplification-6] removed 4610 irredundant clauses 2.6% (173601 remain 66%)
c [simplification-6] maximum reduction of 8% = max (8%, 3%)
c [simplification-6] large reduction 8% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 121019 (soft 111019 + delta 10000)
c [simplification-6] new conflict limit 111019 (hard 121019)
c 
c [simplification-7] limit 111019 conflicts (hard 121019) hit after 111019 conflicts
c [quatres-3] found 74316 quaternary clauses 92% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 56 single-self-subsuming ternary resolvents
c [quatres-3-2] added 181 quaternary resolvents
c [ternres-3] limit 32836217 with penalty 0 = 0 + 0
c [ternres-3] 25 schedulable variables 0%
c [ternres-3] 6408 ternary resolvents (251 bin, 6157 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 3283621 penalty 1 = 1 + 0
c [gauss-2] extracted 4786 xors of average arity 3.0
c [gauss-2] connected 14358 occurrences of 1820 variables (average 7.9)
c [gauss-2] limit 3283621 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 1641810 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 34095 literals 56%
c [treelook-3] scheduling used 757853 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1641810 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 1655559 steps
c [treelook-3] 34065 literals remain 56%
c [treelook-3] 12443 variables remain to probed next time 41%
c [treelook-3] removed 0 variables, found 18362 hbrs
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 467 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 30213 variables 100%
c [elim-6] limit of 656724359 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 85 variables 0% in round 1 in 49221947 steps
c [elim-6-1] backward subsumption/strengthening limit 49221900
c [elim-6-1-1] backward checking 544 touched variables 2%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 4 clauses in 3907799 steps
c [elim-6-1] rescheduled 11 variables 0% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 1836878 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 85 = 0% variables out of 30213 scheduled
c [elim-6] 85 < 1/100 * 30213 = 302 considered unsuccessful
c [bca-3] limit of 10000000 steps and 347104 added (scaled 2)
c [bca-3] 49017 out of 60258 literals actually usable 81%
c [bca-3] added 88 blocked clauses in 154571 steps
c [sweep-3] limit 9850865 penalty 0 = 0 + 0
c [sweep-3-1] 494 pos 3.0% + 16083 neg 97.0% = 16577 sched 55.0% ret 13551
c [sweep-3-1] 9905438 steps 642 queries 534.35 avg class size
c [sweep-3-1] 6658 decisions 641 SAT calls 23.03 avg env size
c [sweep-3-1] 9806 variables remain 33% (20322 retained 67%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 641 queries)
c [sort-queue-7] sorted 7392 enqueued variables after 111019 conflicts
c [score-dist-7] active 22736 (75%), one 0 (0%), zero 7392 (25%)
c [score-dist-7] max exp 518, different 18 (3%)
c [score-dist-7] median active exp 509, avg 508.8
c [simplification-7] removed 85 variables 0.3% (30128 remain 39%)
c [simplification-7] removed 487 irredundant clauses 0.3% (173114 remain 66%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 48000
c [simplification-7] new conflict interval 96000
c [simplification-7] penalized conflict interval 96000 = 1 * 96000
c [simplification-7] hard conflict limit 255019 (soft 207019 + delta 48000)
c [simplification-7] new conflict limit 207019 (hard 255019)
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 -  189.4   30128   173114    144216   29214  23853 36210   14    16   29  90%    907   -0   14   13  109%
c -  228.5   30128   173114    174119   28423  23881 36211   13    14   27  92%    950   -1   12   13   96%
c -  271.3   30128   173114    206106   30408  23927 36213   13    14   28  93%    979   -1   13   13  103%
c 
c [simplification-8] limit 207019 conflicts (hard 255019) hit after 212779 conflicts
c [quatres-4] found 74482 quaternary clauses 91% in total
c [quatres-4-1] added 10 double-self-subsuming ternary resolvents
c [quatres-4-2] added 181 single-self-subsuming ternary resolvents
c [quatres-4-2] added 131 quaternary resolvents
c [ternres-4] limit 71331222 with penalty 0 = 0 + 0
c [ternres-4] all 30128 free variables schedulable
c [ternres-4] 6056 ternary resolvents (115 bin, 5941 trn)
c [ternres-4] fully completed ternary resolution
c [basicprobe-3] limit 356656113 penalty 0 = 0 + 0
c [basicprobe-3-0] 7450 sched 25%, 1 failed, 0 lifted, 2710 hbrs
c [decomp-20] removed 1 variables
c [basicprobe-3-1] 19924 sched 66%, 1 failed, 0 lifted, 4157 hbrs
c [decomp-21] removed 1 variables
c [basicprobe-3-2] 19767 sched 66%, 0 failed, 0 lifted, 217 hbrs
c [basicprobe-3-3] 19766 sched 66%, 0 failed, 0 lifted, 46 hbrs
c [basicprobe-3-4] 19766 sched 66%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-4] fully completed probing
c [basicprobe-3-4] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 2 variables, found 7130 hbrs
c [bate-1] eliminated 10 asymmetric tautologies during probing
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 250 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 30126 variables 100%
c [block-3] limit of 356656113 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 4 blocked clauses
c [block-3] 4 < 1/100 * 173091 = 1730 considered unsuccessful
c [cce-3] limit of 178328056 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 2 clauses out of 33 (6%) of length 13
c [cce-3-1] eliminated 6 clauses out of 88 (7%) of length 12
c [cce-3-1] eliminated 2 clauses out of 102 (2%) of length 11
c [cce-3-1] eliminated 2 clauses out of 105 (2%) of length 10
c [cce-3-1] eliminated 4 clauses out of 72 (6%) of length 9
c [cce-3-1] eliminated 3 clauses out of 129 (2%) of length 8
c [cce-3-1] eliminated 28 clauses out of 214 (13%) of length 7
c [cce-3-1] eliminated 23 clauses out of 289 (8%) of length 6
c [cce-3-1] eliminated 251 clauses out of 2852 (9%) of length 5
c [cce-3-1] eliminated 659 clauses out of 73389 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 980 large clauses in 43866126 steps
c [cce-3-1] allowing another 21933063 steps for small clauses
c [cce-3-1] scheduling 42672 clauses = 22115 binary + 20557 ternary
c [cce-3-1] tried to eliminate 42672 small clauses 100%
c [cce-3-1] eliminated 89 binary clauses 0%
c [cce-3-1] eliminated 806 ternary clauses 4%
c [cce-3-1] eliminated 895 small clauses 2%
c [cce-3-1] eliminated 895 small clauses in 73076551 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] completed small and large (ACCE)
c [cce-3-1] eliminated 1875 covered clauses in round 1
c [cce-3-2] eliminated 4 clauses out of 31 (13%) of length 13
c [cce-3-2] eliminated 10 clauses out of 100 (10%) of length 11
c [cce-3-2] eliminated 2 clauses out of 103 (2%) of length 10
c [cce-3-2] eliminated 3 clauses out of 186 (2%) of length 7
c [cce-3-2] eliminated 10 clauses out of 266 (4%) of length 6
c [cce-3-2] eliminated 5 clauses out of 2601 (0%) of length 5
c [cce-3-2] eliminated 567 clauses out of 72730 (1%) of length 4
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] eliminated 601 large clauses in 42065715 steps
c [cce-3-2] allowing another 21032857 steps for small clauses
c [cce-3-2] scheduling 41777 clauses = 22026 binary + 19751 ternary
c [cce-3-2] tried to eliminate 41777 small clauses 100%
c [cce-3-2] eliminated 5 binary clauses 0%
c [cce-3-2] eliminated 16 ternary clauses 0%
c [cce-3-2] eliminated 21 small clauses 0%
c [cce-3-2] eliminated 21 small clauses in 70967647 steps
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 622 covered clauses in round 2
c [cce-3-3] eliminated 7 clauses out of 72163 (0%) of length 4
c [cce-3-3] incomplete large round (ACCE)
c [cce-3-3] eliminated 7 large clauses in 34283907 steps
c [cce-3-3] allowing another 17141953 steps for small clauses
c [cce-3-3] scheduling 41756 clauses = 22021 binary + 19735 ternary
c [cce-3-3] tried to eliminate 12000 small clauses 29%
c [cce-3-3] incomplete small round (ACCE)
c [cce-3-3] eliminated 7 covered clauses in round 3
c [cce-3] eliminated 2504 covered clauses in TOTAL during 3 rounds
c [bca-4] limit of 10000000 steps and 342086 added (scaled 2)
c [bca-4] 48294 out of 60254 literals actually usable 80%
c [bca-4] added 24 blocked clauses in 164735 steps
c [sweep-4] limit 21399366 penalty 0 = 0 + 0
c [sweep-4-1] 379 pos 3.9% + 9427 neg 96.1% = 9806 sched 32.5% ret 20320
c [sweep-4-1] 12984617 steps 2062 queries 155.07 avg class size
c [sweep-4-1] 18225 decisions 2061 SAT calls 22.40 avg env size
c [sweep-4-1] fully completed sweeping round
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 3 impls)
c [sweep-4-2] 844 pos 2.8% + 29282 neg 97.2% = 30126 sched 100.0% ret 0
c [sweep-4-2] 8504449 steps 194 queries 432.52 avg class size
c [sweep-4-2] 3159 decisions 193 SAT calls 92.33 avg env size
c [sweep-4-2] 21129 variables remain 70% (8997 retained 30%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 2254 queries)
c [sort-queue-8] sorted 7025 enqueued variables after 212779 conflicts
c [score-dist-8] active 23101 (77%), one 0 (0%), zero 7025 (23%)
c [score-dist-8] max exp 519, different 19 (4%)
c [score-dist-8] median active exp 510, avg 509.5
c [simplification-8] removed 2 variables 0.0% (30126 remain 39%)
c [simplification-8] removed 2531 irredundant clauses 1.5% (170583 remain 65%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 48000 = 96000 / 2
c [simplification-8] new conflict interval 144000
c [simplification-8] penalized conflict interval 144000 = 1 * 144000
c [simplification-8] hard conflict limit 428779 (soft 356779 + delta 72000)
c [simplification-8] new conflict limit 356779 (hard 428779)
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 -  313.0   30126   170583    236389   30627  30529 43382   12    13   28  92%    995   -2   12   13   91%
c -  349.4   30126   170583    268097   31270  30565 43382   14    16   30  89%   1006    1   14   13  106%
c -  382.0   30126   170583    301071   32241  30588 43383   12    14   29  89%   1013   -1   11   13   84%
c -  424.4   30126   170583    334792   33346  30613 43383   12    13   29  92%   1018   -1   13   13   99%
c 
c [simplification-9] limit 356779 conflicts (hard 428779) hit after 356779 conflicts
c [quatres-5] found 73383 quaternary clauses 90% in total
c [quatres-5-2] added 130 single-self-subsuming ternary resolvents
c [quatres-5-2] added 79 quaternary resolvents
c [ternres-5] limit 121575911 with penalty 0 = 0 + 0
c [ternres-5] all 30126 free variables schedulable
c [ternres-5] 963 ternary resolvents (2 bin, 961 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-4] 254 schedulable variables 1%
c [simpleprobe-4] limit 200000000 penalty 0 = 0 + 0
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 0 variables, found 7703 hbrs, 0 units
c [unhide-5] limit 5000000 with penalty 2 = 2 + 0
c [unhide-5-10] 0 units, 0 failed, 4019 tauts, 0 hbrs, 101998 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 313 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 6078795560 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 71843 (0%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 1 large clauses in 38015933 steps
c [cce-4-1] allowing another 19007966 steps for small clauses
c [cce-4-1] scheduling 41909 clauses = 22060 binary + 19849 ternary
c [cce-4-1] tried to eliminate 41909 small clauses 100%
c [cce-4-1] eliminated 9 binary clauses 0%
c [cce-4-1] eliminated 3 ternary clauses 0%
c [cce-4-1] eliminated 12 small clauses 0%
c [cce-4-1] eliminated 12 small clauses in 68082979 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 13 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 18985715 steps for small clauses
c [cce-4-2] scheduling 41897 clauses = 22051 binary + 19846 ternary
c [cce-4-2] tried to eliminate 41897 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 13 covered clauses in TOTAL during 2 rounds
c [cce-4] 13 < 1/100 * 170581 = 1705 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 30126 variables 100%
c [elim-7] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 326 variables 1% in round 1 in 47748027 steps
c [elim-7-1] backward subsumption/strengthening limit 47748000
c [elim-7-1-1] backward checking 1472 touched variables 5%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 1 and strengthened 15 clauses in 4476069 steps
c [elim-7-1] rescheduled 44 variables 0% by backward subsumption
c [elim-7-2] eliminated 3 variables 0% in round 2 in 19693 steps
c [elim-7-2] backward subsumption/strengthening limit 19600
c [elim-7-2-1] backward checking 23 touched variables 0%
c [elim-7-2-1] incomplete backward checking 11 remain 48%
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 19755 steps
c [elim-7-2] fully rescheduled 29797 variables 99%
c [elim-7-3] eliminated 12 variables 0% in round 3 in 47697820 steps
c [elim-7-3] backward subsumption/strengthening limit 47697800
c [elim-7-3-1] backward checking 76 touched variables 0%
c [elim-7-3-1] fully completed backward checking in 1 rounds
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 1464501 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 341 = 1% variables out of 30126 scheduled
c [bca-5] limit of 10000000 steps and 340552 added (scaled 2)
c [bca-5] 46905 out of 59572 literals actually usable 79%
c [bca-5] added 326 blocked clauses in 162353 steps
c [sort-queue-9] sorted 5231 enqueued variables after 356779 conflicts
c [score-dist-9] active 24554 (82%), one 0 (0%), zero 5231 (18%)
c [score-dist-9] max exp 520, different 20 (4%)
c [score-dist-9] median active exp 510, avg 509.9
c [simplification-9] removed 341 variables 1.1% (29785 remain 39%)
c [simplification-9] removed 773 irredundant clauses 0.5% (169810 remain 65%)
c [simplification-9] maximum reduction of 1% = max (1%, 0%)
c [simplification-9] geometric conflict interval increment 72000 = 144000 / 2
c [simplification-9] new conflict interval 216000
c [simplification-9] penalized conflict interval 216000 = 1 * 216000
c [simplification-9] hard conflict limit 680779 (soft 572779 + delta 108000)
c [simplification-9] new conflict limit 572779 (hard 680779)
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 -  508.8   29785   169810    386629   33928  27994 46776   12    13   29  89%   1021   -1   11   13   89%
c -  551.0   29785   169810    420990   34282  28013 46776   12    13   29  92%   1022   -1   11   12   87%
c -  599.5   29785   169810    457236   35074  28037 46778   10    11   30  89%   1023   -2    9   12   78%
c -  683.9   29785   169810    505960   35776  28052 46780   11    11   29  95%   1024   -1    9   11   76%
c -  739.8   29785   169810    547185   37565  28104 46781   12    13   30  86%   1024    1   12   11  108%
c 
c [simplification-10] limit 572779 conflicts (hard 680779) hit after 572779 conflicts
c [quatres-6] found 73537 quaternary clauses 88% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 112 single-self-subsuming ternary resolvents
c [quatres-6-2] added 183 quaternary resolvents
c [ternres-6] limit 200000000 with penalty 0 = 0 + 0
c [ternres-6] all 29785 free variables schedulable
c [ternres-6] 2551 ternary resolvents (52 bin, 2499 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 12958904 penalty 3 = 3 + 0
c [card-4] found 175 at-most-one constraints of average size 3.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 12958904 for elimination
c [card-4] 175 out of 175 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] generated 11 at-most-one constraints, 4 used 36%
c [card-4] exported 14 binary clauses, 3.5 per/constraint
c [gauss-3] limit 10367123 penalty 2 = 2 + 0
c [gauss-3] extracted 63127 xors of average arity 3.9
c [gauss-3] connected 246373 occurrences of 24674 variables (average 10.0)
c [gauss-3] limit 10367123 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 422 transitive binary clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 29785 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1 variables 0% in round 1 in 47675003 steps
c [elim-8-1] backward subsumption/strengthening limit 47675000
c [elim-8-1-1] backward checking 11 touched variables 0%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 320022 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1 = 0% variables out of 29785 scheduled
c [elim-8] 1 < 1/100 * 29785 = 297 considered unsuccessful
c [bca-6] limit of 10000000 steps and 340709 added (scaled 2)
c [bca-6] 42919 out of 59570 literals actually usable 72%
c [bca-6] added 2 blocked clauses in 173060 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 311013700 penalty 1 = 1 + 0
c [sweep-5-1] 615 pos 2.9% + 20360 neg 97.1% = 20975 sched 70.4% ret 8809
c [sweep-5-1] 31244822 steps 2442 queries 80.16 avg class size
c [sweep-5-1] 27454 decisions 2441 SAT calls 35.78 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-5-2] 794 pos 2.7% + 28990 neg 97.3% = 29784 sched 100.0% ret 0
c [sweep-5-2] 37620871 steps 2478 queries 118.51 avg class size
c [sweep-5-2] 29521 decisions 2478 SAT calls 41.21 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-30] removed 2 variables
c [sweep-5-2] removed 2 vars (0 failed, 1 eqs, 5 impls)
c [sweep-5-3] 794 pos 2.7% + 28988 neg 97.3% = 29782 sched 100.0% ret 0
c [sweep-5-3] 40024928 steps 2500 queries 42.88 avg class size
c [sweep-5-3] 29859 decisions 2500 SAT calls 36.93 avg env size
c [sweep-5-3] fully completed sweeping round
c [decomp-31] removed 2 variables
c [sweep-5-3] removed 2 vars (0 failed, 1 eqs, 4 impls)
c [sweep-5] 4 < 1/1000 * 29784 = 29 considered unsuccessful
c [sweep-5] removed 4 vars in TOTAL (3 rounds, 7417 queries)
c [sort-queue-10] sorted 3811 enqueued variables after 572779 conflicts
c [score-dist-10] active 25969 (87%), one 0 (0%), zero 3811 (13%)
c [score-dist-10] max exp 520, different 20 (4%)
c [score-dist-10] median active exp 512, avg 511.0
c [simplification-10] removed 5 variables 0.0% (29780 remain 39%)
c [simplification-10] removed 23 irredundant clauses 0.0% (169787 remain 65%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 216000
c [simplification-10] new conflict interval 432000
c [simplification-10] penalized conflict interval 432000 = 1 * 432000
c [simplification-10] hard conflict limit 1220779 (soft 1004779 + delta 216000)
c [simplification-10] new conflict limit 1004779 (hard 1220779)
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 -  804.1   29780   169787    586137   38545  30884 47064   12    13   29  91%   1024    0   12   12  107%
c -  870.0   29780   169787    632545   38966  30911 47065   11    11   31  93%   1024   -1    9   11   82%
c -  923.2   29780   169787    674538   39360  31014 47067   20    34   31  59%   1024   16   21   13  166%
c -  954.1   29780   169787    713081   39378  31054 47071   18    22   31  83%   1024   -2   13   18   76%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 10 basic ate = 6 trn 60% + 4 lrg 40% in 1 updates
c bcas: 6 count, 1193 added (915 skipped), 988661 steps
c bkwd: tried 181080 clauses, 362092 lits, 2.00 lits/clause
c bkwd: checked 36270157 occs, 200.30 occs/clause, 100.17 occs/lit
c bkwd: subsumed 0 binary, 6 ternary, 4 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 275 large (0% self)
c blkd: 3 bces, 3618 removed, 2823227 resolutions, 7029906 steps
c blkd: 2501 blocking literals 2%, 0 pure
c bump: 751228 bumped seen, 322816501 lits 429.7 on average
c card: 4 count, 0 units, 148 am1, 42362070 steps
c card: 168 rescheduled, 527 eliminated, 76619 resolved, 4274 subsumed
c card: 853 at-most-one constraints found, average size 3.06
c card: 853 at-most-one constraints used 100%, average size 3.06
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: 4 cces, 7683 eliminated, 6383 ate 83%, 1300 abce 17%
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: 942686 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 55 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 31 decompositions, 1120 equivalent 1%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1182116 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 45729 eliminated 59%, 0 pure 0%
c elms: 19 rounds, 2.4 rounds/bve
c elms: 45026 small 98%, 703 large 2%
c elms: 264316 tried small, 45026 succeeded 17%, 219290 failed 83%
c elms: 2652 subsumed, 4444 strengthened, 1377 blocked
c elms: 9047670 copies, 11603358 resolutions, 17090061 ipos
c elms: 4520379 subchks, 4990623 strchks
c gaus: 3 extractions, 76449 extracted, 3.7 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 31304904 steps, 15652452 extr 50%, 13473607 elim 43%
c glue: 13.3 orig avg, 13.3 real avg, 3.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 72390 = 30034 simple 41% + 33412 trn 46% + 8944 lrg 12%, 995 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 751228 clauses, 97.4 length
c lrnd: 73181545 lits = 155931411 orig - 82749866 removed 53%
c lrnd: 134150 uips 18%, 562768 flips 75%
c mins: 749275 mins 100%, 85 bin 0%, 1868 size 0%
c mins: 373740929 poisoned searches, 38829701 hits, 10% hit rate
c mins: 488039066 used twice searches, 3209811 hits, 1% hit rate
c move: moved 5791, 1022 bin 18%, 4769 trn 82%
c otfs: 862 driving 21%, 3278 restarting 79%
c otfs: str 4140, 4080 red 99%, 60 irr 1%
c otfs: str 4140, 0 bin 0%, 36 trn 1%, 4104 lrg 99%
c otfs: sub 30, 30 red 100%, 0 irr 0%
c otfs: sub 30, 0 bin 0%, 1 trn 3%, 29 lrg 97%
c phas: 3 computed, 33921 set, 0 pos (0%), 33921 neg (100%)
c prbs: 3 basic, 288329 probed, 32 failed, 5 lifted
c prbs: 4 simple, 265399 probed, 113 failed, 138 eqs
c prbs: 3 treelook, 423 probed, 2 failed, 0 lifted
c prom: 89084 locked 4% out of 2195159 tried
c prps: 3185865391 props, 2683 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 6 count, 1285 quat, 1167 self1, 14 self2, 2 dup
c queu: 10 sorted, 1182116 next (102773 steps 0.09)
c queu: 323049396 enq (908166984 steps 2.81), 322816501 deq 100%
c redc: 2057 clauses 7%, 27985 tried 4%, 2 sat 0%
c redc: 2594 lits 1%, 350987 tried 0%, 2 sat 0%
c redc: 42 times jump level reduced, 2.6 levels on average
c reds: 18 count, 41572.0 conflicts per reduce
c reds: 0 memlim 0%, 18 arith 100%
c reds: 526549 collected 93%, 36918 retired 7%
c rmbd: 3621 removed, 3602 red 99%
c rsts: 11540 restarts 67%, 5753 skipped 33%
c rsts: 5753 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 10 count, 9 confs 90%, 0 vars 0%
c simp: 1 its 10%, 0 bin 0%, 0 trns 0%
c subl: 751228 count (962689 tried 1.3), 63873 sub out of 749113 (8.5%)
c swps: 5 count, 8 rounds, 11148 queries (1393.5/round)
c swps: 11150 sat calls, 4 unsat (0.3% success rate)
c swps: 124130 decisions 11.1, 3794 conflicts 0.3
c swps; 188.7 avg class size, 34.8 avg environment size
c swps: 0 failed, 21 impls, 2 equivs
c swp0: 3713 type 0 queries, 104 unsat (2.8%), 3713 sat (100.0%)
c swp1: 7435 type 1 queries, 255 unsat (3.4%), 7433 sat (100.0%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 3866886 calls to obtain time
c tops: 633 fixed 1%, 10 its, 74829.60 confs/it
c trds: 6 transitive reductions, 2824 removed, 0 failed
c trds: 176958 nodes, 129739 edges, 12005257 steps
c trim: 524951 words, 2.0 MB
c trnr: 6 count, 781 bin, 40303 trn, 286717370 steps
c unhd: 5 count, 10 rounds, 13556841 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 5 failed, 4 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 12477 tauts, 520 bin 4%, 6517 trn 52%, 104 lrg 1%
c unhd: 12477 tauts, 5336 stamp 43%, 11864 red 95%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 226559 str, 0 bin 0%, 2640 trn 1%, 223919 lrg 99%, 221782 red 98%
c vars: 29780 remaining 39% and 47482 removed 61% out of 77262
c vars: 633 fixed 1%, 45729 eliminated 59%, 1120 equivalent 1%
c vsts: 26541655725 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 8.3 search visits per propagation, 35248.2 per conflict
c wchs: 2108898903 pushed, 14111503 enlarged, 96 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         750398        526549         36918      46076800      16034701        295255
c 
c  0 0         14476   2       601   0         0   0  32461791  70   9384343  59     82369  28     0.5
c  1 5          7940   1      1218   0      1545   4   4139774   9<  1707595  11<    25579   9     0.3
c  2 6         60986   8     24102   5     10164  28   6149019  13   2858205  18     63129  21<    2.3
c  3 9        357394  48<   251209  48     17623  48<  2476598   5   1454604   9     80311  27    12.1
c  4 14       259589  35    206749  39<     5131  14    680927   1    512687   3     36674  12    18.5
c  5 21        41405   6     35022   7      1820   5    145839   0    102175   1      6280   2    20.4
c  6 30         8534   1      7598   1       619   2     22706   0     15004   0       896   0     6.9
c  7 41           64   0        45   0        14   0       122   0        76   0        13   0     0.0
c  8 54            8   0         5   0         2   0        18   0        11   0         4   0     0.0
c  9 69            0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 10 86            2   0         0   0         0   0         6   0         1   0         0   0     0.0
c 
c avg                  3.3           3.5           2.9           0.6           0.9           2.0
c std                  0.9           0.8           1.0           1.0           1.2           1.5
c 
c   73.205   7% bump
c   17.928   2% elim
c   10.322   1% cce
c   10.265   1% sweep
c    4.786   0% probe
c 
c   12.053 < 1% rest (below)
c 
c    3.884   0% unhide
c    2.511   0% ternres
c    1.357   0% gauss
c    1.008   0% decide
c    0.939   0% quatres
c    0.700   0% bca
c    0.620   0% block
c    0.554   0% transred
c    0.480   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    3.337   0% preprocessing     6%
c   52.967   5% inprocessing     94%
c ==================================
c   56.305   6% simplifying
c  943.599  94% search
c ==================================
c  999.908 100% all
c 
c        748296 conflicts,         748.4 confs/sec
c          1532 ternaries,         488.4 confs/ternary
c           116 binaries,         6450.8 confs/binary
c            10 iterations,      74829.6 confs/iteration
c 
c            18 reductions,          0.0 redus/sec,  41572.0 confs/reduction
c         11540 restarts,           11.5 rests/sec,     64.8 confs/restart
c       1182116 decisions,        1182.2 decis/sec,      1.6 decis/conflict
c    3185865391 propagations,  3186159.2 props/sec,   2695.1 props/decision
c 
c 999.9 seconds, 83.8 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
