c launch: /data/cnf/sc2014/app/q_query_3_l45_lambda.cnf.bz2
c host: atom25
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/q_query_3_l45_lambda.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/q_query_3_l45_lambda.cnf.bz2
c no embedded options
c found 'p cnf 32313 161529' header
c read 32313 variables, 161529 clauses, 465707 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 27542 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   27542   151127         0       0      0     0    0     0   11   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 697 at-most-one constraints of average size 4.5
c [card-1] found 5 at-most-two constraints of average size 4.2
c [card-1] using previous limit 2000000 for elimination
c [card-1] 702 out of 702 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 11566 variables
c [simpleprobe-1] all 20747 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 7268 variables
c [simpleprobe-1] 781 variables remain 6% (12698 retained 94%)
c [simpleprobe-1] removed 7268 variables, found 28708 hbrs, 28 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 1301 tauts, 0 hbrs, 324 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 13479 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 7695 variables 57% in round 1 in 4863761 steps
c [elim-1-1] backward subsumption/strengthening limit 4863700
c [elim-1-1-1] backward checking 9456 touched variables 70%
c [elim-1-1-1] incomplete backward checking 6896 remain 73%
c [elim-1-1] subsumed 99 and strengthened 725 clauses in 4863718 steps
c [elim-1-1] rescheduled 1042 variables 8% by backward subsumption
c [elim-1-2] eliminated 10 variables 0% in round 2 in 1649312 steps
c [elim-1-2] backward subsumption/strengthening limit 1649300
c [elim-1-2-1] backward checking 7225 touched variables 54%
c [elim-1-2-1] incomplete backward checking 6658 remain 92%
c [elim-1-2] subsumed 15 and strengthened 68 clauses in 1649338 steps
c [elim-1-2] rescheduled 137 variables 1% by backward subsumption
c [elim-1-3] eliminated 9 variables 0% in round 3 in 67746 steps
c [elim-1-3] backward subsumption/strengthening limit 67700
c [elim-1-3-1] backward checking 6744 touched variables 50%
c [elim-1-3-1] incomplete backward checking 6678 remain 99%
c [elim-1-3] subsumed 33 and strengthened 5 clauses in 67826 steps
c [elim-1] incomplete 56 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 7714 = 57% variables out of 13479 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 54941 negative 96.7% of 56839 except 1898 3.3%
c [phase-count-1] 43389 positive 76.3% of 56839 except 13450 23.7%
c [phase-count-1] less non-negative clauses 1898 than limit 5600 (10.0%)
c [phase-count-1] non-pos/non-neg = 13450/1898 = 7.09 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 5765 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 5765 zero 100.00%
c [score-distribution-1] 1 different 0.02% out of total 5765 variables
c [simplification-1] removed 21453 variables 78.8% (5765 remain 21%)
c [simplification-1] removed 94288 irredundant clauses 62.4% (56839 remain 38%)
c [simplification-1] maximum reduction of 79% = max (79%, 62%)
c [simplification-1] large reduction 79% >= 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    5764    56837        20      13      5  1267    0     0    5  14%      0    0    0    0 24813%
c i    0.8    5763    56830       218     173     30  1271    0     1    5  21%      0    1    3    0 17505%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 3 variables
c [simpleprobe-2] 326 schedulable variables 6%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 315 variables remain 5% (5447 retained 95%)
c [simpleprobe-2] removed 0 variables, found 144 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 11524 literals 100%
c [treelook-1] scheduling used 238134 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300423 steps
c [treelook-1] 11254 literals remain 98%
c [treelook-1] 5758 variables remain to probed next time 100%
c [treelook-1] removed 4 variables, found 1260 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 2844 sched 50%, 68 failed, 0 lifted, 3587 hbrs
c [decomp-6] removed 70 variables
c [basicprobe-1-1] 1936 probes remain 34% after last round
c [basicprobe-1-1] 71 units = 71 failed (100%) + 0 lifted (0%)
c [basicprobe-1-1] removed 73 variables, found 3708 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 5685 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 8 not tried 0% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 91 = 2% variables out of 5685 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 52514 negative 96.5% of 54406 except 1892 3.5%
c [phase-count-2] 40718 positive 74.8% of 54406 except 13688 25.2%
c [phase-count-2] less non-negative clauses 1892 than limit 5400 (10.0%)
c [phase-count-2] non-pos/non-neg = 13688/1892 = 7.23 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 4427 negative 100%
c [score-distribution-2] 819 pos 14.64%, 0 min 0.00%, 4775 zero 85.36%
c [score-distribution-2] 625 different 11.17% out of total 5594 variables
c [simplification-2] removed 169 variables 2.9% (5594 remain 20%)
c [simplification-2] removed 2419 irredundant clauses 4.3% (54406 remain 36%)
c [simplification-2] maximum reduction of 4% = max (3%, 4%)
c [simplification-2] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-2] new conflict interval 4000
c [simplification-2] penalized conflict interval 4000 = 1 * 4000
c [simplification-2] hard conflict limit 15000 (soft 5000 + delta 10000)
c [simplification-2] new conflict limit 5000 (hard 15000)
c 
c [simplification-3] limit 5000 conflicts (hard 15000) hit after 5001 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 870 at-most-one constraints of average size 3.6
c [card-2] found 15 at-most-two constraints of average size 4.5
c [card-2] using previous limit 1000000 for elimination
c [card-2] 885 out of 885 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 4 at-most-one constraints, 1 used 25%
c [card-2] exported 1 binary clauses, 1.0 per/constraint
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 11188 literals 100%
c [treelook-2] scheduling used 239236 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 308905 steps
c [treelook-2] 11029 literals remain 99%
c [treelook-2] 5594 variables remain to probed next time 100%
c [treelook-2] removed 0 variables, found 174 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 454 tauts, 0 hbrs, 1896 literals
c [elim-3] 8 variables 0% will be scheduled this time
c [elim-3] scheduled 8 variables 0%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 824601 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 0 = 0% variables out of 8 scheduled
c [phase-count-3] 52511 negative 96.5% of 54404 except 1893 3.5%
c [phase-count-3] 40690 positive 74.8% of 54404 except 13714 25.2%
c [phase-count-3] less non-negative clauses 1893 than limit 5400 (10.0%)
c [phase-count-3] non-pos/non-neg = 13714/1893 = 7.24 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1881 negative 100%
c [score-distribution-3] 1515 pos 27.08%, 456 min 8.15%, 3623 zero 64.77%
c [score-distribution-3] 988 different 17.66% out of total 5594 variables
c [simplification-3] removed 0 variables 0.0% (5594 remain 20%)
c [simplification-3] removed 2 irredundant clauses 0.0% (54404 remain 36%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 24000
c [simplification-3] penalized conflict interval 24000 = 1 * 24000
c [simplification-3] hard conflict limit 41001 (soft 29001 + delta 12000)
c [simplification-3] new conflict limit 29001 (hard 41001)
c 
c [simplification-4] limit 29001 conflicts (hard 41001) hit after 29001 conflicts
c [basicprobe-2] limit 4654423 penalty 0 = 0 + 0
c [basicprobe-2-0] 1974 sched 35%, 10 failed, 0 lifted, 662 hbrs
c [decomp-10] removed 10 variables
c [basicprobe-2-1] 2502 sched 45%, 9 failed, 0 lifted, 90 hbrs
c [decomp-11] removed 9 variables
c [basicprobe-2-2] 2499 sched 45%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-2-3] 2499 sched 45%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-2-4] 2499 sched 45%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-5] 2058 probes remain 37% after last round
c [basicprobe-2-5] 19 units = 19 failed (100%) + 0 lifted (0%)
c [basicprobe-2-5] removed 19 variables, found 777 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 5575 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 9 blocked clauses
c [block-1] 9 < 1/100 * 54126 = 541 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 168 (1%) of length 9
c [cce-1-1] eliminated 350 clauses out of 544 (64%) of length 7
c [cce-1-1] eliminated 104 clauses out of 4431 (2%) of length 6
c [cce-1-1] eliminated 1678 clauses out of 3487 (48%) of length 5
c [cce-1-1] eliminated 854 clauses out of 4238 (20%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 2987 large clauses in 8916797 steps
c [cce-1-1] allowing another 4458398 steps for small clauses
c [cce-1-1] scheduling 26890 clauses = 7936 binary + 18954 ternary
c [cce-1-1] tried to eliminate 26890 small clauses 100%
c [cce-1-1] eliminated 2540 binary clauses 32%
c [cce-1-1] eliminated 5566 ternary clauses 29%
c [cce-1-1] eliminated 8106 small clauses 30%
c [cce-1-1] eliminated 8106 small clauses in 18164470 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 11093 covered clauses in round 1
c [cce-1-2] eliminated 7 clauses out of 3384 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 7 large clauses in 5727772 steps
c [cce-1-2] allowing another 2863886 steps for small clauses
c [cce-1-2] scheduling 18784 clauses = 5396 binary + 13388 ternary
c [cce-1-2] tried to eliminate 18784 small clauses 100%
c [cce-1-2] eliminated 99 binary clauses 2%
c [cce-1-2] eliminated 2106 ternary clauses 16%
c [cce-1-2] eliminated 2205 small clauses 12%
c [cce-1-2] eliminated 2205 small clauses in 8445061 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 2212 covered clauses in round 2
c [cce-1-3] eliminated 20 clauses out of 194 (10%) of length 7
c [cce-1-3] eliminated 2 clauses out of 4327 (0%) of length 6
c [cce-1-3] eliminated 5 clauses out of 1809 (0%) of length 5
c [cce-1-3] incomplete large round (ACCE)
c [cce-1-3] eliminated 27 large clauses in 3390472 steps
c [cce-1-3] allowing another 1695236 steps for small clauses
c [cce-1-3] scheduling 16579 clauses = 5297 binary + 11282 ternary
c [cce-1-3] tried to eliminate 5129 small clauses 31%
c [cce-1-3] eliminated 209 binary clauses 4%
c [cce-1-3] eliminated 474 ternary clauses 4%
c [cce-1-3] eliminated 683 small clauses 4%
c [cce-1-3] eliminated 683 small clauses in 3390506 steps
c [cce-1-3] incomplete small round (ACCE)
c [cce-1-3] eliminated 710 covered clauses in round 3
c [cce-1] eliminated 14015 covered clauses in TOTAL during 3 rounds
c [bca-1] limit of 10000000 steps and 80704 added (scaled 2)
c [bca-1] 8072 out of 11152 literals actually usable 72%
c [bca-1] added 0 blocked clauses in 43497 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2281 pos 40.9% + 3294 neg 59.1% = 5575 sched 100.0% ret 0
c [sweep-1-1] 1014532 steps 51 queries 620.35 avg class size
c [sweep-1-1] 1313 decisions 50 SAT calls 72.00 avg env size
c [sweep-1-1] 4885 variables remain 88% (690 retained 12%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 50 queries)
c [phase-count-4] 38350 negative 95.6% of 40102 except 1752 4.4%
c [phase-count-4] 29003 positive 72.3% of 40102 except 11099 27.7%
c [phase-count-4] less non-negative clauses 1752 than limit 4000 (10.0%)
c [phase-count-4] non-pos/non-neg = 11099/1752 = 6.34 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 819 negative 100%
c [score-distribution-4] 2191 pos 39.30%, 983 min 17.63%, 2401 zero 43.07%
c [score-distribution-4] 1317 different 23.62% out of total 5575 variables
c [simplification-4] removed 19 variables 0.3% (5575 remain 20%)
c [simplification-4] removed 14302 irredundant clauses 26.3% (40102 remain 27%)
c [simplification-4] maximum reduction of 26% = max (0%, 26%)
c [simplification-4] large reduction 26% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 41001 (soft 31001 + delta 10000)
c [simplification-4] new conflict limit 31001 (hard 41001)
c 
c [simplification-5] limit 31001 conflicts (hard 41001) hit after 31002 conflicts
c [quatres-1] found 4509 quaternary clauses 27% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 32 single-self-subsuming ternary resolvents
c [quatres-1-2] added 566 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 5575 free variables schedulable
c [ternres-1] 7342 ternary resolvents (10 bin, 7332 trn)
c [ternres-1] 1 variables remain 0% (5574 retained 100%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [transred-1] limit 1019827 with penalty 0 = 0 + 0
c [transred-1] removed 1140 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 4 clauses out of 1804 (0%) of length 5
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 4 large clauses in 5450609 steps
c [cce-2-1] allowing another 2725304 steps for small clauses
c [cce-2-1] scheduling 15899 clauses = 5093 binary + 10806 ternary
c [cce-2-1] tried to eliminate 15899 small clauses 100%
c [cce-2-1] eliminated 17 binary clauses 0%
c [cce-2-1] eliminated 8 ternary clauses 0%
c [cce-2-1] eliminated 25 small clauses 0%
c [cce-2-1] eliminated 25 small clauses in 6424458 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 29 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 2737943 steps for small clauses
c [cce-2-2] scheduling 15874 clauses = 5076 binary + 10798 ternary
c [cce-2-2] tried to eliminate 15874 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 29 covered clauses in TOTAL during 2 rounds
c [cce-2] 29 < 1/100 * 40102 = 401 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5575 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 203965460 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 728 variables 13% in round 1 in 12509984 steps
c [elim-4-1] backward subsumption/strengthening limit 12509900
c [elim-4-1-1] backward checking 2108 touched variables 38%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 21 and strengthened 8 clauses in 1537638 steps
c [elim-4-1] rescheduled 82 variables 1% by backward subsumption
c [elim-4-2] eliminated 9 variables 0% in round 2 in 465417 steps
c [elim-4-2] backward subsumption/strengthening limit 465400
c [elim-4-2-1] backward checking 59 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 4 and strengthened 0 clauses in 89662 steps
c [elim-4-2] rescheduled 11 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 97221 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 737 = 13% variables out of 5575 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1899 pos 44.2% + 2396 neg 55.8% = 4295 sched 88.8% ret 543
c [sweep-2-1] 1081321 steps 19 queries 560.74 avg class size
c [sweep-2-1] 1114 decisions 18 SAT calls 157.89 avg env size
c [sweep-2-1] 4078 variables remain 84% (760 retained 16%)
c [decomp-17] removed 1 variables
c [sweep-2-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 1 vars in TOTAL (1 rounds, 18 queries)
c [phase-count-5] 36626 negative 96.0% of 38163 except 1537 4.0%
c [phase-count-5] 27216 positive 71.3% of 38163 except 10947 28.7%
c [phase-count-5] less non-negative clauses 1537 than limit 3800 (10.0%)
c [phase-count-5] non-pos/non-neg = 10947/1537 = 7.12 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 634 negative 100%
c [score-distribution-5] 2087 pos 43.15%, 860 min 17.78%, 1890 zero 39.07%
c [score-distribution-5] 1384 different 28.61% out of total 4837 variables
c [simplification-5] removed 738 variables 13.2% (4837 remain 18%)
c [simplification-5] removed 1939 irredundant clauses 4.8% (38163 remain 25%)
c [simplification-5] maximum reduction of 13% = max (13%, 5%)
c [simplification-5] large reduction 13% >= 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 43002 (soft 33002 + delta 10000)
c [simplification-5] new conflict limit 33002 (hard 43002)
c 
c [simplification-6] limit 33002 conflicts (hard 43002) hit after 33003 conflicts
c [quatres-2] found 4687 quaternary clauses 27% in total
c [quatres-2-2] added 43 single-self-subsuming ternary resolvents
c [quatres-2-2] added 160 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 1 schedulable variables 0%
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 511 at-most-one constraints of average size 3.8
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 511 out of 511 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 250 schedulable variables 5%
c [simpleprobe-3] limit 2206244 penalty 1 = 1 + 0
c [simpleprobe-3] 375 variables remain 8% (4462 retained 92%)
c [simpleprobe-3] removed 0 variables, found 474 hbrs, 0 units
c [unhide-3] limit 55156 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 139 tauts, 0 hbrs, 9438 literals
c [transred-2] limit 1103122 with penalty 0 = 0 + 0
c [transred-2] removed 341 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 4837 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 20 blocked clauses
c [block-2] 20 < 1/100 * 38148 = 381 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 4837 variables 100%
c [elim-5] limit of 22062448 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 22 variables 0% in round 1 in 11988874 steps
c [elim-5-1] backward subsumption/strengthening limit 10073574
c [elim-5-1-1] backward checking 123 touched variables 3%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 2 and strengthened 1 clauses in 149134 steps
c [elim-5-1] rescheduled 11 variables 0% by backward subsumption
c [elim-5-2] eliminated 1 variables 0% in round 2 in 45520 steps
c [elim-5-2] backward subsumption/strengthening limit 45500
c [elim-5-2-1] backward checking 7 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 12638 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 23 = 0% variables out of 4837 scheduled
c [elim-5] 23 < 1/100 * 4837 = 48 considered unsuccessful
c [bca-2] limit of 10000000 steps and 76614 added (scaled 2)
c [bca-2] 6149 out of 9630 literals actually usable 64%
c [bca-2] added 0 blocked clauses in 42767 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1769 pos 43.6% + 2292 neg 56.4% = 4061 sched 84.4% ret 753
c [sweep-3-1] 1092723 steps 51 queries 788.92 avg class size
c [sweep-3-1] 1260 decisions 50 SAT calls 77.30 avg env size
c [sweep-3-1] 3613 variables remain 75% (1201 retained 25%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 50 queries)
c [phase-count-6] 36530 negative 96.0% of 38057 except 1527 4.0%
c [phase-count-6] 27108 positive 71.2% of 38057 except 10949 28.8%
c [phase-count-6] less non-negative clauses 1527 than limit 3800 (10.0%)
c [phase-count-6] non-pos/non-neg = 10949/1527 = 7.17 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 441 negative 100%
c [score-distribution-6] 1877 pos 38.99%, 1225 min 25.45%, 1712 zero 35.56%
c [score-distribution-6] 1260 different 26.17% out of total 4814 variables
c [simplification-6] removed 23 variables 0.5% (4814 remain 17%)
c [simplification-6] removed 106 irredundant clauses 0.3% (38057 remain 25%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 24000
c [simplification-6] new conflict interval 48000
c [simplification-6] penalized conflict interval 48000 = 1 * 48000
c [simplification-6] hard conflict limit 105003 (soft 81003 + delta 24000)
c [simplification-6] new conflict limit 81003 (hard 105003)
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    9.0    4813    38057     50377   46233  14857  4015    9    20   10  42%    540   10    9    4  216%
c -   11.5    4802    38057     66527   22694  14961  4029    9    20   12  45%     24    8    9    5  175%
c 
c [simplification-7] limit 81003 conflicts (hard 105003) hit after 81003 conflicts
c [quatres-3] found 4933 quaternary clauses 23% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 33 single-self-subsuming ternary resolvents
c [quatres-3-2] added 116 quaternary resolvents
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 89 xors of average arity 3.0
c [gauss-2] connected 267 occurrences of 42 variables (average 6.4)
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 [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 149 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 3 clauses out of 166 (2%) of length 9
c [cce-3-1] eliminated 3 clauses out of 331 (1%) of length 8
c [cce-3-1] eliminated 1 clauses out of 170 (1%) of length 7
c [cce-3-1] eliminated 8 clauses out of 4344 (0%) of length 6
c [cce-3-1] eliminated 242 clauses out of 1757 (14%) of length 5
c [cce-3-1] eliminated 432 clauses out of 3131 (14%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 689 large clauses in 6001944 steps
c [cce-3-1] allowing another 3000972 steps for small clauses
c [cce-3-1] scheduling 16998 clauses = 4086 binary + 12912 ternary
c [cce-3-1] tried to eliminate 16998 small clauses 100%
c [cce-3-1] eliminated 196 binary clauses 5%
c [cce-3-1] eliminated 2574 ternary clauses 20%
c [cce-3-1] eliminated 2770 small clauses 16%
c [cce-3-1] eliminated 2770 small clauses in 8992083 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] completed small and large (ACCE)
c [cce-3-1] eliminated 3459 covered clauses in round 1
c [cce-3-2] eliminated 2 clauses out of 163 (1%) of length 9
c [cce-3-2] eliminated 2 clauses out of 328 (1%) of length 8
c [cce-3-2] eliminated 27 clauses out of 1515 (2%) of length 5
c [cce-3-2] eliminated 34 clauses out of 2699 (1%) of length 4
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] eliminated 65 large clauses in 5531748 steps
c [cce-3-2] allowing another 2765874 steps for small clauses
c [cce-3-2] scheduling 14228 clauses = 3890 binary + 10338 ternary
c [cce-3-2] tried to eliminate 10329 small clauses 73%
c [cce-3-2] eliminated 10 binary clauses 0%
c [cce-3-2] eliminated 7 ternary clauses 0%
c [cce-3-2] eliminated 17 small clauses 0%
c [cce-3-2] eliminated 17 small clauses in 6007923 steps
c [cce-3-2] incomplete small round (ACCE)
c [cce-3-2] eliminated 82 covered clauses in round 2
c [cce-3] eliminated 3541 covered clauses in TOTAL during 2 rounds
c [sweep-4] limit 1074243 penalty 0 = 0 + 0
c [sweep-4-1] 1723 pos 47.8% + 1884 neg 52.2% = 3607 sched 75.1% ret 1195
c [sweep-4-1] 1133927 steps 61 queries 382.21 avg class size
c [sweep-4-1] 1224 decisions 54 SAT calls 48.81 avg env size
c [sweep-4-1] 3045 variables remain 63% (1757 retained 37%)
c [decomp-22] removed 6 variables
c [sweep-4-1] removed 6 vars (0 failed, 6 eqs, 13 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 6 vars in TOTAL (1 rounds, 60 queries)
c [phase-count-7] 32225 negative 95.5% of 33749 except 1524 4.5%
c [phase-count-7] 23658 positive 70.1% of 33749 except 10091 29.9%
c [phase-count-7] less non-negative clauses 1524 than limit 3300 (10.0%)
c [phase-count-7] non-pos/non-neg = 10091/1524 = 6.62 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 316 negative 100%
c [score-distribution-7] 2160 pos 45.04%, 1420 min 29.61%, 1216 zero 25.35%
c [score-distribution-7] 1527 different 31.84% out of total 4796 variables
c [simplification-7] removed 6 variables 0.1% (4796 remain 17%)
c [simplification-7] removed 4308 irredundant clauses 11.3% (33749 remain 22%)
c [simplification-7] maximum reduction of 11% = max (0%, 11%)
c [simplification-7] large reduction 11% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 93003 (soft 83003 + delta 10000)
c [simplification-7] new conflict limit 83003 (hard 93003)
c 
c [simplification-8] limit 83003 conflicts (hard 93003) hit after 83003 conflicts
c [quatres-4] found 4854 quaternary clauses 22% in total
c [quatres-4-1] removed 4 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 48 quaternary resolvents
c [ternres-3] limit 2000000 with penalty 1 = 1 + 0
c [ternres-3] all 4796 free variables schedulable
c [ternres-3] 453 ternary resolvents (1 bin, 452 trn)
c [ternres-3] 3121 variables remain 65% (1675 retained 35%)
c [treelook-3] limit 184230 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 6026 literals 63%
c [treelook-3] scheduling used 184501 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 184230 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 185983 steps
c [treelook-3] 5961 literals remain 62%
c [treelook-3] 4305 variables remain to probed next time 90%
c [treelook-3] removed 6 variables, found 659 hbrs
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 152 transitive binary clauses
c [transred-4] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 13 clauses out of 2665 (0%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 13 large clauses in 4447252 steps
c [cce-4-1] allowing another 2223626 steps for small clauses
c [cce-4-1] scheduling 14188 clauses = 3888 binary + 10300 ternary
c [cce-4-1] tried to eliminate 14188 small clauses 100%
c [cce-4-1] eliminated 142 ternary clauses 1%
c [cce-4-1] eliminated 142 small clauses 1%
c [cce-4-1] eliminated 149 small clauses in 5116367 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 162 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 2238179 steps for small clauses
c [cce-4-2] scheduling 14046 clauses = 3888 binary + 10158 ternary
c [cce-4-2] tried to eliminate 14046 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 162 covered clauses in TOTAL during 2 rounds
c [cce-4] 162 < 1/100 * 33503 = 335 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 4789 variables 100%
c [elim-6] limit of 36846122 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 86 variables 2% in round 1 in 10248283 steps
c [elim-6-1] backward subsumption/strengthening limit 10248200
c [elim-6-1-1] backward checking 448 touched variables 9%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 7 clauses in 367238 steps
c [elim-6-1] rescheduled 30 variables 1% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 187663 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 86 = 2% variables out of 4789 scheduled
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 11053830 penalty 0 = 0 + 0
c [sweep-5-1] 1468 pos 48.8% + 1539 neg 51.2% = 3007 sched 63.9% ret 1696
c [sweep-5-1] 4886126 steps 611 queries 48.21 avg class size
c [sweep-5-1] 6092 decisions 539 SAT calls 24.47 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-25] removed 75 variables
c [sweep-5-1] removed 75 vars (0 failed, 75 eqs, 153 impls)
c [sweep-5-2] 2117 pos 45.7% + 2511 neg 54.3% = 4628 sched 100.0% ret 0
c [sweep-5-2] 6003134 steps 570 queries 51.24 avg class size
c [sweep-5-2] 7153 decisions 571 SAT calls 30.53 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-26] removed 8 variables
c [sweep-5-2] removed 8 vars (0 failed, 8 eqs, 19 impls)
c [sweep-5-3] 2112 pos 45.7% + 2508 neg 54.3% = 4620 sched 100.0% ret 0
c [sweep-5-3] 166438 steps 11 queries 1199.55 avg class size
c [sweep-5-3] 315 decisions 10 SAT calls 88.50 avg env size
c [sweep-5-3] 4552 variables remain 99% (68 retained 1%)
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-5] removed 83 vars in TOTAL (3 rounds, 1189 queries)
c [phase-count-8] 31618 negative 95.4% of 33150 except 1532 4.6%
c [phase-count-8] 22984 positive 69.3% of 33150 except 10166 30.7%
c [phase-count-8] less non-negative clauses 1532 than limit 3300 (10.0%)
c [phase-count-8] non-pos/non-neg = 10166/1532 = 6.64 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 1 negative 100%
c [score-distribution-8] 3302 pos 71.47%, 812 min 17.58%, 506 zero 10.95%
c [score-distribution-8] 1690 different 36.58% out of total 4620 variables
c [simplification-8] removed 176 variables 3.7% (4620 remain 17%)
c [simplification-8] removed 599 irredundant clauses 1.8% (33150 remain 22%)
c [simplification-8] maximum reduction of 4% = max (4%, 2%)
c [simplification-8] geometric conflict interval increment 9600 = 48000 / 5
c [simplification-8] new conflict interval 57600
c [simplification-8] penalized conflict interval 57600 = 1 * 57600
c [simplification-8] hard conflict limit 169403 (soft 140603 + delta 28800)
c [simplification-8] new conflict limit 140603 (hard 169403)
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 -   19.4    4620    33150    111660   28465  14751  4598   10    21   12  46%    522    5   10    7  142%
c 
c [simplification-9] limit 140603 conflicts (hard 169403) hit after 140603 conflicts
c [quatres-5] found 5122 quaternary clauses 19% in total
c [quatres-5-1] removed 5 duplicate quaternary clauses
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 35 single-self-subsuming ternary resolvents
c [quatres-5-2] added 85 quaternary resolvents
c [ternres-4] limit 6847804 with penalty 0 = 0 + 0
c [ternres-4] 2998 schedulable variables 65%
c [ternres-4] 1839 ternary resolvents (6 bin, 1833 trn)
c [ternres-4] 169 variables remain 4% (4451 retained 96%)
c [basicprobe-3] limit 34239024 penalty 0 = 0 + 0
c [basicprobe-3-0] 2309 sched 50%, 13 failed, 0 lifted, 701 hbrs
c [decomp-29] removed 13 variables
c [basicprobe-3-1] 2582 sched 56%, 3 failed, 0 lifted, 212 hbrs
c [decomp-30] removed 3 variables
c [basicprobe-3-2] 2609 sched 57%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-3-3] 2609 sched 57%, 0 failed, 0 lifted, 10 hbrs
c [basicprobe-3-4] 2610 sched 57%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-4] fully completed probing
c [basicprobe-3-4] 16 units = 16 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 16 variables, found 937 hbrs
c [bate-1] eliminated 15 asymmetric tautologies during probing
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 311 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 4604 variables 100%
c [block-3] limit of 17119512 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 6 blocked clauses
c [block-3] 6 < 1/100 * 32880 = 328 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 4604 variables 100%
c [elim-7] limit of 136956099 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 30 variables 1% in round 1 in 9743257 steps
c [elim-7-1] backward subsumption/strengthening limit 9743200
c [elim-7-1-1] backward checking 239 touched variables 5%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 1 and strengthened 6 clauses in 183615 steps
c [elim-7-1] rescheduled 30 variables 1% by backward subsumption
c [elim-7-2] eliminated 1 variables 0% in round 2 in 88515 steps
c [elim-7-2] backward subsumption/strengthening limit 88500
c [elim-7-2-1] backward checking 7 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 1 clauses in 11692 steps
c [elim-7-2] rescheduled 4 variables 0% by backward subsumption
c [elim-7-3] eliminated 2 variables 0% in round 3 in 943 steps
c [elim-7-3] backward subsumption/strengthening limit 900
c [elim-7-3-1] backward checking 10 touched variables 0%
c [elim-7-3-1] incomplete backward checking 7 remain 70%
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 1244 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 33 = 1% variables out of 4604 scheduled
c [elim-7] 33 < 1/100 * 4604 = 46 considered unsuccessful
c [bca-3] limit of 10000000 steps and 65176 added (scaled 2)
c [bca-3] 4867 out of 9144 literals actually usable 53%
c [bca-3] added 0 blocked clauses in 66409 steps
c [sweep-6] limit 2054341 penalty 0 = 0 + 0
c [sweep-6-1] 2072 pos 46.0% + 2432 neg 54.0% = 4504 sched 98.5% ret 67
c [sweep-6-1] 2077486 steps 35 queries 433.69 avg class size
c [sweep-6-1] 1249 decisions 34 SAT calls 100.79 avg env size
c [sweep-6-1] 3495 variables remain 76% (1076 retained 24%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 34 queries)
c [score-distribution-9] 2030 pos 44.41%, 2112 min 46.20%, 429 zero 9.39%
c [score-distribution-9] 1408 different 30.80% out of total 4571 variables
c [simplification-9] removed 49 variables 1.1% (4571 remain 17%)
c [simplification-9] removed 812 irredundant clauses 2.4% (32338 remain 21%)
c [simplification-9] maximum reduction of 2% = max (1%, 2%)
c [simplification-9] geometric conflict interval increment 19200 = 57600 / 3
c [simplification-9] new conflict interval 76800
c [simplification-9] penalized conflict interval 76800 = 1 * 76800
c [simplification-9] hard conflict limit 255803 (soft 217403 + delta 38400)
c [simplification-9] new conflict limit 217403 (hard 255803)
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.5    4571    32338    155943   34127  16436  4857   10    21    9  48%    768    2   11    8  128%
c -   31.5    4571    32338    200180   44883  16500  4860   10    20   15  48%    894    2   10    9  110%
c 
c [simplification-10] limit 217403 conflicts (hard 255803) hit after 217406 conflicts
c [quatres-6] found 5379 quaternary clauses 16% in total
c [quatres-6-2] added 32 single-self-subsuming ternary resolvents
c [quatres-6-2] added 73 quaternary resolvents
c [ternres-5] limit 10826063 with penalty 0 = 0 + 0
c [ternres-5] 165 schedulable variables 4%
c [ternres-5] 2002 ternary resolvents (9 bin, 1993 trn)
c [ternres-5] 14 variables remain 0% (4557 retained 100%)
c [card-4] limit 676628 penalty 3 = 3 + 0
c [card-4] found 536 at-most-one constraints of average size 3.7
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 676628 for elimination
c [card-4] 536 out of 536 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 541303 penalty 2 = 2 + 0
c [gauss-3] extracted 104 xors of average arity 3.0
c [gauss-3] connected 312 occurrences of 73 variables (average 4.3)
c [gauss-3] limit 541303 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-4] limit 270651 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 4 failed, 1557 tauts, 0 hbrs, 26253 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 158 transitive binary clauses
c [transred-6] found 2 units
c [cce-5] limit of 27065159 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 10
c [cce-5-1] eliminated 2 clauses out of 109 (2%) of length 9
c [cce-5-1] eliminated 1 clauses out of 357 (0%) of length 8
c [cce-5-1] eliminated 2 clauses out of 144 (1%) of length 7
c [cce-5-1] eliminated 11 clauses out of 4235 (0%) of length 6
c [cce-5-1] eliminated 204 clauses out of 1405 (15%) of length 5
c [cce-5-1] eliminated 218 clauses out of 2594 (8%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 439 large clauses in 5002205 steps
c [cce-5-1] allowing another 2501102 steps for small clauses
c [cce-5-1] scheduling 13713 clauses = 3921 binary + 9792 ternary
c [cce-5-1] tried to eliminate 13713 small clauses 100%
c [cce-5-1] eliminated 226 binary clauses 6%
c [cce-5-1] eliminated 1406 ternary clauses 14%
c [cce-5-1] eliminated 1632 small clauses 12%
c [cce-5-1] eliminated 1714 small clauses in 6483826 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 2153 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 2272762 steps for small clauses
c [cce-5-2] scheduling 12081 clauses = 3695 binary + 8386 ternary
c [cce-5-2] tried to eliminate 12081 small clauses 100%
c [cce-5-2] eliminated 1 binary clauses 0%
c [cce-5-2] eliminated 1 ternary clauses 0%
c [cce-5-2] eliminated 2 small clauses 0%
c [cce-5-2] eliminated 2 small clauses in 4829460 steps
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 2 covered clauses in round 2
c [cce-5-3] completed large round (ACCE)
c [cce-5-3] allowing another 2277118 steps for small clauses
c [cce-5-3] scheduling 12079 clauses = 3694 binary + 8385 ternary
c [cce-5-3] tried to eliminate 12079 small clauses 100%
c [cce-5-3] completed small round (ACCE)
c [cce-5-3] eliminated 0 covered clauses in round 3
c [cce-5] eliminated 2155 covered clauses in TOTAL during 3 rounds
c [score-distribution-10] 1611 pos 35.27%, 2565 min 56.15%, 392 zero 8.58%
c [score-distribution-10] 1127 different 24.67% out of total 4568 variables
c [simplification-10] removed 3 variables 0.1% (4568 remain 17%)
c [simplification-10] removed 2168 irredundant clauses 6.7% (30170 remain 20%)
c [simplification-10] maximum reduction of 7% = max (0%, 7%)
c [simplification-10] large reduction 7% >= 5% limit
c [simplification-10] next conflict interval 2174 = min (217406/100, 76800)
c [simplification-10] penalized conflict interval 2174 = 1 * 2174
c [simplification-10] hard conflict limit 229580 (soft 219580 + delta 10000)
c [simplification-10] new conflict limit 219580 (hard 229580)
c 
c [simplification-11] limit 219580 conflicts (hard 229580) hit after 221205 conflicts
c [quatres-7] found 5227 quaternary clauses 16% in total
c [quatres-7-1] removed 4 duplicate quaternary clauses
c [quatres-7-2] added 47 single-self-subsuming ternary resolvents
c [quatres-7-2] added 106 quaternary resolvents
c [ternres-6] limit 11043481 with penalty 0 = 0 + 0
c [ternres-6] 14 schedulable variables 0%
c [ternres-6] 1075 ternary resolvents (6 bin, 1069 trn)
c [ternres-6] 2 variables remain 0% (4566 retained 100%)
c [decomp-35] removed 1 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 81 transitive binary clauses
c [cce-6] limit of 55217409 steps penalty 0 = 0 + 0
c [cce-6-1] completed large round (ATE)
c [cce-6-1] allowing another 1904205 steps for small clauses
c [cce-6-1] scheduling 13381 clauses = 3693 binary + 9688 ternary
c [cce-6-1] tried to eliminate 13381 small clauses 100%
c [cce-6-1] eliminated 59 ternary clauses 1%
c [cce-6-1] eliminated 59 small clauses 0%
c [cce-6-1] eliminated 59 small clauses in 5201230 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 59 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 1918278 steps for small clauses
c [cce-6-2] scheduling 13322 clauses = 3693 binary + 9629 ternary
c [cce-6-2] tried to eliminate 13322 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 59 covered clauses in TOTAL during 2 rounds
c [cce-6] 59 < 1/100 * 30168 = 301 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 4567 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2208696390 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 48 variables 1% in round 1 in 8875902 steps
c [elim-8-1] backward subsumption/strengthening limit 8875900
c [elim-8-1-1] backward checking 741 touched variables 16%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 8 clauses in 549960 steps
c [elim-8-1] rescheduled 25 variables 1% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 326826 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 48 = 1% variables out of 4567 scheduled
c [sweep-7] limit 1656522 penalty 1 = 1 + 0
c [sweep-7-1] 1626 pos 47.0% + 1833 neg 53.0% = 3459 sched 76.5% ret 1060
c [sweep-7-1] 1773113 steps 68 queries 432.65 avg class size
c [sweep-7-1] 1548 decisions 67 SAT calls 59.28 avg env size
c [sweep-7-1] 2766 variables remain 61% (1748 retained 39%)
c [decomp-36] removed 6 variables
c [sweep-7-1] removed 6 vars (0 failed, 1 eqs, 1 impls)
c [sweep-7] removed 6 vars in TOTAL (1 rounds, 67 queries)
c [score-distribution-11] 1797 pos 39.82%, 2378 min 52.69%, 338 zero 7.49%
c [score-distribution-11] 1192 different 26.41% out of total 4513 variables
c [simplification-11] removed 55 variables 1.2% (4513 remain 16%)
c [simplification-11] removed 439 irredundant clauses 1.5% (29731 remain 20%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 38400 = 76800 / 2
c [simplification-11] new conflict interval 115200
c [simplification-11] penalized conflict interval 115200 = 1 * 115200
c [simplification-11] hard conflict limit 394005 (soft 336405 + delta 57600)
c [simplification-11] new conflict limit 336405 (hard 394005)
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 -   37.7    4513    29731    237956   47633  20115  4689    9    17   10  52%    951   -1    9    9  103%
c -   42.2    4513    29731    273955   50833  20153  4695    9    17   16  53%    982   -2    9    9  102%
c -   46.7    4513    29731    310812   54503  20179  4699   10    18   16  53%   1000   -0    9    9   97%
c 
c [simplification-12] limit 336405 conflicts (hard 394005) hit after 337256 conflicts
c [quatres-8] found 5054 quaternary clauses 13% in total
c [quatres-8-1] removed 7 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 421 single-self-subsuming ternary resolvents
c [quatres-8-2] added 174 quaternary resolvents
c [ternres-7] limit 17904477 with penalty 0 = 0 + 0
c [ternres-7] 1 schedulable variables 0%
c [ternres-7] 2918 ternary resolvents (41 bin, 2877 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-37] removed 1 variables
c [simpleprobe-4] 334 schedulable variables 7%
c [simpleprobe-4] limit 17904477 penalty 2 = 2 + 0
c [decomp-38] removed 2 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 2 variables, found 2304 hbrs, 2 units
c [unhide-5] limit 895223 with penalty 2 = 2 + 0
c [unhide-5-5] 0 units, 0 failed, 154 tauts, 0 hbrs, 11234 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 740 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 4510 variables 100%
c [elim-9] limit of 358089551 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 76 variables 2% in round 1 in 8564676 steps
c [elim-9-1] backward subsumption/strengthening limit 8564600
c [elim-9-1-1] backward checking 744 touched variables 16%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 24 and strengthened 26 clauses in 503325 steps
c [elim-9-1] rescheduled 221 variables 5% by backward subsumption
c [elim-9-2] eliminated 14 variables 0% in round 2 in 745564 steps
c [elim-9-2] backward subsumption/strengthening limit 745500
c [elim-9-2-1] backward checking 108 touched variables 2%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 1 and strengthened 44 clauses in 159791 steps
c [elim-9-2] rescheduled 103 variables 2% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 145523 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 90 = 2% variables out of 4510 scheduled
c [sweep-8] limit 5371343 penalty 0 = 0 + 0
c [sweep-8-1] 1339 pos 49.4% + 1370 neg 50.6% = 2709 sched 61.3% ret 1711
c [sweep-8-1] 5523785 steps 335 queries 62.05 avg class size
c [sweep-8-1] 4371 decisions 335 SAT calls 32.66 avg env size
c [sweep-8-1] 254 variables remain 6% (4166 retained 94%)
c [decomp-39] removed 2 variables
c [sweep-8-1] removed 2 vars (0 failed, 2 eqs, 7 impls)
c [sweep-8] 2 < 1/1000 * 4420 = 4 considered unsuccessful
c [sweep-8] removed 2 vars in TOTAL (1 rounds, 334 queries)
c [score-distribution-12] 2188 pos 49.52%, 1994 min 45.13%, 236 zero 5.34%
c [score-distribution-12] 1281 different 29.00% out of total 4418 variables
c [simplification-12] removed 95 variables 2.1% (4418 remain 16%)
c [simplification-12] removed 325 irredundant clauses 1.1% (29406 remain 19%)
c [simplification-12] maximum reduction of 2% = max (2%, 1%)
c [simplification-12] geometric conflict interval increment 38400 = 115200 / 3
c [simplification-12] new conflict interval 153600
c [simplification-12] penalized conflict interval 153600 = 1 * 153600
c [simplification-12] hard conflict limit 567656 (soft 490856 + delta 76800)
c [simplification-12] new conflict limit 490856 (hard 567656)
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 -   52.6    4418    29406    347806   56877  22150  6091   10    19   11  53%   1010    1   11    9  117%
c -   57.6    4418    29406    385295   59843  22173  6092   10    19   18  54%   1016    0   10   10  104%
c -   62.8    4418    29406    423094   63088  22187  6092    9    14   19  63%   1020   -3    9   10   96%
c i   66.1    4417    29406    447096   85748  22202  6094   10    16   23  62%   1021   -1   10   10  104%
c i   66.2    4416    29406    447728   86217  22220  6100    9    14   23  63%  -1820   -2    5    9   57%
c -   68.5    4416    29406    461490   65859  22221  6100   10    17   19  60%  -4042   -0   11   10  113%
c -   74.8    4416    29406    501710   69506  22235  6101    9    14   19  60%  -1718   -2    9    9   98%
c -   80.2    4416    29406    541738   72650  22260  6108    9    17   19  56%   -465    2   10    9  115%
c 
c [simplification-13] limit 490856 conflicts (hard 567656) hit after 567658 conflicts
c [quatres-9] found 4683 quaternary clauses 10% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 86 single-self-subsuming ternary resolvents
c [quatres-9-2] added 109 quaternary resolvents
c [ternres-8] limit 34371534 with penalty 0 = 0 + 0
c [ternres-8] all 4416 free variables schedulable
c [ternres-8] 4009 ternary resolvents (33 bin, 3976 trn)
c [ternres-8] 26 variables remain 1% (4390 retained 99%)
c [decomp-40] removed 2 variables
c [treelook-4] limit 3437153 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 8125 literals 92%
c [treelook-4] scheduling used 447047 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 3437153 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 2635521 steps
c [treelook-4] fully completed tree based probing
c [treelook-4] removed 10 variables, found 2406 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 713 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 4406 variables 100%
c [block-4] limit of 42964418 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 8 blocked clauses
c [block-4] 8 < 1/100 * 28963 = 289 considered unsuccessful
c [cce-7] limit of 85928836 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 1 clauses out of 103 (1%) of length 9
c [cce-7-1] eliminated 2 clauses out of 179 (1%) of length 7
c [cce-7-1] eliminated 4 clauses out of 4254 (0%) of length 6
c [cce-7-1] eliminated 13 clauses out of 484 (3%) of length 5
c [cce-7-1] eliminated 88 clauses out of 1972 (4%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 108 large clauses in 3715651 steps
c [cce-7-1] allowing another 1857825 steps for small clauses
c [cce-7-1] scheduling 13119 clauses = 3514 binary + 9605 ternary
c [cce-7-1] tried to eliminate 13119 small clauses 100%
c [cce-7-1] eliminated 61 binary clauses 2%
c [cce-7-1] eliminated 207 ternary clauses 2%
c [cce-7-1] eliminated 268 small clauses 2%
c [cce-7-1] eliminated 268 small clauses in 5070236 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 376 covered clauses in round 1
c [cce-7-2] eliminated 7 clauses out of 1884 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 7 large clauses in 3679004 steps
c [cce-7-2] allowing another 1839502 steps for small clauses
c [cce-7-2] scheduling 12851 clauses = 3453 binary + 9398 ternary
c [cce-7-2] tried to eliminate 12851 small clauses 100%
c [cce-7-2] eliminated 1 binary clauses 0%
c [cce-7-2] eliminated 2 ternary clauses 0%
c [cce-7-2] eliminated 3 small clauses 0%
c [cce-7-2] eliminated 3 small clauses in 4896536 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 10 covered clauses in round 2
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] allowing another 1840729 steps for small clauses
c [cce-7-3] scheduling 12848 clauses = 3452 binary + 9396 ternary
c [cce-7-3] tried to eliminate 12848 small clauses 100%
c [cce-7-3] eliminated 1 ternary clauses 0%
c [cce-7-3] eliminated 1 small clauses 0%
c [cce-7-3] eliminated 1 small clauses in 4885884 steps
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 1 covered clauses in round 3
c [cce-7] eliminated 387 covered clauses in TOTAL during 3 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 4406 variables 100%
c [elim-10] limit of 687430689 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 56 variables 1% in round 1 in 8179422 steps
c [elim-10-1] backward subsumption/strengthening limit 8179400
c [elim-10-1-1] backward checking 613 touched variables 14%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 1 and strengthened 38 clauses in 366283 steps
c [elim-10-1] rescheduled 240 variables 5% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 649981 steps
c [elim-10-2] backward subsumption/strengthening limit 649900
c [elim-10-2-1] backward checking 7 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 23557 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 57 = 1% variables out of 4406 scheduled
c [bca-4] limit of 10000000 steps and 57486 added (scaled 2)
c [bca-4] 4318 out of 8700 literals actually usable 50%
c [bca-4] added 0 blocked clauses in 103814 steps
c [score-distribution-13] 948 pos 21.80%, 3184 min 73.21%, 217 zero 4.99%
c [score-distribution-13] 689 different 15.84% out of total 4349 variables
c [simplification-13] removed 67 variables 1.5% (4349 remain 16%)
c [simplification-13] removed 913 irredundant clauses 3.1% (28493 remain 19%)
c [simplification-13] maximum reduction of 3% = max (2%, 3%)
c [simplification-13] geometric conflict interval increment 38400 = 153600 / 4
c [simplification-13] new conflict interval 192000
c [simplification-13] penalized conflict interval 192000 = 1 * 192000
c [simplification-13] hard conflict limit 855658 (soft 759658 + delta 96000)
c [simplification-13] new conflict limit 759658 (hard 855658)
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 -   87.9    4349    28493    582237   73792  24812  6629    9    16   13  57%    221    1    9    9   96%
c -   95.0    4349    28493    622956   76392  24830  6629   10    17   21  58%    593    1   11    9  120%
c -  102.5    4349    28493    664884   79528  24845  6630    9    15   21  61%    797   -1   10    9  109%
c -  110.5    4349    28493    706948   81585  24862  6631   10    16   21  64%    904    0   10    9  105%
c i  114.4    4348    28493    729057  100823  24886  6642    8    10   26  73%    939   -4    6    9   62%
c i  117.9    4345    28493    750453  120718  24892  6645    9    15   30  65%  -2259   -0   10    9  113%
c i  117.9    4344    28493    750460  120711  24895  6648    9    14   30  65%  -2261   -0   10    9  111%
c -  118.2    4342    28493    752302   86162  24895  6648    9    14   21  64%  -2442   -1    8    9   89%
c i  124.0    4341    28493    787333  118104  24946  6663    7    10   29  72%  -1040   -4    5    9   52%
c i  125.4    4336    28493    793479  123410  24968  6671    7    10   29  72%  -1387   -4    6    9   66%
c i  125.5    4335    28493    794154  123965  24982  6672    7    10   29  74%  -1409   -4    6    9   67%
c i  126.4    4333    28493    798396  127411  25012  6684    7     9   29  76%  -1313   -4    5    8   55%
c -  126.6    4312    28493    799341   91662  25012  6685    7    10   22  73%  -1320   -4    8    8   93%
c i  127.0    4311    28493    801752   93658  25037  6694    7    10   26  72%  -1259   -3    5    8   63%
c i  127.1    4309    28493    802736   94554  25050  6698    7    10   26  70%  -1259   -3    6    8   72%
c i  127.2    4291    28493    802822   94612  25057  6700    7    10   26  70%  -1258   -3    5    8   64%
c i  127.2    4252    28493    803252   94991  25061  6701    7    10   26  70%  -1255   -3    6    8   67%
c i  127.2    4222    28493    803274   94995  25061  6704    7    10   26  70%  -1255   -3    6    8   66%
c i  127.2    4186    28493    803312   95020  25065  6707    7    10   26  70%  -1255   -3    5    8   64%
c i  127.2    4185    28493    803313   95020  25065  6707    7    10   26  70%  -1255   -3    5    8   64%
c i  127.3    4182    28493    803397   95055  25078  6712    7    10   26  70%  -1254   -3    5    8   58%
c i  127.3    4157    28493    803399   95055  25077  6713    7    10   26  70%  -1254   -3    5    8   58%
c i  127.3    4145    28493    803404   95054  25077  6716    7    10   26  70%  -1254   -3    5    8   57%
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  127.3    4052    28493    803404   95054  25077  6716    7    10   26  70%  -1254   -3    5    8   57%
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: 15 basic ate = 12 trn 80% + 3 lrg 20% in 1 updates
c bcas: 4 count, 0 added (408 skipped), 256487 steps
c bkwd: tried 122395 clauses, 243745 lits, 1.99 lits/clause
c bkwd: checked 7300158 occs, 59.64 occs/clause, 29.95 occs/lit
c bkwd: subsumed 8 binary, 148 ternary, 45 large
c bkwd: strengthened 0 binary, 145 ternary (100% self), 792 large (0% self)
c blkd: 4 bces, 43 removed, 637998 resolutions, 1790416 steps
c blkd: 3083 blocking literals 5%, 0 pure
c bump: 803229 bumped seen, 38614750 lits 48.1 on average
c card: 4 count, 0 units, 1 am1, 10530529 steps
c card: 118 rescheduled, 170 eliminated, 1358 resolved, 14209 subsumed
c card: 2614 at-most-one constraints found, average size 3.88
c card: 2614 at-most-one constraints used 100%, average size 3.88
c card: 20 at-most-two constraints found, average size 4.40
c card: 20 at-most-two constraints used 100%, average size 4.40
c cces: 7 cces, 20259 eliminated, 16788 ate 83%, 3471 abce 17%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 627236 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 73 gcs, 0 rescored clauses, 422 rescored vars
c dcps: 41 decompositions, 13569 equivalent 42%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1446033 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 6429205 push, 6396940 pop (6396940 dec 100%)
c dsch: 126504620 swaps, 0 down, 43772430 up
c elms: 10 elims, 8879 eliminated 27%, 48 pure 1%
c elms: 26 rounds, 2.6 rounds/bve
c elms: 8541 small 96%, 290 large 3%
c elms: 9232 tried small, 8541 succeeded 93%, 691 failed 7%
c elms: 2431 subsumed, 5691 strengthened, 71 blocked
c elms: 1498789 copies, 1760718 resolutions, 116671 ipos
c elms: 1461506 subchks, 453372 strchks
c gaus: 3 extractions, 193 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 7084494 steps, 3542247 extr 50%, 2297 elim 0%
c glue: 9.1 orig avg, 9.1 real avg, 2.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 42441 = 31630 simple 75% + 10121 trn 24% + 690 lrg 2%, 1784 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 803229 clauses, 21.9 length
c lrnd: 17578550 lits = 25688516 orig - 8109966 removed 32%
c lrnd: 137876 uips 17%, 575821 flips 72%
c mins: 798038 mins 99%, 105 bin 0%, 5086 size 1%
c mins: 20861616 poisoned searches, 3241792 hits, 16% hit rate
c mins: 42483344 used twice searches, 3261367 hits, 8% hit rate
c move: moved 16093, 3372 bin 21%, 12721 trn 79%
c otfs: 3294 driving 24%, 10589 restarting 76%
c otfs: str 13883, 13815 red 100%, 68 irr 0%
c otfs: str 13883, 0 bin 0%, 113 trn 1%, 13770 lrg 99%
c otfs: sub 51, 37 red 73%, 14 irr 27%
c otfs: sub 51, 0 bin 0%, 8 trn 16%, 43 lrg 84%
c phas: 8 computed, 14284 set, 0 pos (0%), 14284 neg (100%)
c prbs: 3 basic, 56620 probed, 106 failed, 0 lifted
c prbs: 4 simple, 46616 probed, 30 failed, 28480 eqs
c prbs: 4 treelook, 8598 probed, 12 failed, 0 lifted
c prom: 282661 locked 18% out of 1562568 tried
c prps: 114665325 props, 78 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 9 count, 1437 quat, 742 self1, 4 self2, 31 dup
c redc: 23621 clauses 11%, 208889 tried 26%, 8 sat 0%
c redc: 29535 lits 1%, 2789372 tried 11%, 8 sat 0%
c redc: 500 times jump level reduced, 2.0 levels on average
c reds: 19 count, 42284.4 conflicts per reduce
c reds: 0 memlim 0%, 19 arith 100%
c reds: 560535 collected 86%, 89022 retired 14%
c rmbd: 7811 removed, 7023 red 90%
c rsts: 17066 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 13 count, 13 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 803229 count (258709 tried 0.3), 47561 sub out of 800696 (5.9%)
c swps: 8 count, 10 rounds, 1802 queries (180.2/round)
c swps: 1728 sat calls, 19 unsat (1.8% success rate)
c swps: 25639 decisions 14.8, 3119 conflicts 1.8
c swps; 134.9 avg class size, 36.3 avg environment size
c swps: 0 failed, 196 impls, 93 equivs
c swp0: 597 type 0 queries, 56 unsat (9.4%), 581 sat (97.3%)
c swp1: 1205 type 1 queries, 221 unsat (18.3%), 1128 sat (93.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: 4499628 calls to obtain time
c tops: 5813 fixed 18%, 22 its, 36518.36 confs/it
c trds: 9 transitive reductions, 3785 removed, 3 failed
c trds: 84965 nodes, 72417 edges, 1282421 steps
c trim: 300507 words, 1.1 MB
c trnr: 8 count, 106 bin, 19532 trn, 103048462 steps
c unhd: 5 count, 5 rounds, 3316177 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 4 failed, 4 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 3605 tauts, 189 bin 5%, 979 trn 27%, 880 lrg 24%
c unhd: 3605 tauts, 1557 stamp 43%, 2490 red 69%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 49145 str, 0 bin 0%, 997 trn 2%, 48148 lrg 98%, 48190 red 98%
c vars: 4052 remaining 13% and 28261 removed 87% out of 32313
c vars: 5813 fixed 18%, 8879 eliminated 27%, 13569 equivalent 42%
c vsts: 5602334648 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 49.1 search visits per propagation, 6931.1 per conflict
c wchs: 1586259625 pushed, 3122339 enlarged, 127 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         802133        560535         89022      15224137       6158473        454936
c 
c  0 0         80616  10     13429   2         0   0   9164053  60   3011201  49    186613  41     2.7
c  1 5         65074   8     42907   8      9528  11   1996706  13<   858862  14<    61830  14<    0.8
c  2 6        243603  30<   187019  33     27938  31   2879124  19   1482875  24    129509  28     2.2
c  3 9        306445  38    240831  43<    34387  39<  1022080   7    685856  11     67752  15     2.4
c  4 14       100545  13     72759  13     15609  18    154734   1    114818   2      8915   2     1.0
c  5 21         5790   1      3565   1      1535   2      7367   0      4825   0       316   0     0.1
c  6 30           60   0        25   0        25   0        73   0        36   0         1   0     0.0
c 
c avg                  2.4           2.6           2.7           0.8           1.0           1.2
c std                  1.1           0.9           0.9           1.0           1.2           1.2
c 
c    2.445   2% cce
c    1.800   1% elim
c    1.533   1% bump
c    1.488   1% probe
c    1.474   1% decide
c    1.273   1% sweep
c    0.775   1% ternres
c 
c    1.444 < 1% rest (below)
c 
c    0.443   0% unhide
c    0.273   0% quatres
c    0.174   0% block
c    0.144   0% gauss
c    0.121   0% card
c    0.116   0% bca
c    0.107   0% transred
c    0.065   0% rescore
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.808   1% preprocessing     8%
c    9.258   7% inprocessing     92%
c ==================================
c   10.067   8% simplifying
c  117.186  92% search
c ==================================
c  127.253 100% all
c 
c        803404 conflicts,        6313.4 confs/sec
c          1997 ternaries,         402.3 confs/ternary
c           224 binaries,         3586.6 confs/binary
c            22 iterations,      36518.4 confs/iteration
c 
c            19 reductions,          0.1 redus/sec,  42284.4 confs/reduction
c         17066 restarts,          134.1 rests/sec,     47.1 confs/restart
c       1446033 decisions,       11363.4 decis/sec,      1.8 decis/conflict
c     114665325 propagations,   901079.0 props/sec,     79.3 props/decision
c 
c 127.3 seconds, 32.2 MB
c launch: done
