c launch: /data/cnf/sc2014/app/slp-synthesis-aes-top29.cnf.bz2
c host: atom19
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/slp-synthesis-aes-top29.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/slp-synthesis-aes-top29.cnf.bz2
c no embedded options
c found 'p cnf 94998 302862' header
c read 94998 variables, 302862 clauses, 740744 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=6
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 91435 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] AVG (--score=6)
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   91435   284752         0       0      0     0    0     0   17   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 57 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 57 out of 57 constraints (100%) meet size limits
c [card-1] found 1 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 5165 variables
c [simpleprobe-1] all 89833 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 819 variables
c [simpleprobe-1] 1737 variables remain 2% (87277 retained 98%)
c [simpleprobe-1] removed 819 variables, found 6467 hbrs, 86 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 2 failed, 1008 tauts, 0 hbrs, 384 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 89013 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 64372 variables 72% in round 1 in 14604295 steps
c [elim-1-1] backward subsumption/strengthening limit 5395705
c [elim-1-1-1] backward checking 64470 touched variables 72%
c [elim-1-1-1] incomplete backward checking 63356 remain 98%
c [elim-1-1] subsumed 161 and strengthened 553 clauses in 5395908 steps
c [elim-1] incomplete 868 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 64372 = 72% variables out of 89013 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 135503 negative 95.8% of 141475 except 5972 4.2%
c [phase-count-1] 133194 positive 94.1% of 141475 except 8281 5.9%
c [phase-1] phase bias: 4189 positive 17%, 20452 negative 83%
c [sort-queue-1] sorted 24641 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 24641 (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 66794 variables 73.1% (24641 remain 27%)
c [simplification-1] removed 143277 irredundant clauses 50.3% (141475 remain 50%)
c [simplification-1] maximum reduction of 73% = max (73%, 50%)
c [simplification-1] large reduction 73% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 134 variables
c [simpleprobe-2] 582 schedulable variables 2%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 3 variables
c [simpleprobe-2] 837 variables remain 3% (23667 retained 97%)
c [simpleprobe-2] removed 3 variables, found 382 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 26645 literals 54%
c [treelook-1] scheduling used 300005 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 325340 steps
c [treelook-1] 26623 literals remain 54%
c [treelook-1] 19047 variables remain to probed next time 78%
c [decomp-5] removed 1 variables
c [treelook-1] removed 2 variables, found 524 hbrs
c [basicprobe-1] limit 1129456 based on 141182 irredundant clauses
c [basicprobe-1-0] 7066 probes remain 29% after last round
c [basicprobe-1-0] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 5 variables, found 934 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 3 failed, 37 tauts, 0 hbrs, 1038 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 24496 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 620 not tried 3% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 197 = 1% variables out of 24496 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 133276 negative 95.7% of 139262 except 5986 4.3%
c [phase-count-2] 131153 positive 94.2% of 139262 except 8109 5.8%
c [phase-2] phase bias: 14 positive 27%, 38 negative 73%
c [sort-queue-2] sorted 20531 enqueued variables after 1000 conflicts
c [score-dist-2] active 3768 (16%), one 0 (0%), zero 20531 (84%)
c [score-dist-2] max exp 511, different 11 (2%)
c [score-dist-2] median active exp 509, avg 508.8
c [simplification-2] removed 342 variables 1.4% (24299 remain 27%)
c [simplification-2] removed 2213 irredundant clauses 1.6% (139262 remain 49%)
c [simplification-2] maximum reduction of 2% = max (1%, 2%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 6666
c [simplification-2] penalized conflict interval 6666 = 1 * 6666
c [simplification-2] hard conflict limit 17666 (soft 7666 + delta 10000)
c [simplification-2] new conflict limit 7666 (hard 17666)
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    4.7   24298   139262      3826    3321    131  3196    6    37   17  16%     43   35    9    1 1717%
c 
c [simplification-3] limit of 146 binary hit after 146 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 173 at-most-one constraints of average size 3.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 173 out of 173 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 18 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 23321 literals 48%
c [treelook-2] scheduling used 300008 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 470112 steps
c [treelook-2] 23227 literals remain 48%
c [treelook-2] 17085 variables remain to probed next time 70%
c [decomp-7] removed 23 variables
c [treelook-2] removed 55 variables, found 2031 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 5 failed, 45 tauts, 0 hbrs, 485 literals
c [elim-3] 619 variables 3% will be scheduled this time
c [elim-3] scheduled 619 variables 3%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 288 not tried 1% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 619 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 131974 negative 96.5% of 136789 except 4815 3.5%
c [phase-count-3] 128713 positive 94.1% of 136789 except 8076 5.9%
c [phase-3] phase bias: 1 positive 8%, 12 negative 92%
c [sort-queue-3] sorted 18168 enqueued variables after 4114 conflicts
c [score-dist-3] active 6053 (25%), one 0 (0%), zero 18168 (75%)
c [score-dist-3] max exp 513, different 13 (3%)
c [score-dist-3] median active exp 513, avg 511.2
c [simplification-3] removed 77 variables 0.3% (24221 remain 26%)
c [simplification-3] removed 2473 irredundant clauses 1.8% (136789 remain 48%)
c [simplification-3] maximum reduction of 2% = max (0%, 2%)
c [simplification-3] forced so keeping old conflict interval 6666
c [simplification-3] conflict limit remains at 7666 (hard 17666)
c [simplification-3] new binary interval 1000
c 
c [simplification-4] limit 7666 conflicts (hard 17666) hit after 7667 conflicts
c [decomp-8] removed 2 variables
c [basicprobe-2] limit 1513751 penalty 0 = 0 + 0
c [basicprobe-2-0] 5080 probes remain 21% after last round
c [basicprobe-2-0] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 9 variables, found 2915 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 1 units, 0 failed, 111 tauts, 0 hbrs, 1676 literals
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 24209 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 370 variables 2% in round 1 in 70435779 steps
c [elim-4-1] backward subsumption/strengthening limit 70435700
c [elim-4-1-1] backward checking 2511 touched variables 10%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 21 clauses in 7086637 steps
c [elim-4-1] rescheduled 168 variables 1% by backward subsumption
c [elim-4-2] eliminated 1 variables 0% in round 2 in 1465022 steps
c [elim-4-2] backward subsumption/strengthening limit 1465000
c [elim-4-2-1] backward checking 20 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 145157 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 372 = 2% variables out of 24209 scheduled
c [phase-count-4] 130235 negative 96.2% of 135320 except 5085 3.8%
c [phase-count-4] 127285 positive 94.1% of 135320 except 8035 5.9%
c [phase-4] phase bias: 3 positive 16%, 16 negative 84%
c [sort-queue-4] sorted 15972 enqueued variables after 7667 conflicts
c [score-dist-4] active 7865 (33%), one 0 (0%), zero 15972 (67%)
c [score-dist-4] max exp 514, different 14 (3%)
c [score-dist-4] median active exp 514, avg 512.6
c [simplification-4] removed 384 variables 1.6% (23837 remain 26%)
c [simplification-4] removed 1469 irredundant clauses 1.1% (135320 remain 48%)
c [simplification-4] maximum reduction of 2% = max (2%, 1%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 13332
c [simplification-4] penalized conflict interval 13332 = 1 * 13332
c [simplification-4] hard conflict limit 30999 (soft 20999 + delta 10000)
c [simplification-4] new conflict limit 20999 (hard 30999)
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.9   23836   135320     15761   13213    640  7608   10    56   18  18%    155   47   10    2  475%
c i    9.6   23835   135320     19047   15847    812  7941   10    56   18  17%     25   44   10    2  405%
c 
c [simplification-5] limit 20999 conflicts (hard 30999) hit after 20999 conflicts
c [quatres-1] found 52276 quaternary clauses 76% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 39 single-self-subsuming ternary resolvents
c [quatres-1-2] added 40961 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 23828 free variables schedulable
c [ternres-1] 16412 ternary resolvents (73 bin, 16339 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 13107 xors of average arity 3.0
c [gauss-1] connected 39101 occurrences of 2451 variables (average 16.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 112 variables
c [simpleprobe-3] 752 schedulable variables 3%
c [simpleprobe-3] limit 4079091 penalty 0 = 0 + 0
c [decomp-10] removed 7 variables
c [simpleprobe-3] 912 variables remain 4% (22797 retained 96%)
c [simpleprobe-3] removed 7 variables, found 441 hbrs, 1 units
c [unhide-5] limit 203954 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 3 failed, 42 tauts, 0 hbrs, 1741 literals
c [transred-1] limit 1019772 with penalty 0 = 0 + 0
c [transred-1] removed 73 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 23705 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 14213 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 36
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 35
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 34
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 33
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 32
c [cce-1-1] eliminated 1 clauses out of 4 (25%) of length 31
c [cce-1-1] eliminated 1 clauses out of 8 (12%) of length 30
c [cce-1-1] eliminated 1 clauses out of 9 (11%) of length 29
c [cce-1-1] eliminated 1 clauses out of 12 (8%) of length 28
c [cce-1-1] eliminated 1 clauses out of 11 (9%) of length 27
c [cce-1-1] eliminated 3 clauses out of 24 (12%) of length 26
c [cce-1-1] eliminated 1 clauses out of 34 (3%) of length 25
c [cce-1-1] eliminated 1 clauses out of 24 (4%) of length 24
c [cce-1-1] eliminated 2 clauses out of 34 (6%) of length 23
c [cce-1-1] eliminated 1 clauses out of 38 (3%) of length 22
c [cce-1-1] eliminated 1 clauses out of 45 (2%) of length 21
c [cce-1-1] eliminated 1 clauses out of 44 (2%) of length 20
c [cce-1-1] eliminated 11 clauses out of 61 (18%) of length 19
c [cce-1-1] eliminated 11 clauses out of 67 (16%) of length 18
c [cce-1-1] eliminated 11 clauses out of 73 (15%) of length 17
c [cce-1-1] eliminated 4 clauses out of 62 (6%) of length 16
c [cce-1-1] eliminated 28 clauses out of 127 (22%) of length 15
c [cce-1-1] eliminated 9 clauses out of 91 (10%) of length 14
c [cce-1-1] eliminated 19 clauses out of 120 (16%) of length 13
c [cce-1-1] eliminated 27 clauses out of 132 (20%) of length 12
c [cce-1-1] eliminated 56 clauses out of 3229 (2%) of length 11
c [cce-1-1] eliminated 56 clauses out of 272 (21%) of length 10
c [cce-1-1] eliminated 90 clauses out of 2169 (4%) of length 9
c [cce-1-1] eliminated 61 clauses out of 1093 (6%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 403 large clauses in 30000058 steps
c [cce-1-1] allowing another 15000029 steps for small clauses
c [cce-1-1] scheduling 35221 clauses = 19565 binary + 15656 ternary
c [cce-1-1] tried to eliminate 3961 small clauses 11%
c [cce-1-1] eliminated 136 binary clauses 1%
c [cce-1-1] eliminated 87 ternary clauses 1%
c [cce-1-1] eliminated 223 small clauses 1%
c [cce-1-1] eliminated 223 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 626 covered clauses in round 1
c [cce-1] eliminated 626 covered clauses in TOTAL during 1 rounds
c [cce-1] 626 < 1/100 * 119946 = 1199 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 23694 variables 100%
c [elim-5] limit of 20395459 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 478 not tried 2% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 267 = 1% variables out of 23694 scheduled
c [bca-1] limit of 10000000 steps and 238220 added (scaled 2)
c [bca-1] 18936 out of 46856 literals actually usable 40%
c [bca-1] added 676 blocked clauses in 101252 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 7400 pos 31.6% + 16027 neg 68.4% = 23427 sched 100.0% ret 0
c [sweep-1-1] 1052578 steps 45 queries 4136.13 avg class size
c [sweep-1-1] 1353 decisions 42 SAT calls 78.43 avg env size
c [sweep-1-1] 22037 variables remain 94% (1390 retained 6%)
c [decomp-11] removed 5 variables
c [sweep-1-1] removed 5 vars (0 failed, 2 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 5 vars in TOTAL (1 rounds, 44 queries)
c [phase-count-5] 114539 negative 96.4% of 118852 except 4313 3.6%
c [phase-count-5] 111018 positive 93.4% of 118852 except 7834 6.6%
c [phase-5] phase bias: 692 positive 93%, 51 negative 7%
c [sort-queue-5] sorted 12908 enqueued variables after 20999 conflicts
c [score-dist-5] active 10514 (45%), one 0 (0%), zero 12908 (55%)
c [score-dist-5] max exp 516, different 14 (3%)
c [score-dist-5] median active exp 516, avg 515.4
c [simplification-5] removed 406 variables 1.7% (23422 remain 26%)
c [simplification-5] removed 16468 irredundant clauses 12.2% (118852 remain 42%)
c [simplification-5] maximum reduction of 12% = max (2%, 12%)
c [simplification-5] large reduction 12% >= 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 32999 (soft 22999 + delta 10000)
c [simplification-5] new conflict limit 22999 (hard 32999)
c 
c [simplification-6] limit 22999 conflicts (hard 32999) hit after 22999 conflicts
c [quatres-2] found 91026 quaternary clauses 86% in total
c [quatres-2-1] removed 3 duplicate quaternary clauses
c [quatres-2-2] added 137 single-self-subsuming ternary resolvents
c [quatres-2-2] added 31721 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 23422 free variables schedulable
c [ternres-2] 149 ternary resolvents (2 bin, 147 trn)
c [ternres-2] 12069 variables remain 52% (11353 retained 48%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 102 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] 102 out of 102 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 15054 literals 32%
c [treelook-3] scheduling used 300004 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 301246 steps
c [treelook-3] 15047 literals remain 32%
c [treelook-3] 11753 variables remain to probed next time 50%
c [treelook-3] removed 0 variables, found 1149 hbrs
c [unhide-6] limit 231847 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 3 failed, 588 tauts, 0 hbrs, 2125 literals
c [transred-2] limit 1159235 with penalty 0 = 0 + 0
c [transred-2] removed 55 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 23415 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 14 blocked clauses
c [block-2] 14 < 1/100 * 118752 = 1187 considered unsuccessful
c [elim-6] 478 variables 2% will be scheduled this time
c [elim-6] scheduled 478 variables 2%
c [elim-6] limit of 23184700 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 95 not tried 0% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 478 scheduled
c [bca-2] limit of 10000000 steps and 238190 added (scaled 2)
c [bca-2] 18455 out of 46832 literals actually usable 39%
c [bca-2] added 3 blocked clauses in 132666 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 7572 pos 34.4% + 14455 neg 65.6% = 22027 sched 94.1% ret 1388
c [sweep-2-1] 1005418 steps 57 queries 4324.37 avg class size
c [sweep-2-1] 1547 decisions 55 SAT calls 50.27 avg env size
c [sweep-2-1] 20669 variables remain 88% (2720 retained 12%)
c [decomp-14] removed 331 variables
c [sweep-2-1] removed 331 vars (0 failed, 1 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 331 vars in TOTAL (1 rounds, 56 queries)
c [phase-count-6] 112201 negative 96.4% of 116438 except 4237 3.6%
c [phase-count-6] 108683 positive 93.3% of 116438 except 7755 6.7%
c [phase-6] phase bias: 330 positive 65%, 181 negative 35%
c [sort-queue-6] sorted 12468 enqueued variables after 22999 conflicts
c [score-dist-6] active 10616 (46%), one 0 (0%), zero 12468 (54%)
c [score-dist-6] max exp 516, different 14 (3%)
c [score-dist-6] median active exp 516, avg 515.6
c [simplification-6] removed 338 variables 1.4% (23084 remain 25%)
c [simplification-6] removed 2414 irredundant clauses 2.0% (116438 remain 41%)
c [simplification-6] maximum reduction of 2% = max (1%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 19998
c [simplification-6] penalized conflict interval 19998 = 1 * 19998
c [simplification-6] hard conflict limit 52997 (soft 42997 + delta 10000)
c [simplification-6] new conflict limit 42997 (hard 52997)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   15.3   23083   116438     24432   88992  25625 11961   10    55   27  18%     49   40   11    3  342%
c i   15.3   23082   116438     24612   89139  25635 11971   10    56   27  18%     39   41   12    3  402%
c i   15.3   23081   116438     24620   89143  25635 11974   10    56   27  18%     38   41   12    3  391%
c i   15.4   23046   116438     25109   89587  25660 11983   10    57   27  18%     18   41   12    3  366%
c i   15.5   23042   116438     25376   89796  25684 12003   10    58   27  18%     10   42   12    3  378%
c i   15.7   23040   116438     25984   90358  25701 12010   11    60   27  18%     -1   44   11    3  343%
c i   19.5   23039   116438     40615  103756  26141 12244   12    64   29  19%    176   39   13    5  258%
c i   19.9   23010   116438     42243  105272  26189 12265   12    66   29  19%     18   40   12    5  224%
c 
c [simplification-7] limit 42998 conflicts (hard 52997) hit after 45509 conflicts
c [quatres-3] found 110846 quaternary clauses 88% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-2] added 186 single-self-subsuming ternary resolvents
c [quatres-3-2] added 4660 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 11856 schedulable variables 51%
c [ternres-3] 210 ternary resolvents (1 bin, 209 trn)
c [ternres-3] 1029 variables remain 4% (21981 retained 96%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 7119 xors of average arity 2.9
c [gauss-2] connected 20294 occurrences of 3039 variables (average 6.7)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [decomp-15] removed 845 variables
c [gauss-2] exported 0 unary, 1 binary and 0 ternary equations
c [basicprobe-3] limit 15027562 penalty 0 = 0 + 0
c [basicprobe-3-0] 5698 sched 26%, 42 failed, 2 lifted, 8609 hbrs
c [decomp-17] removed 698 variables
c [basicprobe-3-1] 9516 sched 45%, 148 failed, 14 lifted, 5332 hbrs
c [decomp-18] removed 415 variables
c [basicprobe-3-2] 9352 sched 45%, 108 failed, 15 lifted, 1288 hbrs
c [decomp-19] removed 182 variables
c [basicprobe-3-3] 8815 probes remain 42% after last round
c [basicprobe-3-3] 334 units = 303 failed (91%) + 31 lifted (9%)
c [basicprobe-3-3] removed 1305 variables, found 15339 hbrs
c [bate-1] eliminated 446 asymmetric tautologies during probing
c [unhide-7] limit 601102 with penalty 0 = 0 + 0
c [unhide-7-7] 7 units, 1 failed, 192 tauts, 0 hbrs, 4014 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 235 transitive binary clauses
c [transred-3] found 2 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 30
c [cce-2-1] eliminated 1 clauses out of 34 (3%) of length 25
c [cce-2-1] eliminated 1 clauses out of 46 (2%) of length 21
c [cce-2-1] eliminated 1 clauses out of 48 (2%) of length 20
c [cce-2-1] eliminated 4 clauses out of 55 (7%) of length 19
c [cce-2-1] eliminated 3 clauses out of 69 (4%) of length 17
c [cce-2-1] eliminated 5 clauses out of 59 (8%) of length 16
c [cce-2-1] eliminated 7 clauses out of 91 (8%) of length 14
c [cce-2-1] eliminated 4 clauses out of 105 (4%) of length 13
c [cce-2-1] eliminated 7 clauses out of 109 (6%) of length 12
c [cce-2-1] eliminated 16 clauses out of 2811 (1%) of length 11
c [cce-2-1] eliminated 11 clauses out of 319 (3%) of length 10
c [cce-2-1] eliminated 1 clauses out of 2096 (0%) of length 9
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 63 large clauses in 15000015 steps
c [cce-2-1] allowing another 7500007 steps for small clauses
c [cce-2-1] scheduling 38664 clauses = 17776 binary + 20888 ternary
c [cce-2-1] tried to eliminate 2240 small clauses 6%
c [cce-2-1] eliminated 31 binary clauses 0%
c [cce-2-1] eliminated 25 ternary clauses 0%
c [cce-2-1] eliminated 56 small clauses 0%
c [cce-2-1] eliminated 115 small clauses in 15000058 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 178 covered clauses in round 1
c [cce-2] eliminated 178 covered clauses in TOTAL during 1 rounds
c [cce-2] 178 < 1/100 * 101050 = 1010 considered unsuccessful
c [bca-3] limit of 10000000 steps and 202583 added (scaled 2)
c [bca-3] 15579 out of 41694 literals actually usable 37%
c [bca-3] added 14 blocked clauses in 128511 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 8468 pos 46.0% + 9957 neg 54.0% = 18425 sched 88.4% ret 2421
c [sweep-3-1] 1076445 steps 43 queries 2943.98 avg class size
c [sweep-3-1] 1568 decisions 42 SAT calls 79.36 avg env size
c [sweep-3-1] 17544 variables remain 84% (3298 retained 16%)
c [decomp-20] removed 5 variables
c [sweep-3-1] removed 5 vars (0 failed, 2 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 5 vars in TOTAL (1 rounds, 42 queries)
c [phase-count-7] 96957 negative 96.1% of 100843 except 3886 3.9%
c [phase-count-7] 93292 positive 92.5% of 100843 except 7551 7.5%
c [phase-7] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-7] sorted 9566 enqueued variables after 45509 conflicts
c [score-dist-7] active 11275 (54%), one 0 (0%), zero 9566 (46%)
c [score-dist-7] max exp 517, different 12 (2%)
c [score-dist-7] median active exp 517, avg 516.5
c [simplification-7] removed 2169 variables 9.4% (20841 remain 23%)
c [simplification-7] removed 15595 irredundant clauses 13.4% (100843 remain 35%)
c [simplification-7] maximum reduction of 13% = max (9%, 13%)
c [simplification-7] large reduction 13% >= 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 57509 (soft 47509 + delta 10000)
c [simplification-7] new conflict limit 47509 (hard 57509)
c 
c [simplification-8] limit 47509 conflicts (hard 57509) hit after 47509 conflicts
c [quatres-4] found 99980 quaternary clauses 87% in total
c [quatres-4-1] removed 5 duplicate quaternary clauses
c [quatres-4-2] added 1858 single-self-subsuming ternary resolvents
c [quatres-4-2] added 3757 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 914 schedulable variables 4%
c [ternres-4] 354 ternary resolvents (9 bin, 345 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 11593 xors of average arity 3.0
c [gauss-3] connected 34655 occurrences of 2131 variables (average 16.3)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] 783 schedulable variables 4%
c [simpleprobe-4] limit 12738274 penalty 0 = 0 + 0
c [decomp-22] removed 67 variables
c [simpleprobe-4] 676 variables remain 3% (20098 retained 97%)
c [simpleprobe-4] removed 67 variables, found 836 hbrs, 15 units
c [unhide-8] limit 636913 with penalty 0 = 0 + 0
c [unhide-8-8] 0 units, 17 failed, 1740 tauts, 0 hbrs, 6443 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 110 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 20736 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 433 blocked clauses
c [block-3] 433 < 1/100 * 100545 = 1005 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 20709 variables 100%
c [elim-7] limit of 31845687 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 116 not tried 1% in round 1
c [gc-52] reconnected 19789 binary clauses (produced 0 empty 1 units)
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 565 = 3% variables out of 20709 scheduled
c [bca-4] limit of 10000000 steps and 198044 added (scaled 2)
c [bca-4] 15508 out of 40290 literals actually usable 38%
c [bca-4] added 105 blocked clauses in 128126 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 7918 pos 46.7% + 9042 neg 53.3% = 16960 sched 84.2% ret 3184
c [sweep-4-1] 1005483 steps 74 queries 3091.91 avg class size
c [sweep-4-1] 1449 decisions 69 SAT calls 51.61 avg env size
c [sweep-4-1] 16094 variables remain 80% (4050 retained 20%)
c [decomp-23] removed 5 variables
c [sweep-4-1] removed 5 vars (0 failed, 4 eqs, 7 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 5 vars in TOTAL (1 rounds, 73 queries)
c [phase-count-8] 94702 negative 96.1% of 98588 except 3886 3.9%
c [phase-count-8] 91091 positive 92.4% of 98588 except 7497 7.6%
c [phase-8] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-8] sorted 8916 enqueued variables after 47509 conflicts
c [score-dist-8] active 11223 (56%), one 0 (0%), zero 8916 (44%)
c [score-dist-8] max exp 517, different 12 (2%)
c [score-dist-8] median active exp 517, avg 516.5
c [simplification-8] removed 702 variables 3.4% (20139 remain 22%)
c [simplification-8] removed 2255 irredundant clauses 2.2% (98588 remain 35%)
c [simplification-8] maximum reduction of 3% = max (3%, 2%)
c [simplification-8] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-8] new conflict interval 24998
c [simplification-8] penalized conflict interval 24998 = 1 * 24998
c [simplification-8] hard conflict limit 85006 (soft 72507 + delta 12499)
c [simplification-8] new conflict limit 72507 (hard 85006)
c 
c [simplification-9] limit 72507 conflicts (hard 85006) hit after 72508 conflicts
c [quatres-5] found 98419 quaternary clauses 85% in total
c [quatres-5-1] removed 3 duplicate quaternary clauses
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 1559 single-self-subsuming ternary resolvents
c [quatres-5-2] added 3695 quaternary resolvents
c [ternres-5] limit 5747213 with penalty 0 = 0 + 0
c [ternres-5] all 20139 free variables schedulable
c [ternres-5] 607 ternary resolvents (2 bin, 605 trn)
c [ternres-5] 8643 variables remain 43% (11496 retained 57%)
c [decomp-24] removed 1 variables
c [unhide-9] limit 1149442 with penalty 0 = 0 + 0
c [unhide-9-9] 2 units, 3 failed, 225 tauts, 0 hbrs, 6878 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 94 transitive binary clauses
c [elim-8] 67 variables 0% will be scheduled this time
c [elim-8] scheduled 67 variables 0%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2298885300 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 6824152 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 67 scheduled
c [bca-5] limit of 10000000 steps and 197635 added (scaled 2)
c [bca-5] 14410 out of 40230 literals actually usable 36%
c [bca-5] added 4 blocked clauses in 151370 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 17241630 penalty 0 = 0 + 0
c [sweep-5-1] 7474 pos 46.5% + 8599 neg 53.5% = 16073 sched 79.9% ret 4041
c [sweep-5-1] 17254020 steps 780 queries 461.29 avg class size
c [sweep-5-1] 16731 decisions 759 SAT calls 49.83 avg env size
c [sweep-5-1] 8065 variables remain 40% (11992 retained 60%)
c [decomp-25] removed 102 variables
c [sweep-5-1] removed 102 vars (0 failed, 29 eqs, 41 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 102 vars in TOTAL (1 rounds, 779 queries)
c [phase-count-9] 93875 negative 96.0% of 97795 except 3920 4.0%
c [phase-count-9] 90273 positive 92.3% of 97795 except 7522 7.7%
c [phase-9] phase bias: 4 positive 100%, 0 negative 0%
c [sort-queue-9] sorted 7798 enqueued variables after 72508 conflicts
c [score-dist-9] active 12214 (61%), one 0 (0%), zero 7798 (39%)
c [score-dist-9] max exp 518, different 13 (3%)
c [score-dist-9] median active exp 517, avg 517.1
c [simplification-9] removed 127 variables 0.6% (20012 remain 22%)
c [simplification-9] removed 793 irredundant clauses 0.8% (97795 remain 34%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 12499 = 24998 / 2
c [simplification-9] new conflict interval 37497
c [simplification-9] penalized conflict interval 37497 = 1 * 37497
c [simplification-9] hard conflict limit 128753 (soft 110005 + delta 18748)
c [simplification-9] new conflict limit 110005 (hard 128753)
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 -   38.7   20012    97795     73539   75690  25139 20328   16    83   24  19%    354   38   16    9  185%
c i   48.8   20011    97795    103369  104373  25440 20377   16    75   30  21%    599   18   14   11  128%
c i   53.3   20010    97795    114383  115033  25512 20387   17    78   33  22%   -155   17   19   12  160%
c -   58.0   20010    97795    124839   81697  25571 20398   17    78   24  22%   -130   15   17   13  135%
c 
c [simplification-10] limit 110005 conflicts (hard 128753) hit after 128756 conflicts
c [quatres-6] found 99485 quaternary clauses 83% in total
c [quatres-6-1] removed 5 duplicate quaternary clauses
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 559 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1590 quaternary resolvents
c [ternres-6] limit 11506390 with penalty 0 = 0 + 0
c [ternres-6] 8577 schedulable variables 43%
c [ternres-6] 2894 ternary resolvents (9 bin, 2885 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 719149 penalty 3 = 3 + 0
c [card-4] found 135 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 719149 for elimination
c [card-4] 135 out of 135 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-4] limit 1150639 penalty 1 = 1 + 0
c [gauss-4] extracted 6638 xors of average arity 3.0
c [gauss-4] connected 19907 occurrences of 1975 variables (average 10.1)
c [gauss-4] limit 1150639 penalty 1 = 1 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-26] removed 7 variables
c [treelook-4] limit 575319 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 23427 literals 59%
c [treelook-4] scheduling used 575325 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 575319 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 578939 steps
c [treelook-4] 23392 literals remain 58%
c [treelook-4] 10225 variables remain to probed next time 51%
c [treelook-4] removed 1 variables, found 822 hbrs
c [unhide-10] limit 2301278 with penalty 0 = 0 + 0
c [unhide-10-12] 4 units, 27 failed, 1512 tauts, 0 hbrs, 7935 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 83 transitive binary clauses
c [cce-3] limit of 14382987 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 33
c [cce-3-1] eliminated 4 clauses out of 8 (50%) of length 28
c [cce-3-1] eliminated 1 clauses out of 38 (3%) of length 22
c [cce-3-1] eliminated 1 clauses out of 48 (2%) of length 20
c [cce-3-1] eliminated 3 clauses out of 54 (6%) of length 19
c [cce-3-1] eliminated 5 clauses out of 60 (8%) of length 18
c [cce-3-1] eliminated 2 clauses out of 67 (3%) of length 17
c [cce-3-1] eliminated 10 clauses out of 64 (16%) of length 16
c [cce-3-1] eliminated 4 clauses out of 101 (4%) of length 15
c [cce-3-1] eliminated 9 clauses out of 85 (11%) of length 14
c [cce-3-1] eliminated 9 clauses out of 109 (8%) of length 13
c [cce-3-1] eliminated 5 clauses out of 102 (5%) of length 12
c [cce-3-1] eliminated 20 clauses out of 2772 (1%) of length 11
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 77 large clauses in 14382988 steps
c [cce-3-1] allowing another 7191494 steps for small clauses
c [cce-3-1] scheduling 37815 clauses = 17835 binary + 19980 ternary
c [cce-3-1] tried to eliminate 1797 small clauses 5%
c [cce-3-1] eliminated 68 binary clauses 0%
c [cce-3-1] eliminated 25 ternary clauses 0%
c [cce-3-1] eliminated 93 small clauses 0%
c [cce-3-1] eliminated 121 small clauses in 14383001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 198 covered clauses in round 1
c [cce-3] eliminated 198 covered clauses in TOTAL during 1 rounds
c [cce-3] 198 < 1/100 * 97191 = 971 considered unsuccessful
c [bca-6] limit of 10000000 steps and 194887 added (scaled 2)
c [bca-6] 16716 out of 39908 literals actually usable 42%
c [bca-6] added 28 blocked clauses in 123316 steps
c [sweep-6] limit 3451917 penalty 0 = 0 + 0
c [sweep-6-1] 4702 pos 58.6% + 3327 neg 41.4% = 8029 sched 40.2% ret 11924
c [sweep-6-1] 3463750 steps 358 queries 798.32 avg class size
c [sweep-6-1] 2848 decisions 332 SAT calls 19.62 avg env size
c [sweep-6-1] 6933 variables remain 35% (13003 retained 65%)
c [decomp-28] removed 120 variables
c [sweep-6-1] removed 120 vars (0 failed, 27 eqs, 32 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 120 vars in TOTAL (1 rounds, 357 queries)
c [phase-count-10] 92097 negative 95.8% of 96089 except 3992 4.2%
c [phase-count-10] 88566 positive 92.2% of 96089 except 7523 7.8%
c [phase-10] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-10] sorted 7162 enqueued variables after 128756 conflicts
c [score-dist-10] active 12671 (64%), one 0 (0%), zero 7162 (36%)
c [score-dist-10] max exp 518, different 12 (2%)
c [score-dist-10] median active exp 518, avg 517.5
c [simplification-10] removed 177 variables 0.9% (19833 remain 22%)
c [simplification-10] removed 1706 irredundant clauses 1.7% (96089 remain 34%)
c [simplification-10] maximum reduction of 2% = max (1%, 2%)
c [simplification-10] geometric conflict interval increment 12499 = 37497 / 3
c [simplification-10] new conflict interval 49996
c [simplification-10] penalized conflict interval 49996 = 1 * 49996
c [simplification-10] hard conflict limit 203750 (soft 178752 + delta 24998)
c [simplification-10] new conflict limit 178752 (hard 203750)
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   65.9   19832    96089    145243  100372  28391 20150   16    69   28  23%    178    3   15   14  111%
c -   76.6   19832    96089    174974   88611  28506 20161   17    73   33  23%    176    5   20   15  134%
c 
c [simplification-11] limit 178752 conflicts (hard 203750) hit after 184771 conflicts
c [quatres-7] found 98504 quaternary clauses 81% in total
c [quatres-7-1] removed 5 duplicate quaternary clauses
c [quatres-7-2] added 942 single-self-subsuming ternary resolvents
c [quatres-7-2] added 890 quaternary resolvents
c [ternres-7] limit 16603425 with penalty 0 = 0 + 0
c [ternres-7] all 19832 free variables schedulable
c [ternres-7] 1429 ternary resolvents (10 bin, 1419 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-29] removed 1 variables
c [basicprobe-4] limit 83017128 penalty 0 = 0 + 0
c [basicprobe-4-0] 8692 sched 44%, 85 failed, 25 lifted, 1754 hbrs
c [decomp-30] removed 381 variables
c [basicprobe-4-1] 9070 sched 47%, 60 failed, 17 lifted, 1031 hbrs
c [decomp-31] removed 162 variables
c [basicprobe-4-2] 9051 sched 47%, 54 failed, 10 lifted, 625 hbrs
c [decomp-32] removed 172 variables
c [basicprobe-4-3] 9032 sched 48%, 43 failed, 8 lifted, 593 hbrs
c [decomp-33] removed 126 variables
c [basicprobe-4-4] 9039 sched 48%, 60 failed, 14 lifted, 456 hbrs
c [decomp-34] removed 137 variables
c [basicprobe-4-5] 9036 sched 48%, 58 failed, 24 lifted, 685 hbrs
c [decomp-35] removed 132 variables
c [basicprobe-4-6] 9011 sched 49%, 49 failed, 13 lifted, 705 hbrs
c [decomp-36] removed 158 variables
c [basicprobe-4-7] 9021 sched 49%, 56 failed, 14 lifted, 557 hbrs
c [decomp-37] removed 170 variables
c [basicprobe-4-8] 9012 sched 49%, 39 failed, 9 lifted, 548 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 638 units = 504 failed (79%) + 134 lifted (21%)
c [basicprobe-4-8] removed 1596 variables, found 6954 hbrs
c [bate-2] eliminated 609 asymmetric tautologies during probing
c [unhide-11] limit 3320685 with penalty 0 = 0 + 0
c [unhide-11-15] 8 units, 32 failed, 1693 tauts, 0 hbrs, 12907 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 130 transitive binary clauses
c [transred-7] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 18164 variables 100%
c [block-4] limit of 41508564 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 959 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 18046 variables 100%
c [elim-9] limit of 166034256 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 455 variables 3% in round 1 in 36807571 steps
c [elim-9-1] backward subsumption/strengthening limit 36807500
c [elim-9-1-1] backward checking 2560 touched variables 14%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 2 and strengthened 26 clauses in 3238502 steps
c [elim-9-1] rescheduled 60 variables 0% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 1169652 steps
c [elim-9-2] backward subsumption/strengthening limit 1169600
c [elim-9-2-1] backward checking 16 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 3 clauses in 122630 steps
c [elim-9-2] rescheduled 5 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 150692 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 458 = 3% variables out of 18046 scheduled
c [bca-7] limit of 10000000 steps and 167031 added (scaled 2)
c [bca-7] 15524 out of 35178 literals actually usable 44%
c [bca-7] added 53 blocked clauses in 109745 steps
c [sweep-7] limit 4981027 penalty 0 = 0 + 0
c [sweep-7-1] 3700 pos 64.4% + 2046 neg 35.6% = 5746 sched 32.7% ret 11842
c [sweep-7-1] 4990487 steps 438 queries 476.78 avg class size
c [sweep-7-1] 4527 decisions 435 SAT calls 24.35 avg env size
c [sweep-7-1] 4292 variables remain 24% (13272 retained 76%)
c [decomp-38] removed 42 variables
c [sweep-7-1] removed 42 vars (0 failed, 17 eqs, 20 impls)
c [sweep-7] removed 42 vars in TOTAL (1 rounds, 437 queries)
c [phase-count-11] 78816 negative 95.1% of 82919 except 4103 4.9%
c [phase-count-11] 75432 positive 91.0% of 82919 except 7487 9.0%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-11] sorted 4863 enqueued variables after 184771 conflicts
c [score-dist-11] active 12683 (72%), one 0 (0%), zero 4863 (28%)
c [score-dist-11] max exp 519, different 12 (2%)
c [score-dist-11] median active exp 519, avg 518.2
c [simplification-11] removed 2286 variables 11.5% (17546 remain 19%)
c [simplification-11] removed 13170 irredundant clauses 13.7% (82919 remain 29%)
c [simplification-11] maximum reduction of 14% = max (12%, 14%)
c [simplification-11] large reduction 14% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 196771 (soft 186771 + delta 10000)
c [simplification-11] new conflict limit 186771 (hard 196771)
c 
c [simplification-12] limit 186771 conflicts (hard 196771) hit after 186771 conflicts
c [quatres-8] found 70565 quaternary clauses 75% in total
c [quatres-8-1] removed 8 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 2122 single-self-subsuming ternary resolvents
c [quatres-8-2] added 2630 quaternary resolvents
c [ternres-8] limit 16797121 with penalty 0 = 0 + 0
c [ternres-8] all 17546 free variables schedulable
c [ternres-8] 2197 ternary resolvents (4 bin, 2193 trn)
c [ternres-8] fully completed ternary resolution
c [simpleprobe-5] 561 schedulable variables 3%
c [simpleprobe-5] limit 67188485 penalty 0 = 0 + 0
c [decomp-40] removed 56 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 56 variables, found 2063 hbrs, 22 units
c [unhide-12] limit 3359424 with penalty 0 = 0 + 0
c [unhide-12-19] 7 units, 11 failed, 2463 tauts, 0 hbrs, 5540 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 140 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 17439 variables 100%
c [elim-10] limit of 335942425 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 105 variables 1% in round 1 in 34895246 steps
c [elim-10-1] backward subsumption/strengthening limit 34895200
c [elim-10-1-1] backward checking 1027 touched variables 6%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 10 and strengthened 15 clauses in 1895465 steps
c [elim-10-1] rescheduled 36 variables 0% by backward subsumption
c [elim-10-2] eliminated 4 variables 0% in round 2 in 759249 steps
c [elim-10-2] backward subsumption/strengthening limit 759200
c [elim-10-2-1] backward checking 37 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 1 and strengthened 0 clauses in 152802 steps
c [elim-10-2] rescheduled 3 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 21561 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 116 = 1% variables out of 17439 scheduled
c [elim-10] 116 < 1/100 * 17439 = 174 considered unsuccessful
c [bca-8] limit of 10000000 steps and 164499 added (scaled 2)
c [bca-8] 15177 out of 34648 literals actually usable 44%
c [bca-8] added 19 blocked clauses in 108061 steps
c [sweep-8] limit 5039136 penalty 0 = 0 + 0
c [sweep-8-1] 2571 pos 61.3% + 1624 neg 38.7% = 4195 sched 24.2% ret 13128
c [sweep-8-1] 5040500 steps 566 queries 289.43 avg class size
c [sweep-8-1] 4665 decisions 562 SAT calls 19.86 avg env size
c [sweep-8-1] 2639 variables remain 15% (14682 retained 85%)
c [decomp-41] removed 12 variables
c [sweep-8-1] removed 12 vars (0 failed, 10 eqs, 11 impls)
c [sweep-8] 12 < 1/1000 * 17323 = 17 considered unsuccessful
c [sweep-8] removed 12 vars in TOTAL (1 rounds, 565 queries)
c [phase-count-12] 77566 negative 94.9% of 81746 except 4180 5.1%
c [phase-count-12] 74266 positive 90.8% of 81746 except 7480 9.2%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 4300 enqueued variables after 186771 conflicts
c [score-dist-12] active 13011 (75%), one 0 (0%), zero 4300 (25%)
c [score-dist-12] max exp 519, different 12 (2%)
c [score-dist-12] median active exp 519, avg 518.2
c [simplification-12] removed 235 variables 1.3% (17311 remain 19%)
c [simplification-12] removed 1173 irredundant clauses 1.4% (81746 remain 29%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 24998 = 49996 / 2
c [simplification-12] new conflict interval 74994
c [simplification-12] penalized conflict interval 74994 = 1 * 74994
c [simplification-12] hard conflict limit 299262 (soft 261765 + delta 37497)
c [simplification-12] new conflict limit 261765 (hard 299262)
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   88.4   17310    81746    190642   76849  28015 19815   15    59   24  25%    356   -9   11   15   72%
c -   99.2   17310    81746    228505   74474  28194 19834   16    62   31  25%    245   -7   15   16   95%
c 
c [simplification-13] limit 261765 conflicts (hard 299262) hit after 261766 conflicts
c [quatres-9] found 69159 quaternary clauses 72% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-1] added 6 double-self-subsuming ternary resolvents
c [quatres-9-2] added 912 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1026 quaternary resolvents
c [ternres-9] limit 23493836 with penalty 0 = 0 + 0
c [ternres-9] all 17310 free variables schedulable
c [ternres-9] 1101 ternary resolvents (2 bin, 1099 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-5] limit 1174691 penalty 2 = 2 + 0
c [gauss-5] extracted 7078 xors of average arity 3.0
c [gauss-5] connected 21215 occurrences of 2031 variables (average 10.4)
c [gauss-5] limit 1174691 penalty 2 = 2 + 0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-42] removed 13 variables
c [treelook-5] limit 2349383 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 23810 literals 69%
c [treelook-5] scheduling used 662612 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2349383 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2355290 steps
c [treelook-5] 23733 literals remain 69%
c [treelook-5] 9352 variables remain to probed next time 54%
c [treelook-5] removed 0 variables, found 3330 hbrs
c [unhide-13] limit 4698767 with penalty 0 = 0 + 0
c [unhide-13-23] 3 units, 28 failed, 1303 tauts, 0 hbrs, 49186 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 97 transitive binary clauses
c [transred-9] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 17271 variables 100%
c [block-5] limit of 117469181 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 66 blocked clauses
c [block-5] 66 < 1/100 * 81429 = 814 considered unsuccessful
c [bca-9] limit of 10000000 steps and 163529 added (scaled 2)
c [bca-9] 13407 out of 34544 literals actually usable 39%
c [bca-9] added 17 blocked clauses in 136784 steps
c [phase-count-13] 77072 negative 94.8% of 81289 except 4217 5.2%
c [phase-count-13] 73808 positive 90.8% of 81289 except 7481 9.2%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 4193 enqueued variables after 261766 conflicts
c [score-dist-13] active 13078 (76%), one 0 (0%), zero 4193 (24%)
c [score-dist-13] max exp 520, different 12 (2%)
c [score-dist-13] median active exp 519, avg 518.5
c [simplification-13] removed 39 variables 0.2% (17271 remain 19%)
c [simplification-13] removed 457 irredundant clauses 0.6% (81289 remain 29%)
c [simplification-13] maximum reduction of 1% = max (0%, 1%)
c [simplification-13] geometric conflict interval increment 37497 = 74994 / 2
c [simplification-13] new conflict interval 112491
c [simplification-13] penalized conflict interval 112491 = 1 * 112491
c [simplification-13] hard conflict limit 430502 (soft 374257 + delta 56245)
c [simplification-13] new conflict limit 374257 (hard 430502)
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  117.5   17270    81289    268834  113049  29879 21809   21    95   35  22%    603   18   20   18  115%
c -  118.3   17270    81289    271456   74634  29882 21809   20    88   23  23%   -477   10   22   18  125%
c -  133.6   17270    81289    316848   80471  29986 21816   22   100   34  22%    225   11   25   19  131%
c i  143.3   17269    81289    351511  114268  30061 21818   21    95   46  22%    553    6   25   19  128%
c -  145.7   17269    81289    359243   85845  30076 21820   20   111   35  18%   -560   20   23   19  118%
c 
c [simplification-14] limit 374257 conflicts (hard 430502) hit after 393657 conflicts
c [quatres-10] found 69064 quaternary clauses 68% in total
c [quatres-10-1] removed 6 duplicate quaternary clauses
c [quatres-10-2] added 446 single-self-subsuming ternary resolvents
c [quatres-10-2] added 445 quaternary resolvents
c [ternres-10] limit 35764605 with penalty 0 = 0 + 0
c [ternres-10] all 17269 free variables schedulable
c [ternres-10] 912 ternary resolvents (11 bin, 901 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-44] removed 25 variables
c [basicprobe-5] limit 178823026 penalty 0 = 0 + 0
c [basicprobe-5-0] 8886 sched 52%, 35 failed, 7 lifted, 737 hbrs
c [decomp-45] removed 131 variables
c [basicprobe-5-1] 8824 sched 52%, 39 failed, 7 lifted, 356 hbrs
c [decomp-46] removed 96 variables
c [basicprobe-5-2] 8794 sched 52%, 38 failed, 7 lifted, 556 hbrs
c [decomp-47] removed 58 variables
c [basicprobe-5-3] 8787 sched 52%, 47 failed, 13 lifted, 999 hbrs
c [decomp-48] removed 86 variables
c [basicprobe-5-4] 8759 sched 52%, 46 failed, 11 lifted, 440 hbrs
c [decomp-49] removed 105 variables
c [basicprobe-5-5] 8738 sched 52%, 30 failed, 8 lifted, 288 hbrs
c [decomp-50] removed 69 variables
c [basicprobe-5-6] 8742 sched 53%, 31 failed, 5 lifted, 573 hbrs
c [decomp-51] removed 79 variables
c [basicprobe-5-7] 8753 sched 53%, 35 failed, 9 lifted, 304 hbrs
c [decomp-52] removed 76 variables
c [basicprobe-5-8] 8740 sched 53%, 39 failed, 11 lifted, 280 hbrs
c [basicprobe-5-8] round limit 8 hit
c [basicprobe-5-8] 418 units = 340 failed (81%) + 78 lifted (19%)
c [basicprobe-5-8] removed 769 variables, found 4533 hbrs
c [bate-3] eliminated 444 asymmetric tautologies during probing
c [unhide-14] limit 7152921 with penalty 0 = 0 + 0
c [unhide-14-28] 5 units, 14 failed, 1485 tauts, 0 hbrs, 91570 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 66 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 223528782 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 47
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 46
c [cce-4-1] eliminated 8 clauses out of 8 (100%) of length 43
c [cce-4-1] eliminated 14 clauses out of 15 (93%) of length 42
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 41
c [cce-4-1] eliminated 4 clauses out of 5 (80%) of length 39
c [cce-4-1] eliminated 2 clauses out of 7 (29%) of length 38
c [cce-4-1] eliminated 4 clauses out of 7 (57%) of length 37
c [cce-4-1] eliminated 6 clauses out of 11 (55%) of length 35
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 34
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 32
c [cce-4-1] eliminated 4 clauses out of 8 (50%) of length 31
c [cce-4-1] eliminated 6 clauses out of 15 (40%) of length 30
c [cce-4-1] eliminated 2 clauses out of 15 (13%) of length 28
c [cce-4-1] eliminated 2 clauses out of 12 (17%) of length 27
c [cce-4-1] eliminated 2 clauses out of 39 (5%) of length 25
c [cce-4-1] eliminated 4 clauses out of 35 (11%) of length 24
c [cce-4-1] eliminated 6 clauses out of 54 (11%) of length 23
c [cce-4-1] eliminated 1 clauses out of 51 (2%) of length 21
c [cce-4-1] eliminated 1 clauses out of 51 (2%) of length 20
c [cce-4-1] eliminated 1 clauses out of 64 (2%) of length 19
c [cce-4-1] eliminated 4 clauses out of 72 (6%) of length 18
c [cce-4-1] eliminated 7 clauses out of 82 (9%) of length 16
c [cce-4-1] eliminated 6 clauses out of 116 (5%) of length 15
c [cce-4-1] eliminated 5 clauses out of 100 (5%) of length 14
c [cce-4-1] eliminated 9 clauses out of 118 (8%) of length 13
c [cce-4-1] eliminated 14 clauses out of 131 (11%) of length 12
c [cce-4-1] eliminated 12 clauses out of 2709 (0%) of length 11
c [cce-4-1] eliminated 33 clauses out of 373 (9%) of length 10
c [cce-4-1] eliminated 39 clauses out of 2103 (2%) of length 9
c [cce-4-1] eliminated 144 clauses out of 901 (16%) of length 8
c [cce-4-1] eliminated 84 clauses out of 907 (9%) of length 7
c [cce-4-1] eliminated 78 clauses out of 843 (9%) of length 6
c [cce-4-1] eliminated 112 clauses out of 1000 (11%) of length 5
c [cce-4-1] eliminated 3057 clauses out of 20669 (15%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 3685 large clauses in 70222437 steps
c [cce-4-1] allowing another 35111218 steps for small clauses
c [cce-4-1] scheduling 28220 clauses = 17523 binary + 10697 ternary
c [cce-4-1] tried to eliminate 28220 small clauses 100%
c [cce-4-1] eliminated 605 binary clauses 3%
c [cce-4-1] eliminated 143 ternary clauses 1%
c [cce-4-1] eliminated 748 small clauses 3%
c [cce-4-1] eliminated 767 small clauses in 90654269 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 4452 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 29710373 steps for small clauses
c [cce-4-2] scheduling 27472 clauses = 16918 binary + 10554 ternary
c [cce-4-2] tried to eliminate 27472 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 4452 covered clauses in TOTAL during 2 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 16441 variables 100%
c [elim-11] limit of 357646052 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 484 variables 3% in round 1 in 27701400 steps
c [elim-11-1] backward subsumption/strengthening limit 27701400
c [elim-11-1-1] backward checking 1777 touched variables 11%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 2 clauses in 1861764 steps
c [elim-11-1] rescheduled 12 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 173552 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 485 = 3% variables out of 16441 scheduled
c [bca-10] limit of 10000000 steps and 142637 added (scaled 2)
c [bca-10] 13675 out of 31914 literals actually usable 43%
c [bca-10] added 21 blocked clauses in 117896 steps
c [sweep-9] limit 5364690 penalty 1 = 1 + 0
c [sweep-9-1] 1444 pos 63.2% + 841 neg 36.8% = 2285 sched 14.3% ret 13671
c [sweep-9-1] 5396572 steps 517 queries 164.25 avg class size
c [sweep-9-1] 6206 decisions 515 SAT calls 24.54 avg env size
c [sweep-9-1] 956 variables remain 6% (14992 retained 94%)
c [decomp-53] removed 22 variables
c [sweep-9-1] removed 22 vars (0 failed, 13 eqs, 17 impls)
c [sweep-9] removed 22 vars in TOTAL (1 rounds, 516 queries)
c [phase-count-14] 67009 negative 94.7% of 70784 except 3775 5.3%
c [phase-count-14] 63324 positive 89.5% of 70784 except 7460 10.5%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 2926 enqueued variables after 393657 conflicts
c [score-dist-14] active 13008 (82%), one 0 (0%), zero 2926 (18%)
c [score-dist-14] max exp 520, different 12 (2%)
c [score-dist-14] median active exp 520, avg 519.2
c [simplification-14] removed 1335 variables 7.7% (15934 remain 17%)
c [simplification-14] removed 10505 irredundant clauses 12.9% (70784 remain 25%)
c [simplification-14] maximum reduction of 13% = max (8%, 13%)
c [simplification-14] large reduction 13% >= 5% limit
c [simplification-14] next conflict interval 3936 = min (393657/100, 112491)
c [simplification-14] penalized conflict interval 3936 = 1 * 3936
c [simplification-14] hard conflict limit 407593 (soft 397593 + delta 10000)
c [simplification-14] new conflict limit 397593 (hard 407593)
c 
c [simplification-15] limit 397593 conflicts (hard 407593) hit after 397594 conflicts
c [quatres-11] found 51777 quaternary clauses 62% in total
c [quatres-11-1] removed 5 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 456 single-self-subsuming ternary resolvents
c [quatres-11-2] added 1927 quaternary resolvents
c [ternres-11] limit 36081226 with penalty 0 = 0 + 0
c [ternres-11] all 15934 free variables schedulable
c [ternres-11] 747 ternary resolvents (4 bin, 743 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1127538 penalty 4 = 4 + 0
c [card-5] found 313 at-most-one constraints of average size 3.4
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1127538 for elimination
c [card-5] 313 out of 313 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [simpleprobe-6] all 15934 free variables schedulable
c [simpleprobe-6] limit 144324904 penalty 0 = 0 + 0
c [decomp-55] removed 11 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 11 variables, found 4322 hbrs, 9 units
c [unhide-15] limit 7216245 with penalty 0 = 0 + 0
c [unhide-15-34] 0 units, 8 failed, 3539 tauts, 0 hbrs, 19747 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 71 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 15895 variables 100%
c [elim-12] limit of 721624524 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 32 variables 0% in round 1 in 27069237 steps
c [elim-12-1] backward subsumption/strengthening limit 27069200
c [elim-12-1-1] backward checking 385 touched variables 2%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 1 and strengthened 0 clauses in 824820 steps
c [elim-12-1] rescheduled 4 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 7339 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 32 = 0% variables out of 15895 scheduled
c [elim-12] 32 < 1/100 * 15895 = 158 considered unsuccessful
c [bca-11] limit of 10000000 steps and 141734 added (scaled 2)
c [bca-11] 13458 out of 31728 literals actually usable 42%
c [bca-11] added 17 blocked clauses in 122073 steps
c [sweep-10] limit 10824367 penalty 0 = 0 + 0
c [sweep-10-1] 579 pos 60.6% + 376 neg 39.4% = 955 sched 6.0% ret 14908
c [sweep-10-1] 4145966 steps 498 queries 63.87 avg class size
c [sweep-10-1] 4954 decisions 496 SAT calls 20.56 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-56] removed 23 variables
c [sweep-10-1] removed 23 vars (0 failed, 6 eqs, 4 impls)
c [sweep-10-2] 7228 pos 45.6% + 8612 neg 54.4% = 15840 sched 100.0% ret 0
c [sweep-10-2] 6684741 steps 217 queries 622.58 avg class size
c [sweep-10-2] 6146 decisions 219 SAT calls 71.06 avg env size
c [sweep-10-2] 8522 variables remain 54% (7318 retained 46%)
c [decomp-57] removed 1 variables
c [sweep-10-2] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-10] removed 24 vars in TOTAL (2 rounds, 713 queries)
c [phase-count-15] 66424 negative 94.6% of 70244 except 3820 5.4%
c [phase-count-15] 62782 positive 89.4% of 70244 except 7462 10.6%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 2670 enqueued variables after 397594 conflicts
c [score-dist-15] active 13169 (83%), one 0 (0%), zero 2670 (17%)
c [score-dist-15] max exp 520, different 12 (2%)
c [score-dist-15] median active exp 520, avg 519.3
c [simplification-15] removed 95 variables 0.6% (15839 remain 17%)
c [simplification-15] removed 540 irredundant clauses 0.8% (70244 remain 25%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 56245 = 112491 / 2
c [simplification-15] new conflict interval 168736
c [simplification-15] penalized conflict interval 168736 = 1 * 168736
c [simplification-15] hard conflict limit 650698 (soft 566330 + delta 84368)
c [simplification-15] new conflict limit 566330 (hard 650698)
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 -  178.4   15839    70244    420746   75837  27374 22288   24   124   31  19%    404   24   26   21  126%
c -  191.0   15839    70244    463698   80972  27433 22289   22   120   32  18%    702    5   27   21  128%
c -  204.1   15839    70244    503692   81681  27502 22294   19   193   32  10%    849   69   20   22   90%
c i  209.3   15838    70244    522487   99899  27527 22297   23   125   41  19%    893   -3   28   22  126%
c -  216.4   15838    70244    545744   84088  27572 22302   25    88   32  28%   -971  -34   27   23  115%
c i  220.4   15837    70244    559526   97432  27598 22306   25   123   39  21%   -593    7   27   23  116%
c -  229.8   15837    70244    587515   85462  27626 22308   27   103   32  27%   -414   -6   32   24  134%
c 
c [simplification-16] limit 566330 conflicts (hard 650698) hit after 609785 conflicts
c [quatres-12] found 53044 quaternary clauses 58% in total
c [quatres-12-1] removed 3 duplicate quaternary clauses
c [quatres-12-1] added 7 double-self-subsuming ternary resolvents
c [quatres-12-2] added 489 single-self-subsuming ternary resolvents
c [quatres-12-2] added 627 quaternary resolvents
c [ternres-12] limit 55172017 with penalty 0 = 0 + 0
c [ternres-12] all 15837 free variables schedulable
c [ternres-12] 1132 ternary resolvents (8 bin, 1124 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-58] removed 9 variables
c [unhide-16] limit 11034403 with penalty 0 = 0 + 0
c [unhide-16-41] 0 units, 7 failed, 767 tauts, 0 hbrs, 70204 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 56 transitive binary clauses
c [transred-12] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 15825 variables 100%
c [block-6] limit of 137930042 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 53 blocked clauses
c [block-6] 53 < 1/100 * 70073 = 700 considered unsuccessful
c [cce-5] limit of 68965021 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 6 clauses out of 7 (86%) of length 35
c [cce-5-1] eliminated 4 clauses out of 6 (67%) of length 32
c [cce-5-1] eliminated 4 clauses out of 6 (67%) of length 31
c [cce-5-1] eliminated 6 clauses out of 15 (40%) of length 30
c [cce-5-1] eliminated 2 clauses out of 7 (29%) of length 29
c [cce-5-1] eliminated 6 clauses out of 17 (35%) of length 28
c [cce-5-1] eliminated 2 clauses out of 10 (20%) of length 27
c [cce-5-1] eliminated 4 clauses out of 26 (15%) of length 26
c [cce-5-1] eliminated 2 clauses out of 36 (6%) of length 25
c [cce-5-1] eliminated 2 clauses out of 30 (7%) of length 24
c [cce-5-1] eliminated 6 clauses out of 59 (10%) of length 22
c [cce-5-1] eliminated 3 clauses out of 75 (4%) of length 18
c [cce-5-1] eliminated 3 clauses out of 88 (3%) of length 17
c [cce-5-1] eliminated 7 clauses out of 67 (10%) of length 16
c [cce-5-1] eliminated 4 clauses out of 117 (3%) of length 15
c [cce-5-1] eliminated 5 clauses out of 95 (5%) of length 14
c [cce-5-1] eliminated 13 clauses out of 115 (11%) of length 13
c [cce-5-1] eliminated 5 clauses out of 118 (4%) of length 12
c [cce-5-1] eliminated 10 clauses out of 2695 (0%) of length 11
c [cce-5-1] eliminated 56 clauses out of 343 (16%) of length 10
c [cce-5-1] eliminated 118 clauses out of 2060 (6%) of length 9
c [cce-5-1] eliminated 63 clauses out of 773 (8%) of length 8
c [cce-5-1] eliminated 50 clauses out of 831 (6%) of length 7
c [cce-5-1] eliminated 92 clauses out of 835 (11%) of length 6
c [cce-5-1] eliminated 317 clauses out of 1527 (21%) of length 5
c [cce-5-1] eliminated 437 clauses out of 16901 (3%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 1227 large clauses in 65173508 steps
c [cce-5-1] allowing another 32586754 steps for small clauses
c [cce-5-1] scheduling 26657 clauses = 16942 binary + 9715 ternary
c [cce-5-1] tried to eliminate 17687 small clauses 66%
c [cce-5-1] eliminated 574 binary clauses 3%
c [cce-5-1] eliminated 124 ternary clauses 1%
c [cce-5-1] eliminated 698 small clauses 3%
c [cce-5-1] eliminated 698 small clauses in 68965028 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1925 covered clauses in round 1
c [cce-5] eliminated 1925 covered clauses in TOTAL during 1 rounds
c [bca-12] limit of 10000000 steps and 137158 added (scaled 2)
c [bca-12] 13067 out of 31652 literals actually usable 41%
c [bca-12] added 9 blocked clauses in 135777 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 165516050 penalty 0 = 0 + 0
c [sweep-11-1] 4649 pos 54.6% + 3863 neg 45.4% = 8512 sched 53.8% ret 7313
c [sweep-11-1] 35207133 steps 1911 queries 94.72 avg class size
c [sweep-11-1] 26031 decisions 1921 SAT calls 33.34 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-59] removed 32 variables
c [sweep-11-1] removed 32 vars (0 failed, 14 eqs, 23 impls)
c [sweep-11-2] 7063 pos 44.7% + 8730 neg 55.3% = 15793 sched 100.0% ret 0
c [sweep-11-2] 41641960 steps 2045 queries 63.72 avg class size
c [sweep-11-2] 30286 decisions 2052 SAT calls 38.80 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-60] removed 12 variables
c [sweep-11-2] removed 12 vars (0 failed, 17 eqs, 23 impls)
c [sweep-11-3] 7052 pos 44.7% + 8729 neg 55.3% = 15781 sched 100.0% ret 0
c [sweep-11-3] 41378611 steps 1991 queries 48.02 avg class size
c [sweep-11-3] 30492 decisions 1997 SAT calls 40.83 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-61] removed 15 variables
c [sweep-11-3] removed 15 vars (0 failed, 14 eqs, 21 impls)
c [sweep-11] removed 59 vars in TOTAL (3 rounds, 5944 queries)
c [sort-queue-16] sorted 1267 enqueued variables after 609785 conflicts
c [score-dist-16] active 14499 (92%), one 0 (0%), zero 1267 (8%)
c [score-dist-16] max exp 521, different 13 (2%)
c [score-dist-16] median active exp 521, avg 520.3
c [simplification-16] removed 71 variables 0.4% (15766 remain 17%)
c [simplification-16] removed 2363 irredundant clauses 3.4% (67881 remain 24%)
c [simplification-16] maximum reduction of 3% = max (0%, 3%)
c [simplification-16] geometric conflict interval increment 42184 = 168736 / 4
c [simplification-16] new conflict interval 210920
c [simplification-16] penalized conflict interval 210920 = 1 * 210920
c [simplification-16] hard conflict limit 926165 (soft 820705 + delta 105460)
c [simplification-16] new conflict limit 820705 (hard 926165)
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 -  252.6   15766    67881    626369   87699  30865 23659   26   128   34  20%    229    8   21   24   87%
c -  265.6   15766    67881    670886   90942  30936 23661   24   119   35  20%    621    6   26   24  109%
c -  280.0   15766    67881    713747   92097  30989 23663   25   133   35  19%    814   15   23   25   90%
c -  293.5   15766    67881    757758   95719  31064 23666   26   123   35  21%    917  -15   25   24  104%
c -  308.4   15766    67881    800693   96092  31110 23669   28   134   35  21%    968    0   24   25   93%
c 
c [simplification-17] limit 820705 conflicts (hard 926165) hit after 820758 conflicts
c [quatres-13] found 52520 quaternary clauses 54% in total
c [quatres-13-1] removed 4 duplicate quaternary clauses
c [quatres-13-1] added 4 double-self-subsuming ternary resolvents
c [quatres-13-2] added 839 single-self-subsuming ternary resolvents
c [quatres-13-2] added 493 quaternary resolvents
c [ternres-13] limit 74986088 with penalty 0 = 0 + 0
c [ternres-13] all 15766 free variables schedulable
c [ternres-13] 2628 ternary resolvents (8 bin, 2620 trn)
c [ternres-13] fully completed ternary resolution
c [gauss-6] limit 1874652 penalty 3 = 3 + 0
c [gauss-6] extracted 11545 xors of average arity 3.0
c [gauss-6] connected 34631 occurrences of 1910 variables (average 18.1)
c [gauss-6] limit 1874652 penalty 3 = 3 + 0
c [gauss-6] connected 9809 occurrences of 1910 variables (average 5.1)
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-6] limit 3749304 penalty 1 = 1 + 0 boost 1
c [treelook-6] scheduled 22956 literals 73%
c [treelook-6] scheduling used 652368 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3749304 penalty 1 = 1 + 0 boost 1
c [treelook-6] used 3772287 steps
c [treelook-6] 22736 literals remain 72%
c [treelook-6] 8866 variables remain to probed next time 56%
c [treelook-6] removed 0 variables, found 3209 hbrs
c [unhide-17] limit 14997217 with penalty 0 = 0 + 0
c [unhide-17-50] 2 units, 18 failed, 1903 tauts, 0 hbrs, 92201 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 28 transitive binary clauses
c [cce-6] limit of 187465220 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 1 clauses out of 1944 (0%) of length 9
c [cce-6-1] eliminated 6 clauses out of 1117 (1%) of length 5
c [cce-6-1] eliminated 34 clauses out of 15658 (0%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 41 large clauses in 46429625 steps
c [cce-6-1] allowing another 23214812 steps for small clauses
c [cce-6-1] scheduling 33020 clauses = 16543 binary + 16477 ternary
c [cce-6-1] tried to eliminate 33020 small clauses 100%
c [cce-6-1] eliminated 109 binary clauses 1%
c [cce-6-1] eliminated 173 ternary clauses 1%
c [cce-6-1] eliminated 282 small clauses 1%
c [cce-6-1] eliminated 282 small clauses in 80217988 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 323 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 22979013 steps for small clauses
c [cce-6-2] scheduling 32738 clauses = 16434 binary + 16304 ternary
c [cce-6-2] tried to eliminate 32738 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 323 covered clauses in TOTAL during 2 rounds
c [cce-6] 323 < 1/100 * 67761 = 677 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 15753 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 566 variables 4% in round 1 in 25070968 steps
c [elim-13-1] backward subsumption/strengthening limit 25070900
c [elim-13-1-1] backward checking 1373 touched variables 9%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 3 and strengthened 0 clauses in 2825752 steps
c [elim-13-1] rescheduled 10 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 73987 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 566 = 4% variables out of 15753 scheduled
c [bca-13] limit of 10000000 steps and 133977 added (scaled 2)
c [bca-13] 12343 out of 30376 literals actually usable 41%
c [bca-13] added 66 blocked clauses in 135157 steps
c [sweep-12] limit 22495826 penalty 0 = 0 + 0
c [sweep-12-1] 7120 pos 46.9% + 8067 neg 53.1% = 15187 sched 100.0% ret 0
c [sweep-12-1] 22593226 steps 798 queries 158.00 avg class size
c [sweep-12-1] 16834 decisions 801 SAT calls 50.73 avg env size
c [sweep-12-1] 3169 variables remain 21% (12017 retained 79%)
c [decomp-64] removed 4 variables
c [sweep-12-1] removed 4 vars (0 failed, 3 eqs, 10 impls)
c [sweep-12] 4 < 1/1000 * 15187 = 15 considered unsuccessful
c [sweep-12] removed 4 vars in TOTAL (1 rounds, 797 queries)
c [sort-queue-17] sorted 1024 enqueued variables after 820758 conflicts
c [score-dist-17] active 14159 (93%), one 0 (0%), zero 1024 (7%)
c [score-dist-17] max exp 521, different 13 (2%)
c [score-dist-17] median active exp 521, avg 520.4
c [simplification-17] removed 583 variables 3.7% (15183 remain 17%)
c [simplification-17] removed 1394 irredundant clauses 2.1% (66487 remain 23%)
c [simplification-17] maximum reduction of 4% = max (4%, 2%)
c [simplification-17] geometric conflict interval increment 42184 = 210920 / 5
c [simplification-17] new conflict interval 253104
c [simplification-17] penalized conflict interval 253104 = 1 * 253104
c [simplification-17] hard conflict limit 1200414 (soft 1073862 + delta 126552)
c [simplification-17] new conflict limit 1073862 (hard 1200414)
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 -  333.1   15183    66487    850502   94770  32811 24272   25   141   35  18%    998    7   21   26   79%
c -  348.9   15183    66487    896266   96569  32862 24276   29   136   35  22%   1011    6   31   27  115%
c -  361.6   15183    66487    941979  102720  32893 24278   19   130   36  14%   1018   -4   20   24   80%
c -  376.1   15183    66487    984058  100428  32963 24280   23    76   36  30%   1021  -51   13   25   52%
c -  392.2   15183    66487   1030362  102143  33013 24285   24   144   36  17%   1022   18   33   25  130%
c 
c [simplification-18] limit 1073862 conflicts (hard 1200414) hit after 1073862 conflicts
c [quatres-14] found 49462 quaternary clauses 49% in total
c [quatres-14-1] removed 6 duplicate quaternary clauses
c [quatres-14-2] added 754 single-self-subsuming ternary resolvents
c [quatres-14-2] added 618 quaternary resolvents
c [ternres-14] limit 100775652 with penalty 0 = 0 + 0
c [ternres-14] all 15183 free variables schedulable
c [ternres-14] 1214 ternary resolvents (0 bin, 1214 trn)
c [ternres-14] fully completed ternary resolution
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 8469 sched 56%, 15 failed, 3 lifted, 417 hbrs
c [decomp-66] removed 20 variables
c [basicprobe-6-1] 8486 sched 56%, 5 failed, 0 lifted, 168 hbrs
c [decomp-67] removed 5 variables
c [basicprobe-6-2] 8483 sched 56%, 6 failed, 1 lifted, 91 hbrs
c [decomp-68] removed 13 variables
c [basicprobe-6-3] 8481 sched 56%, 7 failed, 2 lifted, 90 hbrs
c [decomp-69] removed 7 variables
c [basicprobe-6-4] 8476 sched 56%, 8 failed, 1 lifted, 36 hbrs
c [decomp-70] removed 9 variables
c [basicprobe-6-5] 8473 sched 56%, 4 failed, 0 lifted, 55 hbrs
c [decomp-71] removed 13 variables
c [basicprobe-6-6] 8474 sched 56%, 2 failed, 0 lifted, 27 hbrs
c [decomp-72] removed 2 variables
c [basicprobe-6-7] 8468 sched 56%, 1 failed, 0 lifted, 41 hbrs
c [decomp-73] removed 1 variables
c [basicprobe-6-8] 8472 sched 56%, 2 failed, 0 lifted, 5 hbrs
c [basicprobe-6-8] round limit 8 hit
c [basicprobe-6-8] 57 units = 50 failed (88%) + 7 lifted (12%)
c [basicprobe-6-8] removed 72 variables, found 930 hbrs
c [bate-4] eliminated 32 asymmetric tautologies during probing
c [unhide-18] limit 20000000 with penalty 0 = 0 + 0
c [unhide-18-60] 0 units, 1 failed, 688 tauts, 0 hbrs, 197194 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 16 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 15110 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 64 variables 0% in round 1 in 24614969 steps
c [elim-14-1] backward subsumption/strengthening limit 24614900
c [elim-14-1-1] backward checking 381 touched variables 3%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 771343 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 64 = 0% variables out of 15110 scheduled
c [elim-14] 64 < 1/100 * 15110 = 151 considered unsuccessful
c [bca-14] limit of 10000000 steps and 132780 added (scaled 2)
c [bca-14] 11413 out of 30094 literals actually usable 38%
c [bca-14] added 2 blocked clauses in 169295 steps
c [sort-queue-18] sorted 955 enqueued variables after 1073862 conflicts
c [score-dist-18] active 14091 (94%), one 0 (0%), zero 955 (6%)
c [score-dist-18] max exp 522, different 13 (2%)
c [score-dist-18] median active exp 522, avg 521.0
c [simplification-18] removed 137 variables 0.9% (15046 remain 16%)
c [simplification-18] removed 605 irredundant clauses 0.9% (65882 remain 23%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 126552 = 253104 / 2
c [simplification-18] new conflict interval 379656
c [simplification-18] penalized conflict interval 379656 = 1 * 379656
c [simplification-18] hard conflict limit 1643346 (soft 1453518 + delta 189828)
c [simplification-18] new conflict limit 1453518 (hard 1643346)
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 -  421.9   15046    65882   1078207  101458  34396 22775   26   123   39  21%   1023   -3   12   25   48%
c -  437.7   15046    65882   1127761  106701  34453 22776   21   100   40  21%   1024  -25   21   23   95%
c -  458.3   15046    65882   1174165  102447  34502 22777   26   126   39  21%   1024    4   19   25   77%
c -  479.1   15046    65882   1227942  106240  34549 22781   29   109   63  27%   1024  -19   26   26   97%
c -  499.0   15046    65882   1280487  109086  34598 22784   29   124   63  23%   1024   -5   24   27   89%
c -  517.7   15046    65882   1332239  112108  34639 22790   29   153   64  19%   1024   24   23   28   81%
c -  533.5   15046    65882   1382885  117509  34674 22790   20   161   64  13%   1024   19   25   25   97%
c -  552.7   15046    65882   1430527  114274  34724 22794   26   132   64  20%   1024   -7   26   27   95%
c 
c [simplification-19] limit 1453518 conflicts (hard 1643346) hit after 1462176 conflicts
c [quatres-15] found 48839 quaternary clauses 44% in total
c [quatres-15-1] removed 5 duplicate quaternary clauses
c [quatres-15-2] added 512 single-self-subsuming ternary resolvents
c [quatres-15-2] added 569 quaternary resolvents
c [ternres-15] limit 143117282 with penalty 0 = 0 + 0
c [ternres-15] all 15046 free variables schedulable
c [ternres-15] 1110 ternary resolvents (2 bin, 1108 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-74] removed 1 variables
c [simpleprobe-7] all 15045 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-75] removed 8 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 8 variables, found 4974 hbrs, 2 units
c [unhide-19] limit 20000000 with penalty 0 = 0 + 0
c [unhide-19-70] 0 units, 4 failed, 4153 tauts, 0 hbrs, 170210 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 44 transitive binary clauses
c [cce-7] limit of 178896603 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 33
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 31
c [cce-7-1] eliminated 2 clauses out of 9 (22%) of length 30
c [cce-7-1] eliminated 1 clauses out of 6 (17%) of length 29
c [cce-7-1] eliminated 1 clauses out of 8 (12%) of length 28
c [cce-7-1] eliminated 3 clauses out of 15 (20%) of length 27
c [cce-7-1] eliminated 8 clauses out of 27 (30%) of length 26
c [cce-7-1] eliminated 4 clauses out of 38 (11%) of length 25
c [cce-7-1] eliminated 1 clauses out of 31 (3%) of length 24
c [cce-7-1] eliminated 6 clauses out of 47 (13%) of length 23
c [cce-7-1] eliminated 12 clauses out of 69 (17%) of length 22
c [cce-7-1] eliminated 2 clauses out of 53 (4%) of length 21
c [cce-7-1] eliminated 6 clauses out of 55 (11%) of length 20
c [cce-7-1] eliminated 6 clauses out of 67 (9%) of length 19
c [cce-7-1] eliminated 3 clauses out of 65 (5%) of length 18
c [cce-7-1] eliminated 9 clauses out of 93 (10%) of length 17
c [cce-7-1] eliminated 4 clauses out of 76 (5%) of length 16
c [cce-7-1] eliminated 10 clauses out of 111 (9%) of length 15
c [cce-7-1] eliminated 4 clauses out of 89 (4%) of length 14
c [cce-7-1] eliminated 7 clauses out of 115 (6%) of length 13
c [cce-7-1] eliminated 5 clauses out of 105 (5%) of length 12
c [cce-7-1] eliminated 7 clauses out of 2720 (0%) of length 11
c [cce-7-1] eliminated 17 clauses out of 306 (6%) of length 10
c [cce-7-1] eliminated 28 clauses out of 1946 (1%) of length 9
c [cce-7-1] eliminated 19 clauses out of 679 (3%) of length 8
c [cce-7-1] eliminated 27 clauses out of 872 (3%) of length 7
c [cce-7-1] eliminated 28 clauses out of 804 (3%) of length 6
c [cce-7-1] eliminated 81 clauses out of 1193 (7%) of length 5
c [cce-7-1] eliminated 198 clauses out of 14347 (1%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 501 large clauses in 49077053 steps
c [cce-7-1] allowing another 24538526 steps for small clauses
c [cce-7-1] scheduling 32034 clauses = 16080 binary + 15954 ternary
c [cce-7-1] tried to eliminate 32034 small clauses 100%
c [cce-7-1] eliminated 261 binary clauses 2%
c [cce-7-1] eliminated 171 ternary clauses 1%
c [cce-7-1] eliminated 432 small clauses 1%
c [cce-7-1] eliminated 432 small clauses in 82710687 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 933 covered clauses in round 1
c [cce-7-2] eliminated 1 clauses out of 3 (33%) of length 32
c [cce-7-2] eliminated 2 clauses out of 12 (17%) of length 27
c [cce-7-2] eliminated 2 clauses out of 41 (5%) of length 23
c [cce-7-2] eliminated 2 clauses out of 51 (4%) of length 21
c [cce-7-2] eliminated 2 clauses out of 49 (4%) of length 20
c [cce-7-2] eliminated 4 clauses out of 61 (7%) of length 19
c [cce-7-2] eliminated 1 clauses out of 62 (2%) of length 18
c [cce-7-2] eliminated 5 clauses out of 84 (6%) of length 17
c [cce-7-2] eliminated 1 clauses out of 72 (1%) of length 16
c [cce-7-2] eliminated 3 clauses out of 108 (3%) of length 13
c [cce-7-2] eliminated 2 clauses out of 100 (2%) of length 12
c [cce-7-2] eliminated 2 clauses out of 2713 (0%) of length 11
c [cce-7-2] eliminated 5 clauses out of 289 (2%) of length 10
c [cce-7-2] eliminated 2 clauses out of 1918 (0%) of length 9
c [cce-7-2] eliminated 6 clauses out of 660 (1%) of length 8
c [cce-7-2] eliminated 3 clauses out of 845 (0%) of length 7
c [cce-7-2] eliminated 10 clauses out of 776 (1%) of length 6
c [cce-7-2] eliminated 18 clauses out of 1112 (2%) of length 5
c [cce-7-2] eliminated 55 clauses out of 14149 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 126 large clauses in 45509497 steps
c [cce-7-2] allowing another 22754748 steps for small clauses
c [cce-7-2] scheduling 31602 clauses = 15819 binary + 15783 ternary
c [cce-7-2] tried to eliminate 31602 small clauses 100%
c [cce-7-2] eliminated 21 binary clauses 0%
c [cce-7-2] eliminated 24 ternary clauses 0%
c [cce-7-2] eliminated 45 small clauses 0%
c [cce-7-2] eliminated 45 small clauses in 77648220 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 171 covered clauses in round 2
c [cce-7-3] eliminated 1 clauses out of 61 (2%) of length 18
c [cce-7-3] eliminated 7 clauses out of 79 (9%) of length 17
c [cce-7-3] eliminated 1 clauses out of 105 (1%) of length 13
c [cce-7-3] eliminated 1 clauses out of 654 (0%) of length 8
c [cce-7-3] eliminated 6 clauses out of 842 (1%) of length 7
c [cce-7-3] incomplete large round (ACCE)
c [cce-7-3] eliminated 16 large clauses in 18537726 steps
c [cce-7-3] allowing another 9268863 steps for small clauses
c [cce-7-3] scheduling 31557 clauses = 15798 binary + 15759 ternary
c [cce-7-3] tried to eliminate 5260 small clauses 17%
c [cce-7-3] incomplete small round (ACCE)
c [cce-7-3] eliminated 16 covered clauses in round 3
c [cce-7] eliminated 1120 covered clauses in TOTAL during 3 rounds
c [bca-15] limit of 10000000 steps and 130425 added (scaled 2)
c [bca-15] 11582 out of 30072 literals actually usable 39%
c [bca-15] added 2 blocked clauses in 171617 steps
c [sweep-13] limit 21467592 penalty 1 = 1 + 0
c [sweep-13-1] 2077 pos 66.3% + 1058 neg 33.7% = 3135 sched 20.9% ret 11900
c [sweep-13-1] 21471106 steps 683 queries 75.43 avg class size
c [sweep-13-1] 12613 decisions 690 SAT calls 47.61 avg env size
c [sweep-13-1] 939 variables remain 6% (14088 retained 94%)
c [decomp-76] removed 18 variables
c [sweep-13-1] removed 18 vars (0 failed, 6 eqs, 9 impls)
c [sweep-13] removed 18 vars in TOTAL (1 rounds, 682 queries)
c [sort-queue-19] sorted 855 enqueued variables after 1462176 conflicts
c [score-dist-19] active 14162 (94%), one 0 (0%), zero 855 (6%)
c [score-dist-19] max exp 522, different 13 (2%)
c [score-dist-19] median active exp 522, avg 521.2
c [simplification-19] removed 29 variables 0.2% (15017 remain 16%)
c [simplification-19] removed 1217 irredundant clauses 1.8% (64665 remain 23%)
c [simplification-19] maximum reduction of 2% = max (0%, 2%)
c [simplification-19] geometric conflict interval increment 126552 = 379656 / 3
c [simplification-19] new conflict interval 506208
c [simplification-19] penalized conflict interval 506208 = 1 * 506208
c [simplification-19] hard conflict limit 2221488 (soft 1968384 + delta 253104)
c [simplification-19] new conflict limit 1968384 (hard 2221488)
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 -  582.1   15017    64665   1482919  117900  36583 24120   28   123   41  23%   1024   -6   32   28  117%
c -  601.2   15017    64665   1534789  119347  36627 24123   27   129   41  21%   1024    4   18   27   67%
c -  622.2   15017    64665   1588152  119309  36672 24127   28   144   41  20%   1024   18   24   28   88%
c -  643.4   15017    64665   1644207  122603  36708 24134   30   122   66  25%   1024    3   28   27  100%
c -  663.7   15017    64665   1699938  129941  36725 24135   21    54   69  40%   1024  -27   28   24  118%
c -  685.6   15017    64665   1748409  124080  36767 24138   29   117   66  25%   1024   20   27   25  108%
c -  710.2   15017    64665   1805727  123666  36834 24142   27   126   65  21%   1024   21   31   26  120%
c -  734.9   15017    64665   1865356  127328  36880 24143   25   150   66  17%   1024   30   28   27  103%
c -  756.1   15017    64665   1923411  133055  36903 24144   30   129   66  23%   1024   -1   34   26  133%
c 
c [simplification-20] limit 1968384 conflicts (hard 2221488) hit after 1968384 conflicts
c [quatres-16] found 49217 quaternary clauses 41% in total
c [quatres-16-1] removed 14 duplicate quaternary clauses
c [quatres-16-2] added 710 single-self-subsuming ternary resolvents
c [quatres-16-2] added 503 quaternary resolvents
c [ternres-16] limit 199574941 with penalty 0 = 0 + 0
c [ternres-16] all 15017 free variables schedulable
c [ternres-16] 1431 ternary resolvents (1 bin, 1430 trn)
c [ternres-16] fully completed ternary resolution
c [unhide-20] limit 20000000 with penalty 0 = 0 + 0
c [unhide-20-78] 2 units, 13 failed, 720 tauts, 0 hbrs, 232796 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 27 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 15006 variables 100%
c [block-7] limit of 100000000 steps penalty 3 = 3 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 175 blocked clauses
c [block-7] 175 < 1/100 * 64611 = 646 considered unsuccessful
c [cce-8] boosting limit by 10
c [cce-8] limit of 4989373540 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 1 clauses out of 37 (3%) of length 23
c [cce-8-1] eliminated 1 clauses out of 1920 (0%) of length 9
c [cce-8-1] eliminated 1 clauses out of 757 (0%) of length 6
c [cce-8-1] eliminated 4 clauses out of 1045 (0%) of length 5
c [cce-8-1] eliminated 22 clauses out of 13761 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 29 large clauses in 37990739 steps
c [cce-8-1] allowing another 18995369 steps for small clauses
c [cce-8-1] scheduling 31672 clauses = 15843 binary + 15829 ternary
c [cce-8-1] tried to eliminate 31672 small clauses 100%
c [cce-8-1] eliminated 29 binary clauses 0%
c [cce-8-1] eliminated 47 ternary clauses 0%
c [cce-8-1] eliminated 76 small clauses 0%
c [cce-8-1] eliminated 76 small clauses in 68873681 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 105 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 18928172 steps for small clauses
c [cce-8-2] scheduling 31596 clauses = 15814 binary + 15782 ternary
c [cce-8-2] tried to eliminate 31596 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 105 covered clauses in TOTAL during 2 rounds
c [cce-8] 105 < 1/100 * 64432 = 644 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 14930 variables 100%
c [elim-15] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 155 variables 1% in round 1 in 23665551 steps
c [elim-15-1] backward subsumption/strengthening limit 23665500
c [elim-15-1-1] backward checking 713 touched variables 5%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 1 and strengthened 1 clauses in 1211605 steps
c [elim-15-1] rescheduled 9 variables 0% by backward subsumption
c [elim-15-2] no variable eliminated in round 2 in 97459 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 155 = 1% variables out of 14930 scheduled
c [bca-16] limit of 10000000 steps and 129276 added (scaled 2)
c [bca-16] 10685 out of 29552 literals actually usable 36%
c [bca-16] added 4 blocked clauses in 198575 steps
c [sweep-14] limit 59872482 penalty 0 = 0 + 0
c [sweep-14-1] 628 pos 69.2% + 280 neg 30.8% = 908 sched 6.1% ret 13867
c [sweep-14-1] 11601129 steps 498 queries 35.96 avg class size
c [sweep-14-1] 7812 decisions 499 SAT calls 36.36 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-78] removed 8 variables
c [sweep-14-1] removed 8 vars (0 failed, 3 eqs, 4 impls)
c [sweep-14-2] 6782 pos 45.9% + 7985 neg 54.1% = 14767 sched 100.0% ret 0
c [sweep-14-2] 48287650 steps 867 queries 97.30 avg class size
c [sweep-14-2] 26156 decisions 871 SAT calls 88.20 avg env size
c [sweep-14-2] 1837 variables remain 12% (12929 retained 88%)
c [decomp-79] removed 6 variables
c [sweep-14-2] removed 6 vars (0 failed, 5 eqs, 6 impls)
c [sweep-14] removed 14 vars in TOTAL (2 rounds, 1363 queries)
c [sort-queue-20] sorted 627 enqueued variables after 1968384 conflicts
c [score-dist-20] active 14134 (96%), one 0 (0%), zero 627 (4%)
c [score-dist-20] max exp 522, different 13 (2%)
c [score-dist-20] median active exp 522, avg 521.4
c [simplification-20] removed 256 variables 1.7% (14761 remain 16%)
c [simplification-20] removed 617 irredundant clauses 1.0% (64048 remain 22%)
c [simplification-20] maximum reduction of 2% = max (2%, 1%)
c [simplification-20] geometric conflict interval increment 168736 = 506208 / 3
c [simplification-20] new conflict interval 674944
c [simplification-20] penalized conflict interval 674944 = 1 * 674944
c [simplification-20] hard conflict limit 2980800 (soft 2643328 + delta 337472)
c [simplification-20] new conflict limit 2643328 (hard 2980800)
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 -  789.6   14761    64048   1977113  130532  38026 22995   26    91   45  29%   1024  -34   28   27  102%
c -  812.1   14761    64048   2035385  133186  38068 22997   24   146   45  16%   1024   19   22   28   78%
c -  835.1   14761    64048   2093274  135544  38101 23001   31   128   45  24%   1024  -12   32   28  116%
c -  858.6   14761    64048   2150875  136221  38130 23003   20   151   72  13%   1024   12   14   28   51%
c -  882.0   14761    64048   2210289  138418  38169 23006   30   128   72  24%   1024  -11   34   29  116%
c -  905.6   14761    64048   2270462  140008  38211 23007   27   146   72  18%   1024   17   22   29   77%
c -  929.3   14761    64048   2331177  141754  38250 23009   33   131   72  25%   1024   -3   33   29  115%
c -  952.7   14761    64048   2392945  144895  38290 23017   31   140   72  22%   1024   13   41   30  136%
c -  973.0   14761    64048   2453586  148169  38317 23019   15   137   73  11%   1024    8   14   26   54%
c -  999.1   14761    64048   2512982  145590  38348 23023   27   122   72  22%   1024   -4   20   28   73%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 1531 basic ate = 1122 trn 73% + 409 lrg 27% in 4 updates
c bcas: 16 count, 1040 added (1351 skipped), 2170221 steps
c bkwd: tried 206792 clauses, 413039 lits, 2.00 lits/clause
c bkwd: checked 15590455 occs, 75.39 occs/clause, 37.75 occs/lit
c bkwd: subsumed 18 binary, 17 ternary, 146 large
c bkwd: strengthened 2 binary, 4 ternary (100% self), 615 large (0% self)
c blkd: 7 bces, 15913 removed, 3311977 resolutions, 9666310 steps
c blkd: 10578 blocking literals 6%, 232 pure
c bump: 2523843 bumped seen, 255821084 lits 101.4 on average
c card: 5 count, 1 units, 0 am1, 44064424 steps
c card: 36 rescheduled, 82 eliminated, 4138 resolved, 6411 subsumed
c card: 780 at-most-one constraints found, average size 3.48
c card: 780 at-most-one constraints used 100%, average size 3.48
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 8 cces, 8821 eliminated, 7467 ate 85%, 1354 abce 15%
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: 1043606 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 195 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 79 decompositions, 4932 equivalent 5%
c deco: 4696 decision-only clauses 0%, 48% reduction
c decs: 12077293 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 67828 eliminated 71%, 160 pure 0%
c elms: 27 rounds, 1.8 rounds/bve
c elms: 64985 small 96%, 2451 large 4%
c elms: 178565 tried small, 64985 succeeded 36%, 113580 failed 64%
c elms: 7193 subsumed, 13988 strengthened, 417 blocked
c elms: 6296128 copies, 8448596 resolutions, 6713838 ipos
c elms: 5963820 subchks, 5882740 strchks
c gaus: 6 extractions, 57080 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 1 binary and 0 ternary equations
c gaus: 1 gc, 18402650 steps, 9201325 extr 50%, 9164749 elim 50%
c glue: 24.7 orig avg, 24.7 real avg, 4.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 71186 = 19485 simple 27% + 47768 trn 67% + 3933 lrg 6%, 2480 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2523843 clauses, 60.4 length
c lrnd: 152470463 lits = 192209760 orig - 39739297 removed 21%
c lrnd: 760778 uips 30%, 1464580 flips 58%
c mins: 2488675 mins 99%, 1781 bin 0%, 28651 size 1%
c mins: 172919071 poisoned searches, 40627429 hits, 23% hit rate
c mins: 320243463 used twice searches, 34017755 hits, 11% hit rate
c move: moved 15034, 2266 bin 15%, 12768 trn 85%
c otfs: 8497 driving 29%, 21047 restarting 71%
c otfs: str 29544, 29249 red 99%, 295 irr 1%
c otfs: str 29544, 0 bin 0%, 228 trn 1%, 29316 lrg 99%
c otfs: sub 89, 89 red 100%, 0 irr 0%
c otfs: sub 89, 0 bin 0%, 8 trn 9%, 81 lrg 91%
c phas: 15 computed, 25989 set, 5236 pos (20%), 20753 neg (80%)
c prbs: 6 basic, 530367 probed, 1209 failed, 250 lifted
c prbs: 7 simple, 264636 probed, 136 failed, 1522 eqs
c prbs: 6 treelook, 391 probed, 4 failed, 0 lifted
c prom: 488276 locked 13% out of 3623372 tried
c prps: 1631465837 props, 133 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 16 count, 96112 quat, 12520 self1, 22 self2, 84 dup
c queu: 20 sorted, 12077293 next (2260 steps 0.00)
c queu: 256077892 enq (3705603792 steps 14.47), 255821084 deq 100%
c redc: 16575 clauses 8%, 218733 tried 9%, 4 sat 0%
c redc: 28437 lits 1%, 2541110 tried 1%, 5 sat 0%
c redc: 1273 times jump level reduced, 11.6 levels on average
c reds: 49 count, 51326.7 conflicts per reduce
c reds: 0 memlim 0%, 49 arith 100%
c reds: 1812807 collected 80%, 466929 retired 20%
c rmbd: 2414 removed, 2100 red 87%
c rsts: 52876 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 20 count, 19 confs 95%, 0 vars 0%
c simp: 0 its 0%, 1 bin 5%, 0 trns 0%
c subl: 2523843 count (2708731 tried 1.1), 62801 sub out of 2513180 (2.5%)
c swps: 14 count, 18 rounds, 12368 queries (687.1/round)
c swps: 12357 sat calls, 176 unsat (1.4% success rate)
c swps: 202218 decisions 16.4, 17334 conflicts 1.4
c swps; 221.9 avg class size, 41.4 avg environment size
c swps: 0 failed, 235 impls, 174 equivs
c swp0: 4115 type 0 queries, 179 unsat (4.3%), 4090 sat (99.4%)
c swp1: 8253 type 1 queries, 748 unsat (9.1%), 8104 sat (98.2%)
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: 29202743 calls to obtain time
c tops: 7477 fixed 8%, 19 its, 132368.74 confs/it
c trds: 16 transitive reductions, 1325 removed, 6 failed
c trds: 185737 nodes, 147884 edges, 30187873 steps
c trim: 704314 words, 2.7 MB
c trnr: 16 count, 146 bin, 34381 trn, 225489357 steps
c unhd: 20 count, 78 rounds, 135447665 steps
c unhd: 280 non-trivial sccs of average size 2.0
c unhd: 41 units, 40 bin, 0 trn, 1 lrg
c unhd: 200 failed, 189 stamp, 0 lits, 10 bin, 0 trn, 1 lrg
c unhd: 24214 tauts, 380 bin 2%, 6000 trn 25%, 2235 lrg 9%
c unhd: 24214 tauts, 15599 stamp 64%, 22718 red 94%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 974274 str, 40 bin 0%, 2586 trn 0%, 971648 lrg 100%, 961176 red 99%
c vars: 14761 remaining 16% and 80237 removed 84% out of 94998
c vars: 7477 fixed 8%, 67828 eliminated 71%, 4932 equivalent 5%
c vsts: 26785674116 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 16.4 search visits per propagation, 10496.3 per conflict
c wchs: 7385049664 pushed, 26531754 enlarged, 294 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2609292       1812807        466929     134153274      25911284       1476933
c 
c  0 0        197970   8     10280   1         0   0  98790433  74  15030057  58    566620  38     3.8
c  1 5         62244   2     39751   2     14331   3  10098465   8<  2089608   8<   110944   8     0.3
c  2 6        242956   9    175978  10     49640  11  12676205   9   3223046  12    237121  16<    1.0
c  3 9        441540  17    339817  19     81960  18   5688846   4   2063396   8    194791  13     2.9
c  4 14       504753  19<   393967  22     88692  19   2552542   2   1266413   5    132289   9    10.0
c  5 21       422820  16    326984  18<    70803  15<  2170796   2   1058164   4    116468   8     9.6
c  6 30       315913  12    239778  13     55846  12   1305930   1    661764   3     71166   5     6.1
c  7 41       204601   8    148739   8     43533   9    511626   0    300470   1     30100   2     3.9
c  8 54       119721   5     81431   4     30892   7    218841   0    135074   1     11708   1     2.7
c  9 69        58549   2     36839   2     17856   4     88231   0     53667   0      3974   0     1.4
c 10 86        29829   1     16683   1     10197   2     40534   0     23954   0      1498   0     0.8
c 11 126        8396   0      2560   0      3179   1     10825   0      5671   0       254   0     0.3
c 
c avg                  4.3           4.6           4.8           0.7           1.3           2.1
c std                  2.3           1.9           2.2           1.4           1.9           2.1
c 
c   69.528   7% bump
c   32.139   3% unhide
c   15.989   2% sweep
c   14.698   1% probe
c   12.523   1% elim
c    9.665   1% cce
c    7.547   1% decide
c 
c   12.324 < 1% rest (below)
c 
c    4.623   0% quatres
c    1.961   0% transred
c    1.575   0% ternres
c    1.433   0% block
c    1.280   0% gauss
c    1.263   0% bca
c    0.190   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    2.795   0% preprocessing     3%
c   98.270  10% inprocessing     97%
c ==================================
c  101.066  10% simplifying
c  898.798  90% search
c ==================================
c  999.867 100% all
c 
c       2515006 conflicts,        2515.3 confs/sec
c          5291 ternaries,         475.3 confs/ternary
c          1757 binaries,         1431.4 confs/binary
c            19 iterations,     132368.7 confs/iteration
c 
c            49 reductions,          0.0 redus/sec,  51326.7 confs/reduction
c         52876 restarts,           52.9 rests/sec,     47.6 confs/restart
c      12077293 decisions,       12078.9 decis/sec,      4.8 decis/conflict
c    1631465837 propagations,  1631682.5 props/sec,    135.1 props/decision
c 
c 999.9 seconds, 112.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
