c launch: /data/cnf/sc2014/app/stable-400-0.1-5-9876543214005.cnf.bz2
c host: atom13
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/stable-400-0.1-5-9876543214005.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/stable-400-0.1-5-9876543214005.cnf.bz2
c no embedded options
c found 'p cnf 400 30584' header
c read 400 variables, 30584 clauses, 629054 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 400 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     400    30584         0       0      0     0    0     0    3   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 163 at-most-one constraints of average size 4.1
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 163 out of 163 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [simpleprobe-1] all 400 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 31 variables remain 8% (369 retained 92%)
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 2811 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 400 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] no variable eliminated in round 1 in 0 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 0 = 0% variables out of 400 scheduled
c [phase-count-1] 29407 negative 98.7% of 29807 except 400 1.3%
c [phase-count-1] 14715 positive 49.4% of 29807 except 15092 50.6%
c [phase-count-1] less non-negative clauses 400 than limit 2900 (10.0%)
c [phase-count-1] non-pos/non-neg = 15092/400 = 37.73 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 400 negative 100%
c [sort-queue-1] sorted 400 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 400 (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 0 variables 0.0% (400 remain 100%)
c [simplification-1] removed 777 irredundant clauses 2.5% (29807 remain 97%)
c [simplification-1] maximum reduction of 3% = max (0%, 3%)
c [simplification-1] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-1] new conflict interval 5000
c [simplification-1] penalized conflict interval 5000 = 1 * 5000
c [simplification-1] hard conflict limit 15000 (soft 5000 + delta 10000)
c [simplification-1] new conflict limit 5000 (hard 15000)
c 
c [simplification-2] limit 5000 conflicts (hard 15000) hit after 5001 conflicts
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 800 literals 100%
c [treelook-1] scheduling used 90302 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 484768 steps
c [treelook-1] 798 literals remain 100%
c [treelook-1] 400 variables remain to probed next time 100%
c [basicprobe-1] limit 1095375 penalty 0 = 0 + 0
c [basicprobe-1-0] 107 probes remain 27% after last round
c [block-1] scheduling all variables this time
c [block-1] scheduled 400 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 0 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 13 clauses out of 14 (93%) of length 58
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 57
c [cce-1-1] eliminated 117 clauses out of 121 (97%) of length 56
c [cce-1-1] eliminated 108 clauses out of 111 (97%) of length 55
c [cce-1-1] eliminated 129 clauses out of 133 (97%) of length 54
c [cce-1-1] eliminated 88 clauses out of 126 (70%) of length 53
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 461 large clauses in 30000113 steps
c [cce-1-1] allowing another 15000056 steps for small clauses
c [cce-1-1] scheduling 15092 clauses = 15092 binary + 0 ternary
c [cce-1-1] tried to eliminate 144 small clauses 1%
c [cce-1-1] eliminated 100 binary clauses 1%
c [cce-1-1] eliminated 100 small clauses 1%
c [cce-1-1] eliminated 100 small clauses in 30000895 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 561 covered clauses in round 1
c [cce-1] eliminated 561 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 58992 added (scaled 2)
c [bca-1] 0 out of 802 literals actually usable 0%
c [bca-1] not enough literals usable
c [bca-1] added 0 blocked clauses in 4665 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 21 pos 5.2% + 379 neg 94.8% = 400 sched 100.0% ret 0
c [sweep-1-1] 1020239 steps 25 queries 39.52 avg class size
c [sweep-1-1] 2300 decisions 23 SAT calls 397.57 avg env size
c [sweep-1-1] 63 variables remain 16% (337 retained 84%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 24 queries)
c [score-dist-2] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-2] max exp 514, different 1 (0%)
c [score-dist-2] median active exp 514, avg 514.0
c [simplification-2] removed 0 variables 0.0% (400 remain 100%)
c [simplification-2] removed 561 irredundant clauses 1.9% (29246 remain 96%)
c [simplification-2] maximum reduction of 2% = max (0%, 2%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 11666
c [simplification-2] penalized conflict interval 11666 = 1 * 11666
c [simplification-2] hard conflict limit 26667 (soft 16667 + delta 10000)
c [simplification-2] new conflict limit 16667 (hard 26667)
c 
c [simplification-3] limit 16667 conflicts (hard 26667) hit after 16667 conflicts
c [quatres-1] found 0 quaternary clauses 0% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 400 free variables schedulable
c [ternres-1] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 68 at-most-one constraints of average size 4.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 68 out of 68 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-2] 31 schedulable variables 8%
c [simpleprobe-2] limit 1599755 penalty 1 = 1 + 0
c [simpleprobe-2] 31 variables remain 8% (369 retained 92%)
c [unhide-2] limit 79987 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 0 tauts, 0 hbrs, 12818 literals
c [transred-1] limit 799877 with penalty 0 = 0 + 0
c [transred-1] removed 0 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 30 clauses out of 33 (91%) of length 53
c [cce-2-1] eliminated 97 clauses out of 100 (97%) of length 52
c [cce-2-1] eliminated 227 clauses out of 236 (96%) of length 51
c [cce-2-1] eliminated 169 clauses out of 268 (63%) of length 50
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 523 large clauses in 30000910 steps
c [cce-2-1] allowing another 15000455 steps for small clauses
c [cce-2-1] scheduling 14992 clauses = 14992 binary + 0 ternary
c [cce-2-1] tried to eliminate 141 small clauses 1%
c [cce-2-1] eliminated 87 binary clauses 1%
c [cce-2-1] eliminated 87 small clauses 1%
c [cce-2-1] eliminated 87 small clauses in 30000096 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 610 covered clauses in round 1
c [cce-2] eliminated 610 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 400 variables 100%
c [elim-2] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] no variable eliminated in round 1 in 0 steps
c [elim-2] fully completed in 1 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 0 = 0% variables out of 400 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4 pos 6.3% + 59 neg 93.7% = 63 sched 15.8% ret 337
c [sweep-2-1] 1027328 steps 18 queries 6.67 avg class size
c [sweep-2-1] 1700 decisions 17 SAT calls 386.41 avg env size
c [sweep-2-1] 7 variables remain 2% (393 retained 98%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 17 queries)
c [score-dist-3] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-3] max exp 515, different 1 (0%)
c [score-dist-3] median active exp 515, avg 515.0
c [simplification-3] removed 0 variables 0.0% (400 remain 100%)
c [simplification-3] removed 610 irredundant clauses 2.1% (28636 remain 94%)
c [simplification-3] maximum reduction of 2% = max (0%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 18332
c [simplification-3] penalized conflict interval 18332 = 1 * 18332
c [simplification-3] hard conflict limit 44999 (soft 34999 + delta 10000)
c [simplification-3] new conflict limit 34999 (hard 44999)
c 
c [simplification-4] limit 34999 conflicts (hard 44999) hit after 35000 conflicts
c [block-2] scheduling all variables this time
c [block-2] scheduled 400 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 87 clauses out of 97 (90%) of length 50
c [cce-3-1] eliminated 277 clauses out of 288 (96%) of length 49
c [cce-3-1] eliminated 156 clauses out of 441 (35%) of length 48
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 520 large clauses in 30000890 steps
c [cce-3-1] allowing another 15000445 steps for small clauses
c [cce-3-1] scheduling 14905 clauses = 14905 binary + 0 ternary
c [cce-3-1] tried to eliminate 145 small clauses 1%
c [cce-3-1] eliminated 82 binary clauses 1%
c [cce-3-1] eliminated 82 small clauses 1%
c [cce-3-1] eliminated 82 small clauses in 30000334 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 602 covered clauses in round 1
c [cce-3] eliminated 602 covered clauses in TOTAL during 1 rounds
c [bca-2] limit of 10000000 steps and 56568 added (scaled 2)
c [bca-2] 0 out of 802 literals actually usable 0%
c [bca-2] not enough literals usable
c [bca-2] added 0 blocked clauses in 32365 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 0 pos 0.0% + 7 neg 100.0% = 7 sched 1.8% ret 393
c [sweep-3-1] 599964 steps 6 queries 3.00 avg class size
c [sweep-3-1] 500 decisions 5 SAT calls 398.00 avg env size
c [sweep-3-1] fully completed sweeping round
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3-2] 18 pos 4.5% + 382 neg 95.5% = 400 sched 100.0% ret 0
c [sweep-3-2] 475156 steps 5 queries 131.20 avg class size
c [sweep-3-2] 400 decisions 4 SAT calls 398.00 avg env size
c [sweep-3-2] 386 variables remain 96% (14 retained 4%)
c [sweep-3-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (2 rounds, 9 queries)
c [score-dist-4] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-4] max exp 517, different 1 (0%)
c [score-dist-4] median active exp 517, avg 517.0
c [simplification-4] removed 0 variables 0.0% (400 remain 100%)
c [simplification-4] removed 602 irredundant clauses 2.1% (28034 remain 92%)
c [simplification-4] maximum reduction of 2% = max (0%, 2%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 24998
c [simplification-4] penalized conflict interval 24998 = 1 * 24998
c [simplification-4] hard conflict limit 72497 (soft 59998 + delta 12499)
c [simplification-4] new conflict limit 59998 (hard 72497)
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 -   22.8     400    28034     54496   13375      0   269   63   113   13  56%    571   53   61   34  181%
c 
c [simplification-5] limit 59998 conflicts (hard 72497) hit after 59998 conflicts
c [quatres-2] found 0 quaternary clauses 0% in total
c [ternres-2] limit 2128598 with penalty 1 = 1 + 0
c [ternres-2] all 400 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-2] limit 212859 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 800 literals 100%
c [treelook-2] scheduling used 123642 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 212859 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 374010 steps
c [treelook-2] 798 literals remain 100%
c [treelook-2] 400 variables remain to probed next time 100%
c [transred-2] limit 1000000 with penalty 1 = 1 + 0
c [transred-2] removed 0 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 244 clauses out of 269 (91%) of length 48
c [cce-4-1] eliminated 501 clauses out of 524 (96%) of length 47
c [cce-4-1] eliminated 504 clauses out of 540 (93%) of length 46
c [cce-4-1] eliminated 547 clauses out of 582 (94%) of length 45
c [cce-4-1] eliminated 547 clauses out of 577 (95%) of length 44
c [cce-4-1] eliminated 677 clauses out of 709 (95%) of length 43
c [cce-4-1] eliminated 763 clauses out of 815 (94%) of length 42
c [cce-4-1] eliminated 813 clauses out of 853 (95%) of length 41
c [cce-4-1] eliminated 775 clauses out of 818 (95%) of length 40
c [cce-4-1] eliminated 827 clauses out of 871 (95%) of length 39
c [cce-4-1] eliminated 855 clauses out of 895 (96%) of length 38
c [cce-4-1] eliminated 685 clauses out of 726 (94%) of length 37
c [cce-4-1] eliminated 773 clauses out of 828 (93%) of length 36
c [cce-4-1] eliminated 664 clauses out of 701 (95%) of length 35
c [cce-4-1] eliminated 638 clauses out of 673 (95%) of length 34
c [cce-4-1] eliminated 528 clauses out of 562 (94%) of length 33
c [cce-4-1] eliminated 300 clauses out of 465 (65%) of length 32
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 10641 large clauses in 300000030 steps
c [cce-4-1] allowing another 150000015 steps for small clauses
c [cce-4-1] scheduling 14823 clauses = 14823 binary + 0 ternary
c [cce-4-1] tried to eliminate 5680 small clauses 38%
c [cce-4-1] eliminated 523 binary clauses 4%
c [cce-4-1] eliminated 523 small clauses 4%
c [cce-4-1] eliminated 523 small clauses in 300000231 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 11164 covered clauses in round 1
c [cce-4] eliminated 11164 covered clauses in TOTAL during 1 rounds
c [score-dist-5] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-5] max exp 517, different 1 (0%)
c [score-dist-5] median active exp 517, avg 517.0
c [simplification-5] removed 0 variables 0.0% (400 remain 100%)
c [simplification-5] removed 11164 irredundant clauses 39.8% (16870 remain 55%)
c [simplification-5] maximum reduction of 40% = max (0%, 40%)
c [simplification-5] geometric conflict interval increment 609 = 24998 / 41
c [simplification-5] new conflict interval 25607
c [simplification-5] penalized conflict interval 25607 = 1 * 25607
c [simplification-5] hard conflict limit 98408 (soft 85605 + delta 12803)
c [simplification-5] new conflict limit 85605 (hard 98408)
c 
c [simplification-6] limit 85605 conflicts (hard 98408) hit after 85605 conflicts
c [card-3] limit 706152 penalty 2 = 2 + 0
c [card-3] found 38 at-most-one constraints of average size 4.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 706152 for elimination
c [card-3] 38 out of 38 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-3] limit 282460 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 0 tauts, 0 hbrs, 22418 literals
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 86 clauses out of 133 (65%) of length 32
c [cce-5-1] eliminated 233 clauses out of 333 (70%) of length 31
c [cce-5-1] eliminated 215 clauses out of 327 (66%) of length 30
c [cce-5-1] eliminated 184 clauses out of 274 (67%) of length 29
c [cce-5-1] eliminated 143 clauses out of 222 (64%) of length 28
c [cce-5-1] eliminated 119 clauses out of 177 (67%) of length 27
c [cce-5-1] eliminated 80 clauses out of 139 (58%) of length 26
c [cce-5-1] eliminated 54 clauses out of 105 (51%) of length 25
c [cce-5-1] eliminated 30 clauses out of 56 (54%) of length 24
c [cce-5-1] eliminated 7 clauses out of 52 (13%) of length 23
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1151 large clauses in 30000003 steps
c [cce-5-1] allowing another 15000001 steps for small clauses
c [cce-5-1] scheduling 14300 clauses = 14300 binary + 0 ternary
c [cce-5-1] tried to eliminate 956 small clauses 7%
c [cce-5-1] eliminated 7 binary clauses 0%
c [cce-5-1] eliminated 7 small clauses 0%
c [cce-5-1] eliminated 7 small clauses in 30000132 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1158 covered clauses in round 1
c [cce-5] eliminated 1158 covered clauses in TOTAL during 1 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 400 variables 100%
c [elim-3] limit of 28246088 steps penalty 2 = 2 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 0 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 0 = 0% variables out of 400 scheduled
c [sweep-4] limit 847382 penalty 1 = 1 + 0
c [sweep-4-1] 14 pos 3.6% + 372 neg 96.4% = 386 sched 96.5% ret 14
c [sweep-4-1] 996413 steps 10 queries 69.80 avg class size
c [sweep-4-1] 900 decisions 9 SAT calls 398.00 avg env size
c [sweep-4-1] 294 variables remain 74% (106 retained 26%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 9 queries)
c [score-dist-6] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-6] max exp 518, different 1 (0%)
c [score-dist-6] median active exp 518, avg 518.0
c [simplification-6] removed 0 variables 0.0% (400 remain 100%)
c [simplification-6] removed 1158 irredundant clauses 6.9% (15712 remain 51%)
c [simplification-6] maximum reduction of 7% = max (0%, 7%)
c [simplification-6] geometric conflict interval increment 3200 = 25607 / 8
c [simplification-6] new conflict interval 28807
c [simplification-6] penalized conflict interval 28807 = 1 * 28807
c [simplification-6] hard conflict limit 128815 (soft 114412 + delta 14403)
c [simplification-6] new conflict limit 114412 (hard 128815)
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 -   36.6     400    15712     96914   21117      0   799   37    60   13  62%    787  -22   34   44   77%
c 
c [simplification-7] limit 114412 conflicts (hard 128815) hit after 128816 conflicts
c [basicprobe-2] limit 20797293 penalty 1 = 1 + 0
c [basicprobe-2-0] 107 sched 27%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-0] fully completed probing
c [block-3] scheduling all variables this time
c [block-3] scheduled 400 variables 100%
c [block-3] limit of 20797293 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-6] limit of 41594586 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 53 (2%) of length 25
c [cce-6-1] eliminated 19 clauses out of 43 (44%) of length 23
c [cce-6-1] eliminated 18 clauses out of 30 (60%) of length 22
c [cce-6-1] eliminated 17 clauses out of 23 (74%) of length 21
c [cce-6-1] eliminated 12 clauses out of 18 (67%) of length 20
c [cce-6-1] eliminated 10 clauses out of 15 (67%) of length 19
c [cce-6-1] eliminated 8 clauses out of 12 (67%) of length 18
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 17
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 16
c [cce-6-1] eliminated 3 clauses out of 7 (43%) of length 15
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 14
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 13
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 102 large clauses in 15984015 steps
c [cce-6-1] allowing another 7992007 steps for small clauses
c [cce-6-1] scheduling 14293 clauses = 14293 binary + 0 ternary
c [cce-6-1] tried to eliminate 2233 small clauses 16%
c [cce-6-1] eliminated 12 binary clauses 0%
c [cce-6-1] eliminated 12 small clauses 0%
c [cce-6-1] eliminated 12 small clauses in 41594611 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 114 covered clauses in round 1
c [cce-6] eliminated 114 covered clauses in TOTAL during 1 rounds
c [cce-6] 114 < 1/100 * 15712 = 157 considered unsuccessful
c [bca-3] limit of 10000000 steps and 31696 added (scaled 2)
c [bca-3] 0 out of 802 literals actually usable 0%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 50203 steps
c [score-dist-7] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-7] max exp 518, different 1 (0%)
c [score-dist-7] median active exp 518, avg 518.0
c [simplification-7] removed 0 variables 0.0% (400 remain 100%)
c [simplification-7] removed 114 irredundant clauses 0.7% (15598 remain 51%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 14403 = 28807 / 2
c [simplification-7] new conflict interval 43210
c [simplification-7] penalized conflict interval 43210 = 1 * 43210
c [simplification-7] hard conflict limit 193631 (soft 172026 + delta 21605)
c [simplification-7] new conflict limit 172026 (hard 193631)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   45.5     400    15598    130844   24164      0   811   42    71   13  59%    883    3   70   39  179%
c -   53.8     400    15598    163328   21174      0   811   61   107   12  57%    938   28   51   47  108%
c 
c [simplification-8] limit 172026 conflicts (hard 193631) hit after 177888 conflicts
c [quatres-3] found 0 quaternary clauses 0% in total
c [ternres-3] limit 2790795 with penalty 2 = 2 + 0
c [ternres-3] all 400 free variables schedulable
c [ternres-3] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 558159 penalty 2 = 2 + 0
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-3] limit 500000 with penalty 2 = 2 + 0
c [transred-3] removed 0 transitive binary clauses
c [score-dist-8] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-8] max exp 519, different 1 (0%)
c [score-dist-8] median active exp 519, avg 519.0
c [simplification-8] removed 0 variables 0.0% (400 remain 100%)
c [simplification-8] removed 0 irredundant clauses 0.0% (15598 remain 51%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 43210
c [simplification-8] new conflict interval 86420
c [simplification-8] penalized conflict interval 86420 = 1 * 86420
c [simplification-8] hard conflict limit 307518 (soft 264308 + delta 43210)
c [simplification-8] new conflict limit 264308 (hard 307518)
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 -   62.1     400    15598    200000   22653      0   811   55    93   12  59%    975   14   30   47   63%
c -   70.9     400    15598    237009   24220      0   811   34    48   10  70%    996  -22   33   42   79%
c 
c [simplification-9] limit 264308 conflicts (hard 307518) hit after 264308 conflicts
c [cce-7] limit of 41212654 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 1 clauses out of 82 (1%) of length 30
c [cce-7-1] eliminated 1 clauses out of 80 (1%) of length 29
c [cce-7-1] eliminated 1 clauses out of 92 (1%) of length 28
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 3 large clauses in 14502528 steps
c [cce-7-1] allowing another 7251264 steps for small clauses
c [cce-7-1] scheduling 14281 clauses = 14281 binary + 0 ternary
c [cce-7-1] tried to eliminate 2296 small clauses 16%
c [cce-7-1] eliminated 14 binary clauses 0%
c [cce-7-1] eliminated 14 small clauses 0%
c [cce-7-1] eliminated 14 small clauses in 41212745 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 17 covered clauses in round 1
c [cce-7] eliminated 17 covered clauses in TOTAL during 1 rounds
c [cce-7] 17 < 1/100 * 15598 = 155 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 12363795 penalty 2 = 2 + 0
c [sweep-5-1] 13 pos 4.4% + 281 neg 95.6% = 294 sched 73.5% ret 106
c [sweep-5-1] 2493011 steps 32 queries 20.53 avg class size
c [sweep-5-1] 3100 decisions 31 SAT calls 397.71 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 17 pos 4.2% + 383 neg 95.8% = 400 sched 100.0% ret 0
c [sweep-5-2] 2957419 steps 36 queries 25.58 avg class size
c [sweep-5-2] 3500 decisions 35 SAT calls 397.83 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-3] 17 pos 4.2% + 383 neg 95.8% = 400 sched 100.0% ret 0
c [sweep-5-3] 2840279 steps 39 queries 22.26 avg class size
c [sweep-5-3] 3800 decisions 38 SAT calls 397.71 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 104 queries)
c [score-dist-9] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-9] max exp 519, different 1 (0%)
c [score-dist-9] median active exp 519, avg 519.0
c [simplification-9] removed 0 variables 0.0% (400 remain 100%)
c [simplification-9] removed 17 irredundant clauses 0.1% (15581 remain 51%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 86420
c [simplification-9] new conflict interval 172840
c [simplification-9] penalized conflict interval 172840 = 1 * 172840
c [simplification-9] hard conflict limit 523568 (soft 437148 + delta 86420)
c [simplification-9] new conflict limit 437148 (hard 523568)
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.6     400    15581    272372   23791      0   825   68   118   13  58%   1008   43   72   47  155%
c -   88.4     400    15581    309290   25787      0   825   36    57   11  63%   1015  -13   35   43   82%
c -   96.9     400    15581    345613   25073      0   825   66   115   13  58%   1019   37   67   49  136%
c -  105.2     400    15581    383526   25697      0   825   39    61   13  64%   1021  -21   37   48   77%
c -  112.9     400    15581    421678   26688      0   825   30    48   14  64%   1022  -26   27   44   61%
c 
c [simplification-10] limit 437148 conflicts (hard 523568) hit after 442649 conflicts
c [card-4] limit 1689384 penalty 3 = 3 + 0
c [card-4] found 110 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1689384 for elimination
c [card-4] 110 out of 110 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [simpleprobe-3] 31 schedulable variables 8%
c [simpleprobe-3] limit 27030146 penalty 2 = 2 + 0
c [simpleprobe-3] fully completed simple probing
c [unhide-4] limit 675753 with penalty 3 = 3 + 0
c [unhide-4-5] 0 units, 0 failed, 0 tauts, 0 hbrs, 34735 literals
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 400 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1351507320 steps penalty 3 = 3 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 2430028 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 400 scheduled
c [score-dist-10] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-10] max exp 520, different 1 (0%)
c [score-dist-10] median active exp 520, avg 520.0
c [simplification-10] removed 0 variables 0.0% (400 remain 100%)
c [simplification-10] removed 0 irredundant clauses 0.0% (15581 remain 51%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 172840
c [simplification-10] new conflict interval 345680
c [simplification-10] penalized conflict interval 345680 = 1 * 345680
c [simplification-10] hard conflict limit 961169 (soft 788329 + delta 172840)
c [simplification-10] new conflict limit 788329 (hard 961169)
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 -  122.2     400    15581    459984   27541      0   825   27    42   13  66%   1023  -22   23   39   58%
c -  131.7     400    15581    499118   27313      0   825   70   121   14  58%   1023   56   72   42  171%
c -  140.5     400    15581    539175   27933      0   825   58    96   11  61%   1024   30   71   42  168%
c -  150.0     400    15581    580104   28047      0   825   27    41   11  67%   1024  -31   26   43   60%
c -  160.5     400    15581    621907   29192      0   825   65   107   11  61%   1024   44   60   41  146%
c -  170.1     400    15581    663043   29311      0   825   40    64   14  64%   1024  -12   43   46   94%
c -  180.2     400    15581    705026   30196      0   825   29    44   15  65%   1024  -25   26   42   62%
c -  190.0     400    15581    747362   30443      0   825   39    62   12  62%   1024  -12   38   45   85%
c -  200.4     400    15581    790701   30882      0   825   39    64   15  62%   1024  -14   42   47   88%
c -  213.0     400    15581    834625   31919      0   825   34    52   15  66%   1024  -14   39   41   94%
c 
c [simplification-11] limit 788329 conflicts (hard 961169) hit after 871823 conflicts
c [block-4] scheduling all variables this time
c [block-4] scheduled 400 variables 100%
c [block-4] limit of 69918620 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [bca-4] limit of 10000000 steps and 31662 added (scaled 2)
c [bca-4] 0 out of 802 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 64992 steps
c [score-dist-11] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-11] max exp 521, different 1 (0%)
c [score-dist-11] median active exp 521, avg 521.0
c [simplification-11] removed 0 variables 0.0% (400 remain 100%)
c [simplification-11] removed 0 irredundant clauses 0.0% (15581 remain 51%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 345680
c [simplification-11] new conflict interval 691360
c [simplification-11] penalized conflict interval 691360 = 1 * 691360
c [simplification-11] hard conflict limit 1908863 (soft 1563183 + delta 345680)
c [simplification-11] new conflict limit 1563183 (hard 1908863)
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 -  225.5     400    15581    878745   31879      0   825   67   111   11  60%   1024   50   70   41  171%
c -  236.4     400    15581    924441   31473      0   825   65   107   15  61%   1024   32   66   48  139%
c -  248.1     400    15581    971461   32470      0   825   41    60   16  68%   1024  -14   39   46   84%
c -  258.8     400    15581   1017657   32950      0   825   45    68   12  66%   1024   -4   42   46   91%
c -  269.6     400    15581   1064056   33913      0   825   41    62   16  67%   1024   -6   38   44   87%
c -  281.2     400    15581   1111283   34476      0   825   38    59   16  65%   1024   -3   36   40   91%
c -  294.5     400    15581   1159041   33908      0   825   44    68   13  64%   1024   -7   41   47   86%
c -  308.3     400    15581   1207941   35353      0   825   39    60   16  64%   1024  -10   30   44   68%
c -  321.9     400    15581   1257308   35278      0   825   66   107   17  62%   1024   33  100   48  209%
c -  335.2     400    15581   1307590   35800      0   825   41    64   17  64%   1024  -13   36   48   75%
c -  350.3     400    15581   1357392   36178      0   825   60    99   17  61%   1024   26   56   46  121%
c -  365.0     400    15581   1409054   36384      0   825   38    59   17  65%   1024  -14   36   46   78%
c -  378.9     400    15581   1461404   36608      0   825   52    83   13  63%   1024    9   40   47   85%
c -  394.7     400    15581   1514520   37529      0   825   30    45   14  67%   1024  -20   30   41   72%
c -  412.0     400    15581   1568286   38463      0   825   26    38   17  68%   1024  -14   23   33   68%
c 
c [simplification-12] limit 1563183 conflicts (hard 1908863) hit after 1575724 conflicts
c [quatres-4] found 0 quaternary clauses 0% in total
c [ternres-4] limit 13753707 with penalty 3 = 3 + 0
c [ternres-4] all 400 free variables schedulable
c [ternres-4] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-4] limit 2750741 penalty 3 = 3 + 0
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-4] limit 250000 with penalty 3 = 3 + 0
c [transred-4] removed 0 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 1375370727 steps penalty 2 = 2 + 0
c [cce-8-1] completed large round (ATE)
c [cce-8-1] allowing another 6676144 steps for small clauses
c [cce-8-1] scheduling 14267 clauses = 14267 binary + 0 ternary
c [cce-8-1] tried to eliminate 14267 small clauses 100%
c [cce-8-1] eliminated 63 binary clauses 0%
c [cce-8-1] eliminated 63 small clauses 0%
c [cce-8-1] eliminated 63 small clauses in 208185013 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] completed small and large (ATE)
c [cce-8-1] eliminated 63 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 6584508 steps for small clauses
c [cce-8-2] scheduling 14204 clauses = 14204 binary + 0 ternary
c [cce-8-2] tried to eliminate 14204 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 63 covered clauses in TOTAL during 2 rounds
c [cce-8] 63 < 1/100 * 15581 = 155 considered unsuccessful
c [score-dist-12] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-12] max exp 522, different 1 (0%)
c [score-dist-12] median active exp 522, avg 522.0
c [simplification-12] removed 0 variables 0.0% (400 remain 100%)
c [simplification-12] removed 63 irredundant clauses 0.4% (15518 remain 51%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 691360
c [simplification-12] conflict interval soft limit 1000000 reached
c [simplification-12] new conflict interval 1000000
c [simplification-12] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-12] hard conflict limit 3075724 (soft 2575724 + delta 500000)
c [simplification-12] new conflict limit 2575724 (hard 3075724)
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 -  429.3     400    15518   1622907   38475      0   888   20    28   14  72%   1024  -30   24   36   66%
c -  445.5     400    15518   1678191   39275      0   888   60    98   18  61%   1024   51   72   33  217%
c -  462.3     400    15518   1733429   39117      0   888   58    94   18  62%   1024   36   71   38  185%
c -  479.0     400    15518   1790180   39265      0   888   50    79   18  63%   1024   20   88   39  228%
c -  497.2     400    15518   1847881   39071      0   888   57    90   14  63%   1024   14   69   49  142%
c -  516.2     400    15518   1906716   40125      0   888   58    92   14  63%   1024   16   56   49  115%
c -  532.9     400    15518   1965174   41011      0   888   30    43   18  68%   1024  -30   26   46   56%
c -  552.5     400    15518   2024454   41156      0   888   72   117   19  62%   1024   43   72   48  148%
c -  572.1     400    15518   2083954   42136      0   888   39    60   19  65%   1024   -9   39   44   89%
c -  589.6     400    15518   2143874   42810      0   888   29    41   15  70%   1024  -10   27   33   80%
c -  610.9     400    15518   2205160   42026      0   888   39    56   15  70%   1024  -17   36   46   79%
c -  634.1     400    15518   2269056   44241      0   888   28    41   20  69%   1024  -14   34   37   94%
c -  651.8     400    15518   2329824   44080      0   888   25    37   20  68%   1024  -20   25   37   69%
c -  672.5     400    15518   2391908   44005      0   888   41    64   20  64%   1024  -13   38   48   78%
c -  692.5     400    15518   2454788   45623      0   888   40    62   16  65%   1024   -4   48   42  112%
c -  711.0     400    15518   2517046   44582      0   888   56    88   20  64%   1024   17   76   46  165%
c -  735.4     400    15518   2582798   45446      0   888   35    50   21  71%   1024  -15   36   42   85%
c -  760.7     400    15518   2648944   46602      0   888   31    47   21  67%   1024   -6   35   35   99%
c 
c [simplification-13] limit 2575724 conflicts (hard 3075724) hit after 2667359 conflicts
c [treelook-3] limit 5237506 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 800 literals 100%
c [treelook-3] scheduling used 218465 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 5237506 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 5256459 steps
c [treelook-3] 632 literals remain 79%
c [treelook-3] 400 variables remain to probed next time 100%
c [sweep-6] limit 7856260 penalty 3 = 3 + 0
c [sweep-6-1] 14 pos 3.5% + 386 neg 96.5% = 400 sched 100.0% ret 0
c [sweep-6-1] 2957651 steps 31 queries 21.81 avg class size
c [sweep-6-1] 3000 decisions 30 SAT calls 397.70 avg env size
c [sweep-6-1] fully completed sweeping round
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6-2] 14 pos 3.5% + 386 neg 96.5% = 400 sched 100.0% ret 0
c [sweep-6-2] 4546308 steps 40 queries 22.30 avg class size
c [sweep-6-2] 3900 decisions 39 SAT calls 396.54 avg env size
c [sweep-6-2] fully completed sweeping round
c [sweep-6-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6-3] 14 pos 3.5% + 386 neg 96.5% = 400 sched 100.0% ret 0
c [sweep-6-3] 358063 steps 7 queries 89.86 avg class size
c [sweep-6-3] 600 decisions 6 SAT calls 397.33 avg env size
c [sweep-6-3] 372 variables remain 93% (28 retained 7%)
c [sweep-6-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (3 rounds, 75 queries)
c [score-dist-13] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-13] max exp 523, different 1 (0%)
c [score-dist-13] median active exp 523, avg 523.0
c [simplification-13] removed 0 variables 0.0% (400 remain 100%)
c [simplification-13] removed 0 irredundant clauses 0.0% (15518 remain 51%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 1000000
c [simplification-13] new conflict interval 2000000
c [simplification-13] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-13] hard conflict limit 5667359 (soft 4667359 + delta 1000000)
c [simplification-13] new conflict limit 4667359 (hard 5667359)
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 -  786.8     400    15518   2714282   46326      0   888   52    81   21  64%   1024    3   51   50  102%
c -  808.8     400    15518   2780348   46696      0   888   50    74   16  67%   1024   -8   49   52   94%
c -  830.3     400    15518   2847631   47683      0   888   52    80   21  65%   1024    3   50   50  100%
c -  853.2     400    15518   2914725   47629      0   888   41    64   16  63%   1024   -7   30   46   66%
c -  878.2     400    15518   2983024   47898      0   888   51    78   16  66%   1024   -6   63   53  118%
c -  900.5     400    15518   3051945   48964      0   888   43    66   17  65%   1024   -6   41   46   89%
c -  924.9     400    15518   3121562   48710      0   888   66   105   17  62%   1024   28   47   51   93%
c -  952.5     400    15518   3191709   50075      0   888   34    50   22  67%   1024  -13   32   41   79%
c -  982.3     400    15518   3263058   49789      0   888   76   122   22  63%   1024   55   69   46  150%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 4 count, 0 added (0 skipped), 152225 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 4 bces, 0 removed, 1475116 resolutions, 4203302 steps
c blkd: 3 blocking literals 0%, 0 pure
c bump: 3259998 bumped seen, 505685727 lits 155.1 on average
c card: 4 count, 0 units, 0 am1, 11893095 steps
c card: 25 rescheduled, 74 eliminated, 95704 resolved, 68 subsumed
c card: 379 at-most-one constraints found, average size 4.12
c card: 379 at-most-one constraints used 100%, average size 4.12
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, 14288 eliminated, 14286 ate 100%, 2 abce 0%
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: 659638 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 40 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 27 decompositions, 0 equivalent 0%
c deco: 72621 decision-only clauses 2%, 43% reduction
c decs: 5566493 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 4 elims, 0 eliminated 0%, 0 pure 0%
c elms: 4 rounds, 1.0 rounds/bve
c elms: 0 small 0%, 0 large 0%
c elms: 0 tried small, 0 succeeded 0%, 0 failed 0%
c elms: 0 subsumed, 163 strengthened, 0 blocked
c elms: 16010 copies, 17744 resolutions, 0 ipos
c elms: 128828 subchks, 57230 strchks
c gaus: 4 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12841344 steps, 6420672 extr 50%, 0 elim 0%
c glue: 44.6 orig avg, 44.6 real avg, 6.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 0 = 0 simple 0% + 0 trn 0% + 0 lrg 0%, 0 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3259998 clauses, 100.7 length
c lrnd: 328191550 lits = 462486095 orig - 134294545 removed 29%
c lrnd: 750434 uips 23%, 2136165 flips 66%
c mins: 3185192 mins 98%, 0 bin 0%, 1729 size 0%
c mins: 83649017 poisoned searches, 47190066 hits, 56% hit rate
c mins: 479306438 used twice searches, 116508323 hits, 24% hit rate
c move: moved 888, 888 bin 100%, 0 trn 0%
c otfs: 59513 driving 22%, 211031 restarting 78%
c otfs: str 270544, 255836 red 95%, 14708 irr 5%
c otfs: str 270544, 0 bin 0%, 0 trn 0%, 270544 lrg 100%
c otfs: sub 82, 82 red 100%, 0 irr 0%
c otfs: sub 82, 0 bin 0%, 0 trn 0%, 82 lrg 100%
c phas: 1 computed, 400 set, 0 pos (0%), 400 neg (100%)
c prbs: 2 basic, 800 probed, 0 failed, 0 lifted
c prbs: 3 simple, 840 probed, 0 failed, 0 eqs
c prbs: 3 treelook, 172 probed, 0 failed, 0 lifted
c prom: 203587 locked 13% out of 1570078 tried
c prps: 100247633 props, 18 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 4 count, 0 quat, 0 self1, 0 self2, 0 dup
c queu: 1 sorted, 5566493 next (8 steps 0.00)
c queu: 505686527 enq (1101620372 steps 2.18), 505685727 deq 100%
c redc: 782 clauses 95%, 823 tried 0%, 0 sat 0%
c redc: 2579 lits 14%, 17787 tried 0%, 0 sat 0%
c redc: 30 times jump level reduced, 2.0 levels on average
c reds: 63 count, 52655.5 conflicts per reduce
c reds: 0 memlim 0%, 63 arith 100%
c reds: 2551602 collected 90%, 291354 retired 10%
c rmbd: 777 removed, 0 red 0%
c rsts: 8405 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: 13 count, 13 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 3259998 count (2583946 tried 0.8), 319399 sub out of 3259998 (9.8%)
c swps: 6 count, 11 rounds, 238 queries (21.6/round)
c swps: 237 sat calls, 0 unsat (9.3% success rate)
c swps: 23700 decisions 100.0, 2214 conflicts 9.3
c swps; 29.9 avg class size, 396.7 avg environment size
c swps: 0 failed, 0 impls, 0 equivs
c swp0: 76 type 0 queries, 0 unsat (0.0%), 76 sat (100.0%)
c swp1: 162 type 1 queries, 1 unsat (0.6%), 162 sat (100.0%)
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: 17653208 calls to obtain time
c tops: 0 fixed 0%, 0 its, 0.00 confs/it
c trds: 4 transitive reductions, 0 removed, 0 failed
c trds: 1698 nodes, 33739 edges, 2549943 steps
c trim: 3443792 words, 13.1 MB
c trnr: 4 count, 0 bin, 0 trn, 408462 steps
c unhd: 4 count, 5 rounds, 2430243 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 0 tauts, 0 bin 0%, 0 trn 0%, 0 lrg 0%
c unhd: 0 tauts, 0 stamp 0%, 0 red 0%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 72782 str, 0 bin 0%, 0 trn 0%, 72782 lrg 100%, 67308 red 92%
c vars: 400 remaining 100% and 0 removed 0% out of 400
c vars: 0 fixed 0%, 0 eliminated 0%, 0 equivalent 0%
c vsts: 27520232266 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 274.7 search visits per propagation, 8289.0 per conflict
c wchs: 20137518172 pushed, 2554996 enlarged, 1017 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3259998       2551602        291354      49183081      17994340       2254443
c 
c  0 0            64   0        29   0         0   0     18783   0      5758   0       589   0     0.0
c  1 5           404   0       171   0       142   0     90294   0     28343   0      2635   0     0.0
c  2 6         12216   0      7030   0      3150   1   2203904   4    696853   4     87247   4     0.4
c  3 9        129435   4     84314   3     27331   9  18059379  37   5824901  32    776040  34     3.8
c  4 14       382324  12    294525  12     57746  20  18722974  38<  6219532  35<   846692  38<    7.3
c  5 21       578999  18    495093  19     56750  19   6186225  13   2453561  14    322557  14     8.3
c  6 30       660473  20<   559757  22<    48179  17<  1621372   3   1014318   6    103373   5     9.3
c  7 41       613826  19    494806  19     34563  12    967568   2    741846   4     51736   2     8.2
c  8 54       418117  13    317849  12     22293   8    628367   1    490812   3     30747   1     7.6
c  9 69       195753   6    147207   6     14413   5    293254   1    225378   1     14621   1     4.5
c 10 86       181262   6    109619   4     18186   6    264648   1    198210   1     12171   1     4.3
c 11 126       87105   3     41183   2      8601   3    126263   0     94729   1      5996   0     2.5
c 12 230          20   0        19   0         0   0        50   0        99   0        39   0     0.0
c 
c avg                  6.4           6.3           5.9           3.9           4.2           4.0
c std                  1.9           1.8           2.1           1.3           1.6           1.3
c 
c   52.824   5% bump
c    5.826   1% cce
c    3.549   0% decide
c 
c    5.879 < 1% rest (below)
c 
c    2.067   0% sweep
c    1.602   0% probe
c    1.526   0% unhide
c    1.299   0% block
c    0.589   0% card
c    0.356   0% transred
c    0.255   0% elim
c    0.189   0% gauss
c    0.054   0% bca
c    0.006   0% quatres
c    0.001   0% ternres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.795   0% preprocessing     5%
c   14.124   1% inprocessing     95%
c ==================================
c   14.919   1% simplifying
c  985.108  99% search
c ==================================
c 1000.027 100% all
c 
c       3317297 conflicts,        3317.2 confs/sec
c             0 ternaries,           0.0 confs/ternary
c             0 binaries,            0.0 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            63 reductions,          0.1 redus/sec,  52655.5 confs/reduction
c          8405 restarts,            8.4 rests/sec,    394.7 confs/restart
c       5566493 decisions,        5566.3 decis/sec,      1.7 decis/conflict
c     100247633 propagations,   100244.9 props/sec,     18.0 props/decision
c 
c 1000.0 seconds, 73.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
