c launch: /data/cnf/sc2014/app/AProVE07-27.cnf.bz2
c host: atom26
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/AProVE07-27.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/AProVE07-27.cnf.bz2
c no embedded options
c found 'p cnf 7729 29194' header
c read 7729 variables, 29194 clauses, 77124 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 7511 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    7511    28318         0       0      0     0    0     0    2   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 740 variables
c [simpleprobe-1] all 6989 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 618 variables
c [simpleprobe-1] 57 variables remain 1% (6314 retained 99%)
c [simpleprobe-1] removed 618 variables, found 11177 hbrs, 188 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 41 tauts, 0 hbrs, 145 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 6371 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 3650 variables 57% in round 1 in 2916790 steps
c [elim-1-1] backward subsumption/strengthening limit 2916700
c [elim-1-1-1] backward checking 4378 touched variables 69%
c [elim-1-1-1] incomplete backward checking 4377 remain 100%
c [elim-1-1] subsumed 16 and strengthened 30 clauses in 2916849 steps
c [elim-1-1] rescheduled 81 variables 1% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 30881 steps
c [elim-1-2] backward subsumption/strengthening limit 30800
c [elim-1-2-1] backward checking 4378 touched variables 69%
c [elim-1-2-1] incomplete backward checking 4377 remain 100%
c [elim-1-2] subsumed 5 and strengthened 5 clauses in 30890 steps
c [elim-1-2] rescheduled 20 variables 0% by backward subsumption
c [elim-1-3] eliminated 3 variables 0% in round 3 in 19932 steps
c [elim-1-3] backward subsumption/strengthening limit 19900
c [elim-1-3-1] backward checking 4378 touched variables 69%
c [elim-1-3-1] incomplete backward checking 4372 remain 100%
c [elim-1-3] subsumed 0 and strengthened 1 clauses in 20003 steps
c [elim-1] incomplete 5 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 3655 = 57% variables out of 6371 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 16146 negative 96.0% of 16824 except 678 4.0%
c [phase-count-1] 15705 positive 93.3% of 16824 except 1119 6.7%
c [phase-1] phase bias: 390 positive 14%, 2326 negative 86%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 2716 zero 100.00%
c [score-distribution-1] 1 different 0.04% out of total 2716 variables
c [simplification-1] removed 4787 variables 63.8% (2716 remain 36%)
c [simplification-1] removed 11494 irredundant clauses 40.6% (16824 remain 59%)
c [simplification-1] maximum reduction of 64% = max (64%, 41%)
c [simplification-1] large reduction 64% >= 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    0.8    2715    16824       286     237     22  4412    0     2    2  18%      1    2    4    0 16799%
c i    0.8    2714    16824       421     355     31  4412    1     3    2  18%      1    3    5    0 13387%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 2 variables
c [simpleprobe-2] 23 schedulable variables 1%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 10 variables
c [simpleprobe-2] 93 variables remain 3% (2611 retained 97%)
c [simpleprobe-2] removed 10 variables, found 959 hbrs, 10 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 5408 literals 100%
c [treelook-1] scheduling used 76880 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300127 steps
c [treelook-1] 5386 literals remain 100%
c [treelook-1] 2703 variables remain to probed next time 100%
c [treelook-1] removed 1 variables, found 1149 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 21 probes remain 1% after last round
c [basicprobe-1-0] 62 units = 56 failed (90%) + 6 lifted (10%)
c [basicprobe-1-0] removed 59 variables, found 2628 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 2644 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 232 variables 9% in round 1 in 2850645 steps
c [elim-2-1] backward subsumption/strengthening limit 2850600
c [elim-2-1-1] backward checking 901 touched variables 34%
c [elim-2-1-1] incomplete backward checking 902 remain 100%
c [elim-2-1] subsumed 3 and strengthened 24 clauses in 2851252 steps
c [elim-2-1] rescheduled 61 variables 2% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 626284 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 232 = 9% variables out of 2644 scheduled
c [phase-count-2] 14308 negative 95.5% of 14988 except 680 4.5%
c [phase-count-2] 13755 positive 91.8% of 14988 except 1233 8.2%
c [phase-count-2] less non-negative clauses 680 than limit 1400 (10.0%)
c [phase-count-2] non-pos/non-neg = 1233/680 = 1.81 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 7 negative 100%
c [score-distribution-2] 2003 pos 83.04%, 0 min 0.00%, 409 zero 16.96%
c [score-distribution-2] 1009 different 41.83% out of total 2412 variables
c [simplification-2] removed 302 variables 11.1% (2412 remain 32%)
c [simplification-2] removed 1836 irredundant clauses 10.9% (14988 remain 53%)
c [simplification-2] maximum reduction of 11% = max (11%, 11%)
c [simplification-2] large reduction 11% >= 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] found 614 at-most-one constraints of average size 3.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 614 out of 614 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 76 at-most-one constraints, 7 used 9%
c [card-2] exported 12 binary clauses, 1.7 per/constraint
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 4824 literals 100%
c [treelook-2] scheduling used 75673 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 308382 steps
c [treelook-2] 4797 literals remain 99%
c [treelook-2] 2412 variables remain to probed next time 100%
c [treelook-2] removed 0 variables, found 810 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 763 tauts, 0 hbrs, 1911 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 2412 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 820 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 20 (10%) of length 9
c [cce-1-1] eliminated 19 clauses out of 32 (59%) of length 8
c [cce-1-1] eliminated 6 clauses out of 96 (6%) of length 7
c [cce-1-1] eliminated 112 clauses out of 610 (18%) of length 6
c [cce-1-1] eliminated 89 clauses out of 1558 (6%) of length 5
c [cce-1-1] eliminated 539 clauses out of 2649 (20%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 767 large clauses in 8530438 steps
c [cce-1-1] allowing another 4265219 steps for small clauses
c [cce-1-1] scheduling 5477 clauses = 3942 binary + 1535 ternary
c [cce-1-1] tried to eliminate 5477 small clauses 100%
c [cce-1-1] eliminated 406 binary clauses 10%
c [cce-1-1] eliminated 216 ternary clauses 14%
c [cce-1-1] eliminated 622 small clauses 11%
c [cce-1-1] eliminated 622 small clauses in 23181679 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 1389 covered clauses in round 1
c [cce-1-2] eliminated 3 clauses out of 3 (100%) of length 11
c [cce-1-2] eliminated 18 clauses out of 498 (4%) of length 6
c [cce-1-2] eliminated 10 clauses out of 1469 (1%) of length 5
c [cce-1-2] eliminated 59 clauses out of 2110 (3%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 90 large clauses in 6367812 steps
c [cce-1-2] allowing another 3183906 steps for small clauses
c [cce-1-2] scheduling 4855 clauses = 3536 binary + 1319 ternary
c [cce-1-2] tried to eliminate 2605 small clauses 54%
c [cce-1-2] eliminated 35 binary clauses 1%
c [cce-1-2] eliminated 19 ternary clauses 1%
c [cce-1-2] eliminated 54 small clauses 1%
c [cce-1-2] eliminated 54 small clauses in 6818326 steps
c [cce-1-2] incomplete small round (ABCE)
c [cce-1-2] eliminated 144 covered clauses in round 2
c [cce-1] eliminated 1533 covered clauses in TOTAL during 2 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 2412 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 178 variables 7% in round 1 in 2293397 steps
c [elim-3-1] backward subsumption/strengthening limit 2293300
c [elim-3-1-1] backward checking 809 touched variables 34%
c [elim-3-1-1] incomplete backward checking 771 remain 95%
c [elim-3-1] subsumed 0 and strengthened 10 clauses in 2293836 steps
c [elim-3-1] rescheduled 33 variables 1% by backward subsumption
c [elim-3-2] no variable eliminated in round 2 in 326241 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 178 = 7% variables out of 2412 scheduled
c [bca-1] limit of 10000000 steps and 25156 added (scaled 2)
c [bca-1] 2194 out of 4470 literals actually usable 49%
c [bca-1] added 27 blocked clauses in 7059 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 328 pos 14.7% + 1906 neg 85.3% = 2234 sched 100.0% ret 0
c [sweep-1-1] 1029586 steps 152 queries 55.62 avg class size
c [sweep-1-1] 2043 decisions 152 SAT calls 36.74 avg env size
c [sweep-1-1] 172 variables remain 8% (2061 retained 92%)
c [decomp-8] removed 2 variables
c [sweep-1-1] removed 2 vars (0 failed, 1 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 2 vars in TOTAL (1 rounds, 151 queries)
c [score-distribution-3] 2157 pos 96.64%, 0 min 0.00%, 75 zero 3.36%
c [score-distribution-3] 1088 different 48.75% out of total 2232 variables
c [simplification-3] removed 180 variables 7.5% (2232 remain 30%)
c [simplification-3] removed 2670 irredundant clauses 17.8% (12318 remain 43%)
c [simplification-3] maximum reduction of 18% = max (7%, 18%)
c [simplification-3] large reduction 18% >= 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 5003 conflicts
c [quatres-1] found 2721 quaternary clauses 48% in total
c [quatres-1-1] removed 2 duplicate quaternary clauses
c [quatres-1-2] added 57 single-self-subsuming ternary resolvents
c [quatres-1-2] added 107 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 2232 free variables schedulable
c [ternres-1] 591 ternary resolvents (10 bin, 581 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4488 xors of average arity 3.1
c [gauss-1] connected 13972 occurrences of 959 variables (average 14.6)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 1 variables
c [basicprobe-2] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-2-0] 432 sched 19%, 2 failed, 0 lifted, 229 hbrs
c [decomp-10] removed 2 variables
c [basicprobe-2-1] 1402 sched 63%, 10 failed, 0 lifted, 686 hbrs
c [decomp-11] removed 10 variables
c [basicprobe-2-2] 986 probes remain 44% after last round
c [basicprobe-2-2] 12 units = 12 failed (100%) + 0 lifted (0%)
c [basicprobe-2-2] removed 12 variables, found 1001 hbrs
c [bate-1] eliminated 56 asymmetric tautologies during probing
c [transred-1] limit 115360 with penalty 0 = 0 + 0
c [transred-1] removed 39 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 2219 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 19 blocked clauses
c [block-2] 19 < 1/100 * 12183 = 121 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 7 clauses out of 110 (6%) of length 7
c [cce-2-1] eliminated 15 clauses out of 463 (3%) of length 6
c [cce-2-1] eliminated 18 clauses out of 1538 (1%) of length 5
c [cce-2-1] eliminated 141 clauses out of 2419 (6%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 181 large clauses in 6975866 steps
c [cce-2-1] allowing another 3487933 steps for small clauses
c [cce-2-1] scheduling 4554 clauses = 3311 binary + 1243 ternary
c [cce-2-1] tried to eliminate 4554 small clauses 100%
c [cce-2-1] eliminated 9 binary clauses 0%
c [cce-2-1] eliminated 30 ternary clauses 2%
c [cce-2-1] eliminated 39 small clauses 1%
c [cce-2-1] eliminated 39 small clauses in 16226466 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 220 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 3300679 steps for small clauses
c [cce-2-2] scheduling 4515 clauses = 3302 binary + 1213 ternary
c [cce-2-2] tried to eliminate 3030 small clauses 67%
c [cce-2-2] incomplete small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 220 covered clauses in TOTAL during 2 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 2219 variables 100%
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 74 variables 3% in round 1 in 2159344 steps
c [elim-4-1] backward subsumption/strengthening limit 2159300
c [elim-4-1-1] backward checking 381 touched variables 17%
c [elim-4-1-1] incomplete backward checking 275 remain 72%
c [elim-4-1] subsumed 0 and strengthened 21 clauses in 2159381 steps
c [elim-4-1] rescheduled 58 variables 3% by backward subsumption
c [elim-4-2] eliminated 8 variables 0% in round 2 in 289809 steps
c [elim-4-2] backward subsumption/strengthening limit 289800
c [elim-4-2-1] backward checking 312 touched variables 14%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 90316 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 82 = 4% variables out of 2219 scheduled
c [bca-2] limit of 10000000 steps and 24071 added (scaled 2)
c [bca-2] 1615 out of 4276 literals actually usable 38%
c [bca-2] added 2 blocked clauses in 7192 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 34 pos 21.0% + 128 neg 79.0% = 162 sched 7.6% ret 1975
c [sweep-2-1] 564026 steps 57 queries 11.23 avg class size
c [sweep-2-1] 1241 decisions 56 SAT calls 32.11 avg env size
c [sweep-2-1] fully completed sweeping round
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2-2] 300 pos 14.0% + 1837 neg 86.0% = 2137 sched 100.0% ret 0
c [sweep-2-2] 437719 steps 33 queries 111.85 avg class size
c [sweep-2-2] 941 decisions 32 SAT calls 55.72 avg env size
c [sweep-2-2] 1182 variables remain 55% (955 retained 45%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (2 rounds, 88 queries)
c [score-distribution-4] 2088 pos 97.71%, 14 min 0.66%, 35 zero 1.64%
c [score-distribution-4] 1183 different 55.36% out of total 2137 variables
c [simplification-4] removed 95 variables 4.3% (2137 remain 28%)
c [simplification-4] removed 539 irredundant clauses 4.4% (11779 remain 42%)
c [simplification-4] maximum reduction of 4% = max (4%, 4%)
c [simplification-4] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-4] new conflict interval 4000
c [simplification-4] penalized conflict interval 4000 = 1 * 4000
c [simplification-4] hard conflict limit 19003 (soft 9003 + delta 10000)
c [simplification-4] new conflict limit 9003 (hard 19003)
c 
c [simplification-5] limit 9003 conflicts (hard 19003) hit after 9005 conflicts
c [quatres-2] found 2725 quaternary clauses 45% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-1] added 4 double-self-subsuming ternary resolvents
c [quatres-2-2] added 19 single-self-subsuming ternary resolvents
c [quatres-2-2] added 73 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 2137 free variables schedulable
c [ternres-2] 79 ternary resolvents (2 bin, 77 trn)
c [ternres-2] fully completed ternary resolution
c [simpleprobe-3] 56 schedulable variables 3%
c [simpleprobe-3] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-3] 397 variables remain 19% (1740 retained 81%)
c [simpleprobe-3] removed 0 variables, found 1268 hbrs, 0 units
c [transred-2] limit 222966 with penalty 0 = 0 + 0
c [transred-2] removed 101 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 20 (5%) of length 8
c [cce-3-1] eliminated 3 clauses out of 102 (3%) of length 7
c [cce-3-1] eliminated 40 clauses out of 469 (9%) of length 6
c [cce-3-1] eliminated 72 clauses out of 1560 (5%) of length 5
c [cce-3-1] eliminated 184 clauses out of 2294 (8%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 300 large clauses in 7067481 steps
c [cce-3-1] allowing another 3533740 steps for small clauses
c [cce-3-1] scheduling 4424 clauses = 3202 binary + 1222 ternary
c [cce-3-1] tried to eliminate 4424 small clauses 100%
c [cce-3-1] eliminated 140 binary clauses 4%
c [cce-3-1] eliminated 84 ternary clauses 7%
c [cce-3-1] eliminated 224 small clauses 5%
c [cce-3-1] eliminated 224 small clauses in 15867424 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] completed small and large (ACCE)
c [cce-3-1] eliminated 524 covered clauses in round 1
c [cce-3-2] eliminated 2 clauses out of 99 (2%) of length 7
c [cce-3-2] eliminated 11 clauses out of 429 (3%) of length 6
c [cce-3-2] eliminated 32 clauses out of 1488 (2%) of length 5
c [cce-3-2] eliminated 20 clauses out of 2110 (1%) of length 4
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] eliminated 65 large clauses in 6319549 steps
c [cce-3-2] allowing another 3159774 steps for small clauses
c [cce-3-2] scheduling 4200 clauses = 3062 binary + 1138 ternary
c [cce-3-2] tried to eliminate 4200 small clauses 100%
c [cce-3-2] eliminated 10 binary clauses 0%
c [cce-3-2] eliminated 2 ternary clauses 0%
c [cce-3-2] eliminated 12 small clauses 0%
c [cce-3-2] eliminated 12 small clauses in 14109136 steps
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 77 covered clauses in round 2
c [cce-3-3] incomplete large round (ACCE)
c [cce-3-3] allowing another 11729 steps for small clauses
c [cce-3-3] scheduling 4188 clauses = 3052 binary + 1136 ternary
c [cce-3-3] tried to eliminate 10 small clauses 0%
c [cce-3-3] incomplete small round (ACCE)
c [cce-3-3] eliminated 0 covered clauses in round 3
c [cce-3] eliminated 601 covered clauses in TOTAL during 3 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 2137 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] eliminated 98 variables 5% in round 1 in 1970233 steps
c [elim-5-1] backward subsumption/strengthening limit 1970200
c [elim-5-1-1] backward checking 338 touched variables 16%
c [elim-5-1-1] incomplete backward checking 54 remain 16%
c [elim-5-1] subsumed 0 and strengthened 8 clauses in 1970226 steps
c [elim-5-1] rescheduled 18 variables 1% by backward subsumption
c [elim-5-2] eliminated 1 variables 0% in round 2 in 173545 steps
c [elim-5-2] backward subsumption/strengthening limit 173500
c [elim-5-2-1] backward checking 64 touched variables 3%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 2 clauses in 15002 steps
c [elim-5-2] rescheduled 7 variables 0% by backward subsumption
c [elim-5-3] no variable eliminated in round 3 in 3807 steps
c [elim-5] fully completed in 3 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 99 = 5% variables out of 2137 scheduled
c [bca-3] limit of 10000000 steps and 22242 added (scaled 2)
c [bca-3] 1246 out of 4078 literals actually usable 31%
c [bca-3] added 50 blocked clauses in 8844 steps
c [score-distribution-5] 1985 pos 97.40%, 28 min 1.37%, 25 zero 1.23%
c [score-distribution-5] 1241 different 60.89% out of total 2038 variables
c [simplification-5] removed 99 variables 4.6% (2038 remain 27%)
c [simplification-5] removed 915 irredundant clauses 7.8% (10864 remain 38%)
c [simplification-5] maximum reduction of 8% = max (5%, 8%)
c [simplification-5] large reduction 8% >= 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 21005 (soft 11005 + delta 10000)
c [simplification-5] new conflict limit 11005 (hard 21005)
c 
c [simplification-6] limit 11005 conflicts (hard 21005) hit after 11005 conflicts
c [quatres-3] found 2567 quaternary clauses 44% in total
c [quatres-3-1] added 3 double-self-subsuming ternary resolvents
c [quatres-3-2] added 5 single-self-subsuming ternary resolvents
c [quatres-3-2] added 41 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 2038 free variables schedulable
c [ternres-3] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-3] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 444 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 444 out of 444 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] generated 69 at-most-one constraints, 2 used 3%
c [card-3] exported 3 binary clauses, 1.5 per/constraint
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 4092 xors of average arity 3.1
c [gauss-2] connected 12636 occurrences of 845 variables (average 15.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-3] limit 25000 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 39 tauts, 0 hbrs, 2346 literals
c [transred-3] limit 279403 with penalty 0 = 0 + 0
c [transred-3] removed 242 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 2038 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 3 blocked clauses
c [block-3] 3 < 1/100 * 10860 = 108 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 89 (1%) of length 7
c [cce-4-1] eliminated 2 clauses out of 425 (0%) of length 6
c [cce-4-1] eliminated 7 clauses out of 1449 (0%) of length 5
c [cce-4-1] eliminated 14 clauses out of 2065 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 24 large clauses in 5947326 steps
c [cce-4-1] allowing another 2973663 steps for small clauses
c [cce-4-1] scheduling 5665 clauses = 2965 binary + 2700 ternary
c [cce-4-1] tried to eliminate 5665 small clauses 100%
c [cce-4-1] eliminated 183 ternary clauses 7%
c [cce-4-1] eliminated 183 small clauses 3%
c [cce-4-1] eliminated 183 small clauses in 14469771 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 207 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 2921738 steps for small clauses
c [cce-4-2] scheduling 5482 clauses = 2965 binary + 2517 ternary
c [cce-4-2] tried to eliminate 5482 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 207 covered clauses in TOTAL during 2 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 2038 variables 100%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 35 variables 2% in round 1 in 1909835 steps
c [elim-6-1] backward subsumption/strengthening limit 1909800
c [elim-6-1-1] backward checking 145 touched variables 7%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 2 clauses in 700364 steps
c [elim-6-1] rescheduled 6 variables 0% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 31525 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 35 = 2% variables out of 2038 scheduled
c [bca-4] limit of 10000000 steps and 21603 added (scaled 2)
c [bca-4] 1079 out of 4008 literals actually usable 27%
c [bca-4] added 2 blocked clauses in 9869 steps
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 166 pos 15.3% + 919 neg 84.7% = 1085 sched 54.2% ret 918
c [sweep-3-1] 502856 steps 39 queries 67.18 avg class size
c [sweep-3-1] 872 decisions 38 SAT calls 48.95 avg env size
c [sweep-3-1] 407 variables remain 20% (1596 retained 80%)
c [decomp-17] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-3] 1 < 1/1000 * 2003 = 2 considered unsuccessful
c [sweep-3] removed 1 vars in TOTAL (1 rounds, 38 queries)
c [score-distribution-6] 1974 pos 98.60%, 17 min 0.85%, 11 zero 0.55%
c [score-distribution-6] 993 different 49.60% out of total 2002 variables
c [simplification-6] removed 36 variables 1.8% (2002 remain 27%)
c [simplification-6] removed 332 irredundant clauses 3.1% (10532 remain 37%)
c [simplification-6] maximum reduction of 3% = max (2%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 9000
c [simplification-6] penalized conflict interval 9000 = 1 * 9000
c [simplification-6] hard conflict limit 30005 (soft 20005 + delta 10000)
c [simplification-6] new conflict limit 20005 (hard 30005)
c 
c [simplification-7] limit 20005 conflicts (hard 30005) hit after 20005 conflicts
c [quatres-4] found 2762 quaternary clauses 42% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 13 single-self-subsuming ternary resolvents
c [quatres-4-2] added 52 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 2002 free variables schedulable
c [ternres-4] 131 ternary resolvents (5 bin, 126 trn)
c [ternres-4] fully completed ternary resolution
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 4004 literals 100%
c [treelook-3] scheduling used 101379 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 152594 steps
c [treelook-3] 3978 literals remain 99%
c [treelook-3] 2002 variables remain to probed next time 100%
c [treelook-3] removed 0 variables, found 22 hbrs
c [transred-4] limit 600001 with penalty 0 = 0 + 0
c [transred-4] removed 364 transitive binary clauses
c [transred-4] found 1 units
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 32 (3%) of length 8
c [cce-5-1] eliminated 1 clauses out of 96 (1%) of length 7
c [cce-5-1] eliminated 4 clauses out of 421 (1%) of length 6
c [cce-5-1] eliminated 21 clauses out of 1420 (1%) of length 5
c [cce-5-1] eliminated 90 clauses out of 2076 (4%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 117 large clauses in 6441401 steps
c [cce-5-1] allowing another 3220700 steps for small clauses
c [cce-5-1] scheduling 4017 clauses = 2951 binary + 1066 ternary
c [cce-5-1] tried to eliminate 4017 small clauses 100%
c [cce-5-1] eliminated 25 binary clauses 1%
c [cce-5-1] eliminated 41 ternary clauses 4%
c [cce-5-1] eliminated 66 small clauses 2%
c [cce-5-1] eliminated 72 small clauses in 13443728 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 189 covered clauses in round 1
c [cce-5-2] eliminated 1 clauses out of 31 (3%) of length 8
c [cce-5-2] eliminated 2 clauses out of 1399 (0%) of length 5
c [cce-5-2] eliminated 18 clauses out of 1986 (1%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 21 large clauses in 6178175 steps
c [cce-5-2] allowing another 3089087 steps for small clauses
c [cce-5-2] scheduling 3951 clauses = 2926 binary + 1025 ternary
c [cce-5-2] tried to eliminate 3951 small clauses 100%
c [cce-5-2] eliminated 3 binary clauses 0%
c [cce-5-2] eliminated 6 ternary clauses 1%
c [cce-5-2] eliminated 9 small clauses 0%
c [cce-5-2] eliminated 9 small clauses in 13056910 steps
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 30 covered clauses in round 2
c [cce-5-3] incomplete large round (ACCE)
c [cce-5-3] allowing another 1749710 steps for small clauses
c [cce-5-3] scheduling 3942 clauses = 2923 binary + 1019 ternary
c [cce-5-3] tried to eliminate 1110 small clauses 28%
c [cce-5-3] incomplete small round (ACCE)
c [cce-5-3] eliminated 0 covered clauses in round 3
c [cce-5] eliminated 219 covered clauses in TOTAL during 3 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 2001 variables 100%
c [elim-7] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 64 variables 3% in round 1 in 6070625 steps
c [elim-7-1] backward subsumption/strengthening limit 6070600
c [elim-7-1-1] backward checking 225 touched variables 11%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 35 clauses in 951753 steps
c [elim-7-1] rescheduled 74 variables 4% by backward subsumption
c [elim-7-2] eliminated 6 variables 0% in round 2 in 4226197 steps
c [elim-7-2] backward subsumption/strengthening limit 4226100
c [elim-7-2-1] backward checking 60 touched variables 3%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 10818 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 70 = 3% variables out of 2001 scheduled
c [bca-5] limit of 10000000 steps and 20742 added (scaled 2)
c [bca-5] 763 out of 3864 literals actually usable 20%
c [bca-5] added 59 blocked clauses in 15910 steps
c [score-distribution-7] 1907 pos 98.76%, 23 min 1.19%, 1 zero 0.05%
c [score-distribution-7] 1258 different 65.15% out of total 1931 variables
c [simplification-7] removed 71 variables 3.5% (1931 remain 26%)
c [simplification-7] removed 431 irredundant clauses 4.1% (10101 remain 36%)
c [simplification-7] maximum reduction of 4% = max (4%, 4%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 13000
c [simplification-7] penalized conflict interval 13000 = 1 * 13000
c [simplification-7] hard conflict limit 43005 (soft 33005 + delta 10000)
c [simplification-7] new conflict limit 33005 (hard 43005)
c 
c [simplification-8] limit 33005 conflicts (hard 43005) hit after 33005 conflicts
c [quatres-5] found 2752 quaternary clauses 38% in total
c [quatres-5-1] added 2 double-self-subsuming ternary resolvents
c [quatres-5-2] added 10 single-self-subsuming ternary resolvents
c [quatres-5-2] added 29 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 1931 free variables schedulable
c [ternres-5] 33 ternary resolvents (1 bin, 32 trn)
c [ternres-5] fully completed ternary resolution
c [basicprobe-3] limit 5886800 penalty 0 = 0 + 0
c [basicprobe-3-0] 928 sched 48%, 1 failed, 0 lifted, 329 hbrs
c [decomp-21] removed 1 variables
c [basicprobe-3-1] 1213 sched 63%, 1 failed, 0 lifted, 189 hbrs
c [decomp-22] removed 1 variables
c [basicprobe-3-2] 1214 sched 63%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-3-3] 1214 sched 63%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-3] fully completed probing
c [basicprobe-3-3] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-3-3] removed 2 variables, found 527 hbrs
c [bate-2] eliminated 4 asymmetric tautologies during probing
c [transred-5] limit 1177360 with penalty 0 = 0 + 0
c [transred-5] removed 249 transitive binary clauses
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 414 (0%) of length 6
c [cce-6-1] eliminated 3 clauses out of 1422 (0%) of length 5
c [cce-6-1] eliminated 18 clauses out of 1926 (1%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 22 large clauses in 5809135 steps
c [cce-6-1] allowing another 2904567 steps for small clauses
c [cce-6-1] scheduling 3894 clauses = 2896 binary + 998 ternary
c [cce-6-1] tried to eliminate 3894 small clauses 100%
c [cce-6-1] eliminated 2 binary clauses 0%
c [cce-6-1] eliminated 2 ternary clauses 0%
c [cce-6-1] eliminated 4 small clauses 0%
c [cce-6-1] eliminated 4 small clauses in 12347491 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 26 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 2882519 steps for small clauses
c [cce-6-2] scheduling 3890 clauses = 2894 binary + 996 ternary
c [cce-6-2] tried to eliminate 3890 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 26 covered clauses in TOTAL during 2 rounds
c [cce-6] 26 < 1/100 * 10085 = 100 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 1929 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 470944060 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 21 variables 1% in round 1 in 6037032 steps
c [elim-8-1] backward subsumption/strengthening limit 6037000
c [elim-8-1-1] backward checking 111 touched variables 6%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 326544 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 21 = 1% variables out of 1929 scheduled
c [bca-6] limit of 10000000 steps and 20642 added (scaled 2)
c [bca-6] 543 out of 3818 literals actually usable 14%
c [bca-6] added 0 blocked clauses in 25270 steps
c [score-distribution-8] 1885 pos 98.79%, 22 min 1.15%, 1 zero 0.05%
c [score-distribution-8] 1409 different 73.85% out of total 1908 variables
c [simplification-8] removed 23 variables 1.2% (1908 remain 25%)
c [simplification-8] removed 65 irredundant clauses 0.6% (10036 remain 35%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-8] new conflict interval 23000
c [simplification-8] penalized conflict interval 23000 = 1 * 23000
c [simplification-8] hard conflict limit 67505 (soft 56005 + delta 11500)
c [simplification-8] new conflict limit 56005 (hard 67505)
c 
c [simplification-9] limit 56005 conflicts (hard 67505) hit after 56006 conflicts
c [quatres-6] found 2899 quaternary clauses 36% in total
c [quatres-6-2] added 4 single-self-subsuming ternary resolvents
c [quatres-6-2] added 27 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 1908 free variables schedulable
c [ternres-6] 23 ternary resolvents (0 bin, 23 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 3742 xors of average arity 3.1
c [gauss-3] connected 11530 occurrences of 765 variables (average 15.1)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
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 162 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 1908 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 0 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 1908 variables 100%
c [elim-9] limit of 51573485 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 2 variables 0% in round 1 in 6026531 steps
c [elim-9-1] backward subsumption/strengthening limit 6026500
c [elim-9-1-1] backward checking 14 touched variables 1%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 4710 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 2 = 0% variables out of 1908 scheduled
c [elim-9] 2 < 1/100 * 1908 = 19 considered unsuccessful
c [sweep-4] limit 250000 penalty 2 = 2 + 0
c [sweep-4-1] 74 pos 20.1% + 295 neg 79.9% = 369 sched 19.4% ret 1537
c [sweep-4-1] 350141 steps 2 queries 184.50 avg class size
c [sweep-4-1] 100 decisions 1 SAT calls 233.00 avg env size
c [sweep-4-1] 369 variables remain 19% (1537 retained 81%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 1 queries)
c [score-distribution-9] 1881 pos 98.69%, 24 min 1.26%, 1 zero 0.05%
c [score-distribution-9] 1273 different 66.79% out of total 1906 variables
c [simplification-9] removed 2 variables 0.1% (1906 remain 25%)
c [simplification-9] removed 5 irredundant clauses 0.0% (10031 remain 35%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 23000
c [simplification-9] new conflict interval 46000
c [simplification-9] penalized conflict interval 46000 = 1 * 46000
c [simplification-9] hard conflict limit 125006 (soft 102006 + delta 23000)
c [simplification-9] new conflict limit 102006 (hard 125006)
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 -   16.3    1906    10031     64346   16855   1312  5421   16    27    7  57%    632   11   17    9  191%
c 
c [simplification-10] limit 102006 conflicts (hard 125006) hit after 102006 conflicts
c [quatres-7] found 3071 quaternary clauses 34% in total
c [quatres-7-2] added 12 single-self-subsuming ternary resolvents
c [quatres-7-2] added 19 quaternary resolvents
c [ternres-7] limit 5697886 with penalty 0 = 0 + 0
c [ternres-7] all 1906 free variables schedulable
c [ternres-7] 28 ternary resolvents (0 bin, 28 trn)
c [ternres-7] fully completed ternary resolution
c [card-4] limit 356117 penalty 3 = 3 + 0
c [card-4] found 168 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 356117 for elimination
c [card-4] 168 out of 168 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] generated 5 at-most-one constraints, 0 used 0%
c [card-4] exported 0 binary clauses, 0.0 per/constraint
c [simpleprobe-4] 363 schedulable variables 19%
c [simpleprobe-4] limit 11395773 penalty 1 = 1 + 0
c [decomp-27] removed 1 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 1 variables, found 1488 hbrs, 0 units
c [unhide-4] limit 142447 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 1207 tauts, 0 hbrs, 50851 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 337 transitive binary clauses
c [cce-7] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 12 clauses out of 396 (3%) of length 6
c [cce-7-1] eliminated 17 clauses out of 1414 (1%) of length 5
c [cce-7-1] eliminated 34 clauses out of 1861 (2%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 63 large clauses in 5916801 steps
c [cce-7-1] allowing another 2958400 steps for small clauses
c [cce-7-1] scheduling 3910 clauses = 2870 binary + 1040 ternary
c [cce-7-1] tried to eliminate 3910 small clauses 100%
c [cce-7-1] eliminated 31 binary clauses 1%
c [cce-7-1] eliminated 27 ternary clauses 3%
c [cce-7-1] eliminated 58 small clauses 1%
c [cce-7-1] eliminated 58 small clauses in 12608986 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 121 covered clauses in round 1
c [cce-7-2] incomplete large round (ACCE)
c [cce-7-2] allowing another 1195991 steps for small clauses
c [cce-7-2] scheduling 3852 clauses = 2839 binary + 1013 ternary
c [cce-7-2] tried to eliminate 793 small clauses 21%
c [cce-7-2] incomplete small round (ACCE)
c [cce-7-2] eliminated 0 covered clauses in round 2
c [cce-7] eliminated 121 covered clauses in TOTAL during 2 rounds
c [bca-7] limit of 10000000 steps and 20390 added (scaled 2)
c [bca-7] 422 out of 3812 literals actually usable 11%
c [bca-7] added 1 blocked clauses in 54039 steps
c [score-distribution-10] 1876 pos 98.48%, 28 min 1.47%, 1 zero 0.05%
c [score-distribution-10] 1347 different 70.71% out of total 1905 variables
c [simplification-10] removed 1 variables 0.1% (1905 remain 25%)
c [simplification-10] removed 121 irredundant clauses 1.2% (9910 remain 35%)
c [simplification-10] maximum reduction of 1% = max (0%, 1%)
c [simplification-10] geometric conflict interval increment 23000 = 46000 / 2
c [simplification-10] new conflict interval 69000
c [simplification-10] penalized conflict interval 69000 = 1 * 69000
c [simplification-10] hard conflict limit 205506 (soft 171006 + delta 34500)
c [simplification-10] new conflict limit 171006 (hard 205506)
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 -   26.0    1905     9910    105143   21315   1333  5484   16    26    8  63%    814    4   18   12  149%
c -   32.6    1905     9910    145690   27378   1353  5490   13    16    6  85%    911   -5   15   13  120%
c i   35.0    1904     9910    159503   39839   1364  5491   16    25   11  65%    932    5   17   13  130%
c -   38.3    1904     9910    181991   29350   1386  5494   12    14    6  82%   -833   -5   12   13   92%
c 
c [simplification-11] limit 171006 conflicts (hard 205506) hit after 205506 conflicts
c [quatres-8] found 2599 quaternary clauses 38% in total
c [quatres-8-2] added 15 single-self-subsuming ternary resolvents
c [quatres-8-2] added 119 quaternary resolvents
c [ternres-8] limit 12257719 with penalty 0 = 0 + 0
c [ternres-8] all 1904 free variables schedulable
c [ternres-8] 93 ternary resolvents (1 bin, 92 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 37 variables
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 224 transitive binary clauses
c [transred-8] found 1 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 612885990 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 667 (0%) of length 5
c [cce-8-1] eliminated 4 clauses out of 2601 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 5 large clauses in 1984692 steps
c [cce-8-1] allowing another 992346 steps for small clauses
c [cce-8-1] scheduling 4626 clauses = 2313 binary + 2313 ternary
c [cce-8-1] tried to eliminate 4626 small clauses 100%
c [cce-8-1] eliminated 2 binary clauses 0%
c [cce-8-1] eliminated 19 ternary clauses 1%
c [cce-8-1] eliminated 21 small clauses 0%
c [cce-8-1] eliminated 30 small clauses in 3290590 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 35 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 988274 steps for small clauses
c [cce-8-2] scheduling 4605 clauses = 2311 binary + 2294 ternary
c [cce-8-2] tried to eliminate 4605 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 35 covered clauses in TOTAL during 2 rounds
c [cce-8] 35 < 1/100 * 9316 = 93 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 1867 variables 100%
c [elim-10] limit of 122577199 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 215 variables 12% in round 1 in 2157122 steps
c [elim-10-1] backward subsumption/strengthening limit 2157100
c [elim-10-1-1] backward checking 524 touched variables 28%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 3 clauses in 268657 steps
c [elim-10-1] rescheduled 13 variables 1% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 105536 steps
c [elim-10-2] backward subsumption/strengthening limit 105500
c [elim-10-2-1] backward checking 8 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 1 clauses in 8400 steps
c [elim-10-2] rescheduled 5 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 2155 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 216 = 12% variables out of 1867 scheduled
c [bca-8] limit of 10000000 steps and 18462 added (scaled 2)
c [bca-8] 517 out of 3304 literals actually usable 16%
c [bca-8] added 38 blocked clauses in 35773 steps
c [score-distribution-11] 1498 pos 90.73%, 152 min 9.21%, 1 zero 0.06%
c [score-distribution-11] 1107 different 67.05% out of total 1651 variables
c [simplification-11] removed 253 variables 13.3% (1651 remain 22%)
c [simplification-11] removed 964 irredundant clauses 9.7% (8946 remain 32%)
c [simplification-11] maximum reduction of 13% = max (13%, 10%)
c [simplification-11] large reduction 13% >= 5% limit
c [simplification-11] next conflict interval 2055 = min (205506/100, 69000)
c [simplification-11] penalized conflict interval 2055 = 1 * 2055
c [simplification-11] hard conflict limit 217561 (soft 207561 + delta 10000)
c [simplification-11] new conflict limit 207561 (hard 217561)
c 
c [simplification-12] limit 207561 conflicts (hard 217561) hit after 217562 conflicts
c [quatres-9] found 4231 quaternary clauses 43% in total
c [quatres-9-1] removed 10 duplicate quaternary clauses
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 35 single-self-subsuming ternary resolvents
c [quatres-9-2] added 46 quaternary resolvents
c [ternres-9] limit 13077248 with penalty 0 = 0 + 0
c [ternres-9] all 1651 free variables schedulable
c [ternres-9] 448 ternary resolvents (11 bin, 437 trn)
c [ternres-9] fully completed ternary resolution
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 136 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 1651 variables 100%
c [elim-11] limit of 261544964 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 14 variables 1% in round 1 in 2110499 steps
c [elim-11-1] backward subsumption/strengthening limit 2110400
c [elim-11-1-1] backward checking 59 touched variables 4%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 0 clauses in 92570 steps
c [elim-11-1] rescheduled 3 variables 0% by backward subsumption
c [elim-11-2] eliminated 3 variables 0% in round 2 in 413 steps
c [elim-11-2] backward subsumption/strengthening limit 400
c [elim-11-2-1] backward checking 6 touched variables 0%
c [elim-11-2-1] incomplete backward checking 5 remain 83%
c [elim-11-2] subsumed 2 and strengthened 0 clauses in 461 steps
c [elim-11-2] rescheduled 4 variables 0% by backward subsumption
c [elim-11-3] eliminated 2 variables 0% in round 3 in 47968 steps
c [elim-11-3] backward subsumption/strengthening limit 47900
c [elim-11-3-1] backward checking 5 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 0 and strengthened 0 clauses in 6266 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 19 = 1% variables out of 1651 scheduled
c [bca-9] limit of 10000000 steps and 18333 added (scaled 2)
c [bca-9] 460 out of 3266 literals actually usable 14%
c [bca-9] added 0 blocked clauses in 45274 steps
c [score-distribution-12] 1511 pos 92.59%, 121 min 7.41%, 0 zero 0.00%
c [score-distribution-12] 1029 different 63.05% out of total 1632 variables
c [simplification-12] removed 19 variables 1.2% (1632 remain 22%)
c [simplification-12] removed 74 irredundant clauses 0.8% (8872 remain 31%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 34500 = 69000 / 2
c [simplification-12] new conflict interval 103500
c [simplification-12] penalized conflict interval 103500 = 1 * 103500
c [simplification-12] hard conflict limit 372812 (soft 321062 + delta 51750)
c [simplification-12] new conflict limit 321062 (hard 372812)
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 -   47.3    1632     8872    236812   30879   2041  3021   12    15    6  79%    220   -2   13   12  109%
c -   53.9    1632     8872    270786   29586   2076  3025   15    22    9  68%    545    4   12   13   93%
c -   60.2    1632     8872    312049   33587   2092  3030   11    13    7  85%    769   -3   12   12   96%
c 
c [simplification-13] limit 321062 conflicts (hard 372812) hit after 323759 conflicts
c [quatres-10] found 4339 quaternary clauses 38% in total
c [quatres-10-1] removed 2 duplicate quaternary clauses
c [quatres-10-2] added 15 single-self-subsuming ternary resolvents
c [quatres-10-2] added 18 quaternary resolvents
c [ternres-10] limit 20592696 with penalty 0 = 0 + 0
c [ternres-10] all 1632 free variables schedulable
c [ternres-10] 253 ternary resolvents (7 bin, 246 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 514817 penalty 3 = 3 + 0
c [gauss-4] extracted 2470 xors of average arity 3.1
c [gauss-4] connected 7690 occurrences of 557 variables (average 13.8)
c [gauss-4] limit 514817 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-4] limit 514817 penalty 2 = 2 + 0 boost 1
c [treelook-4] scheduled 3264 literals 100%
c [treelook-4] scheduling used 168465 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 514817 penalty 2 = 2 + 0 boost 1
c [treelook-4] used 528961 steps
c [treelook-4] 3177 literals remain 97%
c [treelook-4] 1632 variables remain to probed next time 100%
c [decomp-31] removed 1 variables
c [treelook-4] removed 1 variables, found 2725 hbrs
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 268 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 1631 variables 100%
c [block-5] limit of 25740871 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 0 blocked clauses
c [cce-9] limit of 51481742 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 1 clauses out of 48 (2%) of length 7
c [cce-9-1] eliminated 2 clauses out of 211 (1%) of length 6
c [cce-9-1] eliminated 19 clauses out of 989 (2%) of length 5
c [cce-9-1] eliminated 35 clauses out of 2504 (1%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 57 large clauses in 2473380 steps
c [cce-9-1] allowing another 1236690 steps for small clauses
c [cce-9-1] scheduling 3048 clauses = 1877 binary + 1171 ternary
c [cce-9-1] tried to eliminate 3048 small clauses 100%
c [cce-9-1] eliminated 17 binary clauses 1%
c [cce-9-1] eliminated 18 ternary clauses 2%
c [cce-9-1] eliminated 35 small clauses 1%
c [cce-9-1] eliminated 35 small clauses in 3366399 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 92 covered clauses in round 1
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] allowing another 1187911 steps for small clauses
c [cce-9-2] scheduling 3013 clauses = 1860 binary + 1153 ternary
c [cce-9-2] tried to eliminate 3013 small clauses 100%
c [cce-9-2] eliminated 1 binary clauses 0%
c [cce-9-2] eliminated 1 small clauses 0%
c [cce-9-2] eliminated 1 small clauses in 3258224 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 1 covered clauses in round 2
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] allowing another 1187336 steps for small clauses
c [cce-9-3] scheduling 3012 clauses = 1859 binary + 1153 ternary
c [cce-9-3] tried to eliminate 3012 small clauses 100%
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 0 covered clauses in round 3
c [cce-9] eliminated 93 covered clauses in TOTAL during 3 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 1631 variables 100%
c [elim-12] limit of 411853939 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 10 variables 1% in round 1 in 2068243 steps
c [elim-12-1] backward subsumption/strengthening limit 2068200
c [elim-12-1-1] backward checking 75 touched variables 5%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 95303 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 10 = 1% variables out of 1631 scheduled
c [elim-12] 10 < 1/100 * 1631 = 16 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 7722261 penalty 3 = 3 + 0
c [sweep-5-1] 96 pos 28.7% + 239 neg 71.3% = 335 sched 20.7% ret 1286
c [sweep-5-1] 6178933 steps 65 queries 9.17 avg class size
c [sweep-5-1] 2565 decisions 64 SAT calls 69.98 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 354 pos 21.8% + 1267 neg 78.2% = 1621 sched 100.0% ret 0
c [sweep-5-2] 2068767 steps 8 queries 302.88 avg class size
c [sweep-5-2] 596 decisions 7 SAT calls 202.29 avg env size
c [sweep-5-2] 1539 variables remain 95% (82 retained 5%)
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (2 rounds, 71 queries)
c [score-distribution-13] 1604 pos 98.95%, 17 min 1.05%, 0 zero 0.00%
c [score-distribution-13] 1043 different 64.34% out of total 1621 variables
c [simplification-13] removed 11 variables 0.7% (1621 remain 22%)
c [simplification-13] removed 111 irredundant clauses 1.3% (8761 remain 31%)
c [simplification-13] maximum reduction of 1% = max (1%, 1%)
c [simplification-13] geometric conflict interval increment 51750 = 103500 / 2
c [simplification-13] new conflict interval 155250
c [simplification-13] penalized conflict interval 155250 = 1 * 155250
c [simplification-13] hard conflict limit 556634 (soft 479009 + delta 77625)
c [simplification-13] new conflict limit 479009 (hard 556634)
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 -   66.4    1621     8761    347153   33289   2348  5492   11    14    9  83%    875   -2   11   12   88%
c -   73.2    1621     8761    386939   34386   2377  5495   15    20    7  71%    943    5   14   12  114%
c -   80.1    1621     8761    425278   33760   2413  5497   13    17   10  75%    979   -0   17   13  139%
c -   88.3    1621     8761    466416   35629   2433  5499   16    22   11  73%   1000    5   18   13  135%
c 
c [simplification-14] limit 479009 conflicts (hard 556634) hit after 480640 conflicts
c [quatres-11] found 4602 quaternary clauses 32% in total
c [quatres-11-1] removed 1 duplicate quaternary clauses
c [quatres-11-2] added 22 single-self-subsuming ternary resolvents
c [quatres-11-2] added 19 quaternary resolvents
c [ternres-11] limit 32318769 with penalty 0 = 0 + 0
c [ternres-11] all 1621 free variables schedulable
c [ternres-11] 109 ternary resolvents (2 bin, 107 trn)
c [ternres-11] fully completed ternary resolution
c [basicprobe-4] limit 161593845 penalty 0 = 0 + 0
c [basicprobe-4-0] 1054 sched 65%, 5 failed, 0 lifted, 950 hbrs
c [decomp-35] removed 6 variables
c [basicprobe-4-1] 1050 sched 65%, 2 failed, 0 lifted, 38 hbrs
c [decomp-36] removed 2 variables
c [basicprobe-4-2] 1049 sched 65%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-2] fully completed probing
c [basicprobe-4-2] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-4-2] removed 8 variables, found 988 hbrs
c [bate-3] eliminated 3 asymmetric tautologies during probing
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 281 transitive binary clauses
c [cce-10] limit of 161593845 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 2 clauses out of 210 (1%) of length 6
c [cce-10-1] eliminated 9 clauses out of 957 (1%) of length 5
c [cce-10-1] eliminated 15 clauses out of 2462 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 26 large clauses in 2242155 steps
c [cce-10-1] allowing another 1121077 steps for small clauses
c [cce-10-1] scheduling 3803 clauses = 1860 binary + 1943 ternary
c [cce-10-1] tried to eliminate 3803 small clauses 100%
c [cce-10-1] eliminated 2 binary clauses 0%
c [cce-10-1] eliminated 8 ternary clauses 0%
c [cce-10-1] eliminated 10 small clauses 0%
c [cce-10-1] eliminated 10 small clauses in 3200753 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 36 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 1109214 steps for small clauses
c [cce-10-2] scheduling 3793 clauses = 1858 binary + 1935 ternary
c [cce-10-2] tried to eliminate 3793 small clauses 100%
c [cce-10-2] completed small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 36 covered clauses in TOTAL during 2 rounds
c [cce-10] 36 < 1/100 * 8714 = 87 considered unsuccessful
c [bca-10] limit of 10000000 steps and 17945 added (scaled 2)
c [bca-10] 344 out of 3228 literals actually usable 11%
c [bca-10] added 0 blocked clauses in 49018 steps
c [score-distribution-14] 1566 pos 97.09%, 47 min 2.91%, 0 zero 0.00%
c [score-distribution-14] 1244 different 77.12% out of total 1613 variables
c [simplification-14] removed 8 variables 0.5% (1613 remain 21%)
c [simplification-14] removed 83 irredundant clauses 0.9% (8678 remain 31%)
c [simplification-14] maximum reduction of 1% = max (0%, 1%)
c [simplification-14] geometric conflict interval increment 77625 = 155250 / 2
c [simplification-14] new conflict interval 232875
c [simplification-14] penalized conflict interval 232875 = 1 * 232875
c [simplification-14] hard conflict limit 829952 (soft 713515 + delta 116437)
c [simplification-14] new conflict limit 713515 (hard 829952)
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 -   96.2    1613     8678    508299   37516   2570  6067   13    17    7  77%   1011    0   18   13  137%
c -  103.9    1613     8678    551457   39506   2612  6074   16    21    8  76%   1017    4   18   13  138%
c i  109.4    1612     8678    583547   66346   2641  6084   10    11   17  86%   1020   -5    5   13   43%
c -  111.6    1612     8678    593589   40803   2644  6084   14    18    8  77%  -4754    2   10   13   77%
c -  118.9    1612     8678    637158   42552   2663  6085   11    13   11  84%  -1948   -2   13   12  108%
c i  122.3    1611     8678    655894   59873   2668  6088   15    20   15  73%  -1209    4   12   13   89%
c -  126.6    1611     8678    677335   42553   2676  6088   12    15   12  84%  -1414   -2   12   13   88%
c -  135.6    1611     8678    722909   44241   2690  6089   12    15   12  80%   -192   -1   12   13   92%
c 
c [simplification-15] limit 713515 conflicts (hard 829952) hit after 740802 conflicts
c [quatres-12] found 4545 quaternary clauses 32% in total
c [quatres-12-2] added 24 single-self-subsuming ternary resolvents
c [quatres-12-2] added 16 quaternary resolvents
c [ternres-12] limit 54395594 with penalty 0 = 0 + 0
c [ternres-12] all 1611 free variables schedulable
c [ternres-12] 67 ternary resolvents (2 bin, 65 trn)
c [ternres-12] fully completed ternary resolution
c [card-5] limit 1699862 penalty 4 = 4 + 0
c [card-5] found 318 at-most-one constraints of average size 3.1
c [card-5] found 58 at-most-two constraints of average size 4.1
c [card-5] using previous limit 1699862 for elimination
c [card-5] 375 out of 376 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] generated 8 at-most-one constraints, 3 used 38%
c [card-5] exported 7 binary clauses, 2.3 per/constraint
c [decomp-37] removed 4 variables
c [simpleprobe-5] all 1609 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 0 variables, found 1413 hbrs, 0 units
c [unhide-5] limit 679944 with penalty 4 = 4 + 0
c [unhide-5-5] 0 units, 0 failed, 156 tauts, 0 hbrs, 16960 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 242 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 1609 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 14 variables 1% in round 1 in 1980690 steps
c [elim-13-1] backward subsumption/strengthening limit 1980600
c [elim-13-1-1] backward checking 88 touched variables 5%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 2 clauses in 92640 steps
c [elim-13-1] rescheduled 6 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 57618 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 14 = 1% variables out of 1609 scheduled
c [elim-13] 14 < 1/100 * 1609 = 16 considered unsuccessful
c [score-distribution-15] 1528 pos 95.80%, 67 min 4.20%, 0 zero 0.00%
c [score-distribution-15] 1208 different 75.74% out of total 1595 variables
c [simplification-15] removed 16 variables 1.0% (1595 remain 21%)
c [simplification-15] removed 112 irredundant clauses 1.3% (8566 remain 30%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 116437 = 232875 / 2
c [simplification-15] new conflict interval 349312
c [simplification-15] penalized conflict interval 349312 = 1 * 349312
c [simplification-15] hard conflict limit 1264770 (soft 1090114 + delta 174656)
c [simplification-15] new conflict limit 1090114 (hard 1264770)
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 -  144.3    1595     8566    773778   43887   2614  6765   10    12   10  83%    464   -1   11   11  100%
c i  148.6    1594     8566    801713   64537   2681  6780    9    10   12  89%    659   -3    5   11   49%
c -  153.1    1593     8566    819770   43821   2692  6780   15    21   12  73%  -1011    6   14   12  122%
c -  162.4    1593     8566    865408   44669   2707  6781   12    14   11  84%     10   -1   14   12  116%
c -  171.5    1593     8566    910221   45305   2725  6783   15    20   12  76%    512    4   13   13  104%
c -  180.6    1593     8566    955892   48011   2729  6783   12    14    9  89%    769   -2   10   13   81%
c -  189.7    1593     8566   1002939   48681   2748  6784   13    16   13  82%    900    1   18   13  142%
c -  197.2    1593     8566   1049005   49472   2771  6787   10    12    9  86%    962   -3    9   12   73%
c i  203.1    1592     8566   1085696   81475   2802  6794   11    13   15  81%    989   -2   11   12   88%
c -  205.4    1592     8566   1096571   50552   2810  6795   14    18   12  76%  -2824    2   17   13  132%
c i  211.5    1591     8566   1132235   80570   2878  6814    8     9   17  85%  -1209   -6    5   12   40%
c -  215.0    1579     8566   1148889   53303   2896  6815   10    11   12  85%  -1281   -3   10   11   87%
c i  216.1    1578     8566   1155636   59462   2904  6816   15    21   12  69%  -1055    7   18   12  157%
c -  223.6    1578     8566   1196435   53677   2919  6817   13    18   12  74%   -291    3   16   12  132%
c 
c [simplification-16] limit 1090114 conflicts (hard 1264770) hit after 1213010 conflicts
c [quatres-13] found 4633 quaternary clauses 29% in total
c [quatres-13-1] removed 5 duplicate quaternary clauses
c [quatres-13-2] added 42 single-self-subsuming ternary resolvents
c [quatres-13-2] added 43 quaternary resolvents
c [ternres-13] limit 98292245 with penalty 0 = 0 + 0
c [ternres-13] all 1578 free variables schedulable
c [ternres-13] 371 ternary resolvents (13 bin, 358 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-39] removed 17 variables
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 243 transitive binary clauses
c [transred-13] found 10 units
c [cce-11] limit of 245730613 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 2 clauses out of 21 (10%) of length 16
c [cce-11-1] eliminated 1 clauses out of 200 (0%) of length 6
c [cce-11-1] eliminated 22 clauses out of 837 (3%) of length 5
c [cce-11-1] eliminated 64 clauses out of 2365 (3%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 89 large clauses in 2559831 steps
c [cce-11-1] allowing another 1279915 steps for small clauses
c [cce-11-1] scheduling 2867 clauses = 1706 binary + 1161 ternary
c [cce-11-1] tried to eliminate 2867 small clauses 100%
c [cce-11-1] eliminated 9 binary clauses 1%
c [cce-11-1] eliminated 13 ternary clauses 1%
c [cce-11-1] eliminated 22 small clauses 1%
c [cce-11-1] eliminated 87 small clauses in 3385217 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 176 covered clauses in round 1
c [cce-11-2] eliminated 1 clauses out of 2301 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 1 large clauses in 2471035 steps
c [cce-11-2] allowing another 1235517 steps for small clauses
c [cce-11-2] scheduling 2845 clauses = 1697 binary + 1148 ternary
c [cce-11-2] tried to eliminate 2845 small clauses 100%
c [cce-11-2] eliminated 1 binary clauses 0%
c [cce-11-2] eliminated 1 small clauses 0%
c [cce-11-2] eliminated 1 small clauses in 3323422 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 2 covered clauses in round 2
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] allowing another 1235440 steps for small clauses
c [cce-11-3] scheduling 2844 clauses = 1696 binary + 1148 ternary
c [cce-11-3] tried to eliminate 2844 small clauses 100%
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 0 covered clauses in round 3
c [cce-11] eliminated 178 covered clauses in TOTAL during 3 rounds
c [score-distribution-16] 1501 pos 95.73%, 67 min 4.27%, 0 zero 0.00%
c [score-distribution-16] 1225 different 78.12% out of total 1568 variables
c [simplification-16] removed 10 variables 0.6% (1568 remain 21%)
c [simplification-16] removed 398 irredundant clauses 4.6% (8168 remain 29%)
c [simplification-16] maximum reduction of 5% = max (1%, 5%)
c [simplification-16] large reduction 5% >= 5% limit
c [simplification-16] next conflict interval 12130 = min (1213010/100, 349312)
c [simplification-16] penalized conflict interval 12130 = 1 * 12130
c [simplification-16] hard conflict limit 1235140 (soft 1225140 + delta 10000)
c [simplification-16] new conflict limit 1225140 (hard 1235140)
c 
c [simplification-17] limit 1225140 conflicts (hard 1235140) hit after 1225143 conflicts
c [quatres-14] found 5088 quaternary clauses 26% in total
c [quatres-14-1] removed 8 duplicate quaternary clauses
c [quatres-14-2] added 88 single-self-subsuming ternary resolvents
c [quatres-14-2] added 26 quaternary resolvents
c [ternres-14] limit 99330161 with penalty 0 = 0 + 0
c [ternres-14] all 1568 free variables schedulable
c [ternres-14] 1812 ternary resolvents (22 bin, 1790 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-40] removed 2 variables
c [treelook-5] limit 4966508 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 3132 literals 100%
c [treelook-5] scheduling used 238555 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 4966508 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 2826786 steps
c [treelook-5] fully completed tree based probing
c [decomp-41] removed 2 variables
c [treelook-5] removed 13 variables, found 8017 hbrs
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 597 transitive binary clauses
c [cce-12] limit of 496650807 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 7 clauses out of 803 (1%) of length 5
c [cce-12-1] eliminated 9 clauses out of 2264 (0%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 16 large clauses in 2320659 steps
c [cce-12-1] allowing another 1160329 steps for small clauses
c [cce-12-1] scheduling 2827 clauses = 1675 binary + 1152 ternary
c [cce-12-1] tried to eliminate 2827 small clauses 100%
c [cce-12-1] eliminated 2 ternary clauses 0%
c [cce-12-1] eliminated 2 small clauses 0%
c [cce-12-1] eliminated 2 small clauses in 3173452 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 18 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 1156578 steps for small clauses
c [cce-12-2] scheduling 2825 clauses = 1675 binary + 1150 ternary
c [cce-12-2] tried to eliminate 2825 small clauses 100%
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 18 covered clauses in TOTAL during 2 rounds
c [cce-12] 18 < 1/100 * 8099 = 80 considered unsuccessful
c [bca-11] limit of 10000000 steps and 16751 added (scaled 2)
c [bca-11] 321 out of 3108 literals actually usable 10%
c [bca-11] added 4 blocked clauses in 73288 steps
c [score-distribution-17] 1477 pos 95.11%, 76 min 4.89%, 0 zero 0.00%
c [score-distribution-17] 1149 different 73.99% out of total 1553 variables
c [simplification-17] removed 15 variables 1.0% (1553 remain 21%)
c [simplification-17] removed 87 irredundant clauses 1.1% (8081 remain 29%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 174656 = 349312 / 2
c [simplification-17] new conflict interval 523968
c [simplification-17] penalized conflict interval 523968 = 1 * 523968
c [simplification-17] hard conflict limit 2011095 (soft 1749111 + delta 261984)
c [simplification-17] new conflict limit 1749111 (hard 2011095)
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 -  235.1    1553     8081   1248043   50572   5183 12526   17    23    9  71%    426    7   14   13  108%
c i  236.9    1552     8081   1260097   60441   5223 12531   10    12   12  84%    526   -5    6   13   50%
c -  244.9    1531     8081   1299701   52827   5240 12531   13    16   10  79%   -154   -0   13   13  104%
c -  255.4    1531     8081   1350964   53925   5274 12536   14    19   13  77%    485    2   14   13  105%
c i  260.5    1530     8081   1380852   79571   5303 12543   11    14   17  81%    682   -3    7   13   56%
c i  264.6    1508     8081   1401348   96807   5334 12550   11    13   25  86%   -628   -3    8   13   66%
c -  265.4    1486     8081   1404492   56214   5336 12550   11    13   14  86%   -845   -3   13   13  103%
c i  271.1    1485     8081   1436465   82360   5405 12563    9    11   16  88%   -133   -5    7   12   54%
c i  272.6    1463     8081   1443269   87772   5425 12566   10    12   20  86%   -521   -3    7   12   61%
c -  275.8    1439     8081   1458762   58120   5429 12567   14    17   13  80%   -281    3   17   12  142%
c -  286.0    1439     8081   1511030   59044   5455 12570   13    16   15  82%    436    1   12   13   99%
c i  295.1    1438     8081   1555234   96071   5492 12576   15    18   24  81%    725    3   17   12  135%
c i  297.6    1433     8081   1565179  103382   5521 12583   10    12   26  88%   -760   -3    6   12   52%
c -  298.2    1408     8081   1567903   60926   5521 12584   12    14   16  86%   -828   -1   12   12   96%
c i  298.6    1407     8081   1570268   63025   5521 12584   12    14   12  84%   -772   -1   12   12  101%
c i  304.5    1405     8081   1606349   92911   5561 12595    8    10   20  88%    -59   -4    6   11   53%
c i  304.6    1386     8081   1607066   93492   5568 12600    9    10   20  87%   -329   -4    8   11   71%
c i  305.1    1363     8081   1609077   95137   5574 12604    9    11   22  87%   -534   -3    8   11   71%
c i  306.9    1338     8081   1617405  101140   5600 12612    9    10   22  89%   -412   -3    7   11   65%
c i  307.3    1333     8081   1619115  102534   5617 12620    9    10   22  88%   -479   -3    7   11   59%
c i  308.6    1290     8081   1624733  107436   5630 12623   12    14   28  85%   -403    1    9   11   83%
c i  308.8    1266     8081   1625633  108094   5643 12627   11    13   28  85%   -435    0    7   11   66%
c -  308.8    1244     8081   1625672   63249   5643 12627   11    13   13  85%   -436    0    8   11   70%
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  309.9    1243     8081   1632196   68509   5666 12631   10    12   16  85%   -342   -1    7   11   59%
c i  311.4    1228     8081   1641458   75826   5685 12637   10    11   17  88%   -253   -2    7   11   65%
c i  313.1    1192     8081   1652650   84012   5702 12644    9    10   19  87%   -176   -3    6   11   55%
c i  313.1    1183     8081   1652804   84102   5709 12648    9    10   19  88%   -198   -3    6   11   56%
c i  315.1    1153     8081   1663277   91698   5743 12663    8     9   19  89%   -150   -3    6   11   60%
c i  315.4    1038     8081   1664833   92716   5770 12670    8     9   19  89%   -248   -3    5   10   51%
c i  315.4     612     8081   1664840   92718   5770 12672    8     9   19  89%   -248   -3    5   10   50%
c i  315.4     462     8081   1664844   92717   5771 12674    8     9   19  89%   -249   -3    5   10   49%
c 0  315.4     291     8081   1664844   92717   5771 12674    8     9   19  89%   -249   -3    5   10   49%
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: 63 basic ate = 60 trn 95% + 3 lrg 5% in 3 updates
c bcas: 11 count, 183 added (25 skipped), 331536 steps
c bkwd: tried 33798 clauses, 67483 lits, 2.00 lits/clause
c bkwd: checked 14159759 occs, 418.95 occs/clause, 209.83 occs/lit
c bkwd: subsumed 1 binary, 11 ternary, 15 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 144 large (0% self)
c blkd: 5 bces, 842 removed, 278855 resolutions, 737846 steps
c blkd: 982 blocking literals 6%, 0 pure
c bump: 1662751 bumped seen, 154070815 lits 92.7 on average
c card: 5 count, 0 units, 22 am1, 9322509 steps
c card: 80 rescheduled, 728 eliminated, 34455 resolved, 4687 subsumed
c card: 1544 at-most-one constraints found, average size 3.09
c card: 1544 at-most-one constraints used 100%, average size 3.09
c card: 58 at-most-two constraints found, average size 4.07
c card: 57 at-most-two constraints used 98%, average size 4.07
c cces: 12 cces, 3207 eliminated, 2430 ate 76%, 777 abce 24%
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: 106318 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 104 gcs, 0 rescored clauses, 874 rescored vars
c dcps: 41 decompositions, 820 equivalent 11%
c deco: 1 decision-only clauses 0%, 43% reduction
c decs: 2771531 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 7319651 push, 7311966 pop (7311966 dec 100%)
c dsch: 194646211 swaps, 0 down, 115615565 up
c elms: 13 elims, 4633 eliminated 60%, 13 pure 0%
c elms: 34 rounds, 2.6 rounds/bve
c elms: 4525 small 98%, 95 large 2%
c elms: 23303 tried small, 4525 succeeded 19%, 18778 failed 81%
c elms: 1050 subsumed, 1856 strengthened, 560 blocked
c elms: 796082 copies, 954997 resolutions, 1078654 ipos
c elms: 369909 subchks, 1026452 strchks
c gaus: 4 extractions, 14792 extracted, 3.1 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 3213618 steps, 1606809 extr 50%, 589320 elim 18%
c glue: 12.5 orig avg, 12.5 real avg, 3.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 34554 = 16305 simple 47% + 14992 trn 43% + 3257 lrg 9%, 425 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1662751 clauses, 30.6 length
c lrnd: 50903352 lits = 112149212 orig - 61245860 removed 55%
c lrnd: 381401 uips 23%, 1171686 flips 70%
c mins: 1655203 mins 100%, 78 bin 0%, 7469 size 0%
c mins: 151331483 poisoned searches, 11757228 hits, 8% hit rate
c mins: 250017572 used twice searches, 8161919 hits, 3% hit rate
c move: moved 1756, 710 bin 40%, 1046 trn 60%
c otfs: 3655 driving 25%, 11037 restarting 75%
c otfs: str 14692, 14441 red 98%, 251 irr 2%
c otfs: str 14692, 0 bin 0%, 119 trn 1%, 14573 lrg 99%
c otfs: sub 69, 69 red 100%, 0 irr 0%
c otfs: sub 69, 0 bin 0%, 3 trn 4%, 66 lrg 96%
c phas: 2 computed, 2723 set, 390 pos (14%), 2333 neg (86%)
c prbs: 4 basic, 22805 probed, 77 failed, 6 lifted
c prbs: 5 simple, 29193 probed, 198 failed, 673 eqs
c prbs: 5 treelook, 3279 probed, 12 failed, 0 lifted
c prom: 528228 locked 8% out of 6448238 tried
c prps: 335108478 props, 121 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 14 count, 635 quat, 361 self1, 12 self2, 40 dup
c redc: 14939 clauses 11%, 142123 tried 9%, 2 sat 0%
c redc: 19719 lits 1%, 1557663 tried 1%, 2 sat 0%
c redc: 466 times jump level reduced, 1.9 levels on average
c reds: 35 count, 47567.0 conflicts per reduce
c reds: 0 memlim 0%, 35 arith 100%
c reds: 1172594 collected 90%, 132992 retired 10%
c rmbd: 835 removed, 835 red 100%
c rsts: 28503 restarts 97%, 1023 skipped 3%
c rsts: 1023 saturating 100%, 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: 17 count, 17 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 1662751 count (1107774 tried 0.7), 223287 sub out of 1660628 (13.4%)
c swps: 5 count, 7 rounds, 349 queries (49.9/round)
c swps: 350 sat calls, 4 unsat (4.5% success rate)
c swps: 8358 decisions 23.9, 1562 conflicts 4.5
c swps; 53.8 avg class size, 49.0 avg environment size
c swps: 0 failed, 4 impls, 2 equivs
c swp0: 113 type 0 queries, 15 unsat (13.3%), 112 sat (99.1%)
c swp1: 236 type 1 queries, 34 unsat (14.4%), 235 sat (99.6%)
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: 8870675 calls to obtain time
c tops: 1985 fixed 26%, 32 its, 52026.38 confs/it
c trds: 14 transitive reductions, 3485 removed, 12 failed
c trds: 41119 nodes, 61795 edges, 4855655 steps
c trim: 1157556 words, 4.4 MB
c trnr: 14 count, 76 bin, 3984 trn, 62641692 steps
c unhd: 5 count, 5 rounds, 2076688 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 2206 tauts, 116 bin 5%, 202 trn 9%, 24 lrg 1%
c unhd: 2206 tauts, 1864 stamp 84%, 2175 red 99%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 72213 str, 0 bin 0%, 210 trn 0%, 72003 lrg 100%, 71518 red 99%
c vars: 291 remaining 4% and 7438 removed 96% out of 7729
c vars: 1985 fixed 26%, 4633 eliminated 60%, 820 equivalent 11%
c vsts: 14277033541 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 42.7 search visits per propagation, 8564.6 per conflict
c wchs: 4233073264 pushed, 4037155 enlarged, 240 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1661263       1172594        132992      79968919      18981274       1115105
c 
c  0 0         42364   3      3844   0         0   0  41296912  52   6037861  32    238003  21     1.0
c  1 5         46993   3     22015   2      7438   6  12079432  15<  2740094  14    136096  12     0.5
c  2 6        292604  18    190863  16     23300  18  18622807  23   6033890  32<   386220  35<    2.2
c  3 9        703204  42<   521481  44<    37582  28<  6461020   8   3201514  17    270734  24     4.4
c  4 14       442752  27    337827  29     41031  31   1227637   2    785204   4     68296   6     3.1
c  5 21       112617   7     81761   7     19300  15    230034   0    151854   1     12879   1     1.6
c  6 30        17019   1     12196   1      3514   3     42143   0     25068   0      2327   0     0.4
c  7 41         3032   0      2139   0       669   1      7879   0      5114   0       462   0     0.1
c  8 54          551   0       391   0       121   0       873   0       571   0        76   0     0.0
c  9 69          122   0        76   0        35   0       175   0       102   0        12   0     0.0
c 10 86            5   0         1   0         2   0         7   0         2   0         0   0     0.0
c 
c avg                  3.1           3.3           3.4           0.9           1.5           1.9
c std                  1.1           0.9           1.2           1.1           1.3           1.3
c 
c    5.298   2% bump
c    3.834   1% cce
c    2.157   1% decide
c    1.639   1% elim
c 
c    3.976 < 1% rest (below)
c 
c    1.625   1% probe
c    0.456   0% sweep
c    0.448   0% unhide
c    0.354   0% ternres
c    0.339   0% transred
c    0.281   0% quatres
c    0.156   0% bca
c    0.101   0% gauss
c    0.082   0% block
c    0.079   0% card
c    0.054   0% rescore
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.790   0% preprocessing     8%
c    9.228   3% inprocessing     92%
c ==================================
c   10.018   3% simplifying
c  305.396  97% search
c ==================================
c  315.414 100% all
c 
c       1664844 conflicts,        5278.3 confs/sec
c          1751 ternaries,         950.8 confs/ternary
c           292 binaries,         5701.5 confs/binary
c            32 iterations,      52026.4 confs/iteration
c 
c            35 reductions,          0.1 redus/sec,  47567.0 confs/reduction
c         28503 restarts,           90.4 rests/sec,     58.4 confs/restart
c       2771531 decisions,        8787.0 decis/sec,      1.7 decis/conflict
c     335108478 propagations,  1062440.3 props/sec,    120.9 props/decision
c 
c 315.4 seconds, 29.4 MB
c launch: done
