c launch: /data/cnf/sc2014/app/smtlib-qfbv-aigs-lfsr_004_127_112-tseitin.cnf.bz2
c host: atom11
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 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-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/smtlib-qfbv-aigs-lfsr_004_127_112-tseitin.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/smtlib-qfbv-aigs-lfsr_004_127_112-tseitin.cnf.bz2
c no embedded options
c found 'p cnf 350506 878969' header
c read 350506 variables, 878969 clauses, 2050925 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 --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 --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 350504 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 [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  350504   878967         0       0      0     0    0     0   50   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 1817 variables
c [simpleprobe-1] all 348689 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] fully completed simple probing
c [unhide-1] limit 54651 based on 874428 irredundant clauses
c [unhide-1-1] 46 units, 4376 failed, 114 tauts, 0 hbrs, 77 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 348554 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 79897 not tried 23% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 268657 = 77% variables out of 348554 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 222917 negative 97.7% of 228229 except 5312 2.3%
c [phase-count-1] 152849 positive 67.0% of 228229 except 75380 33.0%
c [phase-count-1] less non-negative clauses 5312 than limit 22800 (10.0%)
c [phase-count-1] non-pos/non-neg = 75380/5312 = 14.19 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 79897 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 79897 zero 100.00%
c [score-distribution-1] 1 different 0.00% out of total 79897 variables
c [simplification-1] removed 268795 variables 77.1% (79897 remain 23%)
c [simplification-1] removed 650738 irredundant clauses 74.0% (228229 remain 26%)
c [simplification-1] maximum reduction of 77% = max (77%, 74%)
c [simplification-1] large reduction 77% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 2 variables
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 49448 literals 31%
c [treelook-1] scheduling used 300003 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 439398 steps
c [treelook-1] 49375 literals remain 31%
c [treelook-1] 41732 variables remain to probed next time 52%
c [decomp-4] removed 1 variables
c [treelook-1] removed 2 variables, found 218 hbrs
c [basicprobe-1] limit 1887834 penalty 0 = 0 + 0
c [basicprobe-1-0] 59404 probes remain 74% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1 variables, found 2291 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 19 units, 63 failed, 87 tauts, 0 hbrs, 53209 literals
c [elim-2] 79836 variables 100% will be scheduled this time
c [elim-2] scheduled 79836 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 19739 not tried 25% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 60097 = 75% variables out of 79836 scheduled
c [elim-2] considered successful since not run to completion yet
c [score-distribution-2] 15914 pos 80.62%, 0 min 0.00%, 3825 zero 19.38%
c [score-distribution-2] 1347 different 6.82% out of total 19739 variables
c [simplification-2] removed 60158 variables 75.3% (19739 remain 6%)
c [simplification-2] removed 126021 irredundant clauses 55.2% (102208 remain 12%)
c [simplification-2] maximum reduction of 75% = max (75%, 55%)
c [simplification-2] large reduction 75% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3001 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] no at-most-two constraint found
c [simpleprobe-2] all 19739 free variables schedulable
c [simpleprobe-2] limit 1114681 penalty 1 = 1 + 0
c [simpleprobe-2] 18495 variables remain 94% (1244 retained 6%)
c [simpleprobe-2] removed 0 variables, found 380 hbrs, 0 units
c [unhide-3] limit 111468 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 0 tauts, 0 hbrs, 5548 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 19739 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 936 not tried 5% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 16698 = 85% variables out of 19739 scheduled
c [elim-3] considered successful since not run to completion yet
c [score-distribution-3] 2802 pos 92.14%, 0 min 0.00%, 239 zero 7.86%
c [score-distribution-3] 998 different 32.82% out of total 3041 variables
c [simplification-3] removed 16698 variables 84.6% (3041 remain 1%)
c [simplification-3] removed 33901 irredundant clauses 33.2% (68307 remain 8%)
c [simplification-3] maximum reduction of 85% = max (85%, 33%)
c [simplification-3] large reduction 85% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15001 (soft 5001 + delta 10000)
c [simplification-3] new conflict limit 5001 (hard 15001)
c 
c [simplification-4] limit 5001 conflicts (hard 15001) hit after 5002 conflicts
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 4841 literals 80%
c [treelook-2] scheduling used 160216 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 316640 steps
c [treelook-2] 4825 literals remain 79%
c [treelook-2] 1834 variables remain to probed next time 60%
c [decomp-8] removed 15 variables
c [treelook-2] removed 16 variables, found 2161 hbrs
c [elim-4] 935 variables 31% will be scheduled this time
c [elim-4] scheduled 935 variables 31%
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] eliminated 523 variables 17% in round 1 in 12704747 steps
c [elim-4-1] backward subsumption/strengthening limit 12704700
c [elim-4-1-1] backward checking 1363 touched variables 45%
c [elim-4-1-1] incomplete backward checking 1361 remain 100%
c [elim-4-1] subsumed 21 and strengthened 146 clauses in 12705105 steps
c [elim-4-1] rescheduled 150 variables 5% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 321671 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 523 = 56% variables out of 935 scheduled
c [score-distribution-4] 2312 pos 92.41%, 97 min 3.88%, 93 zero 3.72%
c [score-distribution-4] 958 different 38.29% out of total 2502 variables
c [simplification-4] removed 539 variables 17.7% (2502 remain 1%)
c [simplification-4] removed 1580 irredundant clauses 2.3% (66727 remain 8%)
c [simplification-4] maximum reduction of 18% = max (18%, 2%)
c [simplification-4] large reduction 18% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 17002 (soft 7002 + delta 10000)
c [simplification-4] new conflict limit 7002 (hard 17002)
c 
c [simplification-5] limit 7002 conflicts (hard 17002) hit after 7002 conflicts
c [quatres-1] found 5764 quaternary clauses 50% in total
c [quatres-1-2] added 5046 single-self-subsuming ternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 2502 free variables schedulable
c [ternres-1] 30 ternary resolvents (0 bin, 30 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 2520 xors of average arity 3.0
c [gauss-1] connected 7560 occurrences of 563 variables (average 13.4)
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 [basicprobe-2] limit 3806824 penalty 0 = 0 + 0
c [basicprobe-2-0] 895 probes remain 36% after last round
c [basicprobe-2-0] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2 variables, found 13940 hbrs
c [bate-1] eliminated 234 asymmetric tautologies during probing
c [unhide-4] limit 76136 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 0 failed, 614 tauts, 0 hbrs, 5029 literals
c [transred-1] limit 761364 with penalty 0 = 0 + 0
c [transred-1] removed 2 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 2500 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 1944 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 8 clauses out of 8 (100%) of length 236
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 193
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 184
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 147
c [cce-1-1] eliminated 1 clauses out of 13 (8%) of length 104
c [cce-1-1] eliminated 1 clauses out of 13 (8%) of length 102
c [cce-1-1] eliminated 1 clauses out of 14 (7%) of length 99
c [cce-1-1] eliminated 1 clauses out of 15 (7%) of length 94
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 18 large clauses in 30001301 steps
c [cce-1-1] allowing another 15000650 steps for small clauses
c [cce-1-1] scheduling 51938 clauses = 47833 binary + 4105 ternary
c [cce-1-1] tried to eliminate 240 small clauses 0%
c [cce-1-1] eliminated 97 binary clauses 0%
c [cce-1-1] eliminated 97 small clauses 0%
c [cce-1-1] eliminated 97 small clauses in 30000147 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 115 covered clauses in round 1
c [cce-1] eliminated 115 covered clauses in TOTAL during 1 rounds
c [cce-1] 115 < 1/100 * 63531 = 635 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 2500 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] no variable eliminated in round 1 in 7397820 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 0 = 0% variables out of 2500 scheduled
c [bca-1] limit of 10000000 steps and 126994 added (scaled 2)
c [bca-1] 1931 out of 5002 literals actually usable 39%
c [bca-1] added 0 blocked clauses in 7133 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1033 pos 41.3% + 1467 neg 58.7% = 2500 sched 100.0% ret 0
c [sweep-1-1] 1041053 steps 66 queries 156.27 avg class size
c [sweep-1-1] 2854 decisions 65 SAT calls 130.72 avg env size
c [sweep-1-1] 1907 variables remain 77% (585 retained 23%)
c [decomp-10] removed 8 variables
c [sweep-1-1] removed 8 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 8 vars in TOTAL (1 rounds, 65 queries)
c [score-distribution-5] 2241 pos 89.93%, 216 min 8.67%, 35 zero 1.40%
c [score-distribution-5] 891 different 35.75% out of total 2492 variables
c [simplification-5] removed 10 variables 0.4% (2492 remain 1%)
c [simplification-5] removed 7526 irredundant clauses 11.3% (59201 remain 7%)
c [simplification-5] maximum reduction of 11% = max (0%, 11%)
c [simplification-5] large reduction 11% >= 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 19002 (soft 9002 + delta 10000)
c [simplification-5] new conflict limit 9002 (hard 19002)
c 
c [simplification-6] limit 9002 conflicts (hard 19002) hit after 9003 conflicts
c [quatres-2] found 1090 quaternary clauses 18% in total
c [quatres-2-2] added 133 single-self-subsuming ternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 2492 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 493 variables remain 20% (1999 retained 80%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] no at-most-one constraint found
c [card-3] no at-most-two constraint found
c [transred-2] limit 850419 with penalty 0 = 0 + 0
c [transred-2] removed 0 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 2492 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 0 blocked clauses
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 829 pos 43.5% + 1078 neg 56.5% = 1907 sched 76.5% ret 585
c [sweep-2-1] 1001474 steps 54 queries 93.52 avg class size
c [sweep-2-1] 1951 decisions 53 SAT calls 144.02 avg env size
c [sweep-2-1] 1366 variables remain 55% (1109 retained 45%)
c [decomp-12] removed 17 variables
c [sweep-2-1] removed 17 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 17 vars in TOTAL (1 rounds, 53 queries)
c [score-distribution-6] 2429 pos 98.14%, 37 min 1.49%, 9 zero 0.36%
c [score-distribution-6] 904 different 36.53% out of total 2475 variables
c [simplification-6] removed 17 variables 0.7% (2475 remain 1%)
c [simplification-6] removed 8626 irredundant clauses 14.6% (50575 remain 6%)
c [simplification-6] maximum reduction of 15% = max (1%, 15%)
c [simplification-6] large reduction 15% >= 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 21003 (soft 11003 + delta 10000)
c [simplification-6] new conflict limit 11003 (hard 21003)
c 
c [simplification-7] limit 11003 conflicts (hard 21003) hit after 11003 conflicts
c [quatres-3] found 875 quaternary clauses 16% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 2572 xors of average arity 3.0
c [gauss-2] connected 7716 occurrences of 696 variables (average 11.1)
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 [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7500400 steps for small clauses
c [cce-2-1] scheduling 41949 clauses = 39247 binary + 2702 ternary
c [cce-2-1] tried to eliminate 129 small clauses 0%
c [cce-2-1] eliminated 77 binary clauses 0%
c [cce-2-1] eliminated 77 small clauses 0%
c [cce-2-1] eliminated 77 small clauses in 15000071 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 77 covered clauses in round 1
c [cce-2] eliminated 77 covered clauses in TOTAL during 1 rounds
c [cce-2] 77 < 1/100 * 50575 = 505 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 2475 variables 100%
c [elim-6] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 4945446 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 2475 scheduled
c [bca-2] limit of 10000000 steps and 101496 added (scaled 2)
c [bca-2] 730 out of 4952 literals actually usable 15%
c [bca-2] added 0 blocked clauses in 7684 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 396 pos 29.0% + 970 neg 71.0% = 1366 sched 55.2% ret 1109
c [sweep-3-1] 1002794 steps 65 queries 65.57 avg class size
c [sweep-3-1] 2577 decisions 64 SAT calls 116.52 avg env size
c [sweep-3-1] 850 variables remain 34% (1615 retained 66%)
c [decomp-14] removed 11 variables
c [sweep-3-1] removed 11 vars (0 failed, 2 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 11 vars in TOTAL (1 rounds, 64 queries)
c [score-distribution-7] 2376 pos 96.43%, 86 min 3.49%, 2 zero 0.08%
c [score-distribution-7] 1076 different 43.67% out of total 2464 variables
c [simplification-7] removed 11 variables 0.4% (2464 remain 1%)
c [simplification-7] removed 5149 irredundant clauses 10.2% (45426 remain 5%)
c [simplification-7] maximum reduction of 10% = max (0%, 10%)
c [simplification-7] large reduction 10% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 23003 (soft 13003 + delta 10000)
c [simplification-7] new conflict limit 13003 (hard 23003)
c 
c [simplification-8] limit 13003 conflicts (hard 23003) hit after 13004 conflicts
c [quatres-4] found 902 quaternary clauses 17% in total
c [quatres-4-2] added 21 single-self-subsuming ternary resolvents
c [quatres-4-2] added 2 quaternary resolvents
c [ternres-3] limit 2000000 with penalty 1 = 1 + 0
c [ternres-3] 488 schedulable variables 20%
c [ternres-3] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-3] fully completed ternary resolution
c [simpleprobe-3] 2302 schedulable variables 93%
c [simpleprobe-3] limit 1001060 penalty 2 = 2 + 0
c [simpleprobe-3] 1696 variables remain 69% (768 retained 31%)
c [simpleprobe-3] removed 0 variables, found 2444 hbrs, 0 units
c [unhide-5] limit 50053 with penalty 2 = 2 + 0
c [unhide-5-5] 0 units, 0 failed, 0 tauts, 0 hbrs, 4858 literals
c [transred-3] limit 500530 with penalty 1 = 1 + 0
c [transred-3] removed 0 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 2464 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 286 pos 33.6% + 564 neg 66.4% = 850 sched 34.5% ret 1614
c [sweep-4-1] 1002064 steps 75 queries 33.39 avg class size
c [sweep-4-1] 3329 decisions 73 SAT calls 139.44 avg env size
c [sweep-4-1] 422 variables remain 17% (2017 retained 83%)
c [decomp-17] removed 25 variables
c [sweep-4-1] removed 25 vars (0 failed, 1 eqs, 2 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 25 vars in TOTAL (1 rounds, 74 queries)
c [score-distribution-8] 2379 pos 97.54%, 60 min 2.46%, 0 zero 0.00%
c [score-distribution-8] 1191 different 48.83% out of total 2439 variables
c [simplification-8] removed 25 variables 1.0% (2439 remain 1%)
c [simplification-8] removed 13184 irredundant clauses 29.0% (32242 remain 4%)
c [simplification-8] maximum reduction of 29% = max (1%, 29%)
c [simplification-8] large reduction 29% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 25004 (soft 15004 + delta 10000)
c [simplification-8] new conflict limit 15004 (hard 25004)
c 
c [simplification-9] limit 15004 conflicts (hard 25004) hit after 15005 conflicts
c [quatres-5] found 811 quaternary clauses 15% in total
c [quatres-5-2] added 3 single-self-subsuming ternary resolvents
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 3854 literals 79%
c [treelook-3] scheduling used 112111 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 324453 steps
c [treelook-3] 3840 literals remain 79%
c [treelook-3] 1553 variables remain to probed next time 64%
c [treelook-3] removed 1 variables, found 2055 hbrs
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 128 pos 30.3% + 294 neg 69.7% = 422 sched 17.3% ret 2016
c [sweep-5-1] 1700120 steps 221 queries 7.84 avg class size
c [sweep-5-1] 5057 decisions 204 SAT calls 73.41 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-20] removed 558 variables
c [sweep-5-1] removed 558 vars (0 failed, 19 eqs, 2 impls)
c [sweep-5-2] 741 pos 39.4% + 1139 neg 60.6% = 1880 sched 100.0% ret 0
c [sweep-5-2] 698850 steps 375 queries 26.25 avg class size
c [sweep-5-2] 7851 decisions 374 SAT calls 33.19 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-3] 741 pos 39.4% + 1139 neg 60.6% = 1880 sched 100.0% ret 0
c [sweep-5-3] 688204 steps 393 queries 22.74 avg class size
c [sweep-5-3] 7371 decisions 392 SAT calls 29.30 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 558 vars in TOTAL (3 rounds, 986 queries)
c [score-distribution-9] 1811 pos 96.33%, 69 min 3.67%, 0 zero 0.00%
c [score-distribution-9] 964 different 51.28% out of total 1880 variables
c [simplification-9] removed 559 variables 22.9% (1880 remain 1%)
c [simplification-9] removed 25383 irredundant clauses 78.7% (6859 remain 1%)
c [simplification-9] maximum reduction of 79% = max (23%, 79%)
c [simplification-9] large reduction 79% >= 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 27005 (soft 17005 + delta 10000)
c [simplification-9] new conflict limit 17005 (hard 27005)
c 
c [simplification-10] limit 17005 conflicts (hard 27005) hit after 17005 conflicts
c [quatres-6] found 539 quaternary clauses 12% in total
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] no at-most-one constraint found
c [card-4] no at-most-two constraint found
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 6594 xors of average arity 3.0
c [gauss-3] connected 19782 occurrences of 1044 variables (average 18.9)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] connected 2634 occurrences of 1044 variables (average 2.5)
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 5341782 penalty 0 = 0 + 0
c [basicprobe-3-0] 132 sched 7%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-1] 234 sched 12%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] removed 0 variables, found 1 hbrs
c [cce-3] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 4 clauses out of 396 (1%) of length 7
c [cce-3-1] eliminated 4 clauses out of 1808 (0%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 8 large clauses in 7500008 steps
c [cce-3-1] allowing another 3750004 steps for small clauses
c [cce-3-1] scheduling 2711 clauses = 504 binary + 2207 ternary
c [cce-3-1] tried to eliminate 2711 small clauses 100%
c [cce-3-1] eliminated 3 binary clauses 1%
c [cce-3-1] eliminated 3 small clauses 0%
c [cce-3-1] eliminated 3 small clauses in 5201983 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 11 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 1149009 steps for small clauses
c [cce-3-2] scheduling 2708 clauses = 501 binary + 2207 ternary
c [cce-3-2] tried to eliminate 2008 small clauses 74%
c [cce-3-2] incomplete small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 11 covered clauses in TOTAL during 2 rounds
c [cce-3] 11 < 1/100 * 6859 = 68 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 1880 variables 100%
c [elim-7] limit of 5341782 steps penalty 2 = 2 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 19 variables 1% in round 1 in 742477 steps
c [elim-7-1] backward subsumption/strengthening limit 742400
c [elim-7-1-1] backward checking 84 touched variables 4%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 13150 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 19 = 1% variables out of 1880 scheduled
c [bca-3] limit of 10000000 steps and 13960 added (scaled 2)
c [bca-3] 312 out of 3724 literals actually usable 8%
c [bca-3] added 4 blocked clauses in 11035 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 897 pos 48.2% + 964 neg 51.8% = 1861 sched 100.0% ret 0
c [sweep-6-1] 766485 steps 358 queries 20.65 avg class size
c [sweep-6-1] 7375 decisions 357 SAT calls 34.32 avg env size
c [sweep-6-1] fully completed sweeping round
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6-2] 897 pos 48.2% + 964 neg 51.8% = 1861 sched 100.0% ret 0
c [sweep-6-2] 233881 steps 84 queries 73.57 avg class size
c [sweep-6-2] 2056 decisions 83 SAT calls 42.78 avg env size
c [sweep-6-2] 1049 variables remain 56% (812 retained 44%)
c [sweep-6-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (2 rounds, 440 queries)
c [score-distribution-10] 1732 pos 93.07%, 129 min 6.93%, 0 zero 0.00%
c [score-distribution-10] 1025 different 55.08% out of total 1861 variables
c [simplification-10] removed 19 variables 1.0% (1861 remain 1%)
c [simplification-10] removed 129 irredundant clauses 1.9% (6730 remain 1%)
c [simplification-10] maximum reduction of 2% = max (1%, 2%)
c [simplification-10] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-10] new conflict interval 6666
c [simplification-10] penalized conflict interval 6666 = 1 * 6666
c [simplification-10] hard conflict limit 33671 (soft 23671 + delta 10000)
c [simplification-10] new conflict limit 23671 (hard 33671)
c 
c [simplification-11] limit 23671 conflicts (hard 33671) hit after 23672 conflicts
c [ternres-4] limit 1000000 with penalty 2 = 2 + 0
c [ternres-4] all 1861 free variables schedulable
c [ternres-4] 28 ternary resolvents (2 bin, 26 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-27] removed 1 variables
c [transred-4] limit 274390 with penalty 2 = 2 + 0
c [transred-4] removed 3 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 1860 variables 100%
c [block-4] limit of 12500000 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 1414 blocked clauses
c [score-distribution-11] 1057 pos 56.83%, 803 min 43.17%, 0 zero 0.00%
c [score-distribution-11] 562 different 30.22% out of total 1860 variables
c [simplification-11] removed 1 variables 0.1% (1860 remain 1%)
c [simplification-11] removed 1414 irredundant clauses 21.0% (5316 remain 1%)
c [simplification-11] maximum reduction of 21% = max (0%, 21%)
c [simplification-11] large reduction 21% >= 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 35672 (soft 25672 + delta 10000)
c [simplification-11] new conflict limit 25672 (hard 35672)
c 
c [simplification-12] limit 25672 conflicts (hard 35672) hit after 25673 conflicts
c [quatres-7] found 600 quaternary clauses 9% in total
c [quatres-7-2] added 2 quaternary resolvents
c [unhide-6] limit 27618 with penalty 3 = 3 + 0
c [unhide-6-6] 0 units, 0 failed, 6 tauts, 0 hbrs, 10901 literals
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 1860 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 220946990 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 426 variables 23% in round 1 in 1289431 steps
c [elim-8-1] backward subsumption/strengthening limit 1289400
c [elim-8-1-1] backward checking 749 touched variables 40%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 63934 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 426 = 23% variables out of 1860 scheduled
c [bca-4] limit of 10000000 steps and 10282 added (scaled 2)
c [bca-4] 1719 out of 2870 literals actually usable 60%
c [bca-4] added 102 blocked clauses in 5368 steps
c [sweep-7] limit 500000 penalty 1 = 1 + 0
c [sweep-7-1] 374 pos 45.8% + 443 neg 54.2% = 817 sched 57.0% ret 617
c [sweep-7-1] 160509 steps 366 queries 22.65 avg class size
c [sweep-7-1] 2495 decisions 363 SAT calls 11.11 avg env size
c [sweep-7-1] fully completed sweeping round
c [sweep-7-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7-2] 728 pos 50.8% + 706 neg 49.2% = 1434 sched 100.0% ret 0
c [sweep-7-2] 214553 steps 383 queries 36.93 avg class size
c [sweep-7-2] 3787 decisions 382 SAT calls 15.01 avg env size
c [sweep-7-2] fully completed sweeping round
c [sweep-7-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7-3] 728 pos 50.8% + 706 neg 49.2% = 1434 sched 100.0% ret 0
c [sweep-7-3] 125184 steps 196 queries 39.03 avg class size
c [sweep-7-3] 2514 decisions 195 SAT calls 20.69 avg env size
c [sweep-7-3] 444 variables remain 31% (990 retained 69%)
c [sweep-7-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] removed 0 vars in TOTAL (3 rounds, 942 queries)
c [score-distribution-12] 984 pos 68.62%, 450 min 31.38%, 0 zero 0.00%
c [score-distribution-12] 676 different 47.14% out of total 1434 variables
c [simplification-12] removed 426 variables 22.9% (1434 remain 0%)
c [simplification-12] removed 426 irredundant clauses 8.0% (4890 remain 1%)
c [simplification-12] maximum reduction of 23% = max (23%, 8%)
c [simplification-12] large reduction 23% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 37673 (soft 27673 + delta 10000)
c [simplification-12] new conflict limit 27673 (hard 37673)
c 
c [simplification-13] limit 27673 conflicts (hard 37673) hit after 27673 conflicts
c [quatres-8] found 764 quaternary clauses 25% in total
c [quatres-8-2] added 1 quaternary resolvents
c [ternres-5] limit 2000000 with penalty 1 = 1 + 0
c [ternres-5] all 1434 free variables schedulable
c [ternres-5] 43 ternary resolvents (8 bin, 35 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 553971 with penalty 1 = 1 + 0
c [transred-5] removed 3 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 1434 variables 100%
c [block-5] limit of 25000000 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 0 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 1434 variables 100%
c [elim-9] limit of 22158855 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 3 variables 0% in round 1 in 1682429 steps
c [elim-9-1] backward subsumption/strengthening limit 1682400
c [elim-9-1-1] backward checking 259 touched variables 18%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 31053 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 3 = 0% variables out of 1434 scheduled
c [elim-9] 3 < 1/100 * 1434 = 14 considered unsuccessful
c [bca-5] limit of 10000000 steps and 9825 added (scaled 2)
c [bca-5] 1706 out of 2864 literals actually usable 60%
c [bca-5] added 4 blocked clauses in 5582 steps
c [score-distribution-13] 983 pos 68.69%, 448 min 31.31%, 0 zero 0.00%
c [score-distribution-13] 632 different 44.16% out of total 1431 variables
c [simplification-13] removed 3 variables 0.2% (1431 remain 0%)
c [simplification-13] removed 253 irredundant clauses 5.2% (4636 remain 1%)
c [simplification-13] maximum reduction of 5% = max (0%, 5%)
c [simplification-13] large reduction 5% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 39673 (soft 29673 + delta 10000)
c [simplification-13] new conflict limit 29673 (hard 39673)
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   15.2    1430     4636     28671    1884    108   582    7    77   19   9%    352   35    4    8   46%
c 
c [simplification-14] limit 29673 conflicts (hard 39673) hit after 29674 conflicts
c [quatres-9] found 688 quaternary clauses 30% in total
c [quatres-9-2] added 4 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 1430 free variables schedulable
c [ternres-6] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] extracted 5490 xors of average arity 3.0
c [gauss-4] connected 16470 occurrences of 927 variables (average 17.8)
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] 988 schedulable variables 69%
c [simpleprobe-4] limit 555192 penalty 3 = 3 + 0
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 0 variables, found 5 hbrs, 0 units
c [transred-6] limit 1110384 with penalty 0 = 0 + 0
c [transred-6] removed 3 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 37500000 steps penalty 3 = 3 + 0
c [cce-4-1] completed large round (ATE)
c [cce-4-1] allowing another 182268 steps for small clauses
c [cce-4-1] scheduling 1403 clauses = 55 binary + 1348 ternary
c [cce-4-1] tried to eliminate 1403 small clauses 100%
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 0 covered clauses in round 1
c [cce-4] eliminated 0 covered clauses in TOTAL during 1 rounds
c [bca-6] limit of 10000000 steps and 9315 added (scaled 2)
c [bca-6] 1432 out of 2862 literals actually usable 50%
c [bca-6] added 2 blocked clauses in 4965 steps
c [score-distribution-14] 1190 pos 83.22%, 240 min 16.78%, 0 zero 0.00%
c [score-distribution-14] 456 different 31.89% out of total 1430 variables
c [simplification-14] removed 0 variables 0.0% (1430 remain 0%)
c [simplification-14] removed 256 irredundant clauses 5.5% (4380 remain 0%)
c [simplification-14] maximum reduction of 6% = max (0%, 6%)
c [simplification-14] geometric conflict interval increment 2857 = 20000 / 7
c [simplification-14] new conflict interval 9523
c [simplification-14] penalized conflict interval 9523 = 1 * 9523
c [simplification-14] hard conflict limit 49197 (soft 39197 + delta 10000)
c [simplification-14] new conflict limit 39197 (hard 49197)
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   15.3    1429     4380     31375    2318    120   584    7    89   19   8%    -25   46    4    8   52%
c i   15.4    1428     4380     33257    3551    164   601    6   137   19   4%    -56   92    4    8   49%
c i   15.4    1400     4380     33950    4016    192   608    6   129   19   4%    -65   83    3    8   42%
c i   15.4    1387     4380     33972    4023    197   611    6   129   19   4%    -65   83    3    8   41%
c i   15.4    1386     4380     33974    4019    196   614    6   129   19   4%    -65   83    3    8   40%
c 0   15.4    1379     4380     33974    4019    196   614    6   129   19   4%    -65   83    3    8   40%
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: 234 basic ate = 0 trn 0% + 234 lrg 100% in 1 updates
c bcas: 6 count, 112 added (0 skipped), 41767 steps
c bkwd: tried 22596 clauses, 45025 lits, 1.99 lits/clause
c bkwd: checked 10690018 occs, 473.09 occs/clause, 237.42 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 21 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 146 large (0% self)
c blkd: 5 bces, 3358 removed, 920416 resolutions, 2351406 steps
c blkd: 905 blocking literals 0%, 0 pure
c bump: 31719 bumped seen, 1898322 lits 59.8 on average
c card: 4 count, 0 units, 0 am1, 4295207 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 0 subsumed
c card: 0 at-most-one constraints found, average size 0.00
c card: 0 at-most-one constraints used 0%, average size 0.00
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, 203 eliminated, 192 ate 95%, 11 abce 5%
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: 2929894 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 61 gcs, 0 rescored clauses, 16 rescored vars
c dcps: 34 decompositions, 533 equivalent 0%
c deco: 7 decision-only clauses 0%, 53% reduction
c decs: 630104 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 5916666 push, 5566166 pop (5566166 dec 100%)
c dsch: 84315455 swaps, 0 down, 23541070 up
c elms: 9 elims, 346423 eliminated 99%, 0 pure 0%
c elms: 13 rounds, 1.4 rounds/bve
c elms: 330997 small 96%, 15426 large 4%
c elms: 335189 tried small, 330997 succeeded 99%, 4192 failed 1%
c elms: 997 subsumed, 0 strengthened, 11 blocked
c elms: 1966811 copies, 2084449 resolutions, 1864564 ipos
c elms: 1262422 subchks, 178930 strchks
c gaus: 4 extractions, 17176 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 6535318 steps, 3267659 extr 50%, 767370 elim 12%
c glue: 22.0 orig avg, 22.0 real avg, 3.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 43895 = 2829 simple 6% + 40012 trn 91% + 1054 lrg 2%, 12538 sub 29%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 31719 clauses, 30.8 length
c lrnd: 977555 lits = 1114777 orig - 137222 removed 12%
c lrnd: 7144 uips 23%, 14861 flips 47%
c mins: 30051 mins 95%, 22 bin 0%, 1638 size 5%
c mins: 1166438 poisoned searches, 79543 hits, 7% hit rate
c mins: 2137586 used twice searches, 577121 hits, 27% hit rate
c move: moved 2287, 631 bin 28%, 1656 trn 72%
c otfs: 2987 driving 43%, 3880 restarting 57%
c otfs: str 6867, 6685 red 97%, 182 irr 3%
c otfs: str 6867, 0 bin 0%, 96 trn 1%, 6771 lrg 99%
c otfs: sub 124, 123 red 99%, 1 irr 1%
c otfs: sub 124, 0 bin 0%, 2 trn 2%, 122 lrg 98%
c phas: 1 computed, 79897 set, 0 pos (0%), 79897 neg (100%)
c prbs: 3 basic, 2072 probed, 3 failed, 0 lifted
c prbs: 4 simple, 721001 probed, 0 failed, 0 eqs
c prbs: 3 treelook, 100 probed, 3 failed, 0 lifted
c prom: 0 locked 0% out of 25173 tried
c prps: 18304214 props, 27 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 9 count, 9 quat, 5204 self1, 0 self2, 0 dup
c redc: 290 clauses 2%, 14796 tried 44%, 0 sat 0%
c redc: 580 lits 1%, 105345 tried 9%, 0 sat 0%
c redc: 17 times jump level reduced, 3.3 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 790 removed, 358 red 45%
c rsts: 1495 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 14 count, 14 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 31719 count (11889 tried 0.4), 4345 sub out of 31369 (13.9%)
c swps: 7 count, 12 rounds, 2624 queries (218.7/round)
c swps: 2605 sat calls, 9 unsat (0.3% success rate)
c swps: 49217 decisions 18.9, 732 conflicts 0.3
c swps; 32.9 avg class size, 39.3 avg environment size
c swps: 0 failed, 5 impls, 22 equivs
c swp0: 869 type 0 queries, 208 unsat (23.9%), 868 sat (99.9%)
c swp1: 1755 type 1 queries, 489 unsat (27.9%), 1734 sat (98.8%)
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: 1323887 calls to obtain time
c tops: 2171 fixed 1%, 6 its, 5662.33 confs/it
c trds: 6 transitive reductions, 11 removed, 0 failed
c trds: 10083 nodes, 11340 edges, 2133860 steps
c trim: 258500 words, 1.0 MB
c trnr: 6 count, 10 bin, 91 trn, 21256138 steps
c unhd: 6 count, 6 rounds, 8747843 steps
c unhd: 2 non-trivial sccs of average size 2.0
c unhd: 65 units, 65 bin, 0 trn, 0 lrg
c unhd: 4439 failed, 4439 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 821 tauts, 0 bin 0%, 1 trn 0%, 4 lrg 0%
c unhd: 821 tauts, 816 stamp 99%, 707 red 86%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 79622 str, 65 bin 0%, 57169 trn 72%, 22388 lrg 28%, 22058 red 28%
c vars: 1379 remaining 0% and 349127 removed 100% out of 350506
c vars: 2171 fixed 1%, 346423 eliminated 99%, 533 equivalent 0%
c vsts: 124712093 visits, 90% srch, 10% simp, 0% lkhd
c vsts: 6.4 search visits per propagation, 3285.6 per conflict
c wchs: 27969737 pushed, 8926305 enlarged, 109 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          31378             0             0        307158         94930         15516
c 
c  0 0         10250  33         0   0<        0   0<    91836  30     37985  40      7218  47     0.2
c  1 5          3727  12         0   0         0   0     22163   7     11862  12      2366  15     0.1
c  2 6          4465  14         0   0         0   0     21820   7     10950  12      1888  12<    0.1
c  3 9          2293   7<        0   0         0   0     16505   5      4746   5<      522   3     0.1
c  4 14         1480   5         0   0         0   0     13020   4<     3550   4       374   2     0.1
c  5 21         1361   4         0   0         0   0     13199   4      4086   4       458   3     0.1
c  6 30         1444   5         0   0         0   0     14667   5      4350   5       546   4     0.1
c  7 41         1430   5         0   0         0   0     15776   5      4269   4       528   3     0.1
c  8 54         1527   5         0   0         0   0     20784   7      4266   4       523   3     0.2
c  9 69         1528   5         0   0         0   0     24821   8      4015   4       499   3     0.3
c 10 86         1809   6         0   0         0   0     52486  17      4805   5       594   4     0.4
c 11 126          57   0         0   0         0   0        74   0        42   0         0   0     0.0
c 12 230           7   0         0   0         0   0         7   0         4   0         0   0     0.0
c 
c avg                  3.1           0.0           0.0           4.4           2.7           2.1
c std                  3.3           0.0           0.0           3.9           3.3           3.0
c 
c    3.997  26% elim
c    1.623  11% probe
c    1.283   8% decide
c    1.208   8% cce
c    0.967   6% unhide
c    0.506   3% sweep
c    0.477   3% block
c    0.138   1% card
c    0.126   1% gauss
c    0.122   1% transred
c    0.118   1% bump
c 
c    0.223 < 1% rest (below)
c 
c    0.113   1% ternres
c    0.058   0% quatres
c    0.051   0% bca
c    0.002   0% rescore
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    3.855  25% preprocessing    38%
c    6.421  42% inprocessing     62%
c ==================================
c   10.276  67% simplifying
c    5.085  33% search
c ==================================
c   15.366 100% all
c 
c         33974 conflicts,        2211.0 confs/sec
c           203 ternaries,         167.4 confs/ternary
c            29 binaries,         1171.5 confs/binary
c             6 iterations,       5662.3 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          1495 restarts,           97.3 rests/sec,     22.7 confs/restart
c        630104 decisions,       41006.2 decis/sec,     18.5 decis/conflict
c      18304214 propagations,  1191209.9 props/sec,     29.0 props/decision
c 
c 15.4 seconds, 79.7 MB
c launch: done
