c launch: /data/cnf/sc2014/app/manol-pipe-c10nid_i.cnf.bz2
c host: atom03
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/manol-pipe-c10nid_i.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/manol-pipe-c10nid_i.cnf.bz2
c no embedded options
c found 'p cnf 252516 750877' header
c read 252516 variables, 750877 clauses, 1752045 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=3
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 252515 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] SUM (--score=3)
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  252515   750876         0       0      0     0    0     0   39   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 2 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] 2 out of 2 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 252515 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 239 variables
c [simpleprobe-1] 110275 variables remain 44% (142001 retained 56%)
c [simpleprobe-1] removed 239 variables, found 829 hbrs, 13 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 2 units, 9 failed, 185 tauts, 0 hbrs, 148 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 252032 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 62852 not tried 25% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 189160 = 75% variables out of 252032 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 310185 negative 96.0% of 323133 except 12948 4.0%
c [phase-count-1] 307997 positive 95.3% of 323133 except 15136 4.7%
c [phase-1] phase bias: 21907 positive 35%, 40965 negative 65%
c [sort-queue-1] sorted 62872 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 62872 (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 189643 variables 75.1% (62872 remain 25%)
c [simplification-1] removed 427743 irredundant clauses 57.0% (323133 remain 43%)
c [simplification-1] maximum reduction of 75% = max (75%, 57%)
c [simplification-1] large reduction 75% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.2   62871   323133       127      93     22    26    0     5   36   3%      0    5    2    0 21068%
c i    5.2   62865   323133       172     129     26    30    0     5   36   5%      0    5    3    0 19826%
c i    5.2   62861   323133       183     137     26    30    0     5   36   5%      0    5    3    0 19843%
c i    5.2   62857   323133       187     139     26    30    0     5   36   5%      0    5    3    0 19713%
c i    5.2   62852   323133       193     143     26    30    0     5   36   6%      0    5    3    0 19511%
c i    5.2   62848   323133       204     148     26    32    0     5   36   6%      0    5    4    0 19142%
c i    5.2   62845   323133       226     162     26    33    0     5   36   7%      0    5    4    0 18289%
c i    5.2   62840   323133       303     205     31    37    0     5   36   7%      0    5    4    0 15149%
c i    5.2   62839   323133       338     234     35    38    0     6   36   7%      0    6    4    0 14167%
c 
c [simplification-2] limit 1003 conflicts (hard 11000) hit after 1003 conflicts
c [decomp-3] removed 130 variables
c [simpleprobe-2] 27299 schedulable variables 44%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 26257 variables remain 42% (36485 retained 58%)
c [simpleprobe-2] removed 0 variables, found 31 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 36323 literals 29%
c [treelook-1] scheduling used 300004 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 417837 steps
c [treelook-1] 36259 literals remain 29%
c [treelook-1] 31838 variables remain to probed next time 51%
c [treelook-1] removed 0 variables, found 446 hbrs
c [basicprobe-1] limit 2577400 based on 322175 irredundant clauses
c [basicprobe-1-0] 33942 probes remain 55% after last round
c [basicprobe-1-0] 107 units = 107 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1168 variables, found 4017 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 5 units, 34 failed, 224 tauts, 0 hbrs, 2440 literals
c [elim-2] 61466 variables 100% will be scheduled this time
c [elim-2] scheduled 61466 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 15407 not tried 25% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 25419 = 41% variables out of 61466 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 257947 negative 97.2% of 265402 except 7455 2.8%
c [phase-count-2] 256322 positive 96.6% of 265402 except 9080 3.4%
c [phase-2] phase bias: 1 positive 10%, 9 negative 90%
c [sort-queue-2] sorted 31471 enqueued variables after 1003 conflicts
c [score-dist-2] active 4593 (13%), one 0 (0%), zero 31471 (87%)
c [score-dist-2] max exp 518, different 18 (3%)
c [score-dist-2] median active exp 511, avg 511.3
c [simplification-2] removed 26765 variables 42.6% (36064 remain 14%)
c [simplification-2] removed 57731 irredundant clauses 17.9% (265402 remain 35%)
c [simplification-2] maximum reduction of 43% = max (43%, 18%)
c [simplification-2] large reduction 43% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13003 (soft 3003 + delta 10000)
c [simplification-2] new conflict limit 3003 (hard 13003)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.3   36063   265402      2883    1617     74   610    5   100   35   5%     25   98   13    0 3043%
c 
c [simplification-3] limit 3003 conflicts (hard 13003) hit after 3003 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 31 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 31 out of 31 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 75 variables
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 4 failed, 933 tauts, 0 hbrs, 3596 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 35978 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 4292 not tried 12% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1400 = 4% variables out of 35978 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 252937 negative 97.2% of 260140 except 7203 2.8%
c [phase-count-3] 251372 positive 96.6% of 260140 except 8768 3.4%
c [phase-3] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-3] sorted 26110 enqueued variables after 3003 conflicts
c [score-dist-3] active 8468 (24%), one 0 (0%), zero 26110 (76%)
c [score-dist-3] max exp 520, different 19 (4%)
c [score-dist-3] median active exp 514, avg 513.8
c [simplification-3] removed 1485 variables 4.1% (34578 remain 14%)
c [simplification-3] removed 5262 irredundant clauses 2.0% (260140 remain 35%)
c [simplification-3] maximum reduction of 4% = max (4%, 2%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 4000
c [simplification-3] penalized conflict interval 4000 = 1 * 4000
c [simplification-3] hard conflict limit 17003 (soft 7003 + delta 10000)
c [simplification-3] new conflict limit 7003 (hard 17003)
c 
c [simplification-4] limit 7003 conflicts (hard 17003) hit after 7003 conflicts
c [decomp-7] removed 6 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 10650 literals 15%
c [treelook-2] scheduling used 150100 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 172627 steps
c [treelook-2] 10543 literals remain 15%
c [treelook-2] 7825 variables remain to probed next time 23%
c [treelook-2] removed 0 variables, found 47 hbrs
c [unhide-4] limit 172557 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 5 failed, 22 tauts, 0 hbrs, 7400 literals
c [elim-4] 4289 variables 12% will be scheduled this time
c [elim-4] scheduled 4289 variables 12%
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] no variable eliminated in round 1 in 118339683 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 4289 scheduled
c [sort-queue-4] sorted 21392 enqueued variables after 7003 conflicts
c [score-dist-4] active 13172 (38%), one 0 (0%), zero 21392 (62%)
c [score-dist-4] max exp 523, different 22 (4%)
c [score-dist-4] median active exp 516, avg 516.2
c [simplification-4] removed 14 variables 0.0% (34564 remain 14%)
c [simplification-4] removed 469 irredundant clauses 0.2% (259671 remain 35%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 24000
c [simplification-4] penalized conflict interval 24000 = 1 * 24000
c [simplification-4] hard conflict limit 43003 (soft 31003 + delta 12000)
c [simplification-4] new conflict limit 31003 (hard 43003)
c 
c [simplification-5] limit 31003 conflicts (hard 43003) hit after 31005 conflicts
c [quatres-1] found 29197 quaternary clauses 22% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 301 single-self-subsuming ternary resolvents
c [quatres-1-2] added 9735 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 21019465 with penalty 0 = 0 + 0
c [ternres-1] all 34564 free variables schedulable
c [ternres-1] 8906 ternary resolvents (165 bin, 8741 trn)
c [ternres-1] 5 variables remain 0% (34559 retained 100%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 16300 xors of average arity 3.0
c [gauss-1] connected 48885 occurrences of 6849 variables (average 7.1)
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 13 variables
c [basicprobe-2] limit 21019469 penalty 0 = 0 + 0
c [basicprobe-2-0] 16457 sched 49%, 208 failed, 39 lifted, 2423 hbrs
c [decomp-10] removed 961 variables
c [basicprobe-2-1] 17785 sched 53%, 49 failed, 1 lifted, 1712 hbrs
c [decomp-11] removed 291 variables
c [basicprobe-2-2] 17537 sched 53%, 8 failed, 0 lifted, 280 hbrs
c [decomp-12] removed 16 variables
c [basicprobe-2-3] 17554 sched 53%, 1 failed, 0 lifted, 53 hbrs
c [decomp-13] removed 1 variables
c [basicprobe-2-4] 17547 sched 53%, 11 failed, 5 lifted, 8 hbrs
c [decomp-14] removed 34 variables
c [basicprobe-2-5] 17524 sched 53%, 2 failed, 0 lifted, 255 hbrs
c [decomp-15] removed 6 variables
c [basicprobe-2-6] 17516 sched 53%, 0 failed, 0 lifted, 129 hbrs
c [basicprobe-2-7] 16267 probes remain 49% after last round
c [basicprobe-2-7] 324 units = 279 failed (86%) + 45 lifted (14%)
c [basicprobe-2-7] removed 1309 variables, found 4860 hbrs
c [bate-1] eliminated 247 asymmetric tautologies during probing
c [unhide-5] limit 840778 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 0 failed, 578 tauts, 0 hbrs, 42656 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 275 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 33242 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 8168 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 7 (14%) of length 25
c [cce-1-1] eliminated 1 clauses out of 30 (3%) of length 23
c [cce-1-1] eliminated 1 clauses out of 26 (4%) of length 22
c [cce-1-1] eliminated 10 clauses out of 93 (11%) of length 21
c [cce-1-1] eliminated 11 clauses out of 116 (9%) of length 20
c [cce-1-1] eliminated 4 clauses out of 128 (3%) of length 19
c [cce-1-1] eliminated 13 clauses out of 187 (7%) of length 18
c [cce-1-1] eliminated 36 clauses out of 315 (11%) of length 17
c [cce-1-1] eliminated 40 clauses out of 301 (13%) of length 16
c [cce-1-1] eliminated 58 clauses out of 431 (13%) of length 15
c [cce-1-1] eliminated 51 clauses out of 499 (10%) of length 14
c [cce-1-1] eliminated 68 clauses out of 684 (10%) of length 13
c [cce-1-1] eliminated 131 clauses out of 938 (14%) of length 12
c [cce-1-1] eliminated 231 clauses out of 1802 (13%) of length 11
c [cce-1-1] eliminated 420 clauses out of 2529 (17%) of length 10
c [cce-1-1] eliminated 670 clauses out of 4061 (16%) of length 9
c [cce-1-1] eliminated 142 clauses out of 7243 (2%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1888 large clauses in 30000038 steps
c [cce-1-1] allowing another 15000019 steps for small clauses
c [cce-1-1] scheduling 104986 clauses = 28950 binary + 76036 ternary
c [cce-1-1] tried to eliminate 14074 small clauses 13%
c [cce-1-1] eliminated 68 binary clauses 0%
c [cce-1-1] eliminated 127 ternary clauses 0%
c [cce-1-1] eliminated 195 small clauses 0%
c [cce-1-1] eliminated 195 small clauses in 30000035 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2083 covered clauses in round 1
c [cce-1] eliminated 2083 covered clauses in TOTAL during 1 rounds
c [cce-1] 2083 < 1/100 * 233826 = 2338 considered unsuccessful
c [bca-1] limit of 10000000 steps and 463986 added (scaled 2)
c [bca-1] 46994 out of 65322 literals actually usable 72%
c [bca-1] added 139 blocked clauses in 170588 steps
c [sweep-1] limit 1261168 penalty 0 = 0 + 0
c [sweep-1-1] 13564 pos 41.5% + 19096 neg 58.5% = 32660 sched 100.0% ret 0
c [sweep-1-1] 1262347 steps 121 queries 5827.60 avg class size
c [sweep-1-1] 4570 decisions 120 SAT calls 86.06 avg env size
c [sweep-1-1] 30439 variables remain 93% (2221 retained 7%)
c [decomp-17] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 120 queries)
c [sort-queue-5] sorted 17421 enqueued variables after 31005 conflicts
c [score-dist-5] active 15238 (47%), one 0 (0%), zero 17421 (53%)
c [score-dist-5] max exp 529, different 26 (5%)
c [score-dist-5] median active exp 519, avg 519.3
c [simplification-5] removed 1905 variables 5.5% (32659 remain 13%)
c [simplification-5] removed 27930 irredundant clauses 10.8% (231741 remain 31%)
c [simplification-5] maximum reduction of 11% = max (6%, 11%)
c [simplification-5] large reduction 11% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 43005 (soft 33005 + delta 10000)
c [simplification-5] new conflict limit 33005 (hard 43005)
c 
c [simplification-6] limit 33005 conflicts (hard 43005) hit after 33006 conflicts
c [quatres-2] found 37193 quaternary clauses 29% in total
c [quatres-2-1] added 8 double-self-subsuming ternary resolvents
c [quatres-2-2] added 154 single-self-subsuming ternary resolvents
c [quatres-2-2] added 6047 quaternary resolvents
c [ternres-2] limit 4502765 with penalty 0 = 0 + 0
c [ternres-2] 4 schedulable variables 0%
c [ternres-2] 2643 ternary resolvents (29 bin, 2614 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 562845 penalty 2 = 2 + 0
c [card-3] found 110 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 562845 for elimination
c [card-3] 110 out of 110 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-18] removed 6 variables
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 141 transitive binary clauses
c [transred-2] found 15 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 32638 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 1464 blocked clauses
c [block-2] 1464 < 1/100 * 231659 = 2316 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 32297 variables 100%
c [elim-5] limit of 45027659 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 1629 not tried 5% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1924 = 6% variables out of 32297 scheduled
c [bca-2] limit of 10000000 steps and 451351 added (scaled 2)
c [bca-2] 43254 out of 60748 literals actually usable 71%
c [bca-2] added 25 blocked clauses in 162807 steps
c [sweep-2] limit 1350829 penalty 0 = 0 + 0
c [sweep-2-1] 11212 pos 39.6% + 17104 neg 60.4% = 28316 sched 93.2% ret 2057
c [sweep-2-1] 1371269 steps 144 queries 5062.76 avg class size
c [sweep-2-1] 4925 decisions 143 SAT calls 67.21 avg env size
c [sweep-2-1] 26421 variables remain 87% (3952 retained 13%)
c [decomp-19] removed 4 variables
c [sweep-2-1] removed 4 vars (0 failed, 4 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 4 vars in TOTAL (1 rounds, 143 queries)
c [sort-queue-6] sorted 15906 enqueued variables after 33006 conflicts
c [score-dist-6] active 14463 (48%), one 0 (0%), zero 15906 (52%)
c [score-dist-6] max exp 529, different 26 (5%)
c [score-dist-6] median active exp 520, avg 519.5
c [simplification-6] removed 2290 variables 7.0% (30369 remain 12%)
c [simplification-6] removed 6376 irredundant clauses 2.8% (225365 remain 30%)
c [simplification-6] maximum reduction of 7% = max (7%, 3%)
c [simplification-6] large reduction 7% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 45006 (soft 35006 + delta 10000)
c [simplification-6] new conflict limit 35006 (hard 45006)
c 
c [simplification-7] limit 35006 conflicts (hard 45006) hit after 35008 conflicts
c [quatres-3] found 37586 quaternary clauses 29% in total
c [quatres-3-2] added 134 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1682 quaternary resolvents
c [ternres-3] limit 4746786 with penalty 0 = 0 + 0
c [ternres-3] all 30369 free variables schedulable
c [ternres-3] 1070 ternary resolvents (0 bin, 1070 trn)
c [ternres-3] 19155 variables remain 63% (11214 retained 37%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 8225 xors of average arity 3.0
c [gauss-2] connected 24674 occurrences of 4739 variables (average 5.2)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 12745 schedulable variables 42%
c [simpleprobe-3] limit 9493573 penalty 1 = 1 + 0
c [decomp-21] removed 8 variables
c [simpleprobe-3] 12832 variables remain 42% (17529 retained 58%)
c [simpleprobe-3] removed 8 variables, found 141 hbrs, 7 units
c [unhide-6] limit 474678 with penalty 1 = 1 + 0
c [unhide-6-6] 0 units, 4 failed, 679 tauts, 0 hbrs, 17903 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 124 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 36
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 25
c [cce-2-1] eliminated 1 clauses out of 39 (3%) of length 23
c [cce-2-1] eliminated 1 clauses out of 89 (1%) of length 21
c [cce-2-1] eliminated 1 clauses out of 111 (1%) of length 20
c [cce-2-1] eliminated 4 clauses out of 148 (3%) of length 19
c [cce-2-1] eliminated 12 clauses out of 221 (5%) of length 18
c [cce-2-1] eliminated 14 clauses out of 341 (4%) of length 17
c [cce-2-1] eliminated 14 clauses out of 354 (4%) of length 16
c [cce-2-1] eliminated 20 clauses out of 493 (4%) of length 15
c [cce-2-1] eliminated 22 clauses out of 609 (4%) of length 14
c [cce-2-1] eliminated 37 clauses out of 846 (4%) of length 13
c [cce-2-1] eliminated 73 clauses out of 1126 (6%) of length 12
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 201 large clauses in 15000044 steps
c [cce-2-1] allowing another 7500022 steps for small clauses
c [cce-2-1] scheduling 37145 clauses = 26935 binary + 10210 ternary
c [cce-2-1] tried to eliminate 5796 small clauses 16%
c [cce-2-1] eliminated 70 binary clauses 0%
c [cce-2-1] eliminated 65 ternary clauses 1%
c [cce-2-1] eliminated 135 small clauses 0%
c [cce-2-1] eliminated 139 small clauses in 15000760 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 340 covered clauses in round 1
c [cce-2] eliminated 340 covered clauses in TOTAL during 1 rounds
c [cce-2] 340 < 1/100 * 225284 = 2252 considered unsuccessful
c [elim-6] 1629 variables 5% will be scheduled this time
c [elim-6] scheduled 1629 variables 5%
c [elim-6] limit of 94935731 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 75005015 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 1629 scheduled
c [bca-3] limit of 10000000 steps and 449266 added (scaled 2)
c [bca-3] 42617 out of 60716 literals actually usable 70%
c [bca-3] added 3 blocked clauses in 163504 steps
c [sweep-3] limit 1424035 penalty 0 = 0 + 0
c [sweep-3-1] 10416 pos 39.4% + 15992 neg 60.6% = 26408 sched 87.0% ret 3949
c [sweep-3-1] 1431270 steps 193 queries 3605.09 avg class size
c [sweep-3-1] 5326 decisions 188 SAT calls 44.22 avg env size
c [sweep-3-1] 23983 variables remain 79% (6374 retained 21%)
c [decomp-22] removed 9 variables
c [sweep-3-1] removed 9 vars (0 failed, 4 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 9 vars in TOTAL (1 rounds, 192 queries)
c [sort-queue-7] sorted 15715 enqueued variables after 35008 conflicts
c [score-dist-7] active 14633 (48%), one 0 (0%), zero 15715 (52%)
c [score-dist-7] max exp 529, different 26 (5%)
c [score-dist-7] median active exp 520, avg 519.6
c [simplification-7] removed 21 variables 0.1% (30348 remain 12%)
c [simplification-7] removed 1047 irredundant clauses 0.5% (224318 remain 30%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 24000
c [simplification-7] new conflict interval 48000
c [simplification-7] penalized conflict interval 48000 = 1 * 48000
c [simplification-7] hard conflict limit 107008 (soft 83008 + delta 24000)
c [simplification-7] new conflict limit 83008 (hard 107008)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   52.3   30348   224318     73568   37749  10957  2934   69   191   39  36%    670   55   65   30  217%
c 
c [simplification-8] limit 83008 conflicts (hard 107008) hit after 83009 conflicts
c [quatres-4] found 38896 quaternary clauses 29% in total
c [quatres-4-1] removed 9 duplicate quaternary clauses
c [quatres-4-1] added 6 double-self-subsuming ternary resolvents
c [quatres-4-2] added 110 single-self-subsuming ternary resolvents
c [quatres-4-2] added 957 quaternary resolvents
c [ternres-4] limit 9527636 with penalty 0 = 0 + 0
c [ternres-4] 19141 schedulable variables 63%
c [ternres-4] 2484 ternary resolvents (73 bin, 2411 trn)
c [ternres-4] 87 variables remain 0% (30261 retained 100%)
c [decomp-23] removed 1 variables
c [unhide-7] limit 1905527 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 0 failed, 1940 tauts, 0 hbrs, 29786 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 78 transitive binary clauses
c [transred-4] found 3 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 30344 variables 100%
c [block-3] limit of 47638181 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 911 blocked clauses
c [block-3] 911 < 1/100 * 222478 = 2224 considered unsuccessful
c [bca-4] limit of 10000000 steps and 443687 added (scaled 2)
c [bca-4] 41638 out of 60422 literals actually usable 69%
c [bca-4] added 6 blocked clauses in 171549 steps
c [sweep-4] limit 2858290 penalty 0 = 0 + 0
c [sweep-4-1] 10685 pos 44.8% + 13168 neg 55.2% = 23853 sched 79.0% ret 6357
c [sweep-4-1] 2858341 steps 340 queries 2890.07 avg class size
c [sweep-4-1] 8641 decisions 337 SAT calls 39.72 avg env size
c [sweep-4-1] 20325 variables remain 67% (9885 retained 33%)
c [decomp-24] removed 20 variables
c [sweep-4-1] removed 20 vars (0 failed, 9 eqs, 10 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 20 vars in TOTAL (1 rounds, 339 queries)
c [sort-queue-8] sorted 14617 enqueued variables after 83009 conflicts
c [score-dist-8] active 15573 (52%), one 0 (0%), zero 14617 (48%)
c [score-dist-8] max exp 532, different 29 (5%)
c [score-dist-8] median active exp 522, avg 521.5
c [simplification-8] removed 158 variables 0.5% (30190 remain 12%)
c [simplification-8] removed 2863 irredundant clauses 1.3% (221455 remain 29%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 24000 = 48000 / 2
c [simplification-8] new conflict interval 72000
c [simplification-8] penalized conflict interval 72000 = 1 * 72000
c [simplification-8] hard conflict limit 191009 (soft 155009 + delta 36000)
c [simplification-8] new conflict limit 155009 (hard 191009)
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 -   80.1   30190   221455    132173   43849  13289  3030   98   200   40  49%    879   16  137   66  206%
c 
c [simplification-9] limit 155009 conflicts (hard 191009) hit after 155009 conflicts
c [quatres-5] found 36193 quaternary clauses 28% in total
c [quatres-5-1] removed 13 duplicate quaternary clauses
c [quatres-5-1] added 3 double-self-subsuming ternary resolvents
c [quatres-5-2] added 3141 single-self-subsuming ternary resolvents
c [quatres-5-2] added 277 quaternary resolvents
c [ternres-5] limit 18388569 with penalty 0 = 0 + 0
c [ternres-5] 84 schedulable variables 0%
c [ternres-5] 6123 ternary resolvents (124 bin, 5999 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-25] removed 7 variables
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 121 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 30183 variables 100%
c [elim-7] limit of 183885698 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 403 variables 1% in round 1 in 159966563 steps
c [elim-7-1] backward subsumption/strengthening limit 23919135
c [elim-7-1-1] backward checking 2438 touched variables 8%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 7 clauses in 4099617 steps
c [elim-7-1] rescheduled 15 variables 0% by backward subsumption
c [elim-7-2] eliminated 1 variables 0% in round 2 in 6524463 steps
c [elim-7-2] backward subsumption/strengthening limit 6524400
c [elim-7-2-1] backward checking 7 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 169306 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 404 = 1% variables out of 30183 scheduled
c [bca-5] limit of 10000000 steps and 441928 added (scaled 2)
c [bca-5] 40757 out of 59560 literals actually usable 68%
c [bca-5] added 19 blocked clauses in 175325 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 55165700 penalty 0 = 0 + 0
c [sweep-5-1] 7530 pos 37.6% + 12489 neg 62.4% = 20019 sched 67.2% ret 9760
c [sweep-5-1] 20201711 steps 5268 queries 527.92 avg class size
c [sweep-5-1] 83925 decisions 5243 SAT calls 22.76 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-26] removed 121 variables
c [sweep-5-1] removed 121 vars (0 failed, 45 eqs, 42 impls)
c [sweep-5-2] 10760 pos 36.3% + 18898 neg 63.7% = 29658 sched 100.0% ret 0
c [sweep-5-2] 23568771 steps 4739 queries 292.57 avg class size
c [sweep-5-2] 79918 decisions 4694 SAT calls 25.67 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-27] removed 164 variables
c [sweep-5-2] removed 164 vars (0 failed, 61 eqs, 54 impls)
c [sweep-5-3] 10718 pos 36.3% + 18776 neg 63.7% = 29494 sched 100.0% ret 0
c [sweep-5-3] 11398854 steps 1519 queries 796.69 avg class size
c [sweep-5-3] 35521 decisions 1512 SAT calls 38.03 avg env size
c [sweep-5-3] 10110 variables remain 34% (19376 retained 66%)
c [decomp-28] removed 33 variables
c [sweep-5-3] removed 33 vars (0 failed, 15 eqs, 13 impls)
c [sweep-5] removed 318 vars in TOTAL (3 rounds, 11523 queries)
c [sort-queue-9] sorted 12749 enqueued variables after 155009 conflicts
c [score-dist-9] active 16712 (57%), one 0 (0%), zero 12749 (43%)
c [score-dist-9] max exp 534, different 31 (6%)
c [score-dist-9] median active exp 523, avg 523.0
c [simplification-9] removed 729 variables 2.4% (29461 remain 12%)
c [simplification-9] removed 4791 irredundant clauses 2.2% (216664 remain 29%)
c [simplification-9] maximum reduction of 2% = max (2%, 2%)
c [simplification-9] geometric conflict interval increment 24000 = 72000 / 3
c [simplification-9] new conflict interval 96000
c [simplification-9] penalized conflict interval 96000 = 1 * 96000
c [simplification-9] hard conflict limit 299009 (soft 251009 + delta 48000)
c [simplification-9] new conflict limit 251009 (hard 299009)
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 -  101.5   29461   216664    173163   41951  16243  2881   21   276   39   8%    947   53   21   54   38%
c -  105.7   29461   216664    207033   40095  16243  2881   21   232   39   9%    978    2   20   41   48%
c -  108.9   29461   216664    243450   40550  16243  2881   21   232   39   9%    997    1   22   32   68%
c 
c [simplification-10] limit 251009 conflicts (hard 299009) hit after 251012 conflicts
c [quatres-6] found 32357 quaternary clauses 26% in total
c [quatres-6-1] removed 106 duplicate quaternary clauses
c [quatres-6-2] added 317 single-self-subsuming ternary resolvents
c [quatres-6-2] added 985 quaternary resolvents
c [ternres-6] limit 23271721 with penalty 0 = 0 + 0
c [ternres-6] all 29461 free variables schedulable
c [ternres-6] 4371 ternary resolvents (87 bin, 4284 trn)
c [ternres-6] 3 variables remain 0% (29458 retained 100%)
c [card-4] limit 1454482 penalty 3 = 3 + 0
c [card-4] found 195 at-most-one constraints of average size 3.0
c [card-4] found 160 at-most-two constraints of average size 4.0
c [card-4] using previous limit 1454482 for elimination
c [card-4] 351 out of 355 constraints (99%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1163586 penalty 2 = 2 + 0
c [gauss-3] extracted 8298 xors of average arity 3.0
c [gauss-3] connected 24875 occurrences of 4811 variables (average 5.2)
c [gauss-3] limit 1163586 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-29] removed 12 variables
c [treelook-3] limit 581793 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 17887 literals 30%
c [treelook-3] scheduling used 581809 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 581793 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 632255 steps
c [treelook-3] 17655 literals remain 30%
c [treelook-3] 5927 variables remain to probed next time 20%
c [treelook-3] removed 52 variables, found 548 hbrs
c [unhide-8] limit 2327172 with penalty 1 = 1 + 0
c [unhide-8-9] 3 units, 6 failed, 2778 tauts, 0 hbrs, 24987 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 202 transitive binary clauses
c [cce-3] limit of 29089652 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 27
c [cce-3-1] eliminated 11 clauses out of 135 (8%) of length 20
c [cce-3-1] eliminated 6 clauses out of 193 (3%) of length 18
c [cce-3-1] eliminated 3 clauses out of 339 (1%) of length 17
c [cce-3-1] eliminated 8 clauses out of 283 (3%) of length 16
c [cce-3-1] eliminated 25 clauses out of 415 (6%) of length 15
c [cce-3-1] eliminated 33 clauses out of 568 (6%) of length 14
c [cce-3-1] eliminated 25 clauses out of 730 (3%) of length 13
c [cce-3-1] eliminated 35 clauses out of 989 (4%) of length 12
c [cce-3-1] eliminated 114 clauses out of 1832 (6%) of length 11
c [cce-3-1] eliminated 166 clauses out of 2318 (7%) of length 10
c [cce-3-1] eliminated 157 clauses out of 3645 (4%) of length 9
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 584 large clauses in 29089736 steps
c [cce-3-1] allowing another 14544868 steps for small clauses
c [cce-3-1] scheduling 97285 clauses = 25131 binary + 72154 ternary
c [cce-3-1] tried to eliminate 16574 small clauses 17%
c [cce-3-1] eliminated 103 binary clauses 0%
c [cce-3-1] eliminated 339 ternary clauses 0%
c [cce-3-1] eliminated 442 small clauses 0%
c [cce-3-1] eliminated 442 small clauses in 29089796 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1026 covered clauses in round 1
c [cce-3] eliminated 1026 covered clauses in TOTAL during 1 rounds
c [cce-3] 1026 < 1/100 * 214847 = 2148 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 29389 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 9308688640 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1205 variables 4% in round 1 in 150384915 steps
c [elim-8-1] backward subsumption/strengthening limit 150384900
c [elim-8-1-1] backward checking 3280 touched variables 11%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1 and strengthened 58 clauses in 5093930 steps
c [elim-8-1] rescheduled 101 variables 0% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 1417699 steps
c [elim-8-2] backward subsumption/strengthening limit 1417600
c [elim-8-2-1] backward checking 10 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 189564 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1206 = 4% variables out of 29389 scheduled
c [bca-6] limit of 10000000 steps and 420062 added (scaled 2)
c [bca-6] 39355 out of 56368 literals actually usable 70%
c [bca-6] added 46 blocked clauses in 165604 steps
c [sweep-6] limit 6981516 penalty 0 = 0 + 0
c [sweep-6-1] 3626 pos 37.7% + 5983 neg 62.3% = 9609 sched 34.1% ret 18574
c [sweep-6-1] 6983472 steps 2302 queries 669.25 avg class size
c [sweep-6-1] 35684 decisions 2288 SAT calls 21.64 avg env size
c [sweep-6-1] 3428 variables remain 12% (24749 retained 88%)
c [decomp-31] removed 29 variables
c [sweep-6-1] removed 29 vars (0 failed, 16 eqs, 9 impls)
c [sweep-6] removed 29 vars in TOTAL (1 rounds, 2301 queries)
c [sort-queue-10] sorted 11782 enqueued variables after 251012 conflicts
c [score-dist-10] active 16372 (58%), one 0 (0%), zero 11782 (42%)
c [score-dist-10] max exp 536, different 33 (6%)
c [score-dist-10] median active exp 523, avg 523.3
c [simplification-10] removed 1307 variables 4.4% (28154 remain 11%)
c [simplification-10] removed 7148 irredundant clauses 3.3% (209516 remain 28%)
c [simplification-10] maximum reduction of 4% = max (4%, 3%)
c [simplification-10] geometric conflict interval increment 19200 = 96000 / 5
c [simplification-10] new conflict interval 115200
c [simplification-10] penalized conflict interval 115200 = 1 * 115200
c [simplification-10] hard conflict limit 423812 (soft 366212 + delta 57600)
c [simplification-10] new conflict limit 366212 (hard 423812)
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 -  123.1   28154   209516    321093   40045  15153  1856   10   233   38   4%   1016   84   15   19   82%
c 
c [simplification-11] limit 366212 conflicts (hard 423812) hit after 366214 conflicts
c [quatres-7] found 31563 quaternary clauses 25% in total
c [quatres-7-1] removed 17 duplicate quaternary clauses
c [quatres-7-1] added 6 double-self-subsuming ternary resolvents
c [quatres-7-2] added 236 single-self-subsuming ternary resolvents
c [quatres-7-2] added 597 quaternary resolvents
c [ternres-7] limit 30818759 with penalty 0 = 0 + 0
c [ternres-7] 3 schedulable variables 0%
c [ternres-7] 1414 ternary resolvents (43 bin, 1371 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-32] removed 7 variables
c [basicprobe-3] limit 154093797 penalty 0 = 0 + 0
c [basicprobe-3-0] 13877 sched 49%, 25 failed, 0 lifted, 468 hbrs
c [decomp-33] removed 84 variables
c [basicprobe-3-1] 14886 sched 53%, 2 failed, 0 lifted, 52 hbrs
c [decomp-34] removed 2 variables
c [basicprobe-3-2] 14879 sched 53%, 1 failed, 0 lifted, 8 hbrs
c [decomp-35] removed 1 variables
c [basicprobe-3-3] 14889 sched 53%, 1 failed, 0 lifted, 57 hbrs
c [decomp-36] removed 1 variables
c [basicprobe-3-4] 14879 sched 53%, 2 failed, 0 lifted, 15 hbrs
c [decomp-37] removed 2 variables
c [basicprobe-3-5] 14884 sched 53%, 1 failed, 0 lifted, 24 hbrs
c [decomp-38] removed 2 variables
c [basicprobe-3-6] 14880 sched 53%, 1 failed, 0 lifted, 24 hbrs
c [decomp-39] removed 1 variables
c [basicprobe-3-7] 14888 sched 53%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-3-8] 14888 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-8] round limit 8 hit
c [basicprobe-3-8] 33 units = 33 failed (100%) + 0 lifted (0%)
c [basicprobe-3-8] removed 93 variables, found 652 hbrs
c [bate-2] eliminated 35 asymmetric tautologies during probing
c [unhide-9] limit 6163751 with penalty 0 = 0 + 0
c [unhide-9-12] 0 units, 0 failed, 2416 tauts, 0 hbrs, 77576 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 107 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 28054 variables 100%
c [block-4] limit of 77046898 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 952 blocked clauses
c [block-4] 952 < 1/100 * 206971 = 2069 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 27941 variables 100%
c [elim-9] limit of 616375191 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 377 variables 1% in round 1 in 160972370 steps
c [elim-9-1] backward subsumption/strengthening limit 160972300
c [elim-9-1-1] backward checking 1922 touched variables 7%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 2 and strengthened 9 clauses in 3212041 steps
c [elim-9-1] rescheduled 28 variables 0% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 3830142 steps
c [elim-9-2] backward subsumption/strengthening limit 3830100
c [elim-9-2-1] backward checking 11 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 129530 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 378 = 1% variables out of 27941 scheduled
c [bca-7] limit of 10000000 steps and 410689 added (scaled 2)
c [bca-7] 37336 out of 55128 literals actually usable 68%
c [bca-7] added 10 blocked clauses in 177667 steps
c [sweep-7] limit 9245627 penalty 0 = 0 + 0
c [sweep-7-1] 1644 pos 49.6% + 1668 neg 50.4% = 3312 sched 12.0% ret 24251
c [sweep-7-1] 3046471 steps 1978 queries 516.10 avg class size
c [sweep-7-1] 21790 decisions 1973 SAT calls 16.10 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-41] removed 5 variables
c [sweep-7-1] removed 5 vars (0 failed, 6 eqs, 4 impls)
c [sweep-7-2] 11113 pos 40.3% + 16445 neg 59.7% = 27558 sched 100.0% ret 0
c [sweep-7-2] 6200590 steps 785 queries 1158.18 avg class size
c [sweep-7-2] 21487 decisions 784 SAT calls 42.54 avg env size
c [sweep-7-2] 14326 variables remain 52% (13224 retained 48%)
c [decomp-42] removed 9 variables
c [sweep-7-2] removed 9 vars (0 failed, 1 eqs, 0 impls)
c [sweep-7] 14 < 1/1000 * 27563 = 27 considered unsuccessful
c [sweep-7] removed 14 vars in TOTAL (2 rounds, 2761 queries)
c [sort-queue-11] sorted 10296 enqueued variables after 366214 conflicts
c [score-dist-11] active 17253 (63%), one 0 (0%), zero 10296 (37%)
c [score-dist-11] max exp 537, different 32 (6%)
c [score-dist-11] median active exp 524, avg 524.0
c [simplification-11] removed 605 variables 2.1% (27549 remain 11%)
c [simplification-11] removed 4648 irredundant clauses 2.2% (204868 remain 27%)
c [simplification-11] maximum reduction of 2% = max (2%, 2%)
c [simplification-11] geometric conflict interval increment 38400 = 115200 / 3
c [simplification-11] new conflict interval 153600
c [simplification-11] penalized conflict interval 153600 = 1 * 153600
c [simplification-11] hard conflict limit 596614 (soft 519814 + delta 76800)
c [simplification-11] new conflict limit 519814 (hard 596614)
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 -  146.4   27549   204868    376880   42122  14775  1558   36   235   39  15%   1021   36   57   20  278%
c -  157.7   27549   204868    415417   44775  14918  1564   24   210   39  12%   1022    5   15   25   62%
c -  167.2   27549   204868    453128   43170  15068  1565   33   143   39  23%   1023  -46   50   27  182%
c -  176.8   27549   204868    493170   45831  15126  1566   55    87   40  63%   1023  -74   58   34  171%
c -  188.3   27549   204868    533091   49145  15202  1568   43    90   41  47%   1024  -65   46   39  117%
c 
c [simplification-12] limit 519814 conflicts (hard 596614) hit after 551013 conflicts
c [quatres-8] found 29983 quaternary clauses 24% in total
c [quatres-8-1] removed 109 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 815 single-self-subsuming ternary resolvents
c [quatres-8-2] added 369 quaternary resolvents
c [ternres-8] limit 45227941 with penalty 0 = 0 + 0
c [ternres-8] all 27549 free variables schedulable
c [ternres-8] 2431 ternary resolvents (96 bin, 2335 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-43] removed 8 variables
c [simpleprobe-4] 11599 schedulable variables 42%
c [simpleprobe-4] limit 180911765 penalty 0 = 0 + 0
c [decomp-44] removed 14 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 14 variables, found 336 hbrs, 1 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 224 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 27527 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 55 variables 0% in round 1 in 157717173 steps
c [elim-10-1] backward subsumption/strengthening limit 157717100
c [elim-10-1-1] backward checking 253 touched variables 1%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 950903 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 55 = 0% variables out of 27527 scheduled
c [elim-10] 55 < 1/100 * 27527 = 275 considered unsuccessful
c [bca-8] limit of 10000000 steps and 409468 added (scaled 2)
c [bca-8] 37049 out of 54946 literals actually usable 67%
c [bca-8] added 70 blocked clauses in 178264 steps
c [sort-queue-12] sorted 9596 enqueued variables after 551013 conflicts
c [score-dist-12] active 17876 (65%), one 0 (0%), zero 9596 (35%)
c [score-dist-12] max exp 538, different 33 (6%)
c [score-dist-12] median active exp 525, avg 525.1
c [simplification-12] removed 77 variables 0.3% (27472 remain 11%)
c [simplification-12] removed 446 irredundant clauses 0.2% (204422 remain 27%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 153600
c [simplification-12] new conflict interval 307200
c [simplification-12] penalized conflict interval 307200 = 1 * 307200
c [simplification-12] hard conflict limit 1011813 (soft 858213 + delta 153600)
c [simplification-12] new conflict limit 858213 (hard 1011813)
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 -  201.7   27472   204422    575768   49363  17618  1767   41   195   41  21%   1024   45   41   45   91%
c -  211.4   27472   204422    617091   50554  17634  1767   76   105   43  73%   1024  -40   80   58  139%
c -  221.7   27472   204422    659962   51663  17694  1767   93   117   44  80%   1024  -14   96   65  147%
c -  236.5   27472   204422    721305   51245  17733  1767   87   122   44  71%   1024    2  109   80  136%
c -  247.9   27472   204422    769918   53190  17772  1768   63    95   44  67%   1024  -19   46   79   59%
c -  258.9   27472   204422    812351   54836  17846  1769   64    95   58  67%   1024  -22   71   70  102%
c -  269.4   27472   204422    853108   55924  17875  1770   64   101   58  64%   1024   -5   71   67  106%
c 
c [simplification-13] limit 858213 conflicts (hard 1011813) hit after 858214 conflicts
c [quatres-9] found 29576 quaternary clauses 23% in total
c [quatres-9-1] removed 21 duplicate quaternary clauses
c [quatres-9-1] added 8 double-self-subsuming ternary resolvents
c [quatres-9-2] added 75 single-self-subsuming ternary resolvents
c [quatres-9-2] added 65 quaternary resolvents
c [ternres-9] limit 66748387 with penalty 0 = 0 + 0
c [ternres-9] all 27472 free variables schedulable
c [ternres-9] 322 ternary resolvents (34 bin, 288 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-45] removed 1 variables
c [unhide-10] limit 6674838 with penalty 1 = 1 + 0
c [unhide-10-16] 0 units, 0 failed, 1282 tauts, 0 hbrs, 61124 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 45 transitive binary clauses
c [bca-9] limit of 10000000 steps and 409341 added (scaled 2)
c [bca-9] 37655 out of 54944 literals actually usable 69%
c [bca-9] added 11 blocked clauses in 176397 steps
c [sweep-8] limit 10012258 penalty 1 = 1 + 0
c [sweep-8-1] 6357 pos 44.5% + 7929 neg 55.5% = 14286 sched 52.0% ret 13185
c [sweep-8-1] 10012295 steps 3028 queries 737.00 avg class size
c [sweep-8-1] 50447 decisions 3023 SAT calls 23.66 avg env size
c [sweep-8-1] 3301 variables remain 12% (24169 retained 88%)
c [decomp-46] removed 10 variables
c [sweep-8-1] removed 10 vars (0 failed, 8 eqs, 11 impls)
c [sweep-8] 10 < 1/1000 * 27471 = 27 considered unsuccessful
c [sweep-8] removed 10 vars in TOTAL (1 rounds, 3027 queries)
c [sort-queue-13] sorted 9317 enqueued variables after 858214 conflicts
c [score-dist-13] active 18144 (66%), one 0 (0%), zero 9317 (34%)
c [score-dist-13] max exp 540, different 35 (6%)
c [score-dist-13] median active exp 526, avg 525.6
c [simplification-13] removed 11 variables 0.0% (27461 remain 11%)
c [simplification-13] removed 200 irredundant clauses 0.1% (204222 remain 27%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 307200
c [simplification-13] new conflict interval 614400
c [simplification-13] penalized conflict interval 614400 = 1 * 614400
c [simplification-13] hard conflict limit 1779814 (soft 1472614 + delta 307200)
c [simplification-13] new conflict limit 1472614 (hard 1779814)
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 -  287.9   27461   204222    903213   57009  16778  1729   68    79   45  86%   1024  -32   66   74   89%
c -  299.5   27461   204222    947310   57581  16852  1731   74    91   45  82%   1024  -19   68   67  101%
c -  311.8   27461   204222    990784   59251  16874  1731   58    93   46  63%   1024   -9   55   65   84%
c -  323.6   27461   204222   1033095   59412  16884  1731   70    82   48  85%   1024  -12   70   66  106%
c -  337.7   27461   204222   1077213   59890  16887  1731   62    69   63  89%   1024  -15   57   64   89%
c -  352.8   27461   204222   1122266   60631  16887  1731   55    69   64  80%   1024   -8   59   61   97%
c -  366.7   27461   204222   1169581   61613  16887  1731   60    67   63  88%   1024   -5   63   58  109%
c -  380.1   27461   204222   1217974   61302  16892  1731   56    65   62  85%   1024   -4   57   55  103%
c -  393.6   27461   204222   1266198   62977  16892  1731   61    70   64  87%   1024    2   65   56  116%
c -  407.0   27461   204222   1312812   62374  16893  1731   59    66   64  90%   1024   -2   62   56  110%
c -  420.6   27461   204222   1362259   63189  16894  1731   47    64   64  74%   1024   -3   45   55   83%
c -  433.6   27461   204222   1414285   62976  16899  1731   54    72   64  74%   1024    6   58   54  107%
c -  449.4   27461   204222   1463059   65313  16903  1731   63    66   66  95%   1024   -2   63   58  108%
c -  463.4   27461   204222   1512084   65771  16903  1731   61    64   65  96%   1024   -3   60   56  108%
c 
c [simplification-14] limit 1472614 conflicts (hard 1779814) hit after 1518123 conflicts
c [quatres-10] found 30128 quaternary clauses 23% in total
c [quatres-10-1] removed 7 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 20 single-self-subsuming ternary resolvents
c [quatres-10-2] added 49 quaternary resolvents
c [ternres-10] limit 131783126 with penalty 0 = 0 + 0
c [ternres-10] all 27461 free variables schedulable
c [ternres-10] 883 ternary resolvents (43 bin, 840 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 3294578 penalty 3 = 3 + 0
c [gauss-4] extracted 24928 xors of average arity 3.0
c [gauss-4] connected 74780 occurrences of 5773 variables (average 13.0)
c [gauss-4] limit 3294578 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-4] limit 6589156 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 18074 literals 33%
c [treelook-4] scheduling used 705935 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 6589156 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 6320297 steps
c [treelook-4] fully completed tree based probing
c [decomp-48] removed 8 variables
c [treelook-4] removed 37 variables, found 1130 hbrs
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 207 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 823644540 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 28
c [cce-4-1] eliminated 2 clauses out of 10 (20%) of length 27
c [cce-4-1] eliminated 4 clauses out of 9 (44%) of length 26
c [cce-4-1] eliminated 4 clauses out of 12 (33%) of length 25
c [cce-4-1] eliminated 3 clauses out of 32 (9%) of length 23
c [cce-4-1] eliminated 3 clauses out of 67 (4%) of length 21
c [cce-4-1] eliminated 1 clauses out of 148 (1%) of length 20
c [cce-4-1] eliminated 4 clauses out of 113 (4%) of length 19
c [cce-4-1] eliminated 4 clauses out of 230 (2%) of length 18
c [cce-4-1] eliminated 3 clauses out of 329 (1%) of length 17
c [cce-4-1] eliminated 2 clauses out of 310 (1%) of length 16
c [cce-4-1] eliminated 11 clauses out of 383 (3%) of length 15
c [cce-4-1] eliminated 11 clauses out of 565 (2%) of length 14
c [cce-4-1] eliminated 8 clauses out of 743 (1%) of length 13
c [cce-4-1] eliminated 13 clauses out of 1034 (1%) of length 12
c [cce-4-1] eliminated 32 clauses out of 1781 (2%) of length 11
c [cce-4-1] eliminated 40 clauses out of 2319 (2%) of length 10
c [cce-4-1] eliminated 126 clauses out of 3648 (3%) of length 9
c [cce-4-1] eliminated 858 clauses out of 6835 (13%) of length 8
c [cce-4-1] eliminated 1594 clauses out of 14423 (11%) of length 7
c [cce-4-1] eliminated 1544 clauses out of 30503 (5%) of length 6
c [cce-4-1] eliminated 1544 clauses out of 19521 (8%) of length 5
c [cce-4-1] eliminated 611 clauses out of 19597 (3%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 6423 large clauses in 133683720 steps
c [cce-4-1] allowing another 66841860 steps for small clauses
c [cce-4-1] scheduling 90175 clauses = 23326 binary + 66849 ternary
c [cce-4-1] tried to eliminate 90175 small clauses 100%
c [cce-4-1] eliminated 158 binary clauses 1%
c [cce-4-1] eliminated 440 ternary clauses 1%
c [cce-4-1] eliminated 598 small clauses 1%
c [cce-4-1] eliminated 598 small clauses in 124683871 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 7021 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 57021924 steps for small clauses
c [cce-4-2] scheduling 89584 clauses = 23168 binary + 66416 ternary
c [cce-4-2] tried to eliminate 89584 small clauses 100%
c [cce-4-2] eliminated 4 ternary clauses 0%
c [cce-4-2] eliminated 4 small clauses 0%
c [cce-4-2] eliminated 4 small clauses in 112410843 steps
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 4 covered clauses in round 2
c [cce-4-3] completed large round (ATE)
c [cce-4-3] allowing another 57001356 steps for small clauses
c [cce-4-3] scheduling 89580 clauses = 23168 binary + 66412 ternary
c [cce-4-3] tried to eliminate 89580 small clauses 100%
c [cce-4-3] completed small round (ATE)
c [cce-4-3] eliminated 0 covered clauses in round 3
c [cce-4] eliminated 7025 covered clauses in TOTAL during 3 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 27424 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 1692 variables 6% in round 1 in 130535290 steps
c [elim-11-1] backward subsumption/strengthening limit 130535200
c [elim-11-1-1] backward checking 5865 touched variables 21%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 6 clauses in 4707124 steps
c [elim-11-1] rescheduled 40 variables 0% by backward subsumption
c [elim-11-2] eliminated 2 variables 0% in round 2 in 21565482 steps
c [elim-11-2] backward subsumption/strengthening limit 21565400
c [elim-11-2-1] backward checking 11 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 250748 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 1694 = 6% variables out of 27424 scheduled
c [bca-10] limit of 10000000 steps and 385722 added (scaled 2)
c [bca-10] 36925 out of 51462 literals actually usable 72%
c [bca-10] added 74 blocked clauses in 166707 steps
c [sort-queue-14] sorted 8423 enqueued variables after 1518123 conflicts
c [score-dist-14] active 17307 (67%), one 0 (0%), zero 8423 (33%)
c [score-dist-14] max exp 541, different 36 (7%)
c [score-dist-14] median active exp 526, avg 526.2
c [simplification-14] removed 1731 variables 6.3% (25730 remain 10%)
c [simplification-14] removed 11693 irredundant clauses 5.7% (192529 remain 26%)
c [simplification-14] maximum reduction of 6% = max (6%, 6%)
c [simplification-14] large reduction 6% >= 5% limit
c [simplification-14] next conflict interval 15181 = min (1518123/100, 614400)
c [simplification-14] penalized conflict interval 15181 = 1 * 15181
c [simplification-14] hard conflict limit 1543304 (soft 1533304 + delta 10000)
c [simplification-14] new conflict limit 1533304 (hard 1543304)
c 
c [simplification-15] limit 1533304 conflicts (hard 1543304) hit after 1543307 conflicts
c [quatres-11] found 23934 quaternary clauses 20% in total
c [quatres-11-2] added 16 single-self-subsuming ternary resolvents
c [quatres-11-2] added 157 quaternary resolvents
c [ternres-11] limit 134254899 with penalty 0 = 0 + 0
c [ternres-11] all 25730 free variables schedulable
c [ternres-11] 429 ternary resolvents (35 bin, 394 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 4195465 penalty 4 = 4 + 0
c [card-5] found 185 at-most-one constraints of average size 3.1
c [card-5] found 95 at-most-two constraints of average size 4.0
c [card-5] using previous limit 4195465 for elimination
c [card-5] 277 out of 280 constraints (99%) meet size limits
c [card-5] no units found
c [card-5] generated 16 at-most-one constraints, 10 used 62%
c [card-5] exported 27 binary clauses, 2.7 per/constraint
c [decomp-49] removed 2 variables
c [basicprobe-4] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 13862 sched 54%, 3 failed, 0 lifted, 91 hbrs
c [decomp-50] removed 4 variables
c [basicprobe-4-1] 13860 sched 54%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-4-2] 13860 sched 54%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-2] fully completed probing
c [basicprobe-4-2] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-4-2] removed 4 variables, found 93 hbrs
c [bate-3] eliminated 2 asymmetric tautologies during probing
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 143 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 25724 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 246 blocked clauses
c [block-5] 246 < 1/100 * 192481 = 1924 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 25690 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 53 variables 0% in round 1 in 127909610 steps
c [elim-12-1] backward subsumption/strengthening limit 127909600
c [elim-12-1-1] backward checking 275 touched variables 1%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 1 clauses in 825483 steps
c [elim-12-1] rescheduled 9 variables 0% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 4563 steps
c [elim-12-2] backward subsumption/strengthening limit 4500
c [elim-12-2-1] backward checking 12 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 0 and strengthened 0 clauses in 4501 steps
c [elim-12-2] fully rescheduled 25636 variables 100%
c [elim-12-3] eliminated 6 variables 0% in round 3 in 127798461 steps
c [elim-12-3] backward subsumption/strengthening limit 127798400
c [elim-12-3-1] backward checking 26 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 0 and strengthened 0 clauses in 150073 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 60 = 0% variables out of 25690 scheduled
c [elim-12] 60 < 1/100 * 25690 = 256 considered unsuccessful
c [bca-11] limit of 10000000 steps and 384913 added (scaled 2)
c [bca-11] 36548 out of 51262 literals actually usable 71%
c [bca-11] added 43 blocked clauses in 189146 steps
c [sort-queue-15] sorted 8370 enqueued variables after 1543307 conflicts
c [score-dist-15] active 17260 (67%), one 0 (0%), zero 8370 (33%)
c [score-dist-15] max exp 541, different 36 (7%)
c [score-dist-15] median active exp 526, avg 526.2
c [simplification-15] removed 100 variables 0.4% (25630 remain 10%)
c [simplification-15] removed 423 irredundant clauses 0.2% (192106 remain 26%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 614400
c [simplification-15] conflict interval soft limit 1000000 reached
c [simplification-15] new conflict interval 1000000
c [simplification-15] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-15] hard conflict limit 3043307 (soft 2543307 + delta 500000)
c [simplification-15] new conflict limit 2543307 (hard 3043307)
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 -  500.8   25630   192106   1578961   62832  13579  2334   57    65   51  88%   1024   -1   49   58   86%
c -  514.7   25630   192106   1631755   63234  13623  2334   52    61   50  85%   1024   -9   57   51  111%
c -  527.9   25630   192106   1685871   65063  13625  2334   50    58   51  86%   1024   -6   48   50   96%
c -  542.2   25630   192106   1737158   64958  13635  2335   53    60   63  88%   1024   -2   56   51  110%
c -  558.6   25630   192106   1793208   64297  13635  2335   51    57   63  89%   1024   -2   51   51  100%
c -  577.4   25630   192106   1855744   65832  13640  2335   55    63   63  88%   1024    2   55   53  105%
c -  597.5   25630   192106   1920023   66087  13643  2335   53    57   63  92%   1024   -3   52   51  101%
c -  615.8   25630   192106   1985010   66422  13658  2335   40    70   62  57%   1024   11   15   47   32%
c -  628.3   25630   192106   2042478   67289  13867  2336   24   185   58  13%   1024   91   37   32  116%
c -  640.9   25630   192106   2101703   69343  13972  2336   35   158   57  22%   1024   16   44   31  142%
c -  654.8   25630   192106   2161643   72123  14024  2337   48    62   58  78%   1024  -59   47   37  129%
c -  671.5   25630   192106   2221528   76090  14029  2337   55    60   60  91%   1024  -26   56   45  124%
c -  689.3   25630   192106   2281851   76391  14038  2337   44    90   59  49%   1024   20   16   49   32%
c -  706.7   25630   192106   2338821   76730  14074  2337   39    76   61  51%   1024  -14   36   46   79%
c -  726.4   25630   192106   2395882   77633  14076  2337   40    72   61  56%   1024   -5   44   44  100%
c -  748.6   25630   192106   2454121   76441  14076  2339   42    71   61  60%   1024   -1   45   45   99%
c -  770.4   25630   192106   2514792   77228  14082  2341   51    66   63  78%   1024   -3   50   47  107%
c 
c [simplification-16] limit 2543307 conflicts (hard 3043307) hit after 2543308 conflicts
c [quatres-12] found 25030 quaternary clauses 19% in total
c [quatres-12-1] removed 14 duplicate quaternary clauses
c [quatres-12-1] added 2 double-self-subsuming ternary resolvents
c [quatres-12-2] added 9 single-self-subsuming ternary resolvents
c [quatres-12-2] added 41 quaternary resolvents
c [ternres-12] limit 200000000 with penalty 0 = 0 + 0
c [ternres-12] all 25630 free variables schedulable
c [ternres-12] 151 ternary resolvents (34 bin, 117 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-52] removed 2 variables
c [simpleprobe-5] all 25628 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 0 variables, found 783 hbrs, 0 units
c [unhide-11] limit 2500000 with penalty 3 = 2 + 1
c [unhide-11-17] 0 units, 0 failed, 234 tauts, 0 hbrs, 172924 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 347 transitive binary clauses
c [cce-5] limit of 313860657 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 19 (5%) of length 25
c [cce-5-1] eliminated 1 clauses out of 41 (2%) of length 24
c [cce-5-1] eliminated 3 clauses out of 39 (8%) of length 23
c [cce-5-1] eliminated 1 clauses out of 30 (3%) of length 22
c [cce-5-1] eliminated 1 clauses out of 71 (1%) of length 21
c [cce-5-1] eliminated 2 clauses out of 177 (1%) of length 20
c [cce-5-1] eliminated 3 clauses out of 140 (2%) of length 19
c [cce-5-1] eliminated 3 clauses out of 256 (1%) of length 18
c [cce-5-1] eliminated 5 clauses out of 380 (1%) of length 17
c [cce-5-1] eliminated 3 clauses out of 367 (1%) of length 16
c [cce-5-1] eliminated 18 clauses out of 465 (4%) of length 15
c [cce-5-1] eliminated 11 clauses out of 634 (2%) of length 14
c [cce-5-1] eliminated 14 clauses out of 886 (2%) of length 13
c [cce-5-1] eliminated 21 clauses out of 1208 (2%) of length 12
c [cce-5-1] eliminated 26 clauses out of 2012 (1%) of length 11
c [cce-5-1] eliminated 61 clauses out of 2668 (2%) of length 10
c [cce-5-1] eliminated 138 clauses out of 4045 (3%) of length 9
c [cce-5-1] eliminated 291 clauses out of 6477 (4%) of length 8
c [cce-5-1] eliminated 577 clauses out of 13484 (4%) of length 7
c [cce-5-1] eliminated 764 clauses out of 29476 (3%) of length 6
c [cce-5-1] eliminated 739 clauses out of 17853 (4%) of length 5
c [cce-5-1] eliminated 789 clauses out of 16692 (5%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 3472 large clauses in 168144247 steps
c [cce-5-1] allowing another 84072123 steps for small clauses
c [cce-5-1] scheduling 32289 clauses = 21874 binary + 10415 ternary
c [cce-5-1] tried to eliminate 32289 small clauses 100%
c [cce-5-1] eliminated 164 binary clauses 1%
c [cce-5-1] eliminated 440 ternary clauses 4%
c [cce-5-1] eliminated 604 small clauses 2%
c [cce-5-1] eliminated 604 small clauses in 114455742 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 4076 covered clauses in round 1
c [cce-5-2] eliminated 2 clauses out of 1187 (0%) of length 12
c [cce-5-2] eliminated 4 clauses out of 1986 (0%) of length 11
c [cce-5-2] eliminated 8 clauses out of 6186 (0%) of length 8
c [cce-5-2] eliminated 12 clauses out of 12907 (0%) of length 7
c [cce-5-2] eliminated 49 clauses out of 28712 (0%) of length 6
c [cce-5-2] eliminated 115 clauses out of 17114 (1%) of length 5
c [cce-5-2] eliminated 158 clauses out of 15903 (1%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 348 large clauses in 154192393 steps
c [cce-5-2] allowing another 77096196 steps for small clauses
c [cce-5-2] scheduling 31685 clauses = 21710 binary + 9975 ternary
c [cce-5-2] tried to eliminate 31685 small clauses 100%
c [cce-5-2] eliminated 18 binary clauses 0%
c [cce-5-2] eliminated 12 ternary clauses 0%
c [cce-5-2] eliminated 30 small clauses 0%
c [cce-5-2] eliminated 30 small clauses in 105694941 steps
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 378 covered clauses in round 2
c [cce-5-3] eliminated 3 clauses out of 2607 (0%) of length 10
c [cce-5-3] eliminated 2 clauses out of 3907 (0%) of length 9
c [cce-5-3] eliminated 4 clauses out of 12895 (0%) of length 7
c [cce-5-3] eliminated 3 clauses out of 28663 (0%) of length 6
c [cce-5-3] incomplete large round (ACCE)
c [cce-5-3] eliminated 12 large clauses in 93710099 steps
c [cce-5-3] allowing another 46855049 steps for small clauses
c [cce-5-3] scheduling 31655 clauses = 21692 binary + 9963 ternary
c [cce-5-3] tried to eliminate 31655 small clauses 100%
c [cce-5-3] eliminated 6 binary clauses 0%
c [cce-5-3] eliminated 6 small clauses 0%
c [cce-5-3] eliminated 6 small clauses in 75483155 steps
c [cce-5-3] completed small round (ACCE)
c [cce-5-3] eliminated 18 covered clauses in round 3
c [cce-5] eliminated 4472 covered clauses in TOTAL during 3 rounds
c [bca-12] limit of 10000000 steps and 375969 added (scaled 2)
c [bca-12] 36009 out of 51258 literals actually usable 70%
c [bca-12] added 14 blocked clauses in 215028 steps
c [sweep-9] limit 18831639 penalty 2 = 2 + 0
c [sweep-9-1] 1480 pos 51.5% + 1392 neg 48.5% = 2872 sched 11.2% ret 22756
c [sweep-9-1] 1964802 steps 1731 queries 483.01 avg class size
c [sweep-9-1] 19554 decisions 1728 SAT calls 15.84 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-54] removed 5 variables
c [sweep-9-1] removed 5 vars (0 failed, 3 eqs, 2 impls)
c [sweep-9-2] 10793 pos 42.1% + 14830 neg 57.9% = 25623 sched 100.0% ret 0
c [sweep-9-2] 15454451 steps 3813 queries 294.48 avg class size
c [sweep-9-2] 69856 decisions 3811 SAT calls 27.41 avg env size
c [sweep-9-2] fully completed sweeping round
c [decomp-55] removed 20 variables
c [sweep-9-2] removed 20 vars (0 failed, 6 eqs, 3 impls)
c [sweep-9-3] 10786 pos 42.1% + 14817 neg 57.9% = 25603 sched 100.0% ret 0
c [sweep-9-3] 1416185 steps 181 queries 3908.87 avg class size
c [sweep-9-3] 5262 decisions 180 SAT calls 56.45 avg env size
c [sweep-9-3] 22451 variables remain 88% (3152 retained 12%)
c [decomp-56] removed 1 variables
c [sweep-9-3] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-9] removed 26 vars in TOTAL (3 rounds, 5722 queries)
c [sort-queue-16] sorted 8134 enqueued variables after 2543308 conflicts
c [score-dist-16] active 17468 (68%), one 0 (0%), zero 8134 (32%)
c [score-dist-16] max exp 543, different 38 (7%)
c [score-dist-16] median active exp 527, avg 526.9
c [simplification-16] removed 28 variables 0.1% (25602 remain 10%)
c [simplification-16] removed 4731 irredundant clauses 2.5% (187375 remain 25%)
c [simplification-16] maximum reduction of 2% = max (0%, 2%)
c [simplification-16] geometric conflict interval increment 333333 = 1000000 / 3
c [simplification-16] conflict interval soft limit 1000000 reached
c [simplification-16] new conflict interval 1000000
c [simplification-16] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-16] hard conflict limit 4043308 (soft 3543308 + delta 500000)
c [simplification-16] new conflict limit 3543308 (hard 4043308)
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 -  802.3   25602   187375   2573974   79452  13929  2868   50    66   50  76%   1024   -4   53   48  110%
c -  825.8   25602   187375   2634376   80035  13930  2868   53    62   51  85%   1024   -4   53   51  104%
c -  849.3   25602   187375   2695956   78040  13931  2868   54    58   51  93%   1024   -5   52   52  100%
c -  874.9   25602   187375   2763615   80366  13932  2868   47    56   51  84%   1024   -4   41   52   80%
c -  895.1   25602   187375   2825617   80337  13934  2868   58    63   52  92%   1024    2   57   53  107%
c -  918.1   25602   187375   2888472   79881  13937  2868   56    62   67  90%   1024    1   58   53  110%
c -  938.3   25602   187375   2954202   78016  13937  2868   57    60   68  95%   1024   -0   58   55  105%
c -  961.4   25602   187375   3023186   79743  13937  2868   54    62   68  87%   1024    2   56   54  103%
c -  986.7   25602   187375   3092400   80309  13937  2869   53    56   67  95%   1024   -3   53   53   99%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 284 basic ate = 168 trn 59% + 116 lrg 41% in 3 updates
c bcas: 12 count, 460 added (684 skipped), 2112586 steps
c bkwd: tried 121262 clauses, 242502 lits, 2.00 lits/clause
c bkwd: checked 10447010 occs, 86.15 occs/clause, 43.08 occs/lit
c bkwd: subsumed 1 binary, 2 ternary, 1 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 81 large (0% self)
c blkd: 5 bces, 11741 removed, 7546407 resolutions, 19437438 steps
c blkd: 4040 blocking literals 1%, 1204 pure
c bump: 3113207 bumped seen, 808694966 lits 259.8 on average
c card: 5 count, 0 units, 27 am1, 15137270 steps
c card: 24 rescheduled, 143 eliminated, 21425 resolved, 5447 subsumed
c card: 523 at-most-one constraints found, average size 3.09
c card: 523 at-most-one constraints used 100%, average size 3.09
c card: 255 at-most-two constraints found, average size 4.00
c card: 248 at-most-two constraints used 97%, average size 4.00
c cces: 5 cces, 14942 eliminated, 13263 ate 89%, 1679 abce 11%
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: 2502922 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 100 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 56 decompositions, 939 equivalent 0%
c deco: 90944 decision-only clauses 3%, 62% reduction
c decs: 19930714 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 12 elims, 222902 eliminated 88%, 194 pure 0%
c elms: 24 rounds, 2.0 rounds/bve
c elms: 210235 small 94%, 11269 large 5%
c elms: 318035 tried small, 210235 succeeded 66%, 107800 failed 34%
c elms: 4666 subsumed, 5104 strengthened, 451 blocked
c elms: 12376479 copies, 21579581 resolutions, 7089770 ipos
c elms: 11751255 subchks, 10107735 strchks
c gaus: 4 extractions, 57751 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 14916770 steps, 7458385 extr 50%, 7529511 elim 50%
c glue: 50.9 orig avg, 50.9 real avg, 6.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 15022 = 2120 simple 14% + 12029 trn 80% + 873 lrg 6%, 1057 sub 7%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3113207 clauses, 104.3 length
c lrnd: 324639625 lits = 589566019 orig - 264926394 removed 45%
c lrnd: 693042 uips 22%, 1523254 flips 49%
c mins: 3017089 mins 97%, 108 bin 0%, 4980 size 0%
c mins: 534555436 poisoned searches, 80290708 hits, 15% hit rate
c mins: 1006503253 used twice searches, 86158478 hits, 9% hit rate
c move: moved 10271, 2114 bin 21%, 8157 trn 79%
c otfs: 16980 driving 36%, 30231 restarting 64%
c otfs: str 47211, 47065 red 100%, 146 irr 0%
c otfs: str 47211, 0 bin 0%, 114 trn 0%, 47097 lrg 100%
c otfs: sub 2174, 2173 red 100%, 1 irr 0%
c otfs: sub 2174, 0 bin 0%, 16 trn 1%, 2158 lrg 99%
c phas: 3 computed, 62882 set, 21908 pos (35%), 40974 neg (65%)
c prbs: 4 basic, 604301 probed, 422 failed, 45 lifted
c prbs: 5 simple, 483613 probed, 21 failed, 141 eqs
c prbs: 4 treelook, 18381 probed, 35 failed, 0 lifted
c prom: 98657 locked 1% out of 9276495 tried
c prps: 1588185056 props, 79 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 12 count, 20961 quat, 5328 self1, 36 self2, 450 dup
c queu: 16 sorted, 19930714 next (523328 steps 0.03)
c queu: 809231653 enq (1274458655 steps 1.57), 808694966 deq 100%
c redc: 3737 clauses 5%, 74113 tried 2%, 1 sat 0%
c redc: 4243 lits 1%, 809083 tried 0%, 1 sat 0%
c redc: 82 times jump level reduced, 44.2 levels on average
c reds: 58 count, 53910.7 conflicts per reduce
c reds: 0 memlim 0%, 58 arith 100%
c reds: 2276757 collected 89%, 272374 retired 11%
c rmbd: 923 removed, 505 red 55%
c rsts: 12875 restarts 94%, 798 skipped 6%
c rsts: 798 saturating 100%, 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: 16 count, 16 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 3113207 count (9568715 tried 3.1), 429258 sub out of 3111867 (13.8%)
c swps: 9 count, 14 rounds, 26128 queries (1866.3/round)
c swps: 26024 sat calls, 77 unsat (0.1% success rate)
c swps: 446906 decisions 17.2, 3368 conflicts 0.1
c swps; 645.2 avg class size, 25.6 avg environment size
c swps: 0 failed, 157 impls, 178 equivs
c swp0: 8706 type 0 queries, 597 unsat (6.9%), 8673 sat (99.6%)
c swp1: 17422 type 1 queries, 3779 unsat (21.7%), 17277 sat (99.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: 46088203 calls to obtain time
c tops: 3073 fixed 1%, 10 its, 312681.90 confs/it
c trds: 12 transitive reductions, 2014 removed, 18 failed
c trds: 684776 nodes, 328825 edges, 4440385 steps
c trim: 3259660 words, 12.4 MB
c trnr: 12 count, 763 bin, 30464 trn, 187379356 steps
c unhd: 11 count, 17 rounds, 38932588 steps
c unhd: 476 non-trivial sccs of average size 2.4
c unhd: 11 units, 11 bin, 0 trn, 0 lrg
c unhd: 62 failed, 57 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 11271 tauts, 202 bin 2%, 5697 trn 51%, 4097 lrg 36%
c unhd: 11271 tauts, 1275 stamp 11%, 6538 red 58%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 440540 str, 11 bin 0%, 1191 trn 0%, 439338 lrg 100%, 417759 red 95%
c vars: 25602 remaining 10% and 226914 removed 90% out of 252516
c vars: 3073 fixed 1%, 222902 eliminated 88%, 939 equivalent 0%
c vsts: 34463144931 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 21.8 search visits per propagation, 10990.3 per conflict
c wchs: 4817941426 pushed, 45106291 enlarged, 172 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3132828       2276757        272374     147734629      62501721       2074763
c 
c  0 0         58870   2      2304   0         0   0  65022415  44  16586063  27    219642  11     1.2
c  1 5         20066   1      4542   0     12967   5  12198431   8   4475658   7     55003   3     0.3
c  2 6         79014   3     31874   1     31940  12  19595216  13<  8645467  14    168220   8     1.1
c  3 9        172278   5     96796   4     32764  12  20782620  14  11023352  18<   216903  10     4.0
c  4 14       175337   6    127783   6     18868   7  10963987   7   6507471  10    214718  10     2.9
c  5 21       239816   8    192834   8     17347   6   5645166   4   4181862   7    232837  11<    6.9
c  6 30       187944   6    163786   7     10213   4<  3616043   2   2827021   5    194522   9     9.5
c  7 41       476178  15<   374809  16<    38550  14   3960994   3   3198354   5    316823  15    17.6
c  8 54      1308714  42    996266  44     93409  34   4552936   3   3894057   6    356579  17    33.6
c  9 69       243194   8    210203   9     11274   4    887096   1    740599   1     68403   3    16.1
c 10 86       118150   4     74030   3      3871   1    438322   0    376387   1     30760   1    23.6
c 11 126       51196   2      1411   0      1083   0     68462   0     43687   0       349   0    13.9
c 12 230        2071   0       119   0        88   0      2941   0      1743   0         4   0     1.2
c 
c avg                  6.9           7.1           5.8           1.9           2.9           4.9
c std                  2.2           1.8           2.6           2.3           2.6           2.7
c 
c  114.333  11% bump
c   25.771   3% elim
c   14.274   1% cce
c   13.204   1% decide
c   12.609   1% sweep
c   10.220   1% probe
c 
c   16.330 < 1% rest (below)
c 
c    6.907   1% unhide
c    2.135   0% quatres
c    1.873   0% block
c    1.815   0% bca
c    1.648   0% ternres
c    1.051   0% gauss
c    0.551   0% card
c    0.350   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.073   1% preprocessing     6%
c   78.372   8% inprocessing     94%
c ==================================
c   83.445   8% simplifying
c  916.206  92% search
c ==================================
c  999.655 100% all
c 
c       3126819 conflicts,        3127.9 confs/sec
c           568 ternaries,        5505.0 confs/ternary
c            65 binaries,        48104.9 confs/binary
c            10 iterations,     312681.9 confs/iteration
c 
c            58 reductions,          0.1 redus/sec,  53910.7 confs/reduction
c         12875 restarts,           12.9 rests/sec,    242.9 confs/restart
c      19930714 decisions,       19937.6 decis/sec,      6.4 decis/conflict
c    1588185056 propagations,  1588733.4 props/sec,     79.7 props/decision
c 
c 999.7 seconds, 134.6 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
