c launch: /data/cnf/sc2014/app/stable-400-0.1-7-9876543214007.cnf.bz2
c host: atom16
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-7-9876543214007.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/stable-400-0.1-7-9876543214007.cnf.bz2
c no embedded options
c found 'p cnf 400 30626' header
c read 400 variables, 30626 clauses, 630623 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=2
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] VMTF (--score=2)
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    30626         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 156 at-most-one constraints of average size 4.2
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 156 out of 156 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] 29 variables remain 7% (371 retained 93%)
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 2998 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] 29400 negative 98.7% of 29800 except 400 1.3%
c [phase-count-1] 14687 positive 49.3% of 29800 except 15113 50.7%
c [phase-count-1] less non-negative clauses 400 than limit 2900 (10.0%)
c [phase-count-1] non-pos/non-neg = 15113/400 = 37.78 >= 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 826 irredundant clauses 2.7% (29800 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 5003 conflicts
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 800 literals 100%
c [treelook-1] scheduling used 90296 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 441855 steps
c [treelook-1] 798 literals remain 100%
c [treelook-1] 400 variables remain to probed next time 100%
c [basicprobe-1] limit 1074566 penalty 0 = 0 + 0
c [basicprobe-1-0] 121 probes remain 30% 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 25 clauses out of 26 (96%) of length 64
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 63
c [cce-1-1] eliminated 26 clauses out of 27 (96%) of length 62
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 61
c [cce-1-1] eliminated 32 clauses out of 33 (97%) of length 59
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 58
c [cce-1-1] eliminated 58 clauses out of 60 (97%) of length 57
c [cce-1-1] eliminated 46 clauses out of 48 (96%) of length 56
c [cce-1-1] eliminated 96 clauses out of 98 (98%) of length 55
c [cce-1-1] eliminated 73 clauses out of 75 (97%) of length 54
c [cce-1-1] eliminated 114 clauses out of 123 (93%) of length 53
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 480 large clauses in 30000756 steps
c [cce-1-1] allowing another 15000378 steps for small clauses
c [cce-1-1] scheduling 15113 clauses = 15113 binary + 0 ternary
c [cce-1-1] tried to eliminate 160 small clauses 1%
c [cce-1-1] eliminated 122 binary clauses 1%
c [cce-1-1] eliminated 122 small clauses 1%
c [cce-1-1] eliminated 122 small clauses in 30001296 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 602 covered clauses in round 1
c [cce-1] eliminated 602 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 58896 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 4695 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 13 pos 3.2% + 387 neg 96.8% = 400 sched 100.0% ret 0
c [sweep-1-1] 1006376 steps 27 queries 30.07 avg class size
c [sweep-1-1] 2600 decisions 26 SAT calls 397.69 avg env size
c [sweep-1-1] 16 variables remain 4% (384 retained 96%)
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, 26 queries)
c [sort-queue-2] sorted 400 enqueued variables after 5003 conflicts
c [score-dist-2] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-2] max exp 1, different 1 (50%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 0 variables 0.0% (400 remain 100%)
c [simplification-2] removed 602 irredundant clauses 2.0% (29198 remain 95%)
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 26669 (soft 16669 + delta 10000)
c [simplification-2] new conflict limit 16669 (hard 26669)
c 
c [simplification-3] limit 16669 conflicts (hard 26669) hit after 16671 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 65 at-most-one constraints of average size 4.3
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 65 out of 65 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] 29 schedulable variables 7%
c [simpleprobe-2] limit 1567560 penalty 1 = 1 + 0
c [simpleprobe-2] 28 variables remain 7% (372 retained 93%)
c [unhide-2] limit 78378 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 0 tauts, 0 hbrs, 15193 literals
c [transred-1] limit 783780 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 4 clauses out of 8 (50%) of length 53
c [cce-2-1] eliminated 141 clauses out of 148 (95%) of length 52
c [cce-2-1] eliminated 124 clauses out of 128 (97%) of length 51
c [cce-2-1] eliminated 238 clauses out of 294 (81%) of length 50
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 507 large clauses in 30000137 steps
c [cce-2-1] allowing another 15000068 steps for small clauses
c [cce-2-1] scheduling 14991 clauses = 14991 binary + 0 ternary
c [cce-2-1] tried to eliminate 112 small clauses 1%
c [cce-2-1] eliminated 50 binary clauses 0%
c [cce-2-1] eliminated 50 small clauses 0%
c [cce-2-1] eliminated 50 small clauses in 30001018 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 557 covered clauses in round 1
c [cce-2] eliminated 557 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] 2 pos 12.5% + 14 neg 87.5% = 16 sched 4.0% ret 384
c [sweep-2-1] 721244 steps 9 queries 4.78 avg class size
c [sweep-2-1] 800 decisions 8 SAT calls 398.00 avg env size
c [sweep-2-1] fully completed sweeping round
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2-2] 17 pos 4.2% + 383 neg 95.8% = 400 sched 100.0% ret 0
c [sweep-2-2] 368249 steps 10 queries 73.90 avg class size
c [sweep-2-2] 800 decisions 8 SAT calls 398.00 avg env size
c [sweep-2-2] 303 variables remain 76% (97 retained 24%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (2 rounds, 17 queries)
c [sort-queue-3] sorted 400 enqueued variables after 16671 conflicts
c [score-dist-3] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-3] max exp 1, different 1 (50%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 0 variables 0.0% (400 remain 100%)
c [simplification-3] removed 557 irredundant clauses 1.9% (28641 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 45003 (soft 35003 + delta 10000)
c [simplification-3] new conflict limit 35003 (hard 45003)
c 
c [simplification-4] limit 35003 conflicts (hard 45003) hit after 35003 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 41 clauses out of 52 (79%) of length 50
c [cce-3-1] eliminated 416 clauses out of 432 (96%) of length 49
c [cce-3-1] eliminated 60 clauses out of 417 (14%) of length 48
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 517 large clauses in 30000244 steps
c [cce-3-1] allowing another 15000122 steps for small clauses
c [cce-3-1] scheduling 14941 clauses = 14941 binary + 0 ternary
c [cce-3-1] tried to eliminate 160 small clauses 1%
c [cce-3-1] eliminated 89 binary clauses 1%
c [cce-3-1] eliminated 89 small clauses 1%
c [cce-3-1] eliminated 89 small clauses in 30000193 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 606 covered clauses in round 1
c [cce-3] eliminated 606 covered clauses in TOTAL during 1 rounds
c [bca-2] limit of 10000000 steps and 56570 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 32696 steps
c [sort-queue-4] sorted 400 enqueued variables after 35003 conflicts
c [score-dist-4] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-4] max exp 1, different 1 (50%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 0 variables 0.0% (400 remain 100%)
c [simplification-4] removed 606 irredundant clauses 2.1% (28035 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 72500 (soft 60001 + delta 12499)
c [simplification-4] new conflict limit 60001 (hard 72500)
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.7     400    28035     53927   11591      0   261   58   110   11  53%    567   53   62   30  206%
c 
c [simplification-5] limit 60001 conflicts (hard 72500) hit after 60003 conflicts
c [quatres-2] found 0 quaternary clauses 0% in total
c [ternres-2] limit 2094997 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 209499 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 800 literals 100%
c [treelook-2] scheduling used 120768 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 209499 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 321642 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 311 clauses out of 331 (94%) of length 48
c [cce-4-1] eliminated 375 clauses out of 391 (96%) of length 47
c [cce-4-1] eliminated 430 clauses out of 451 (95%) of length 46
c [cce-4-1] eliminated 514 clauses out of 543 (95%) of length 45
c [cce-4-1] eliminated 522 clauses out of 547 (95%) of length 44
c [cce-4-1] eliminated 749 clauses out of 785 (95%) of length 43
c [cce-4-1] eliminated 763 clauses out of 798 (96%) of length 42
c [cce-4-1] eliminated 818 clauses out of 858 (95%) of length 41
c [cce-4-1] eliminated 868 clauses out of 909 (95%) of length 40
c [cce-4-1] eliminated 925 clauses out of 976 (95%) of length 39
c [cce-4-1] eliminated 973 clauses out of 1023 (95%) of length 38
c [cce-4-1] eliminated 847 clauses out of 889 (95%) of length 37
c [cce-4-1] eliminated 764 clauses out of 798 (96%) of length 36
c [cce-4-1] eliminated 578 clauses out of 605 (96%) of length 35
c [cce-4-1] eliminated 648 clauses out of 703 (92%) of length 34
c [cce-4-1] eliminated 508 clauses out of 546 (93%) of length 33
c [cce-4-1] eliminated 5 clauses out of 444 (1%) of length 32
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 10598 large clauses in 300000163 steps
c [cce-4-1] allowing another 150000081 steps for small clauses
c [cce-4-1] scheduling 14852 clauses = 14852 binary + 0 ternary
c [cce-4-1] tried to eliminate 5691 small clauses 38%
c [cce-4-1] eliminated 511 binary clauses 3%
c [cce-4-1] eliminated 511 small clauses 3%
c [cce-4-1] eliminated 511 small clauses in 300000252 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 11109 covered clauses in round 1
c [cce-4] eliminated 11109 covered clauses in TOTAL during 1 rounds
c [sweep-3] limit 628499 penalty 1 = 1 + 0
c [sweep-3-1] 14 pos 4.6% + 289 neg 95.4% = 303 sched 75.8% ret 97
c [sweep-3-1] 648907 steps 17 queries 37.06 avg class size
c [sweep-3-1] 1600 decisions 16 SAT calls 394.62 avg env size
c [sweep-3-1] 103 variables remain 26% (297 retained 74%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 16 queries)
c [sort-queue-5] sorted 400 enqueued variables after 60003 conflicts
c [score-dist-5] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-5] max exp 1, different 1 (50%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 0 variables 0.0% (400 remain 100%)
c [simplification-5] removed 11109 irredundant clauses 39.6% (16926 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 98413 (soft 85610 + delta 12803)
c [simplification-5] new conflict limit 85610 (hard 98413)
c 
c [simplification-6] limit 85610 conflicts (hard 98413) hit after 85614 conflicts
c [card-3] limit 690882 penalty 2 = 2 + 0
c [card-3] found 36 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 690882 for elimination
c [card-3] 36 out of 36 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-3] limit 276352 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 0 tauts, 0 hbrs, 20448 literals
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 48 (2%) of length 34
c [cce-5-1] eliminated 188 clauses out of 303 (62%) of length 32
c [cce-5-1] eliminated 216 clauses out of 342 (63%) of length 31
c [cce-5-1] eliminated 214 clauses out of 317 (68%) of length 30
c [cce-5-1] eliminated 166 clauses out of 250 (66%) of length 29
c [cce-5-1] eliminated 139 clauses out of 211 (66%) of length 28
c [cce-5-1] eliminated 109 clauses out of 145 (75%) of length 27
c [cce-5-1] eliminated 71 clauses out of 101 (70%) of length 26
c [cce-5-1] eliminated 49 clauses out of 82 (60%) of length 25
c [cce-5-1] eliminated 33 clauses out of 58 (57%) of length 24
c [cce-5-1] eliminated 25 clauses out of 45 (56%) of length 23
c [cce-5-1] eliminated 19 clauses out of 28 (68%) of length 22
c [cce-5-1] eliminated 13 clauses out of 24 (54%) of length 21
c [cce-5-1] eliminated 1 clauses out of 22 (5%) of length 20
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1244 large clauses in 30000061 steps
c [cce-5-1] allowing another 15000030 steps for small clauses
c [cce-5-1] scheduling 14341 clauses = 14341 binary + 0 ternary
c [cce-5-1] tried to eliminate 970 small clauses 7%
c [cce-5-1] eliminated 2 binary clauses 0%
c [cce-5-1] eliminated 2 small clauses 0%
c [cce-5-1] eliminated 2 small clauses in 30000055 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1246 covered clauses in round 1
c [cce-5] eliminated 1246 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 27635290 steps penalty 2 = 2 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 35315 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 [sort-queue-6] sorted 400 enqueued variables after 85614 conflicts
c [score-dist-6] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-6] max exp 1, different 1 (50%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 0 variables 0.0% (400 remain 100%)
c [simplification-6] removed 1246 irredundant clauses 7.4% (15680 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 128824 (soft 114421 + delta 14403)
c [simplification-6] new conflict limit 114421 (hard 128824)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   37.5     400    15680     98012   19289      0   774   51    90    8  56%    791    7   36   44   82%
c 
c [simplification-7] limit 114421 conflicts (hard 128824) hit after 128824 conflicts
c [basicprobe-2] limit 20765578 penalty 1 = 1 + 0
c [basicprobe-2-0] 121 sched 30%, 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 20765578 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 41531156 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 11 clauses out of 18 (61%) of length 20
c [cce-6-1] eliminated 10 clauses out of 21 (48%) of length 19
c [cce-6-1] eliminated 10 clauses out of 18 (56%) of length 18
c [cce-6-1] eliminated 2 clauses out of 12 (17%) of length 17
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 16
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 15
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 14
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 36 large clauses in 14807207 steps
c [cce-6-1] allowing another 7403603 steps for small clauses
c [cce-6-1] scheduling 14339 clauses = 14339 binary + 0 ternary
c [cce-6-1] tried to eliminate 2291 small clauses 16%
c [cce-6-1] eliminated 5 binary clauses 0%
c [cce-6-1] eliminated 5 small clauses 0%
c [cce-6-1] eliminated 5 small clauses in 41531261 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 41 covered clauses in round 1
c [cce-6] eliminated 41 covered clauses in TOTAL during 1 rounds
c [cce-6] 41 < 1/100 * 15680 = 156 considered unsuccessful
c [bca-3] limit of 10000000 steps and 31778 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 46784 steps
c [sort-queue-7] sorted 400 enqueued variables after 128824 conflicts
c [score-dist-7] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-7] max exp 1, different 1 (50%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 0 variables 0.0% (400 remain 100%)
c [simplification-7] removed 41 irredundant clauses 0.3% (15639 remain 51%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 28807
c [simplification-7] new conflict interval 57614
c [simplification-7] penalized conflict interval 57614 = 1 * 57614
c [simplification-7] hard conflict limit 215245 (soft 186438 + delta 28807)
c [simplification-7] new conflict limit 186438 (hard 215245)
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.7     400    15639    134565   23241      0   779   36    59    8  61%    891  -12   34   39   87%
c -   53.0     400    15639    167688   21777      0   779   39    67   10  58%    943   -6   28   41   69%
c 
c [simplification-8] limit 186438 conflicts (hard 215245) hit after 188304 conflicts
c [quatres-3] found 0 quaternary clauses 0% in total
c [ternres-3] limit 2868501 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 573700 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 [sweep-4] limit 860550 penalty 2 = 2 + 0
c [sweep-4-1] 2 pos 1.9% + 101 neg 98.1% = 103 sched 25.8% ret 297
c [sweep-4-1] 914208 steps 11 queries 18.91 avg class size
c [sweep-4-1] 1000 decisions 10 SAT calls 397.90 avg env size
c [sweep-4-1] 60 variables remain 15% (340 retained 85%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 10 queries)
c [sort-queue-8] sorted 400 enqueued variables after 188304 conflicts
c [score-dist-8] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-8] max exp 1, different 1 (50%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 0 variables 0.0% (400 remain 100%)
c [simplification-8] removed 0 irredundant clauses 0.0% (15639 remain 51%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 57614
c [simplification-8] new conflict interval 115228
c [simplification-8] penalized conflict interval 115228 = 1 * 115228
c [simplification-8] hard conflict limit 361146 (soft 303532 + delta 57614)
c [simplification-8] new conflict limit 303532 (hard 361146)
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 -   60.5     400    15639    203350   21890      0   779   37    62   10  60%    977  -13   32   43   76%
c -   68.2     400    15639    239902   22836      0   779   34    58    8  59%    997  -17   33   43   77%
c -   75.8     400    15639    276619   23605      0   779   39    62   10  63%   1009  -13   35   43   81%
c -   83.4     400    15639    313847   24833      0   779   35    53   11  65%   1015  -11   34   38   88%
c 
c [simplification-9] limit 303532 conflicts (hard 361146) hit after 315154 conflicts
c [cce-7] limit of 46741402 steps penalty 1 = 1 + 0
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] allowing another 6996566 steps for small clauses
c [cce-7-1] scheduling 14334 clauses = 14334 binary + 0 ternary
c [cce-7-1] tried to eliminate 2725 small clauses 19%
c [cce-7-1] eliminated 7 binary clauses 0%
c [cce-7-1] eliminated 7 small clauses 0%
c [cce-7-1] eliminated 7 small clauses in 46741406 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 7 covered clauses in round 1
c [cce-7] eliminated 7 covered clauses in TOTAL during 1 rounds
c [cce-7] 7 < 1/100 * 15639 = 156 considered unsuccessful
c [sort-queue-9] sorted 400 enqueued variables after 315154 conflicts
c [score-dist-9] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-9] max exp 1, different 1 (50%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 0 variables 0.0% (400 remain 100%)
c [simplification-9] removed 7 irredundant clauses 0.0% (15632 remain 51%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 115228
c [simplification-9] new conflict interval 230456
c [simplification-9] penalized conflict interval 230456 = 1 * 230456
c [simplification-9] hard conflict limit 660838 (soft 545610 + delta 115228)
c [simplification-9] new conflict limit 545610 (hard 660838)
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 -   92.5     400    15632    350933   23486      0   786   51    86    8  60%   1019    7   42   46   91%
c -  101.2     400    15632    390584   25966      0   786   33    52   11  63%   1021  -18   29   41   69%
c -  110.8     400    15632    429012   26603      0   786   30    46   11  66%   1023  -15   27   37   73%
c -  120.7     400    15632    467678   25213      0   786   47    81   11  58%   1023    9   46   43  107%
c -  130.2     400    15632    508594   26991      0   786   48    81   12  60%   1024   12   68   43  161%
c -  139.3     400    15632    548496   27028      0   786   36    59   12  61%   1024   -2   62   38  165%
c 
c [simplification-10] limit 545610 conflicts (hard 660838) hit after 548608 conflicts
c [card-4] limit 2099875 penalty 3 = 3 + 0
c [card-4] found 158 at-most-one constraints of average size 4.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2099875 for elimination
c [card-4] 158 out of 158 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [simpleprobe-3] 28 schedulable variables 7%
c [simpleprobe-3] limit 33598015 penalty 2 = 2 + 0
c [simpleprobe-3] fully completed simple probing
c [unhide-4] limit 839950 with penalty 3 = 3 + 0
c [unhide-4-6] 0 units, 0 failed, 0 tauts, 0 hbrs, 15066 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 1679900772 steps penalty 3 = 3 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 3096335 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 [sort-queue-10] sorted 400 enqueued variables after 548608 conflicts
c [score-dist-10] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-10] max exp 1, different 1 (50%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 0 variables 0.0% (400 remain 100%)
c [simplification-10] removed 0 irredundant clauses 0.0% (15632 remain 51%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 230456
c [simplification-10] new conflict interval 460912
c [simplification-10] penalized conflict interval 460912 = 1 * 460912
c [simplification-10] hard conflict limit 1239976 (soft 1009520 + delta 230456)
c [simplification-10] new conflict limit 1009520 (hard 1239976)
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 -  149.4     400    15632    589490   26561      0   786   40    64   11  62%   1024   -6   35   42   83%
c -  159.0     400    15632    631742   27990      0   786   39    64   12  60%   1024   -1   63   39  160%
c -  168.6     400    15632    674340   27903      0   786   43    70    9  61%   1024   -1   38   43   89%
c -  177.3     400    15632    718262   28934      0   786   29    45   12  65%   1024  -21   25   40   64%
c -  188.7     400    15632    761956   29612      0   786   54    92    9  59%   1024   39   57   34  168%
c -  199.2     400    15632    805657   29757      0   786   26    40   12  64%   1024  -16   23   34   67%
c -  210.5     400    15632    850400   29660      0   786   60   105   13  57%   1024   38   48   42  116%
c -  221.9     400    15632    896221   30613      0   786   30    43   14  68%   1024  -22   26   39   66%
c -  236.5     400    15632    941622   32152      0   786   23    32   11  70%   1024  -19   20   32   62%
c -  252.0     400    15632    986935   32687      0   786   21    29   14  72%   1024  -13   17   27   61%
c 
c [simplification-11] limit 1009520 conflicts (hard 1239976) hit after 1009521 conflicts
c [block-4] scheduling all variables this time
c [block-4] scheduled 400 variables 100%
c [block-4] limit of 82464021 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 31764 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 52857 steps
c [sort-queue-11] sorted 400 enqueued variables after 1009521 conflicts
c [score-dist-11] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-11] max exp 1, different 1 (50%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 0 variables 0.0% (400 remain 100%)
c [simplification-11] removed 0 irredundant clauses 0.0% (15632 remain 51%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 460912
c [simplification-11] new conflict interval 921824
c [simplification-11] penalized conflict interval 921824 = 1 * 921824
c [simplification-11] hard conflict limit 2392257 (soft 1931345 + delta 460912)
c [simplification-11] new conflict limit 1931345 (hard 2392257)
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 -  266.2     400    15632   1033623   31469      0   786   58    98   13  59%   1024   36   55   40  139%
c -  278.4     400    15632   1082422   31513      0   786   33    51   14  64%   1024  -20   31   42   73%
c -  293.3     400    15632   1132355   32014      0   786   58    96   10  60%   1024   15   43   49   88%
c -  306.0     400    15632   1182296   33236      0   786   48    76   11  63%   1024   -3   46   48   95%
c -  318.2     400    15632   1231950   33807      0   786   38    60   14  63%   1024  -17   35   46   77%
c -  332.3     400    15632   1281887   34451      0   786   47    79   11  60%   1024   11   37   42   87%
c -  345.5     400    15632   1333058   34241      0   786   42    68   14  62%   1024   -6   40   46   88%
c -  363.2     400    15632   1384873   35811      0   786   31    45   15  68%   1024  -18   31   40   78%
c -  379.7     400    15632   1436961   35264      0   786   48    76   15  63%   1024    4   49   45  110%
c -  393.1     400    15632   1490264   35953      0   786   28    44   15  64%   1024  -22   29   41   72%
c -  409.0     400    15632   1544399   35922      0   786   38    61   15  63%   1024  -13   30   45   67%
c -  423.2     400    15632   1598914   36705      0   786   37    57   16  65%   1024  -14   43   44   98%
c -  439.0     400    15632   1653746   37190      0   786   41    69   12  60%   1024   -2   35   44   80%
c -  456.2     400    15632   1710167   37133      0   786   55    91   11  60%   1024   19   58   45  128%
c -  473.3     400    15632   1766931   37324      0   786   53    87   15  62%   1024   10   50   47  106%
c -  490.0     400    15632   1824672   39039      0   786   34    54   15  62%   1024  -14   35   42   83%
c -  507.0     400    15632   1881377   38720      0   786   52    86   12  61%   1024   11   39   46   83%
c -  522.3     400    15632   1939645   39360      0   786   30    42   12  71%   1024  -27   28   42   66%
c 
c [simplification-12] limit 1931345 conflicts (hard 2392257) hit after 1953937 conflicts
c [quatres-4] found 0 quaternary clauses 0% in total
c [ternres-4] limit 17568899 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 3513779 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 1756889907 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 1 clauses out of 31 (3%) of length 31
c [cce-8-1] eliminated 1 clauses out of 85 (1%) of length 25
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 2 large clauses in 12964071 steps
c [cce-8-1] allowing another 6482035 steps for small clauses
c [cce-8-1] scheduling 14327 clauses = 14327 binary + 0 ternary
c [cce-8-1] tried to eliminate 14327 small clauses 100%
c [cce-8-1] eliminated 78 binary clauses 1%
c [cce-8-1] eliminated 78 small clauses 1%
c [cce-8-1] eliminated 78 small clauses in 204145096 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] completed small and large (ATE)
c [cce-8-1] eliminated 80 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 6372528 steps for small clauses
c [cce-8-2] scheduling 14249 clauses = 14249 binary + 0 ternary
c [cce-8-2] tried to eliminate 14249 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 80 covered clauses in TOTAL during 2 rounds
c [cce-8] 80 < 1/100 * 15632 = 156 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 52706696 penalty 3 = 3 + 0
c [sweep-5-1] 1 pos 1.7% + 59 neg 98.3% = 60 sched 15.0% ret 340
c [sweep-5-1] 1350941 steps 21 queries 8.67 avg class size
c [sweep-5-1] 2000 decisions 20 SAT calls 397.40 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] 10 pos 2.5% + 390 neg 97.5% = 400 sched 100.0% ret 0
c [sweep-5-2] 1955023 steps 31 queries 16.94 avg class size
c [sweep-5-2] 3000 decisions 30 SAT calls 397.40 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] 10 pos 2.5% + 390 neg 97.5% = 400 sched 100.0% ret 0
c [sweep-5-3] 1724263 steps 30 queries 18.40 avg class size
c [sweep-5-3] 2900 decisions 29 SAT calls 397.14 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, 79 queries)
c [sort-queue-12] sorted 400 enqueued variables after 1953937 conflicts
c [score-dist-12] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 0 variables 0.0% (400 remain 100%)
c [simplification-12] removed 80 irredundant clauses 0.5% (15552 remain 51%)
c [simplification-12] maximum reduction of 1% = max (0%, 1%)
c [simplification-12] geometric conflict interval increment 460912 = 921824 / 2
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 3453937 (soft 2953937 + delta 500000)
c [simplification-12] new conflict limit 2953937 (hard 3453937)
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 -  540.7     400    15552   1998680   39486      0   864   35    55   12  65%   1024  -17   30   44   68%
c -  560.7     400    15552   2059185   39817      0   864   57    95   17  60%   1024   17   49   49  100%
c -  580.3     400    15552   2118735   41402      0   864   36    55   17  65%   1024  -14   35   43   82%
c -  597.6     400    15552   2178541   41735      0   864   30    45   17  66%   1024  -18   28   39   71%
c -  616.1     400    15552   2239497   41418      0   864   47    77   13  61%   1024    7   39   43   91%
c -  636.4     400    15552   2302108   42296      0   864   50    81   13  61%   1024   16   30   41   71%
c -  655.8     400    15552   2364517   42133      0   864   44    72   13  62%   1024   -1   31   45   68%
c -  676.5     400    15552   2427841   42514      0   864   56    91   18  61%   1024   16   51   47  109%
c -  697.6     400    15552   2491845   43426      0   864   33    49   13  66%   1024  -21   28   43   65%
c -  718.5     400    15552   2556912   44099      0   864   30    45   14  68%   1024  -12   30   36   84%
c -  741.7     400    15552   2622728   43429      0   864   50    80   18  63%   1024    2   80   49  162%
c -  767.1     400    15552   2690200   45459      0   864   41    58   19  71%   1024  -14   39   46   84%
c -  791.1     400    15552   2756188   45614      0   864   34    51   15  67%   1024  -11   36   40   91%
c -  815.0     400    15552   2823162   45185      0   864   51    83   19  61%   1024   10   56   46  123%
c -  840.1     400    15552   2891071   46568      0   864   35    51   20  68%   1024  -15   36   42   88%
c 
c [simplification-13] limit 2953937 conflicts (hard 3453937) hit after 2953939 conflicts
c [treelook-3] limit 5851021 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 800 literals 100%
c [treelook-3] scheduling used 325146 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 5851021 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 5859811 steps
c [treelook-3] 606 literals remain 76%
c [treelook-3] 400 variables remain to probed next time 100%
c [sort-queue-13] sorted 400 enqueued variables after 2953939 conflicts
c [score-dist-13] active 0 (0%), one 400 (100%), zero 0 (0%)
c [score-dist-13] max exp 1, different 1 (50%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 0 variables 0.0% (400 remain 100%)
c [simplification-13] removed 0 irredundant clauses 0.0% (15552 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 5953939 (soft 4953939 + delta 1000000)
c [simplification-13] new conflict limit 4953939 (hard 5953939)
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 -  868.9     400    15552   2959425   46166      0   864   40    65   15  62%   1024   -1   38   42   92%
c -  892.6     400    15552   3027797   46550      0   864   58    96   15  60%   1024   35   74   40  186%
c -  917.2     400    15552   3097118   47828      0   864   23    33   21  68%   1024  -16   19   31   61%
c -  945.0     400    15552   3167595   46601      0   864   41    65   15  64%   1024  -10   39   46   84%
c -  968.1     400    15552   3239194   48924      0   864   28    40   21  70%   1024  -19   25   37   67%
c -  996.1     400    15552   3310609   48410      0   864   34    52   15  66%   1024  -13   37   41   91%
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), 137032 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, 1486690 resolutions, 4211854 steps
c blkd: 2 blocking literals 0%, 0 pure
c bump: 3265384 bumped seen, 507971520 lits 155.6 on average
c card: 4 count, 0 units, 0 am1, 12060682 steps
c card: 248 rescheduled, 91 eliminated, 55845 resolved, 55 subsumed
c card: 415 at-most-one constraints found, average size 4.22
c card: 415 at-most-one constraints used 100%, average size 4.22
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, 14248 eliminated, 14248 ate 100%, 0 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: 661249 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: 24 decompositions, 0 equivalent 0%
c deco: 70126 decision-only clauses 2%, 44% reduction
c decs: 5709916 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, 140 strengthened, 0 blocked
c elms: 20361 copies, 22507 resolutions, 0 ipos
c elms: 165515 subchks, 73521 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, 14272088 steps, 7136044 extr 50%, 0 elim 0%
c glue: 42.5 orig avg, 42.5 real avg, 6.3 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: 3265384 clauses, 102.1 length
c lrnd: 333420143 lits = 466062899 orig - 132642756 removed 28%
c lrnd: 821078 uips 25%, 2092040 flips 64%
c mins: 3193507 mins 98%, 0 bin 0%, 1404 size 0%
c mins: 91245110 poisoned searches, 53762333 hits, 59% hit rate
c mins: 484251489 used twice searches, 109896855 hits, 23% hit rate
c move: moved 864, 864 bin 100%, 0 trn 0%
c otfs: 60089 driving 22%, 216963 restarting 78%
c otfs: str 277052, 262029 red 95%, 15023 irr 5%
c otfs: str 277052, 0 bin 0%, 0 trn 0%, 277052 lrg 100%
c otfs: sub 79, 79 red 100%, 0 irr 0%
c otfs: sub 79, 0 bin 0%, 0 trn 0%, 79 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, 833 probed, 0 failed, 0 eqs
c prbs: 3 treelook, 198 probed, 0 failed, 0 lifted
c prom: 208528 locked 13% out of 1571051 tried
c prps: 95609265 props, 17 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 4 count, 0 quat, 0 self1, 0 self2, 0 dup
c queu: 13 sorted, 5709916 next (0 steps 0.00)
c queu: 507977120 enq (507977105 steps 1.00), 507971520 deq 100%
c redc: 779 clauses 96%, 810 tried 0%, 0 sat 0%
c redc: 2645 lits 15%, 17922 tried 0%, 0 sat 0%
c redc: 25 times jump level reduced, 4.4 levels on average
c reds: 63 count, 52768.8 conflicts per reduce
c reds: 0 memlim 0%, 63 arith 100%
c reds: 2551575 collected 87%, 364790 retired 13%
c rmbd: 826 removed, 0 red 0%
c rsts: 8485 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: 3265383 count (2566770 tried 0.8), 288393 sub out of 3265383 (8.8%)
c swps: 5 count, 8 rounds, 148 queries (18.5/round)
c swps: 147 sat calls, 0 unsat (7.1% success rate)
c swps: 14700 decisions 100.0, 1038 conflicts 7.1
c swps; 24.9 avg class size, 397.2 avg environment size
c swps: 0 failed, 0 impls, 0 equivs
c swp0: 46 type 0 queries, 0 unsat (0.0%), 46 sat (100.0%)
c swp1: 102 type 1 queries, 1 unsat (1.0%), 102 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: 17950824 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: 1667 nodes, 33460 edges, 2533868 steps
c trim: 3085977 words, 11.8 MB
c trnr: 4 count, 0 bin, 0 trn, 431776 steps
c unhd: 4 count, 6 rounds, 2283125 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: 53705 str, 0 bin 0%, 0 trn 0%, 53705 lrg 100%, 47771 red 89%
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: 27162544218 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 284.3 search visits per propagation, 8166.9 per conflict
c wchs: 20863343605 pushed, 2611255 enlarged, 1018 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3265384       2551575        364790      47198859      17381264       2256644
c 
c  0 0            68   0        42   0         0   0     13952   0      4425   0       327   0     0.0
c  1 5           444   0       218   0       135   0     78376   0     25737   0      2235   0     0.0
c  2 6         13587   0      8338   0      3044   1   2275723   5    733592   4     91620   4     0.4
c  3 9        143558   4     99388   4     27040   7  19194980  41   6200056  36    829046  37     3.7
c  4 14       421426  13    333978  13     66010  18  17136721  36<  5822542  33<   849348  38<    9.4
c  5 21       617738  19    523269  21     75704  21   4882949  10   2055878  12    283804  13    10.8
c  6 30       670062  21<   560886  22<    67182  18<  1477034   3    941961   5     91065   4     9.4
c  7 41       611897  19    484276  19     48687  13    956485   2    717058   4     50177   2     8.5
c  8 54       379338  12    283826  11     30126   8    576712   1    435837   3     29259   1     6.7
c  9 69       176936   5    132572   5     18657   5    267026   1    198219   1     13920   1     3.6
c 10 86       161006   5     94902   4     20264   6    237078   1    171999   1     10876   0     4.7
c 11 126       69322   2     29878   1      7941   2    101821   0     73953   0      4963   0     2.5
c 12 230           2   0         2   0         0   0         2   0         7   0         4   0     0.0
c 
c avg                  6.3           6.2           6.0           3.8           4.2           3.9
c std                  1.9           1.8           2.0           1.3           1.6           1.3
c 
c   34.424   3% bump
c    5.816   1% cce
c    3.360   0% decide
c 
c    4.903 < 1% rest (below)
c 
c    1.637   0% probe
c    1.303   0% block
c    1.193   0% unhide
c    0.930   0% sweep
c    0.620   0% card
c    0.354   0% transred
c    0.245   0% elim
c    0.203   0% gauss
c    0.048   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.780   0% preprocessing     6%
c   12.703   1% inprocessing     94%
c ==================================
c   13.483   1% simplifying
c  986.457  99% search
c ==================================
c  999.939 100% all
c 
c       3324435 conflicts,        3324.6 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,  52768.8 confs/reduction
c          8485 restarts,            8.5 rests/sec,    391.8 confs/restart
c       5709916 decisions,        5710.3 decis/sec,      1.7 decis/conflict
c      95609265 propagations,    95615.1 props/sec,     16.7 props/decision
c 
c 999.9 seconds, 77.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
