c launch: /data/cnf/sc2014/app/q_query_3_l48_lambda.cnf.bz2
c host: atom13
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/q_query_3_l48_lambda.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/q_query_3_l48_lambda.cnf.bz2
c no embedded options
c found 'p cnf 34656 174528' header
c read 34656 variables, 174528 clauses, 503708 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --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 29651 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 
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   29651   163622         0       0      0     0    0     0   12   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 742 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] 747 out of 747 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 12214 variables
c [simpleprobe-1] all 22442 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 7455 variables
c [simpleprobe-1] 1712 variables remain 11% (13275 retained 89%)
c [simpleprobe-1] removed 7455 variables, found 29325 hbrs, 28 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 1265 tauts, 0 hbrs, 392 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 14987 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 8626 variables 58% in round 1 in 5356923 steps
c [elim-1-1] backward subsumption/strengthening limit 5356900
c [elim-1-1-1] backward checking 10429 touched variables 70%
c [elim-1-1-1] incomplete backward checking 7857 remain 75%
c [elim-1-1] subsumed 105 and strengthened 701 clauses in 5357028 steps
c [elim-1-1] rescheduled 1003 variables 7% by backward subsumption
c [elim-1-2] eliminated 41 variables 0% in round 2 in 1539871 steps
c [elim-1-2] backward subsumption/strengthening limit 1539800
c [elim-1-2-1] backward checking 8193 touched variables 55%
c [elim-1-2-1] incomplete backward checking 7691 remain 94%
c [elim-1-2] subsumed 31 and strengthened 124 clauses in 1539958 steps
c [elim-1-2] rescheduled 325 variables 2% by backward subsumption
c [elim-1-3] eliminated 49 variables 0% in round 3 in 343757 steps
c [elim-1-3] backward subsumption/strengthening limit 343700
c [elim-1-3-1] backward checking 8098 touched variables 54%
c [elim-1-3-1] incomplete backward checking 7881 remain 97%
c [elim-1-3] subsumed 96 and strengthened 14 clauses in 343736 steps
c [elim-1] incomplete 154 not tried 1% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 8716 = 58% variables out of 14987 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 60629 negative 96.8% of 62644 except 2015 3.2%
c [phase-count-1] 47977 positive 76.6% of 62644 except 14667 23.4%
c [phase-count-1] less non-negative clauses 2015 than limit 6200 (10.0%)
c [phase-count-1] non-pos/non-neg = 14667/2015 = 7.28 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 6271 negative 100%
c [sort-queue-1] sorted 6271 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 6271 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 23056 variables 78.6% (6271 remain 21%)
c [simplification-1] removed 100978 irredundant clauses 61.7% (62644 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.9    6270    62644         9       8      0  1267    0     0    5   4%      0    0    0    0 25220%
c i    0.9    6269    62644        42      30      7  1268    0     1    5   5%      0    1    1    0 23490%
c 
c [simplification-2] limit 1001 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 5 variables
c [simpleprobe-2] 664 schedulable variables 11%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 4 variables
c [simpleprobe-2] 554 variables remain 9% (5708 retained 91%)
c [simpleprobe-2] removed 4 variables, found 289 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 12524 literals 100%
c [treelook-1] scheduling used 262393 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300250 steps
c [treelook-1] 12301 literals remain 98%
c [treelook-1] 6261 variables remain to probed next time 100%
c [decomp-5] removed 1 variables
c [treelook-1] removed 2 variables, found 1985 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 2980 sched 48%, 40 failed, 0 lifted, 3149 hbrs
c [decomp-6] removed 43 variables
c [basicprobe-1-1] 1402 probes remain 23% after last round
c [basicprobe-1-1] 57 units = 57 failed (100%) + 0 lifted (0%)
c [basicprobe-1-1] removed 60 variables, found 3470 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 6200 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 53 not tried 1% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 105 = 2% variables out of 6200 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 58340 negative 96.7% of 60342 except 2002 3.3%
c [phase-count-2] 45509 positive 75.4% of 60342 except 14833 24.6%
c [phase-count-2] less non-negative clauses 2002 than limit 6000 (10.0%)
c [phase-count-2] non-pos/non-neg = 14833/2002 = 7.41 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 375 negative 100%
c [sort-queue-2] sorted 6095 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 1182 (19%), zero 4913 (81%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 174 variables 2.8% (6095 remain 21%)
c [simplification-2] removed 2297 irredundant clauses 3.7% (60342 remain 37%)
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 15001 (soft 5001 + delta 10000)
c [simplification-2] new conflict limit 5001 (hard 15001)
c 
c [simplification-3] limit 5001 conflicts (hard 15001) hit after 5001 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 940 at-most-one constraints of average size 3.7
c [card-2] found 53 at-most-two constraints of average size 4.8
c [card-2] using previous limit 1000000 for elimination
c [card-2] 993 out of 993 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 12190 literals 100%
c [treelook-2] scheduling used 265734 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 308013 steps
c [treelook-2] 12067 literals remain 99%
c [treelook-2] 6093 variables remain to probed next time 100%
c [decomp-8] removed 2 variables
c [treelook-2] removed 4 variables, found 1163 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 1463 tauts, 0 hbrs, 2092 literals
c [elim-3] 53 variables 1% will be scheduled this time
c [elim-3] scheduled 53 variables 1%
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 4340652 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 53 scheduled
c [phase-count-3] 58197 negative 96.7% of 60199 except 2002 3.3%
c [phase-count-3] 45348 positive 75.3% of 60199 except 14851 24.7%
c [phase-count-3] less non-negative clauses 2002 than limit 6000 (10.0%)
c [phase-count-3] non-pos/non-neg = 14851/2002 = 7.42 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 291 negative 100%
c [sort-queue-3] sorted 6091 enqueued variables after 5001 conflicts
c [score-dist-3] active 0 (0%), one 2812 (46%), zero 3279 (54%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 4 variables 0.1% (6091 remain 21%)
c [simplification-3] removed 138 irredundant clauses 0.2% (60199 remain 37%)
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  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    3.7    6090    60199     27911   25847   1059  4334    7    19    8  38%    344   13    7    2  318%
c 
c [simplification-4] limit 29001 conflicts (hard 41001) hit after 29002 conflicts
c [decomp-9] removed 8 variables
c [basicprobe-2] limit 4417326 penalty 0 = 0 + 0
c [basicprobe-2-0] 1713 sched 28%, 24 failed, 0 lifted, 646 hbrs
c [decomp-10] removed 28 variables
c [basicprobe-2-1] 2973 sched 49%, 24 failed, 0 lifted, 354 hbrs
c [decomp-11] removed 29 variables
c [basicprobe-2-2] 2969 sched 49%, 9 failed, 0 lifted, 112 hbrs
c [decomp-12] removed 9 variables
c [basicprobe-2-3] 3018 sched 50%, 3 failed, 0 lifted, 36 hbrs
c [decomp-13] removed 3 variables
c [basicprobe-2-4] 3017 sched 50%, 0 failed, 0 lifted, 28 hbrs
c [basicprobe-2-5] 3025 sched 50%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-2-6] 2326 probes remain 39% after last round
c [basicprobe-2-6] 60 units = 60 failed (100%) + 0 lifted (0%)
c [basicprobe-2-6] removed 69 variables, found 1188 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 6014 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 85 blocked clauses
c [block-1] 85 < 1/100 * 57508 = 575 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 314 clauses out of 596 (53%) of length 7
c [cce-1-1] eliminated 92 clauses out of 4970 (2%) of length 6
c [cce-1-1] eliminated 1528 clauses out of 3263 (47%) of length 5
c [cce-1-1] eliminated 1131 clauses out of 4364 (26%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 3065 large clauses in 8715665 steps
c [cce-1-1] allowing another 4357832 steps for small clauses
c [cce-1-1] scheduling 23496 clauses = 8432 binary + 15064 ternary
c [cce-1-1] tried to eliminate 23496 small clauses 100%
c [cce-1-1] eliminated 2792 binary clauses 33%
c [cce-1-1] eliminated 3076 ternary clauses 20%
c [cce-1-1] eliminated 5868 small clauses 25%
c [cce-1-1] eliminated 5868 small clauses in 14805255 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 8933 covered clauses in round 1
c [cce-1-2] eliminated 16 clauses out of 3233 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 16 large clauses in 5856428 steps
c [cce-1-2] allowing another 2928214 steps for small clauses
c [cce-1-2] scheduling 17628 clauses = 5640 binary + 11988 ternary
c [cce-1-2] tried to eliminate 17628 small clauses 100%
c [cce-1-2] eliminated 220 binary clauses 4%
c [cce-1-2] eliminated 391 ternary clauses 3%
c [cce-1-2] eliminated 611 small clauses 3%
c [cce-1-2] eliminated 611 small clauses in 9459691 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 627 covered clauses in round 2
c [cce-1-3] eliminated 29 clauses out of 1735 (2%) of length 5
c [cce-1-3] eliminated 45 clauses out of 3217 (1%) of length 4
c [cce-1-3] incomplete large round (ACCE)
c [cce-1-3] eliminated 74 large clauses in 5735055 steps
c [cce-1-3] allowing another 2867527 steps for small clauses
c [cce-1-3] scheduling 17017 clauses = 5420 binary + 11597 ternary
c [cce-1-3] tried to eliminate 7073 small clauses 42%
c [cce-1-3] eliminated 139 binary clauses 3%
c [cce-1-3] eliminated 193 ternary clauses 2%
c [cce-1-3] eliminated 332 small clauses 2%
c [cce-1-3] eliminated 332 small clauses in 5735158 steps
c [cce-1-3] incomplete small round (ACCE)
c [cce-1-3] eliminated 406 covered clauses in round 3
c [cce-1] eliminated 9966 covered clauses in TOTAL during 3 rounds
c [bca-1] limit of 10000000 steps and 95414 added (scaled 2)
c [bca-1] 8025 out of 12030 literals actually usable 67%
c [bca-1] added 1 blocked clauses in 41993 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2751 pos 45.7% + 3263 neg 54.3% = 6014 sched 100.0% ret 0
c [sweep-1-1] 1025306 steps 29 queries 479.41 avg class size
c [sweep-1-1] 1095 decisions 29 SAT calls 100.34 avg env size
c [sweep-1-1] 5105 variables remain 85% (909 retained 15%)
c [decomp-16] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 28 queries)
c [phase-count-4] 45558 negative 96.0% of 47457 except 1899 4.0%
c [phase-count-4] 36088 positive 76.0% of 47457 except 11369 24.0%
c [phase-count-4] less non-negative clauses 1899 than limit 4700 (10.0%)
c [phase-count-4] non-pos/non-neg = 11369/1899 = 5.99 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 280 negative 100%
c [sort-queue-4] sorted 6013 enqueued variables after 29002 conflicts
c [score-dist-4] active 0 (0%), one 3489 (58%), zero 2524 (42%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 71 variables 1.2% (6013 remain 20%)
c [simplification-4] removed 12742 irredundant clauses 21.2% (47457 remain 29%)
c [simplification-4] maximum reduction of 21% = max (1%, 21%)
c [simplification-4] large reduction 21% >= 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 41002 (soft 31002 + delta 10000)
c [simplification-4] new conflict limit 31002 (hard 41002)
c 
c [simplification-5] limit 31002 conflicts (hard 41002) hit after 33831 conflicts
c [quatres-1] found 4510 quaternary clauses 25% in total
c [quatres-1-1] removed 8 duplicate quaternary clauses
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 34 single-self-subsuming ternary resolvents
c [quatres-1-2] added 527 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 6013 free variables schedulable
c [ternres-1] 9064 ternary resolvents (19 bin, 9045 trn)
c [ternres-1] 1 variables remain 0% (6012 retained 100%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 55 xors of average arity 3.0
c [gauss-1] connected 165 occurrences of 24 variables (average 6.9)
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 [simpleprobe-3] 503 schedulable variables 8%
c [simpleprobe-3] limit 4323367 penalty 0 = 0 + 0
c [simpleprobe-3] 756 variables remain 13% (5257 retained 87%)
c [simpleprobe-3] removed 0 variables, found 1248 hbrs, 0 units
c [transred-1] limit 1080841 with penalty 0 = 0 + 0
c [transred-1] removed 1498 transitive binary clauses
c [transred-1] found 2 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 1705 (0%) of length 5
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 1 large clauses in 5597938 steps
c [cce-2-1] allowing another 2798969 steps for small clauses
c [cce-2-1] scheduling 25475 clauses = 5279 binary + 20196 ternary
c [cce-2-1] tried to eliminate 25475 small clauses 100%
c [cce-2-1] eliminated 4724 ternary clauses 23%
c [cce-2-1] eliminated 4724 small clauses 19%
c [cce-2-1] eliminated 4731 small clauses in 11491315 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 4732 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 2692482 steps for small clauses
c [cce-2-2] scheduling 20751 clauses = 5279 binary + 15472 ternary
c [cce-2-2] tried to eliminate 20751 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 4732 covered clauses in TOTAL during 2 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 6011 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 216168360 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 681 variables 11% in round 1 in 14393984 steps
c [elim-4-1] backward subsumption/strengthening limit 14393900
c [elim-4-1-1] backward checking 2170 touched variables 36%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 2 clauses in 1963674 steps
c [elim-4-1] rescheduled 15 variables 0% by backward subsumption
c [elim-4-2] eliminated 2 variables 0% in round 2 in 41227 steps
c [elim-4-2] backward subsumption/strengthening limit 41200
c [elim-4-2-1] backward checking 21 touched variables 0%
c [elim-4-2-1] incomplete backward checking 0 remain 0%
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 41201 steps
c [elim-4-2] fully rescheduled 5328 variables 89%
c [elim-4-3] eliminated 15 variables 0% in round 3 in 14167152 steps
c [elim-4-3] backward subsumption/strengthening limit 14167100
c [elim-4-3-1] backward checking 122 touched variables 2%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 0 and strengthened 0 clauses in 261166 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 698 = 12% variables out of 6011 scheduled
c [bca-2] limit of 10000000 steps and 83110 added (scaled 2)
c [bca-2] 6462 out of 10628 literals actually usable 61%
c [bca-2] added 0 blocked clauses in 43674 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2238 pos 48.9% + 2337 neg 51.1% = 4575 sched 86.1% ret 738
c [sweep-2-1] 1049512 steps 24 queries 536.88 avg class size
c [sweep-2-1] 983 decisions 23 SAT calls 121.04 avg env size
c [sweep-2-1] 4367 variables remain 82% (946 retained 18%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 23 queries)
c [phase-count-5] 39629 negative 95.9% of 41305 except 1676 4.1%
c [phase-count-5] 29862 positive 72.3% of 41305 except 11443 27.7%
c [phase-count-5] less non-negative clauses 1676 than limit 4100 (10.0%)
c [phase-count-5] non-pos/non-neg = 11443/1676 = 6.83 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 152 negative 100%
c [sort-queue-5] sorted 5313 enqueued variables after 33831 conflicts
c [score-dist-5] active 0 (0%), one 3255 (61%), zero 2058 (39%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 700 variables 11.6% (5313 remain 18%)
c [simplification-5] removed 6152 irredundant clauses 13.0% (41305 remain 25%)
c [simplification-5] maximum reduction of 13% = max (12%, 13%)
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 45831 (soft 35831 + delta 10000)
c [simplification-5] new conflict limit 35831 (hard 45831)
c 
c [simplification-6] limit 35831 conflicts (hard 45831) hit after 35831 conflicts
c [quatres-2] found 4443 quaternary clauses 24% in total
c [quatres-2-2] added 45 single-self-subsuming ternary resolvents
c [quatres-2-2] added 162 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 1 schedulable variables 0%
c [ternres-2] 490 ternary resolvents (2 bin, 488 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 561 at-most-one constraints of average size 3.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 561 out of 561 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 10069 literals 95%
c [treelook-3] scheduling used 302575 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 321317 steps
c [treelook-3] 9976 literals remain 94%
c [treelook-3] 5307 variables remain to probed next time 100%
c [treelook-3] removed 1 variables, found 851 hbrs
c [unhide-3] limit 58569 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 193 tauts, 0 hbrs, 9286 literals
c [transred-2] limit 1171399 with penalty 0 = 0 + 0
c [transred-2] removed 481 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5312 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 0 blocked clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 4 clauses out of 206 (2%) of length 9
c [cce-3-1] eliminated 1 clauses out of 335 (0%) of length 8
c [cce-3-1] eliminated 26 clauses out of 262 (10%) of length 7
c [cce-3-1] eliminated 7 clauses out of 4895 (0%) of length 6
c [cce-3-1] eliminated 82 clauses out of 1936 (4%) of length 5
c [cce-3-1] eliminated 185 clauses out of 2828 (7%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 305 large clauses in 6351694 steps
c [cce-3-1] allowing another 3175847 steps for small clauses
c [cce-3-1] scheduling 16060 clauses = 4470 binary + 11590 ternary
c [cce-3-1] tried to eliminate 16060 small clauses 100%
c [cce-3-1] eliminated 131 binary clauses 3%
c [cce-3-1] eliminated 458 ternary clauses 4%
c [cce-3-1] eliminated 589 small clauses 4%
c [cce-3-1] eliminated 589 small clauses in 8624863 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] completed small and large (ACCE)
c [cce-3-1] eliminated 894 covered clauses in round 1
c [cce-3-2] eliminated 22 clauses out of 1854 (1%) of length 5
c [cce-3-2] eliminated 43 clauses out of 2643 (2%) of length 4
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] eliminated 65 large clauses in 6269764 steps
c [cce-3-2] allowing another 3134882 steps for small clauses
c [cce-3-2] scheduling 15471 clauses = 4339 binary + 11132 ternary
c [cce-3-2] tried to eliminate 15471 small clauses 100%
c [cce-3-2] eliminated 14 binary clauses 0%
c [cce-3-2] eliminated 7 ternary clauses 0%
c [cce-3-2] eliminated 21 small clauses 0%
c [cce-3-2] eliminated 21 small clauses in 8264815 steps
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 86 covered clauses in round 2
c [cce-3-3] eliminated 1 clauses out of 236 (0%) of length 7
c [cce-3-3] eliminated 6 clauses out of 1832 (0%) of length 5
c [cce-3-3] eliminated 1 clauses out of 2600 (0%) of length 4
c [cce-3-3] completed large round (ACCE)
c [cce-3-3] eliminated 8 large clauses in 6207740 steps
c [cce-3-3] allowing another 3103870 steps for small clauses
c [cce-3-3] scheduling 15450 clauses = 4325 binary + 11125 ternary
c [cce-3-3] tried to eliminate 15450 small clauses 100%
c [cce-3-3] eliminated 2 binary clauses 0%
c [cce-3-3] eliminated 1 ternary clauses 0%
c [cce-3-3] eliminated 3 small clauses 0%
c [cce-3-3] eliminated 3 small clauses in 8213047 steps
c [cce-3-3] completed small round (ACCE)
c [cce-3-3] eliminated 11 covered clauses in round 3
c [cce-3] eliminated 991 covered clauses in TOTAL during 3 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5312 variables 100%
c [elim-5] limit of 23427985 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 53 variables 1% in round 1 in 13778660 steps
c [elim-5-1] backward subsumption/strengthening limit 9649325
c [elim-5-1-1] backward checking 320 touched variables 6%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 1 and strengthened 9 clauses in 370971 steps
c [elim-5-1] rescheduled 39 variables 1% by backward subsumption
c [elim-5-2] eliminated 1 variables 0% in round 2 in 135444 steps
c [elim-5-2] backward subsumption/strengthening limit 135400
c [elim-5-2-1] backward checking 8 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 13662 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 54 = 1% variables out of 5312 scheduled
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2165 pos 50.0% + 2166 neg 50.0% = 4331 sched 82.4% ret 927
c [sweep-3-1] 1033399 steps 49 queries 375.71 avg class size
c [sweep-3-1] 1335 decisions 45 SAT calls 80.53 avg env size
c [sweep-3-1] 3940 variables remain 75% (1318 retained 25%)
c [decomp-22] removed 3 variables
c [sweep-3-1] removed 3 vars (0 failed, 3 eqs, 6 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 3 vars in TOTAL (1 rounds, 48 queries)
c [phase-count-6] 38521 negative 95.9% of 40179 except 1658 4.1%
c [phase-count-6] 29082 positive 72.4% of 40179 except 11097 27.6%
c [phase-count-6] less non-negative clauses 1658 than limit 4000 (10.0%)
c [phase-count-6] non-pos/non-neg = 11097/1658 = 6.69 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 117 negative 100%
c [sort-queue-6] sorted 5255 enqueued variables after 35831 conflicts
c [score-dist-6] active 0 (0%), one 3323 (63%), zero 1932 (37%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 58 variables 1.1% (5255 remain 18%)
c [simplification-6] removed 1126 irredundant clauses 2.7% (40179 remain 25%)
c [simplification-6] maximum reduction of 3% = max (1%, 3%)
c [simplification-6] geometric conflict interval increment 6000 = 24000 / 4
c [simplification-6] new conflict interval 30000
c [simplification-6] penalized conflict interval 30000 = 1 * 30000
c [simplification-6] hard conflict limit 80831 (soft 65831 + delta 15000)
c [simplification-6] new conflict limit 65831 (hard 80831)
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    8.8    5254    40179     41693   37397  16283  5124    8    20   11  39%    115   11    8    3  240%
c i    8.8    5252    40179     41694   37397  16283  5124    8    20   11  39%    114   11    8    3  239%
c i    9.0    5249    40179     43050   38693  16292  5126    8    19   11  40%    -23   11    7    3  213%
c 
c [simplification-7] limit 65841 conflicts (hard 80831) hit after 65842 conflicts
c [quatres-3] found 4360 quaternary clauses 20% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-2] added 42 single-self-subsuming ternary resolvents
c [quatres-3-2] added 92 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 5249 free variables schedulable
c [ternres-3] 546 ternary resolvents (2 bin, 544 trn)
c [ternres-3] 2774 variables remain 53% (2475 retained 47%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 91 xors of average arity 3.0
c [gauss-2] connected 273 occurrences of 43 variables (average 6.3)
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 [basicprobe-3] limit 14179057 penalty 0 = 0 + 0
c [basicprobe-3-0] 2195 sched 42%, 11 failed, 0 lifted, 571 hbrs
c [decomp-24] removed 12 variables
c [basicprobe-3-1] 2744 sched 53%, 11 failed, 0 lifted, 283 hbrs
c [decomp-25] removed 11 variables
c [basicprobe-3-2] 2740 sched 52%, 3 failed, 0 lifted, 53 hbrs
c [decomp-26] removed 3 variables
c [basicprobe-3-3] 2749 sched 53%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-3-4] 2749 sched 53%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-3-5] 2752 sched 53%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-6] 2753 sched 53%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-3-7] 2755 sched 53%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-8] 2755 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-8] round limit 8 hit
c [basicprobe-3-8] 25 units = 25 failed (100%) + 0 lifted (0%)
c [basicprobe-3-8] removed 26 variables, found 933 hbrs
c [bate-1] eliminated 28 asymmetric tautologies during probing
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 250 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 5 clauses out of 200 (2%) of length 7
c [cce-4-1] eliminated 3 clauses out of 4921 (0%) of length 6
c [cce-4-1] eliminated 9 clauses out of 1809 (0%) of length 5
c [cce-4-1] eliminated 29 clauses out of 2519 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 46 large clauses in 5072922 steps
c [cce-4-1] allowing another 2536461 steps for small clauses
c [cce-4-1] scheduling 15170 clauses = 4260 binary + 10910 ternary
c [cce-4-1] tried to eliminate 15170 small clauses 100%
c [cce-4-1] eliminated 39 binary clauses 1%
c [cce-4-1] eliminated 21 ternary clauses 0%
c [cce-4-1] eliminated 60 small clauses 0%
c [cce-4-1] eliminated 60 small clauses in 7015527 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 106 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 2532827 steps for small clauses
c [cce-4-2] scheduling 15110 clauses = 4221 binary + 10889 ternary
c [cce-4-2] tried to eliminate 15110 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 106 covered clauses in TOTAL during 2 rounds
c [cce-4] 106 < 1/100 * 39674 = 396 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 5223 variables 100%
c [elim-6] limit of 56716231 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 51 variables 1% in round 1 in 13518249 steps
c [elim-6-1] backward subsumption/strengthening limit 13518200
c [elim-6-1-1] backward checking 283 touched variables 5%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 4 clauses in 366382 steps
c [elim-6-1] rescheduled 16 variables 0% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 55121 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 51 = 1% variables out of 5223 scheduled
c [elim-6] 51 < 1/100 * 5223 = 52 considered unsuccessful
c [bca-3] limit of 10000000 steps and 79370 added (scaled 2)
c [bca-3] 5816 out of 10346 literals actually usable 56%
c [bca-3] added 1 blocked clauses in 72011 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 2001 pos 51.6% + 1879 neg 48.4% = 3880 sched 75.0% ret 1292
c [sweep-4-1] 1000792 steps 46 queries 541.70 avg class size
c [sweep-4-1] 836 decisions 41 SAT calls 45.54 avg env size
c [sweep-4-1] 3599 variables remain 70% (1573 retained 30%)
c [decomp-32] removed 4 variables
c [sweep-4-1] removed 4 vars (0 failed, 4 eqs, 8 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 4 vars in TOTAL (1 rounds, 45 queries)
c [phase-count-7] 37794 negative 95.8% of 39435 except 1641 4.2%
c [phase-count-7] 28539 positive 72.4% of 39435 except 10896 27.6%
c [phase-count-7] less non-negative clauses 1641 than limit 3900 (10.0%)
c [phase-count-7] non-pos/non-neg = 10896/1641 = 6.64 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 90 negative 100%
c [sort-queue-7] sorted 5168 enqueued variables after 65842 conflicts
c [score-dist-7] active 0 (0%), one 3548 (69%), zero 1620 (31%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 81 variables 1.5% (5168 remain 17%)
c [simplification-7] removed 744 irredundant clauses 1.9% (39435 remain 24%)
c [simplification-7] maximum reduction of 2% = max (2%, 2%)
c [simplification-7] geometric conflict interval increment 10000 = 30000 / 3
c [simplification-7] new conflict interval 40000
c [simplification-7] penalized conflict interval 40000 = 1 * 40000
c [simplification-7] hard conflict limit 125842 (soft 105842 + delta 20000)
c [simplification-7] new conflict limit 105842 (hard 125842)
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 -   14.4    5168    39435     68474   22451  16186  5072    8    20    9  43%    260    7    8    5  166%
c 
c [simplification-8] limit 105842 conflicts (hard 125842) hit after 105845 conflicts
c [quatres-4] found 4913 quaternary clauses 19% in total
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 21 single-self-subsuming ternary resolvents
c [quatres-4-2] added 101 quaternary resolvents
c [ternres-4] limit 5009587 with penalty 0 = 0 + 0
c [ternres-4] 2725 schedulable variables 53%
c [ternres-4] 1275 ternary resolvents (8 bin, 1267 trn)
c [ternres-4] 367 variables remain 7% (4801 retained 93%)
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 109 transitive binary clauses
c [bca-4] limit of 10000000 steps and 79367 added (scaled 2)
c [bca-4] 5824 out of 10338 literals actually usable 56%
c [bca-4] added 0 blocked clauses in 70951 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 15028760 penalty 0 = 0 + 0
c [sweep-5-1] 1863 pos 51.8% + 1736 neg 48.2% = 3599 sched 69.6% ret 1569
c [sweep-5-1] 7160703 steps 710 queries 55.78 avg class size
c [sweep-5-1] 7578 decisions 630 SAT calls 27.03 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-34] removed 85 variables
c [sweep-5-1] removed 85 vars (0 failed, 89 eqs, 170 impls)
c [sweep-5-2] 2465 pos 48.5% + 2618 neg 51.5% = 5083 sched 100.0% ret 0
c [sweep-5-2] 7257399 steps 635 queries 73.98 avg class size
c [sweep-5-2] 8028 decisions 638 SAT calls 30.73 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-35] removed 5 variables
c [sweep-5-2] removed 5 vars (0 failed, 9 eqs, 20 impls)
c [sweep-5-3] 2461 pos 48.5% + 2617 neg 51.5% = 5078 sched 100.0% ret 0
c [sweep-5-3] 779111 steps 8 queries 1615.88 avg class size
c [sweep-5-3] 455 decisions 7 SAT calls 139.14 avg env size
c [sweep-5-3] 5051 variables remain 99% (27 retained 1%)
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 90 vars in TOTAL (3 rounds, 1350 queries)
c [sort-queue-8] sorted 5078 enqueued variables after 105845 conflicts
c [score-dist-8] active 0 (0%), one 4071 (80%), zero 1007 (20%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 90 variables 1.7% (5078 remain 17%)
c [simplification-8] removed 14 irredundant clauses 0.0% (39421 remain 24%)
c [simplification-8] maximum reduction of 2% = max (2%, 0%)
c [simplification-8] geometric conflict interval increment 13333 = 40000 / 3
c [simplification-8] new conflict interval 53333
c [simplification-8] penalized conflict interval 53333 = 1 * 53333
c [simplification-8] hard conflict limit 185844 (soft 159178 + delta 26666)
c [simplification-8] new conflict limit 159178 (hard 185844)
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   21.6    5077    39421    113983   67947  14974  5248    9    20   16  45%    642    4   10    7  144%
c -   21.8    5073    39421    114810   30077  14975  5248    9    20   10  45%     37    4    9    7  136%
c i   27.1    5072    39421    157688   71016  15121  5272    7    14   16  54%    250   -4    6    7   78%
c -   27.9    5072    39421    162745   40680  15132  5273    8    16   10  49%   -330   -1    8    8  111%
c 
c [simplification-9] limit 159178 conflicts (hard 185844) hit after 181275 conflicts
c [quatres-5] found 5088 quaternary clauses 17% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 45 single-self-subsuming ternary resolvents
c [quatres-5-2] added 151 quaternary resolvents
c [ternres-5] limit 8950206 with penalty 0 = 0 + 0
c [ternres-5] 344 schedulable variables 7%
c [ternres-5] 1777 ternary resolvents (8 bin, 1769 trn)
c [ternres-5] 20 variables remain 0% (5052 retained 100%)
c [decomp-37] removed 6 variables
c [simpleprobe-4] 575 schedulable variables 11%
c [simpleprobe-4] limit 17900412 penalty 1 = 1 + 0
c [decomp-38] removed 9 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 9 variables, found 2887 hbrs, 2 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1131 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5063 variables 100%
c [block-3] limit of 22375515 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 16 blocked clauses
c [block-3] 16 < 1/100 * 39028 = 390 considered unsuccessful
c [cce-5] limit of 22375515 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 2 clauses out of 378 (1%) of length 8
c [cce-5-1] eliminated 3 clauses out of 195 (2%) of length 7
c [cce-5-1] eliminated 178 clauses out of 4916 (4%) of length 6
c [cce-5-1] eliminated 16 clauses out of 1499 (1%) of length 5
c [cce-5-1] eliminated 59 clauses out of 2572 (2%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 258 large clauses in 5801925 steps
c [cce-5-1] allowing another 2900962 steps for small clauses
c [cce-5-1] scheduling 18653 clauses = 4274 binary + 14379 ternary
c [cce-5-1] tried to eliminate 18653 small clauses 100%
c [cce-5-1] eliminated 291 binary clauses 7%
c [cce-5-1] eliminated 3341 ternary clauses 23%
c [cce-5-1] eliminated 3632 small clauses 19%
c [cce-5-1] eliminated 3632 small clauses in 9233188 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 3890 covered clauses in round 1
c [cce-5-2] eliminated 11 clauses out of 1483 (1%) of length 5
c [cce-5-2] eliminated 16 clauses out of 2513 (1%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 27 large clauses in 5573713 steps
c [cce-5-2] allowing another 2786856 steps for small clauses
c [cce-5-2] scheduling 15021 clauses = 3983 binary + 11038 ternary
c [cce-5-2] tried to eliminate 15021 small clauses 100%
c [cce-5-2] eliminated 22 binary clauses 1%
c [cce-5-2] eliminated 1 ternary clauses 0%
c [cce-5-2] eliminated 23 small clauses 0%
c [cce-5-2] eliminated 23 small clauses in 6174606 steps
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 50 covered clauses in round 2
c [cce-5-3] eliminated 11 clauses out of 1472 (1%) of length 5
c [cce-5-3] eliminated 12 clauses out of 2497 (0%) of length 4
c [cce-5-3] completed large round (ACCE)
c [cce-5-3] eliminated 23 large clauses in 5575317 steps
c [cce-5-3] allowing another 2787658 steps for small clauses
c [cce-5-3] scheduling 14998 clauses = 3961 binary + 11037 ternary
c [cce-5-3] tried to eliminate 14998 small clauses 100%
c [cce-5-3] completed small round (ACCE)
c [cce-5-3] eliminated 23 covered clauses in round 3
c [cce-5] eliminated 3963 covered clauses in TOTAL during 3 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 5062 variables 100%
c [elim-7] limit of 89502063 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 77 variables 2% in round 1 in 11262655 steps
c [elim-7-1] backward subsumption/strengthening limit 11262600
c [elim-7-1-1] backward checking 774 touched variables 15%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 1 and strengthened 5 clauses in 578293 steps
c [elim-7-1] rescheduled 33 variables 1% by backward subsumption
c [elim-7-2] no variable eliminated in round 2 in 27844 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 77 = 2% variables out of 5062 scheduled
c [sweep-6] limit 2685061 penalty 0 = 0 + 0
c [sweep-6-1] 2375 pos 47.9% + 2584 neg 52.1% = 4959 sched 99.5% ret 26
c [sweep-6-1] 2716770 steps 59 queries 403.86 avg class size
c [sweep-6-1] 1762 decisions 58 SAT calls 83.16 avg env size
c [sweep-6-1] 3415 variables remain 69% (1570 retained 31%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 58 queries)
c [sort-queue-9] sorted 4985 enqueued variables after 181275 conflicts
c [score-dist-9] active 0 (0%), one 4247 (85%), zero 738 (15%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 87 variables 1.7% (4985 remain 17%)
c [simplification-9] removed 4822 irredundant clauses 12.2% (34599 remain 21%)
c [simplification-9] maximum reduction of 12% = max (2%, 12%)
c [simplification-9] large reduction 12% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 193275 (soft 183275 + delta 10000)
c [simplification-9] new conflict limit 183275 (hard 193275)
c 
c [simplification-10] limit 183275 conflicts (hard 193275) hit after 183275 conflicts
c [quatres-6] found 5621 quaternary clauses 17% in total
c [quatres-6-1] removed 6 duplicate quaternary clauses
c [quatres-6-2] added 25 single-self-subsuming ternary resolvents
c [quatres-6-2] added 79 quaternary resolvents
c [ternres-6] limit 9055992 with penalty 0 = 0 + 0
c [ternres-6] 20 schedulable variables 0%
c [ternres-6] 1280 ternary resolvents (7 bin, 1273 trn)
c [ternres-6] 1 variables remain 0% (4984 retained 100%)
c [card-4] limit 565999 penalty 3 = 3 + 0
c [card-4] found 510 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 565999 for elimination
c [card-4] 510 out of 510 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 51 xors of average arity 3.0
c [gauss-3] connected 153 occurrences of 48 variables (average 3.2)
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 [treelook-4] limit 905599 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 9965 literals 100%
c [treelook-4] scheduling used 381836 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 905599 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 905767 steps
c [treelook-4] 9563 literals remain 96%
c [treelook-4] 4969 variables remain to probed next time 100%
c [treelook-4] removed 0 variables, found 1247 hbrs
c [unhide-4] limit 226399 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 2327 tauts, 0 hbrs, 28077 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 591 transitive binary clauses
c [cce-6] limit of 45279964 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 4 clauses out of 1242 (0%) of length 5
c [cce-6-1] eliminated 19 clauses out of 2689 (1%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 23 large clauses in 4681085 steps
c [cce-6-1] allowing another 2340542 steps for small clauses
c [cce-6-1] scheduling 14297 clauses = 3969 binary + 10328 ternary
c [cce-6-1] tried to eliminate 14297 small clauses 100%
c [cce-6-1] eliminated 70 binary clauses 2%
c [cce-6-1] eliminated 73 ternary clauses 1%
c [cce-6-1] eliminated 143 small clauses 1%
c [cce-6-1] eliminated 143 small clauses in 6313479 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 166 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 2358810 steps for small clauses
c [cce-6-2] scheduling 14154 clauses = 3899 binary + 10255 ternary
c [cce-6-2] tried to eliminate 14154 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 166 covered clauses in TOTAL during 2 rounds
c [cce-6] 166 < 1/100 * 34597 = 345 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 4985 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3622397160 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 19 variables 0% in round 1 in 11129592 steps
c [elim-8-1] backward subsumption/strengthening limit 11129500
c [elim-8-1-1] backward checking 215 touched variables 4%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 58503 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 19 = 0% variables out of 4985 scheduled
c [elim-8] 19 < 1/100 * 4985 = 49 considered unsuccessful
c [bca-5] limit of 10000000 steps and 69281 added (scaled 2)
c [bca-5] 5234 out of 9934 literals actually usable 53%
c [bca-5] added 1 blocked clauses in 68380 steps
c [sort-queue-10] sorted 4966 enqueued variables after 183275 conflicts
c [score-dist-10] active 0 (0%), one 4230 (85%), zero 736 (15%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 19 variables 0.4% (4966 remain 17%)
c [simplification-10] removed 209 irredundant clauses 0.6% (34390 remain 21%)
c [simplification-10] maximum reduction of 1% = max (0%, 1%)
c [simplification-10] geometric conflict interval increment 26666 = 53333 / 2
c [simplification-10] new conflict interval 79999
c [simplification-10] penalized conflict interval 79999 = 1 * 79999
c [simplification-10] hard conflict limit 303273 (soft 263274 + delta 39999)
c [simplification-10] new conflict limit 263274 (hard 303273)
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 -   35.4    4966    34390    205814   46568  20120  6374    9    18   16  49%    320    0   10    8  120%
c -   40.0    4966    34390    244442   52244  20174  6378    9    16   17  52%    633   -2    7    8   87%
c 
c [simplification-11] limit 263274 conflicts (hard 303273) hit after 263274 conflicts
c [quatres-7] found 5776 quaternary clauses 14% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 28 single-self-subsuming ternary resolvents
c [quatres-7-2] added 59 quaternary resolvents
c [ternres-7] limit 13285475 with penalty 0 = 0 + 0
c [ternres-7] 1 schedulable variables 0%
c [ternres-7] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-7] fully completed ternary resolution
c [basicprobe-4] limit 66427376 penalty 0 = 0 + 0
c [basicprobe-4-0] 2659 sched 54%, 0 failed, 0 lifted, 259 hbrs
c [basicprobe-4-1] 2659 sched 54%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-4-2] 2659 sched 54%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-4-3] 2659 sched 54%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-3] fully completed probing
c [basicprobe-4-3] removed 0 variables, found 272 hbrs
c [bate-2] eliminated 1 asymmetric tautologies during probing
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 320 transitive binary clauses
c [bca-6] limit of 10000000 steps and 69277 added (scaled 2)
c [bca-6] 5071 out of 9934 literals actually usable 51%
c [bca-6] added 0 blocked clauses in 80946 steps
c [sweep-7] limit 1992821 penalty 1 = 1 + 0
c [sweep-7-1] 1548 pos 45.6% + 1848 neg 54.4% = 3396 sched 68.4% ret 1570
c [sweep-7-1] 2108071 steps 63 queries 308.32 avg class size
c [sweep-7-1] 1717 decisions 62 SAT calls 65.55 avg env size
c [sweep-7-1] 2873 variables remain 58% (2093 retained 42%)
c [decomp-46] removed 1 variables
c [sweep-7-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-7] 1 < 1/1000 * 4966 = 4 considered unsuccessful
c [sweep-7] removed 1 vars in TOTAL (1 rounds, 62 queries)
c [sort-queue-11] sorted 4965 enqueued variables after 263274 conflicts
c [score-dist-11] active 0 (0%), one 4405 (89%), zero 560 (11%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 1 variables 0.0% (4965 remain 17%)
c [simplification-11] removed 2 irredundant clauses 0.0% (34388 remain 21%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 79999
c [simplification-11] new conflict interval 159998
c [simplification-11] penalized conflict interval 159998 = 1 * 159998
c [simplification-11] hard conflict limit 503271 (soft 423272 + delta 79999)
c [simplification-11] new conflict limit 423272 (hard 503271)
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 -   45.3    4965    34388    281974   56948  20178  6373    9    19   12  49%    804    1   11    8  128%
c -   50.4    4965    34388    319124   60336  20207  6375    9    19   19  48%    899    1    9    9  107%
c -   55.2    4965    34388    356604   63948  20241  6379    9    18   19  51%    953    1    9    9  107%
c -   60.5    4965    34388    394345   66595  20262  6381    9    18   19  52%    984    1   10    9  108%
c 
c [simplification-12] limit 423272 conflicts (hard 503271) hit after 428394 conflicts
c [quatres-8] found 6177 quaternary clauses 11% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 20 single-self-subsuming ternary resolvents
c [quatres-8-2] added 33 quaternary resolvents
c [simpleprobe-5] all 4965 free variables schedulable
c [simpleprobe-5] limit 93621977 penalty 0 = 0 + 0
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 0 variables, found 3378 hbrs, 0 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1085 transitive binary clauses
c [cce-7] limit of 58513736 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 7 clauses out of 112 (6%) of length 9
c [cce-7-1] eliminated 5 clauses out of 396 (1%) of length 8
c [cce-7-1] eliminated 1 clauses out of 152 (1%) of length 7
c [cce-7-1] eliminated 5 clauses out of 4823 (0%) of length 6
c [cce-7-1] eliminated 3 clauses out of 1252 (0%) of length 5
c [cce-7-1] eliminated 8 clauses out of 2656 (0%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 29 large clauses in 5609216 steps
c [cce-7-1] allowing another 2804608 steps for small clauses
c [cce-7-1] scheduling 14743 clauses = 3876 binary + 10867 ternary
c [cce-7-1] tried to eliminate 14743 small clauses 100%
c [cce-7-1] eliminated 38 binary clauses 1%
c [cce-7-1] eliminated 49 ternary clauses 0%
c [cce-7-1] eliminated 87 small clauses 1%
c [cce-7-1] eliminated 87 small clauses in 6099626 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 116 covered clauses in round 1
c [cce-7-2] eliminated 5 clauses out of 1249 (0%) of length 5
c [cce-7-2] eliminated 11 clauses out of 2648 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 16 large clauses in 5636733 steps
c [cce-7-2] allowing another 2818366 steps for small clauses
c [cce-7-2] scheduling 14656 clauses = 3838 binary + 10818 ternary
c [cce-7-2] tried to eliminate 14656 small clauses 100%
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 16 covered clauses in round 2
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] allowing another 2814577 steps for small clauses
c [cce-7-3] scheduling 14656 clauses = 3838 binary + 10818 ternary
c [cce-7-3] tried to eliminate 14656 small clauses 100%
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 0 covered clauses in round 3
c [cce-7] eliminated 132 covered clauses in TOTAL during 3 rounds
c [cce-7] 132 < 1/100 * 34388 = 343 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 4965 variables 100%
c [elim-9] limit of 234054944 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 12 variables 0% in round 1 in 11091609 steps
c [elim-9-1] backward subsumption/strengthening limit 11091600
c [elim-9-1-1] backward checking 108 touched variables 2%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 1 clauses in 40890 steps
c [elim-9-1] rescheduled 4 variables 0% by backward subsumption
c [elim-9-2] no variable eliminated in round 2 in 853 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 12 = 0% variables out of 4965 scheduled
c [elim-9] 12 < 1/100 * 4965 = 49 considered unsuccessful
c [sort-queue-12] sorted 4953 enqueued variables after 428394 conflicts
c [score-dist-12] active 0 (0%), one 4428 (89%), zero 525 (11%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 12 variables 0.2% (4953 remain 17%)
c [simplification-12] removed 153 irredundant clauses 0.4% (34235 remain 21%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 159998
c [simplification-12] new conflict interval 319996
c [simplification-12] penalized conflict interval 319996 = 1 * 319996
c [simplification-12] hard conflict limit 908388 (soft 748390 + delta 159998)
c [simplification-12] new conflict limit 748390 (hard 908388)
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 -   67.2    4953    34235    434228   71014  20310  8666    9    19   13  49%   1002    3   10    9  114%
c -   72.9    4953    34235    472778   74252  20348  8668    9    17   14  53%   1012    0    9    9   98%
c -   78.7    4953    34235    511649   76756  20377  8669    9    17   22  53%   1017    1   10    9  110%
c -   84.5    4953    34235    551405   79837  20391  8670   10    17   22  55%   1020    1   11    9  115%
c -   91.0    4953    34235    591301   82562  20409  8672    9    17   22  56%   1022   -0   10    9  109%
c -   97.3    4953    34235    631487   85247  20429  8672   10    17   22  57%   1023    0   10    9  105%
c -  104.3    4953    34235    672436   87576  20443  8673   10    18   22  54%   1023    1   10   10  100%
c -  111.6    4953    34235    714474   91069  20457  8674    9    16   23  58%   1024   -1   10    9  111%
c -  119.7    4953    34235    755963   92757  20471  8675   10    16   23  61%   1024   -0   11   10  117%
c 
c [simplification-13] limit 748390 conflicts (hard 908388) hit after 756440 conflicts
c [quatres-9] found 6603 quaternary clauses 9% in total
c [quatres-9-2] added 24 single-self-subsuming ternary resolvents
c [quatres-9-2] added 47 quaternary resolvents
c [ternres-8] limit 23852654 with penalty 1 = 1 + 0
c [ternres-8] all 4953 free variables schedulable
c [ternres-8] 2646 ternary resolvents (10 bin, 2636 trn)
c [ternres-8] 44 variables remain 1% (4909 retained 99%)
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 621 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 4953 variables 100%
c [block-4] limit of 59631637 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [bca-7] limit of 10000000 steps and 68971 added (scaled 2)
c [bca-7] 4731 out of 9908 literals actually usable 48%
c [bca-7] added 0 blocked clauses in 103282 steps
c [sort-queue-13] sorted 4953 enqueued variables after 756440 conflicts
c [score-dist-13] active 0 (0%), one 4453 (90%), zero 500 (10%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 0 variables 0.0% (4953 remain 17%)
c [simplification-13] removed 0 irredundant clauses 0.0% (34235 remain 21%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 319996
c [simplification-13] new conflict interval 639992
c [simplification-13] penalized conflict interval 639992 = 1 * 639992
c [simplification-13] hard conflict limit 1716428 (soft 1396432 + delta 319996)
c [simplification-13] new conflict limit 1396432 (hard 1716428)
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 -  128.4    4953    34235    799508   95791  23158  8067   10    16   23  61%   1024   -0   11   10  116%
c i  129.3    4952    34235    805850  101703  23170  8079    9    14   27  60%   1024   -2    5    9   58%
c -  136.3    4948    34235    843663   99447  23193  8080    9    15   23  61%  -4754   -1    9    9   95%
c -  144.9    4948    34235    888394  102780  23215  8083    9    15   23  60%  -1896   -1    8    9   90%
c -  153.6    4948    34235    933507  105982  23247  8090    9    15   23  61%   -443   -0    9    9   98%
c -  163.2    4948    34235    980453  110163  23284  8097    8    13   23  67%    307   -2    8    9   97%
c i  165.1    4947    34235    990960  119396  23332  8112    7    10   29  71%    414   -4    6    9   67%
c i  166.5    4946    34235    997848  125707  23338  8116    8    12   30  67%  -2167   -1    7    9   81%
c i  166.6    4942    34235    998061  125870  23344  8117    8    12   30  67%  -2178   -2    6    9   70%
c i  167.7    4938    34235   1004578  131923  23360  8122    7    11   30  68%  -1960   -3    7    8   80%
c i  172.1    4931    34235   1024879  150186  23386  8128    8    11   34  68%  -1241   -2    6    8   68%
c i  172.1    4928    34235   1024880  150186  23386  8128    8    11   34  68%  -1242   -2    6    8   68%
c i  172.2    4894    34235   1025275  150451  23396  8129    7    11   34  69%  -1329   -2    5    8   63%
c i  172.5    4893    34235   1026429  151420  23402  8131    7    10   34  69%  -1436   -3    6    8   73%
c i  172.5    4890    34235   1026649  151623  23403  8132    7    10   34  69%  -1446   -3    6    8   77%
c i  172.7    4888    34235   1027231  152078  23415  8136    7    10   34  69%  -1456   -3    5    8   63%
c i  172.9    4850    34235   1028418  153128  23428  8140    7    10   34  68%  -1447   -3    6    8   71%
c i  172.9    4828    34235   1028484  153174  23431  8143    7    10   34  68%  -1447   -3    6    8   68%
c i  173.0    4825    34235   1028528  153194  23433  8147    7    10   34  68%  -1447   -3    5    8   64%
c i  173.0    4823    34235   1028529  153194  23433  8147    7    10   34  68%  -1447   -3    5    8   64%
c i  173.0    4795    34235   1028545  153203  23436  8148    7    10   34  68%  -1447   -3    5    8   62%
c i  173.0    4776    34235   1028549  153204  23438  8148    7    10   34  68%  -1447   -3    5    8   62%
c i  173.0    4768    34235   1028562  153212  23438  8151    7    10   34  68%  -1447   -3    5    8   60%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  173.0    4767    34235   1028565  153212  23439  8152    7    10   34  68%  -1447   -3    5    8   59%
c i  173.0    4568    34235   1028566  153212  23439  8152    7    10   34  68%  -1447   -3    5    8   59%
c 0  173.0    4479    34235   1028566  153212  23439  8152    7    10   34  68%  -1447   -3    5    8   59%
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: 29 basic ate = 28 trn 97% + 1 lrg 3% in 2 updates
c bcas: 7 count, 3 added (466 skipped), 481237 steps
c bkwd: tried 117639 clauses, 234249 lits, 1.99 lits/clause
c bkwd: checked 7625460 occs, 64.82 occs/clause, 32.55 occs/lit
c bkwd: subsumed 19 binary, 120 ternary, 96 large
c bkwd: strengthened 0 binary, 150 ternary (100% self), 710 large (0% self)
c blkd: 4 bces, 101 removed, 707729 resolutions, 1992966 steps
c blkd: 2714 blocking literals 4%, 1 pure
c bump: 1027982 bumped seen, 51457574 lits 50.1 on average
c card: 4 count, 0 units, 0 am1, 12017913 steps
c card: 97 rescheduled, 100 eliminated, 287 resolved, 15101 subsumed
c card: 2753 at-most-one constraints found, average size 3.85
c card: 2753 at-most-one constraints used 100%, average size 3.85
c card: 58 at-most-two constraints found, average size 4.72
c card: 58 at-most-two constraints used 100%, average size 4.72
c cces: 7 cces, 20049 eliminated, 18345 ate 92%, 1704 abce 8%
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: 678236 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 80 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 49 decompositions, 14191 equivalent 41%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1734920 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 9 elims, 9733 eliminated 28%, 38 pure 0%
c elms: 21 rounds, 2.3 rounds/bve
c elms: 9405 small 97%, 289 large 3%
c elms: 10091 tried small, 9405 succeeded 93%, 686 failed 7%
c elms: 2245 subsumed, 5401 strengthened, 111 blocked
c elms: 1666031 copies, 2001375 resolutions, 124572 ipos
c elms: 1845364 subchks, 531539 strchks
c gaus: 3 extractions, 197 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 7007210 steps, 3503605 extr 50%, 1805 elim 0%
c glue: 8.8 orig avg, 8.8 real avg, 2.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 48851 = 37127 simple 76% + 10749 trn 22% + 975 lrg 2%, 1715 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1027982 clauses, 23.3 length
c lrnd: 23913815 lits = 34641006 orig - 10727191 removed 31%
c lrnd: 163676 uips 16%, 773212 flips 75%
c mins: 1022154 mins 99%, 111 bin 0%, 5717 size 1%
c mins: 31501911 poisoned searches, 5152099 hits, 16% hit rate
c mins: 59938801 used twice searches, 3772970 hits, 6% hit rate
c move: moved 16331, 3811 bin 23%, 12520 trn 77%
c otfs: 3561 driving 22%, 12795 restarting 78%
c otfs: str 16356, 16294 red 100%, 62 irr 0%
c otfs: str 16356, 0 bin 0%, 95 trn 1%, 16261 lrg 99%
c otfs: sub 31, 21 red 68%, 10 irr 32%
c otfs: sub 31, 0 bin 0%, 5 trn 16%, 26 lrg 84%
c phas: 7 computed, 7576 set, 0 pos (0%), 7576 neg (100%)
c prbs: 4 basic, 112731 probed, 142 failed, 0 lifted
c prbs: 5 simple, 67107 probed, 30 failed, 31167 eqs
c prbs: 4 treelook, 837 probed, 4 failed, 0 lifted
c prom: 346491 locked 19% out of 1862586 tried
c prps: 138844476 props, 79 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 9 count, 1251 quat, 284 self1, 4 self2, 33 dup
c queu: 13 sorted, 1734920 next (15 steps 0.00)
c queu: 51562336 enq (0 steps 0.00), 51457574 deq 100%
c redc: 39479 clauses 14%, 279775 tried 27%, 8 sat 0%
c redc: 50392 lits 1%, 3898649 tried 11%, 8 sat 0%
c redc: 859 times jump level reduced, 1.8 levels on average
c reds: 23 count, 44720.3 conflicts per reduce
c reds: 0 memlim 0%, 23 arith 100%
c reds: 701540 collected 86%, 112585 retired 14%
c rmbd: 9475 removed, 8623 red 91%
c rsts: 19379 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 13 count, 13 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 1027982 count (293337 tried 0.3), 51276 sub out of 1025098 (5.0%)
c swps: 7 count, 9 rounds, 1614 queries (179.3/round)
c swps: 1533 sat calls, 27 unsat (1.9% success rate)
c swps: 23789 decisions 15.5, 2977 conflicts 1.9
c swps; 131.9 avg class size, 37.6 avg environment size
c swps: 0 failed, 206 impls, 107 equivs
c swp0: 535 type 0 queries, 52 unsat (9.7%), 517 sat (96.6%)
c swp1: 1079 type 1 queries, 253 unsat (23.4%), 990 sat (91.8%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 5526083 calls to obtain time
c tops: 6253 fixed 18%, 28 its, 36734.50 confs/it
c trds: 9 transitive reductions, 6086 removed, 2 failed
c trds: 92979 nodes, 82784 edges, 1641284 steps
c trim: 361883 words, 1.4 MB
c trnr: 8 count, 56 bin, 17022 trn, 74956069 steps
c unhd: 4 count, 4 rounds, 2112343 steps
c unhd: 40 non-trivial sccs of average size 2.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: 5248 tauts, 131 bin 2%, 1282 trn 24%, 238 lrg 5%
c unhd: 5248 tauts, 3597 stamp 69%, 4178 red 80%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 39847 str, 0 bin 0%, 860 trn 2%, 38987 lrg 98%, 38804 red 97%
c vars: 4479 remaining 13% and 30177 removed 87% out of 34656
c vars: 6253 fixed 18%, 9733 eliminated 28%, 14191 equivalent 41%
c vsts: 7271685600 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 52.6 search visits per propagation, 7032.9 per conflict
c wchs: 2359456448 pushed, 4012891 enlarged, 142 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1026349        701540        112585      19637017       8119998        593950
c 
c  0 0        108555  11     20983   3         0   0  12528137  64   4316529  53    267560  45     3.8
c  1 5         89958   9     58481   8     13402  12   2561414  13<  1143159  14<    83512  14<    0.9
c  2 6        329983  32<   245970  35     38336  34   3303458  17   1771793  22    158210  27     2.5
c  3 9        383365  37    293652  42<    42677  38<  1078671   5    762536   9     75158  13     2.6
c  4 14       108667  11     78788  11     16685  15    158009   1    120962   1      9160   2     0.9
c  5 21         5752   1      3626   1      1461   1      7248   0      4973   0       347   0     0.1
c  6 30           69   0        40   0        24   0        80   0        46   0         3   0     0.0
c 
c avg                  2.3           2.5           2.6           0.7           0.9           1.1
c std                  1.1           0.9           0.9           1.0           1.1           1.2
c 
c    3.008   2% cce
c    2.374   1% probe
c    1.996   1% elim
c    1.967   1% bump
c    1.284   1% sweep
c    1.096   1% decide
c 
c    1.929 < 1% rest (below)
c 
c    0.591   0% ternres
c    0.268   0% unhide
c    0.250   0% quatres
c    0.221   0% bca
c    0.183   0% block
c    0.162   0% gauss
c    0.129   0% transred
c    0.124   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.874   1% preprocessing     7%
c   10.778   6% inprocessing     93%
c ==================================
c   11.652   7% simplifying
c  161.313  93% search
c ==================================
c  172.965 100% all
c 
c       1028566 conflicts,        5946.7 confs/sec
c          2401 ternaries,         428.4 confs/ternary
c           245 binaries,         4198.2 confs/binary
c            28 iterations,      36734.5 confs/iteration
c 
c            23 reductions,          0.1 redus/sec,  44720.3 confs/reduction
c         19379 restarts,          112.0 rests/sec,     53.1 confs/restart
c       1734920 decisions,       10030.5 decis/sec,      1.7 decis/conflict
c     138844476 propagations,   802731.3 props/sec,     80.0 props/decision
c 
c 173.0 seconds, 34.4 MB
c launch: done
