c launch: /data/cnf/sc2014/app/004-22-160.cnf.bz2
c host: atom20
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/004-22-160.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/004-22-160.cnf.bz2
c no embedded options
c found 'p cnf 4128 126580' header
c read 4128 variables, 126580 clauses, 833834 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 3589 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    3589    72259         0       0      0     0    0     0    4   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 3 at-most-one constraints of average size 3.0
c [card-1] found 6 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 9 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 965 variables
c [simpleprobe-1] all 3163 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 6 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 6 variables, found 18 hbrs, 4 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 747 tauts, 0 hbrs, 30 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 3157 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 87 variables 3% in round 1 in 2448234 steps
c [elim-1-1] backward subsumption/strengthening limit 2448200
c [elim-1-1-1] backward checking 1321 touched variables 42%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 4 and strengthened 83 clauses in 757396 steps
c [elim-1-1] rescheduled 152 variables 5% by backward subsumption
c [elim-1-2] eliminated 3 variables 0% in round 2 in 127278 steps
c [elim-1-2] backward subsumption/strengthening limit 127200
c [elim-1-2-1] backward checking 25 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 1 and strengthened 1 clauses in 94937 steps
c [elim-1-2] rescheduled 7 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 4572 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 91 = 3% variables out of 3157 scheduled
c [phase-count-1] 56170 negative 99.0% of 56720 except 550 1.0%
c [phase-count-1] 55926 positive 98.6% of 56720 except 794 1.4%
c [phase-1] phase bias: 1343 positive 44%, 1723 negative 56%
c [sort-queue-1] sorted 3066 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 3066 (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 170 variables 5.3% (3066 remain 85%)
c [simplification-1] removed 15539 irredundant clauses 21.5% (56720 remain 78%)
c [simplification-1] maximum reduction of 22% = max (5%, 22%)
c [simplification-1] large reduction 22% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 3 variables
c [simpleprobe-2] all 3063 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1623 variables remain 53% (1440 retained 47%)
c [simpleprobe-2] removed 0 variables, found 3 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6126 literals 100%
c [treelook-1] scheduling used 246772 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300057 steps
c [treelook-1] 4778 literals remain 78%
c [treelook-1] 2689 variables remain to probed next time 88%
c [treelook-1] removed 1 variables, found 19 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 366 sched 12%, 1 failed, 0 lifted, 10 hbrs
c [decomp-6] removed 1 variables
c [basicprobe-1-1] 368 sched 12%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-1-2] 369 sched 12%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-2] removed 1 variables, found 11 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 3061 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 86 blocked clauses
c [block-1] 86 < 1/100 * 56685 = 566 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2829 clauses out of 16851 (17%) of length 7
c [cce-1-1] eliminated 327 clauses out of 16068 (2%) of length 6
c [cce-1-1] eliminated 2153 clauses out of 12344 (17%) of length 5
c [cce-1-1] eliminated 571 clauses out of 6453 (9%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 5880 large clauses in 25558633 steps
c [cce-1-1] allowing another 12779316 steps for small clauses
c [cce-1-1] scheduling 4276 clauses = 239 binary + 4037 ternary
c [cce-1-1] tried to eliminate 4276 small clauses 100%
c [cce-1-1] eliminated 5 binary clauses 2%
c [cce-1-1] eliminated 1033 ternary clauses 26%
c [cce-1-1] eliminated 1038 small clauses 24%
c [cce-1-1] eliminated 1038 small clauses in 13839273 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 6918 covered clauses in round 1
c [cce-1-2] eliminated 36 clauses out of 14022 (0%) of length 7
c [cce-1-2] incomplete large round (ABCE)
c [cce-1-2] eliminated 36 large clauses in 16160772 steps
c [cce-1-2] allowing another 8080386 steps for small clauses
c [cce-1-2] scheduling 3238 clauses = 234 binary + 3004 ternary
c [cce-1-2] tried to eliminate 3238 small clauses 100%
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] eliminated 36 covered clauses in round 2
c [cce-1-3] incomplete large round (ABCE)
c [cce-1-3] allowing another 3637164 steps for small clauses
c [cce-1-3] scheduling 3238 clauses = 234 binary + 3004 ternary
c [cce-1-3] tried to eliminate 3238 small clauses 100%
c [cce-1-3] completed small round (ABCE)
c [cce-1-3] eliminated 0 covered clauses in round 3
c [cce-1] eliminated 6954 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3061 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 387 not tried 13% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 13 = 0% variables out of 3061 scheduled
c [elim-2] 13 < 1/100 * 3061 = 30 considered unsuccessful
c [bca-1] limit of 10000000 steps and 99256 added (scaled 2)
c [bca-1] 4088 out of 6098 literals actually usable 67%
c [bca-1] added 0 blocked clauses in 26671 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1431 pos 46.9% + 1617 neg 53.1% = 3048 sched 100.0% ret 0
c [sweep-1-1] 426068 steps 504 queries 152.41 avg class size
c [sweep-1-1] 7797 decisions 505 SAT calls 22.02 avg env size
c [sweep-1-1] fully completed sweeping round
c [decomp-8] removed 9 variables
c [sweep-1-1] removed 9 vars (0 failed, 5 eqs, 7 impls)
c [sweep-1-2] 1426 pos 46.9% + 1613 neg 53.1% = 3039 sched 100.0% ret 0
c [sweep-1-2] 410445 steps 532 queries 154.69 avg class size
c [sweep-1-2] 7839 decisions 533 SAT calls 21.01 avg env size
c [sweep-1-2] fully completed sweeping round
c [sweep-1-2] removed 0 vars (0 failed, 0 eqs, 4 impls)
c [sweep-1-3] 1426 pos 46.9% + 1613 neg 53.1% = 3039 sched 100.0% ret 0
c [sweep-1-3] 163900 steps 168 queries 434.55 avg class size
c [sweep-1-3] 2888 decisions 167 SAT calls 24.32 avg env size
c [sweep-1-3] 1952 variables remain 64% (1087 retained 36%)
c [sweep-1-3] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-1] removed 9 vars in TOTAL (3 rounds, 1201 queries)
c [sort-queue-2] sorted 3039 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 2797 (92%), zero 242 (8%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 27 variables 0.9% (3039 remain 85%)
c [simplification-2] removed 7360 irredundant clauses 13.0% (49358 remain 68%)
c [simplification-2] maximum reduction of 13% = max (1%, 13%)
c [simplification-2] large reduction 13% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [quatres-1] found 6566 quaternary clauses 14% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-1] added 16 double-self-subsuming ternary resolvents
c [quatres-1-2] added 135 single-self-subsuming ternary resolvents
c [quatres-1-2] added 442 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 3039 free variables schedulable
c [ternres-1] 525 ternary resolvents (43 bin, 482 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] found 12 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 12 out of 12 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 3236 xors of average arity 5.0
c [gauss-1] connected 16246 occurrences of 750 variables (average 21.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 2 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 5363 literals 88%
c [treelook-2] scheduling used 221520 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 300187 steps
c [treelook-2] 3947 literals remain 65%
c [treelook-2] 2630 variables remain to probed next time 87%
c [treelook-2] removed 0 variables, found 38 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 204 tauts, 0 hbrs, 229 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 33 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 180 clauses out of 16119 (1%) of length 6
c [cce-2-1] eliminated 36 clauses out of 10288 (0%) of length 5
c [cce-2-1] eliminated 59 clauses out of 5873 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 275 large clauses in 22548077 steps
c [cce-2-1] allowing another 11274038 steps for small clauses
c [cce-2-1] scheduling 929 clauses = 280 binary + 649 ternary
c [cce-2-1] tried to eliminate 929 small clauses 100%
c [cce-2-1] eliminated 6 binary clauses 2%
c [cce-2-1] eliminated 78 ternary clauses 12%
c [cce-2-1] eliminated 84 small clauses 9%
c [cce-2-1] eliminated 84 small clauses in 11428685 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 359 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 9285672 steps for small clauses
c [cce-2-2] scheduling 845 clauses = 274 binary + 571 ternary
c [cce-2-2] tried to eliminate 845 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 359 covered clauses in TOTAL during 2 rounds
c [cce-2] 359 < 1/100 * 49347 = 493 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 984 pos 50.5% + 966 neg 49.5% = 1950 sched 64.2% ret 1087
c [sweep-2-1] 361244 steps 458 queries 111.86 avg class size
c [sweep-2-1] 7051 decisions 462 SAT calls 21.82 avg env size
c [sweep-2-1] fully completed sweeping round
c [decomp-13] removed 1 variables
c [sweep-2-1] removed 1 vars (0 failed, 1 eqs, 3 impls)
c [sweep-2-2] 1490 pos 49.1% + 1546 neg 50.9% = 3036 sched 100.0% ret 0
c [sweep-2-2] 425911 steps 493 queries 123.48 avg class size
c [sweep-2-2] 7944 decisions 492 SAT calls 23.64 avg env size
c [sweep-2-2] fully completed sweeping round
c [decomp-14] removed 5 variables
c [sweep-2-2] removed 5 vars (0 failed, 3 eqs, 2 impls)
c [sweep-2-3] 1486 pos 49.0% + 1545 neg 51.0% = 3031 sched 100.0% ret 0
c [sweep-2-3] 213087 steps 202 queries 325.02 avg class size
c [sweep-2-3] 3858 decisions 202 SAT calls 27.69 avg env size
c [sweep-2-3] 1461 variables remain 48% (1570 retained 52%)
c [decomp-15] removed 1 variables
c [sweep-2-3] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-2] removed 7 vars in TOTAL (3 rounds, 1150 queries)
c [sort-queue-3] sorted 3030 enqueued variables after 3000 conflicts
c [score-dist-3] active 0 (0%), one 2947 (97%), zero 83 (3%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 9 variables 0.3% (3030 remain 84%)
c [simplification-3] removed 386 irredundant clauses 0.8% (48972 remain 68%)
c [simplification-3] maximum reduction of 1% = max (0%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23000 (soft 13000 + delta 10000)
c [simplification-3] new conflict limit 13000 (hard 23000)
c 
c [simplification-4] limit 13000 conflicts (hard 23000) hit after 13002 conflicts
c [quatres-2] found 7804 quaternary clauses 15% in total
c [quatres-2-1] added 41 double-self-subsuming ternary resolvents
c [quatres-2-2] added 271 single-self-subsuming ternary resolvents
c [quatres-2-2] added 458 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3030 free variables schedulable
c [ternres-2] 186 ternary resolvents (26 bin, 160 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-16] removed 1 variables
c [basicprobe-2] limit 1185851 penalty 0 = 0 + 0
c [basicprobe-2-0] 546 sched 18%, 2 failed, 0 lifted, 27 hbrs
c [decomp-17] removed 2 variables
c [basicprobe-2-1] 553 sched 18%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-2-2] 553 sched 18%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-2-2] removed 2 variables, found 31 hbrs
c [bate-1] eliminated 53 asymmetric tautologies during probing
c [transred-2] limit 237170 with penalty 0 = 0 + 0
c [transred-2] removed 21 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3027 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 3 blocked clauses
c [block-2] 3 < 1/100 * 48903 = 489 considered unsuccessful
c [elim-3] 387 variables 13% will be scheduled this time
c [elim-3] scheduled 387 variables 13%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 109 not tried 4% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 387 scheduled
c [bca-2] limit of 10000000 steps and 98276 added (scaled 2)
c [bca-2] 556 out of 6056 literals actually usable 9%
c [bca-2] added 0 blocked clauses in 16670 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 749 pos 51.3% + 712 neg 48.7% = 1461 sched 48.3% ret 1566
c [sweep-3-1] 360560 steps 363 queries 93.32 avg class size
c [sweep-3-1] 7840 decisions 362 SAT calls 29.44 avg env size
c [sweep-3-1] fully completed sweeping round
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-3-2] 1554 pos 51.3% + 1473 neg 48.7% = 3027 sched 100.0% ret 0
c [sweep-3-2] 497558 steps 407 queries 112.21 avg class size
c [sweep-3-2] 10560 decisions 407 SAT calls 34.38 avg env size
c [sweep-3-2] fully completed sweeping round
c [sweep-3-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3-3] 1554 pos 51.3% + 1473 neg 48.7% = 3027 sched 100.0% ret 0
c [sweep-3-3] 144552 steps 84 queries 412.74 avg class size
c [sweep-3-3] 2981 decisions 83 SAT calls 49.52 avg env size
c [sweep-3-3] 2091 variables remain 69% (936 retained 31%)
c [sweep-3-3] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3] removed 0 vars in TOTAL (3 rounds, 851 queries)
c [sort-queue-4] sorted 3027 enqueued variables after 13002 conflicts
c [score-dist-4] active 0 (0%), one 2982 (99%), zero 45 (1%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 3 variables 0.1% (3027 remain 84%)
c [simplification-4] removed 83 irredundant clauses 0.2% (48888 remain 68%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 58002 (soft 43002 + delta 15000)
c [simplification-4] new conflict limit 43002 (hard 58002)
c 
c [simplification-5] limit 43002 conflicts (hard 58002) hit after 43002 conflicts
c [quatres-3] found 10292 quaternary clauses 17% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-1] added 48 double-self-subsuming ternary resolvents
c [quatres-3-2] added 413 single-self-subsuming ternary resolvents
c [quatres-3-2] added 454 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3027 free variables schedulable
c [ternres-3] 177 ternary resolvents (12 bin, 165 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 887 xors of average arity 4.9
c [gauss-2] connected 4339 occurrences of 275 variables (average 15.8)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-3] limit 1204989 with penalty 0 = 0 + 0
c [transred-3] removed 9 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 1 clauses out of 12701 (0%) of length 7
c [cce-3-1] eliminated 5 clauses out of 16263 (0%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 6 large clauses in 15000002 steps
c [cce-3-1] allowing another 7500001 steps for small clauses
c [cce-3-1] scheduling 949 clauses = 316 binary + 633 ternary
c [cce-3-1] tried to eliminate 949 small clauses 100%
c [cce-3-1] eliminated 14 ternary clauses 2%
c [cce-3-1] eliminated 14 small clauses 1%
c [cce-3-1] eliminated 14 small clauses in 7694858 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 20 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3652589 steps for small clauses
c [cce-3-2] scheduling 935 clauses = 316 binary + 619 ternary
c [cce-3-2] tried to eliminate 935 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 20 covered clauses in TOTAL during 2 rounds
c [cce-3] 20 < 1/100 * 48888 = 488 considered unsuccessful
c [sort-queue-5] sorted 3027 enqueued variables after 43002 conflicts
c [score-dist-5] active 0 (0%), one 3015 (100%), zero 12 (0%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 0 variables 0.0% (3027 remain 84%)
c [simplification-5] removed 20 irredundant clauses 0.0% (48868 remain 68%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 30000
c [simplification-5] new conflict interval 60000
c [simplification-5] penalized conflict interval 60000 = 1 * 60000
c [simplification-5] hard conflict limit 133002 (soft 103002 + delta 30000)
c [simplification-5] new conflict limit 103002 (hard 133002)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   14.5    3027    48868     75205   28866   4322   251   12   269   13   5%    694  101   14    7  204%
c 
c [simplification-6] limit 103002 conflicts (hard 133002) hit after 103002 conflicts
c [quatres-4] found 13344 quaternary clauses 19% in total
c [quatres-4-1] removed 3 duplicate quaternary clauses
c [quatres-4-1] added 36 double-self-subsuming ternary resolvents
c [quatres-4-2] added 484 single-self-subsuming ternary resolvents
c [quatres-4-2] added 384 quaternary resolvents
c [ternres-4] limit 4056671 with penalty 0 = 0 + 0
c [ternres-4] all 3027 free variables schedulable
c [ternres-4] 145 ternary resolvents (11 bin, 134 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 507083 penalty 2 = 2 + 0
c [card-3] found 5 at-most-one constraints of average size 3.0
c [card-3] found 35 at-most-two constraints of average size 4.1
c [card-3] using previous limit 507083 for elimination
c [card-3] 39 out of 40 constraints (98%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 1604 schedulable variables 53%
c [simpleprobe-3] limit 8113343 penalty 1 = 1 + 0
c [simpleprobe-3] 50 variables remain 2% (2977 retained 98%)
c [simpleprobe-3] removed 0 variables, found 58 hbrs, 0 units
c [unhide-3] limit 202833 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 118 tauts, 0 hbrs, 1578 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 44 transitive binary clauses
c [sweep-4] limit 608500 penalty 1 = 1 + 0
c [sweep-4-1] 981 pos 46.9% + 1110 neg 53.1% = 2091 sched 69.1% ret 936
c [sweep-4-1] 608951 steps 129 queries 154.85 avg class size
c [sweep-4-1] 9384 decisions 128 SAT calls 146.44 avg env size
c [sweep-4-1] 280 variables remain 9% (2747 retained 91%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 128 queries)
c [sort-queue-6] sorted 3027 enqueued variables after 103002 conflicts
c [score-dist-6] active 0 (0%), one 3027 (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% (3027 remain 84%)
c [simplification-6] removed 19 irredundant clauses 0.0% (48849 remain 68%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 60000
c [simplification-6] new conflict interval 120000
c [simplification-6] penalized conflict interval 120000 = 1 * 120000
c [simplification-6] hard conflict limit 283002 (soft 223002 + delta 60000)
c [simplification-6] new conflict limit 223002 (hard 283002)
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 -   25.3    3027    48849    129628   36672   5382   331   14   266   15   5%    880   43   14   10  135%
c -   36.3    3027    48849    182945   44884   5666   335   16   275   16   6%    960   26   16   13  124%
c 
c [simplification-7] limit 223002 conflicts (hard 283002) hit after 223002 conflicts
c [quatres-5] found 17217 quaternary clauses 20% in total
c [quatres-5-1] removed 7 duplicate quaternary clauses
c [quatres-5-1] added 23 double-self-subsuming ternary resolvents
c [quatres-5-2] added 387 single-self-subsuming ternary resolvents
c [quatres-5-2] added 353 quaternary resolvents
c [ternres-5] limit 10425917 with penalty 0 = 0 + 0
c [ternres-5] all 3027 free variables schedulable
c [ternres-5] 78 ternary resolvents (6 bin, 72 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 18 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3027 variables 100%
c [block-3] limit of 26064794 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 [elim-4] scheduling all variables this time
c [elim-4] scheduled 3027 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1042591785 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 5 variables 0% in round 1 in 34379202 steps
c [elim-4-1] backward subsumption/strengthening limit 34379200
c [elim-4-1-1] backward checking 722 touched variables 24%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 7 clauses in 377468 steps
c [elim-4-1] rescheduled 15 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 88339 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 5 = 0% variables out of 3027 scheduled
c [elim-4] 5 < 1/100 * 3027 = 30 considered unsuccessful
c [bca-3] limit of 10000000 steps and 97922 added (scaled 2)
c [bca-3] 3 out of 6046 literals actually usable 0%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 83016 steps
c [sort-queue-7] sorted 3022 enqueued variables after 223002 conflicts
c [score-dist-7] active 0 (0%), one 3022 (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 5 variables 0.2% (3022 remain 84%)
c [simplification-7] removed 138 irredundant clauses 0.3% (48711 remain 67%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 120000
c [simplification-7] new conflict interval 240000
c [simplification-7] penalized conflict interval 240000 = 1 * 240000
c [simplification-7] hard conflict limit 583002 (soft 463002 + delta 120000)
c [simplification-7] new conflict limit 463002 (hard 583002)
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 -   46.9    3022    48711    234579   45400   6241   320   17   294   10   6%    995   26   17   15  116%
c -   55.6    3022    48711    292461   54100   6378   322   18   292   17   6%   1012    9   21   16  129%
c -   64.6    3022    48711    346985   59424   6461   323   20   292   11   7%   1019    3   19   18  109%
c -   73.2    3022    48711    401326   63859   6532   326   21   307   19   7%   1022    9   23   19  118%
c -   82.0    3022    48711    455989   67644   6595   326   23   315   19   7%   1023    9   24   21  117%
c 
c [simplification-8] limit 463002 conflicts (hard 583002) hit after 463002 conflicts
c [quatres-6] found 21103 quaternary clauses 20% in total
c [quatres-6-1] removed 30 duplicate quaternary clauses
c [quatres-6-1] added 18 double-self-subsuming ternary resolvents
c [quatres-6-2] added 221 single-self-subsuming ternary resolvents
c [quatres-6-2] added 220 quaternary resolvents
c [ternres-6] limit 20749787 with penalty 0 = 0 + 0
c [ternres-6] all 3022 free variables schedulable
c [ternres-6] 51 ternary resolvents (2 bin, 49 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1037489 penalty 2 = 2 + 0
c [gauss-3] extracted 54 xors of average arity 3.0
c [gauss-3] connected 162 occurrences of 15 variables (average 10.8)
c [gauss-3] limit 1037489 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 1037489 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 5326 literals 88%
c [treelook-3] scheduling used 488474 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1037489 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 1037612 steps
c [treelook-3] 597 literals remain 10%
c [treelook-3] 585 variables remain to probed next time 19%
c [treelook-3] removed 0 variables, found 22 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 17 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 259372345 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 10 clauses out of 16558 (0%) of length 6
c [cce-4-1] eliminated 53 clauses out of 10271 (1%) of length 5
c [cce-4-1] eliminated 66 clauses out of 5531 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 129 large clauses in 22110161 steps
c [cce-4-1] allowing another 11055080 steps for small clauses
c [cce-4-1] scheduling 1005 clauses = 323 binary + 682 ternary
c [cce-4-1] tried to eliminate 1005 small clauses 100%
c [cce-4-1] eliminated 1 binary clauses 0%
c [cce-4-1] eliminated 7 ternary clauses 1%
c [cce-4-1] eliminated 8 small clauses 1%
c [cce-4-1] eliminated 8 small clauses in 11245046 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 137 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 11028234 steps for small clauses
c [cce-4-2] scheduling 997 clauses = 322 binary + 675 ternary
c [cce-4-2] tried to eliminate 997 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 137 covered clauses in TOTAL during 2 rounds
c [cce-4] 137 < 1/100 * 48711 = 487 considered unsuccessful
c [sort-queue-8] sorted 3022 enqueued variables after 463002 conflicts
c [score-dist-8] active 0 (0%), one 3022 (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% (3022 remain 84%)
c [simplification-8] removed 137 irredundant clauses 0.3% (48574 remain 67%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 240000
c [simplification-8] new conflict interval 480000
c [simplification-8] penalized conflict interval 480000 = 1 * 480000
c [simplification-8] hard conflict limit 1183002 (soft 943002 + delta 240000)
c [simplification-8] new conflict limit 943002 (hard 1183002)
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 -   91.3    3022    48574    511202   71422   6905   334   24   332   19   7%   1024   17   30   22  135%
c -   99.7    3022    48574    566916   76033   6922   334   24   320   12   8%   1024   -2   24   23  105%
c -  108.0    3022    48574    622059   80786   6931   334   25   316   21   8%   1024   -5   29   24  120%
c -  116.4    3022    48574    676441   85310   6944   334   26   329   13   8%   1024    3   29   25  115%
c -  125.0    3022    48574    730151   89168   6968   334   26   328   22   8%   1024   -1   25   26   95%
c -  133.4    3022    48574    783484   92180   6975   334   28   341   13   8%   1024   10   29   27  110%
c -  141.9    3022    48574    837244   95642   6985   334   28   335   14   8%   1024   -2   32   27  116%
c -  150.3    3022    48574    891020   98445   6996   334   29   306   23   9%   1024  -31   25   28   91%
c 
c [simplification-9] limit 943002 conflicts (hard 1183002) hit after 943003 conflicts
c [quatres-7] found 23759 quaternary clauses 18% in total
c [quatres-7-1] removed 69 duplicate quaternary clauses
c [quatres-7-1] added 5 double-self-subsuming ternary resolvents
c [quatres-7-2] added 98 single-self-subsuming ternary resolvents
c [quatres-7-2] added 143 quaternary resolvents
c [ternres-7] limit 43304241 with penalty 0 = 0 + 0
c [ternres-7] all 3022 free variables schedulable
c [ternres-7] 21 ternary resolvents (4 bin, 17 trn)
c [ternres-7] fully completed ternary resolution
c [basicprobe-3] limit 216521207 penalty 0 = 0 + 0
c [basicprobe-3-0] 651 sched 22%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-0] fully completed probing
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 4 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 32478180 penalty 2 = 2 + 0
c [sweep-5-1] 142 pos 50.9% + 137 neg 49.1% = 279 sched 9.2% ret 2743
c [sweep-5-1] 520414 steps 67 queries 15.01 avg class size
c [sweep-5-1] 6135 decisions 66 SAT calls 559.86 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] 1585 pos 52.4% + 1437 neg 47.6% = 3022 sched 100.0% ret 0
c [sweep-5-2] 1385242 steps 172 queries 90.08 avg class size
c [sweep-5-2] 16265 decisions 171 SAT calls 740.79 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] 1585 pos 52.4% + 1437 neg 47.6% = 3022 sched 100.0% ret 0
c [sweep-5-3] 1426147 steps 172 queries 56.67 avg class size
c [sweep-5-3] 16405 decisions 171 SAT calls 700.50 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, 408 queries)
c [sort-queue-9] sorted 3022 enqueued variables after 943003 conflicts
c [score-dist-9] active 0 (0%), one 3022 (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% (3022 remain 84%)
c [simplification-9] removed 0 irredundant clauses 0.0% (48574 remain 67%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 480000
c [simplification-9] new conflict interval 960000
c [simplification-9] penalized conflict interval 960000 = 1 * 960000
c [simplification-9] hard conflict limit 2383003 (soft 1903003 + delta 480000)
c [simplification-9] new conflict limit 1903003 (hard 2383003)
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 -  159.9    3022    48574    945266  101814   7122   334   29   344   23   8%   1024    5   28   28   99%
c -  168.2    3022    48574    999325  105089   7128   334   29   339   14   9%   1024   -6   34   29  116%
c -  176.9    3022    48574   1053388  108063   7132   334   31   354   15   9%   1024    9   32   30  109%
c -  185.6    3022    48574   1107408  110716   7135   334   32   355   25   9%   1024    6   33   31  109%
c -  193.9    3022    48574   1161717  113162   7147   334   32   356   25   9%   1024    4   33   31  106%
c -  202.6    3022    48574   1216496  115588   7158   334   32   345   25   9%   1024   -5   35   31  113%
c -  211.4    3022    48574   1271840  118329   7167   334   32   341   16  10%   1024   -8   32   32  102%
c -  220.2    3022    48574   1327380  120407   7168   334   32   349   16   9%   1024   -2   25   32   78%
c -  229.3    3022    48574   1383882  122794   7173   334   32   361   16   9%   1024    7   36   32  111%
c -  238.3    3022    48574   1440772  125589   7179   334   32   345   16   9%   1024   -6   34   32  106%
c -  248.0    3022    48574   1497683  127608   7183   334   34   346   27  10%   1024   -6   35   33  104%
c -  257.7    3022    48574   1555404  128934   7188   334   34   342   27  10%   1024  -11   40   33  122%
c -  267.6    3022    48574   1614558  131774   7193   334   34   357   28  10%   1024    2   34   34  102%
c -  277.3    3022    48574   1673691  134518   7200   334   34   360   17  10%   1024    7   35   34  103%
c -  287.2    3022    48574   1732832  136649   7206   334   35   353   17  10%   1024    2   34   34  101%
c -  297.2    3022    48574   1792716  139176   7209   334   34   344   18  10%   1024   -8   28   34   83%
c -  307.6    3022    48574   1852572  140997   7211   334   35   345   18  10%   1024   -9   46   35  132%
c 
c [simplification-10] limit 1903003 conflicts (hard 2383003) hit after 1903162 conflicts
c [quatres-8] found 25861 quaternary clauses 16% in total
c [quatres-8-1] removed 124 duplicate quaternary clauses
c [quatres-8-1] added 6 double-self-subsuming ternary resolvents
c [quatres-8-2] added 52 single-self-subsuming ternary resolvents
c [quatres-8-2] added 91 quaternary resolvents
c [ternres-8] limit 98618301 with penalty 0 = 0 + 0
c [ternres-8] all 3022 free variables schedulable
c [ternres-8] 18 ternary resolvents (3 bin, 15 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 6163643 penalty 3 = 3 + 0
c [card-4] found 3 at-most-one constraints of average size 3.0
c [card-4] found 36 at-most-two constraints of average size 4.0
c [card-4] using previous limit 6163643 for elimination
c [card-4] 38 out of 39 constraints (97%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 2465457 with penalty 3 = 3 + 0
c [unhide-4-5] 0 units, 0 failed, 408 tauts, 0 hbrs, 28159 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 7 transitive binary clauses
c [sort-queue-10] sorted 3022 enqueued variables after 1903162 conflicts
c [score-dist-10] active 0 (0%), one 3022 (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% (3022 remain 84%)
c [simplification-10] removed 4 irredundant clauses 0.0% (48570 remain 67%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 960000
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] hard conflict limit 3403162 (soft 2903162 + delta 500000)
c [simplification-10] new conflict limit 2903162 (hard 3403162)
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 -  319.3    3022    48570   1913399  142305   6949   324   34   361   18   9%   1024    7   32   35   93%
c -  330.1    3022    48570   1975499  144505   6950   324   35   357   18  10%   1024    3   40   34  115%
c -  341.1    3022    48570   2038179  146910   6952   324   37   358   18  10%   1024    5   41   35  116%
c -  352.5    3022    48570   2101078  149276   6955   324   36   352   19  10%   1024   -2   40   36  110%
c -  363.6    3022    48570   2164262  151690   6955   324   36   360   19  10%   1024    4   38   36  104%
c -  374.8    3022    48570   2227813  153746   6957   324   36   374   19  10%   1024   17   32   37   89%
c -  386.1    3022    48570   2291778  155702   6958   324   38   370   19  10%   1024    9   44   37  120%
c -  397.3    3022    48570   2356421  158580   6961   324   38   373   19  10%   1024   14   43   37  116%
c -  408.9    3022    48570   2420736  161064   6963   324   37   369   20  10%   1024    6   34   38   91%
c -  420.3    3022    48570   2485035  163450   6967   324   39   349   20  11%   1024  -12   43   38  113%
c -  431.9    3022    48570   2549350  165562   6969   324   39   352   20  11%   1024   -5   43   38  114%
c -  444.1    3022    48570   2614024  166192   6971   324   40   352   20  11%   1024   -7   43   38  112%
c -  456.5    3022    48570   2680610  168086   6973   324   39   369   20  11%   1024    9   35   39   91%
c -  468.6    3022    48570   2747999  170423   6978   324   38   345   21  11%   1024  -13   39   38  103%
c -  481.2    3022    48570   2815538  172282   6979   324   39   361   21  11%   1024    3   38   39   99%
c -  493.3    3022    48570   2883722  174982   6979   324   39   355   21  11%   1024   -2   48   39  124%
c 
c [simplification-11] limit 2903162 conflicts (hard 3403162) hit after 2903162 conflicts
c [quatres-9] found 26949 quaternary clauses 14% in total
c [quatres-9-1] removed 98 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 37 single-self-subsuming ternary resolvents
c [quatres-9-2] added 67 quaternary resolvents
c [ternres-9] limit 167146835 with penalty 0 = 0 + 0
c [ternres-9] all 3022 free variables schedulable
c [ternres-9] 53 ternary resolvents (1 bin, 52 trn)
c [ternres-9] fully completed ternary resolution
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 3 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 3022 variables 100%
c [block-4] limit of 100000000 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 [elim-5] scheduling all variables this time
c [elim-5] scheduled 3022 variables 100%
c [elim-5] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] no variable eliminated in round 1 in 34098489 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 0 = 0% variables out of 3022 scheduled
c [bca-4] limit of 10000000 steps and 97638 added (scaled 2)
c [bca-4] 2 out of 6046 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 194208 steps
c [sort-queue-11] sorted 3022 enqueued variables after 2903162 conflicts
c [score-dist-11] active 0 (0%), one 3022 (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% (3022 remain 84%)
c [simplification-11] removed 1 irredundant clauses 0.0% (48569 remain 67%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] hard conflict limit 4403162 (soft 3903162 + delta 500000)
c [simplification-11] new conflict limit 3903162 (hard 4403162)
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 -  507.0    3022    48569   2951781  175628   7065   322   39   354   21  11%   1024   -6   45   38  117%
c -  520.3    3022    48569   3021532  177398   7065   322   38   361   21  10%   1024   -0   44   38  116%
c -  533.5    3022    48569   3092056  179575   7066   322   39   369   21  11%   1024   10   45   38  118%
c -  547.0    3022    48569   3163004  181885   7069   322   38   350   22  11%   1024   -7   38   39   98%
c -  560.9    3022    48569   3234005  183332   7070   322   40   355   22  11%   1024   -6   37   39   94%
c -  574.8    3022    48569   3305899  185850   7071   322   39   371   22  10%   1024    8   35   39   90%
c -  589.0    3022    48569   3377916  187349   7071   322   39   354   22  11%   1024   -3   36   39   92%
c -  603.1    3022    48569   3450848  189519   7074   322   39   374   22  10%   1024   13   34   39   88%
c -  617.8    3022    48569   3524074  190896   7074   322   41   352   23  12%   1024   -7   41   39  104%
c -  632.5    3022    48569   3598343  192587   7075   322   40   375   23  11%   1024   16   39   39   98%
c -  647.5    3022    48569   3673522  194968   7079   322   39   363   23  11%   1024    4   36   40   91%
c -  662.8    3022    48569   3748980  196246   7081   322   39   356   23  11%   1024   -2   35   40   89%
c -  678.2    3022    48569   3825589  198524   7082   322   39   358   23  11%   1024    0   42   39  107%
c -  693.8    3022    48569   3902590  200390   7082   322   39   342   24  12%   1024  -14   39   39   98%
c 
c [simplification-12] limit 3903162 conflicts (hard 4403162) hit after 3908992 conflicts
c [quatres-10] found 27596 quaternary clauses 13% in total
c [quatres-10-1] removed 79 duplicate quaternary clauses
c [quatres-10-2] added 9 single-self-subsuming ternary resolvents
c [quatres-10-2] added 73 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 3022 free variables schedulable
c [ternres-10] 1 ternary resolvents (1 bin, 0 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 6129683 penalty 3 = 3 + 0
c [gauss-4] extracted 4076 xors of average arity 5.4
c [gauss-4] connected 21892 occurrences of 818 variables (average 26.8)
c [gauss-4] limit 6129683 penalty 3 = 3 + 0
c [gauss-4] connected 2431 occurrences of 818 variables (average 3.0)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] 48 schedulable variables 2%
c [simpleprobe-4] limit 50000000 penalty 2 = 2 + 0
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 0 variables, found 19 hbrs, 0 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 18 transitive binary clauses
c [cce-5] limit of 153242091 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 2 clauses out of 16697 (0%) of length 6
c [cce-5-1] eliminated 10 clauses out of 10227 (0%) of length 5
c [cce-5-1] eliminated 10 clauses out of 5477 (0%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 22 large clauses in 24363905 steps
c [cce-5-1] allowing another 12181952 steps for small clauses
c [cce-5-1] scheduling 1012 clauses = 336 binary + 676 ternary
c [cce-5-1] tried to eliminate 1012 small clauses 100%
c [cce-5-1] eliminated 2 binary clauses 1%
c [cce-5-1] eliminated 4 ternary clauses 1%
c [cce-5-1] eliminated 6 small clauses 1%
c [cce-5-1] eliminated 6 small clauses in 12394304 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 28 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 12158288 steps for small clauses
c [cce-5-2] scheduling 1006 clauses = 334 binary + 672 ternary
c [cce-5-2] tried to eliminate 1006 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 0 covered clauses in round 2
c [cce-5] eliminated 28 covered clauses in TOTAL during 2 rounds
c [cce-5] 28 < 1/100 * 48569 = 485 considered unsuccessful
c [sort-queue-12] sorted 3022 enqueued variables after 3908992 conflicts
c [score-dist-12] active 0 (0%), one 3022 (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% (3022 remain 84%)
c [simplification-12] removed 28 irredundant clauses 0.1% (48541 remain 67%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1000000
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 5408992 (soft 4908992 + delta 500000)
c [simplification-12] new conflict limit 4908992 (hard 5408992)
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 -  711.5    3022    48541   3980208  201655   7098   326   39   356   24  11%   1024   -1   36   39   91%
c -  727.7    3022    48541   4059153  204397   7099   326   40   350   24  11%   1024   -6   46   40  115%
c -  744.2    3022    48541   4137859  205424   7102   326   39   359   24  11%   1024    0   37   40   93%
c -  760.7    3022    48541   4217956  207709   7105   326   41   355   24  12%   1024   -6   46   40  115%
c -  777.4    3022    48541   4298240  209867   7105   326   40   369   24  11%   1024    8   43   40  108%
c -  794.8    3022    48541   4378798  211029   7107   326   42   375   24  11%   1024   11   45   41  111%
c -  812.0    3022    48541   4460787  213590   7109   326   40   369   25  11%   1024    8   29   41   70%
c -  829.4    3022    48541   4542695  215352   7111   326   39   380   25  10%   1024   12   38   40   93%
c -  847.4    3022    48541   4625498  216879   7115   326   40   359   25  11%   1024   -2   43   40  108%
c -  864.8    3022    48541   4709001  220123   7116   326   41   365   25  11%   1024    5   34   41   84%
c -  882.1    3022    48541   4791544  221785   7118   326   40   357   25  11%   1024   -5   47   40  117%
c -  900.4    3022    48541   4875093  222106   7119   326   41   375   26  11%   1024   15   37   40   93%
c 
c [simplification-13] limit 4908992 conflicts (hard 5408992) hit after 4909179 conflicts
c [quatres-11] found 28141 quaternary clauses 12% in total
c [quatres-11-1] removed 68 duplicate quaternary clauses
c [quatres-11-2] added 16 single-self-subsuming ternary resolvents
c [quatres-11-2] added 41 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 3022 free variables schedulable
c [ternres-11] 15 ternary resolvents (1 bin, 14 trn)
c [ternres-11] fully completed ternary resolution
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 3 transitive binary clauses
c [sweep-6] limit 12391863 penalty 3 = 3 + 0
c [sweep-6-1] 1518 pos 50.2% + 1504 neg 49.8% = 3022 sched 100.0% ret 0
c [sweep-6-1] 2320467 steps 185 queries 81.35 avg class size
c [sweep-6-1] 16471 decisions 184 SAT calls 721.32 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] 1518 pos 50.2% + 1504 neg 49.8% = 3022 sched 100.0% ret 0
c [sweep-6-2] 2232782 steps 168 queries 86.45 avg class size
c [sweep-6-2] 15917 decisions 167 SAT calls 731.13 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] 1518 pos 50.2% + 1504 neg 49.8% = 3022 sched 100.0% ret 0
c [sweep-6-3] 2151893 steps 176 queries 52.50 avg class size
c [sweep-6-3] 16536 decisions 175 SAT calls 705.64 avg env size
c [sweep-6-3] fully completed sweeping round
c [sweep-6-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (3 rounds, 526 queries)
c [sort-queue-13] sorted 3022 enqueued variables after 4909179 conflicts
c [score-dist-13] active 0 (0%), one 3022 (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% (3022 remain 84%)
c [simplification-13] removed 0 irredundant clauses 0.0% (48541 remain 67%)
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 7909179 (soft 6909179 + delta 1000000)
c [simplification-13] new conflict limit 6909179 (hard 7909179)
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 -  920.5    3022    48541   4961048  224173   7150   324   41   361   25  11%   1024    2   43   40  109%
c -  939.6    3022    48541   5047523  226231   7151   324   40   372   26  11%   1024   13   42   40  106%
c -  958.6    3022    48541   5134363  228634   7152   324   38   363   26  10%   1024    2   34   40   84%
c -  977.9    3022    48541   5221415  230244   7154   324   40   353   26  11%   1024   -1   43   40  108%
c -  997.9    3022    48541   5309551  232833   7156   324   39   360   26  11%   1024    4   47   40  116%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 53 basic ate = 51 trn 96% + 2 lrg 4% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 320565 steps
c bkwd: tried 5079 clauses, 10091 lits, 1.99 lits/clause
c bkwd: checked 422096 occs, 83.11 occs/clause, 41.83 occs/lit
c bkwd: subsumed 0 binary, 3 ternary, 3 large
c bkwd: strengthened 0 binary, 3 ternary (100% self), 88 large (0% self)
c blkd: 4 bces, 89 removed, 2402880 resolutions, 5044235 steps
c blkd: 29 blocking literals 0%, 0 pure
c bump: 5290875 bumped seen, 532765729 lits 100.7 on average
c card: 4 count, 0 units, 0 am1, 9912215 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1588 subsumed
c card: 11 at-most-one constraints found, average size 3.00
c card: 11 at-most-one constraints used 100%, average size 3.00
c card: 89 at-most-two constraints found, average size 4.07
c card: 87 at-most-two constraints used 98%, average size 4.07
c cces: 5 cces, 7498 eliminated, 7462 ate 100%, 36 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: 960414 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 50 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 40 decompositions, 96 equivalent 2%
c deco: 9334 decision-only clauses 0%, 44% reduction
c decs: 30489830 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 108 eliminated 3%, 0 pure 0%
c elms: 8 rounds, 1.6 rounds/bve
c elms: 108 small 100%, 0 large 0%
c elms: 1640 tried small, 108 succeeded 7%, 1532 failed 93%
c elms: 2498 subsumed, 2822 strengthened, 3 blocked
c elms: 987877 copies, 2330037 resolutions, 426465 ipos
c elms: 178853 subchks, 122172 strchks
c gaus: 4 extractions, 8253 extracted, 5.2 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 18876038 steps, 9438019 extr 50%, 262620 elim 1%
c glue: 34.8 orig avg, 34.8 real avg, 5.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 252 = 98 simple 39% + 134 trn 53% + 20 lrg 8%, 45 sub 18%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5290874 clauses, 74.2 length
c lrnd: 392614739 lits = 418283192 orig - 25668453 removed 6%
c lrnd: 2336271 uips 44%, 2429295 flips 46%
c mins: 4957724 mins 94%, 64 bin 0%, 311999 size 6%
c mins: 347552753 poisoned searches, 32976852 hits, 9% hit rate
c mins: 671896609 used twice searches, 113766447 hits, 17% hit rate
c move: moved 1467, 14 bin 1%, 1453 trn 99%
c otfs: 32381 driving 46%, 37569 restarting 54%
c otfs: str 69950, 68432 red 98%, 1518 irr 2%
c otfs: str 69950, 0 bin 0%, 154 trn 0%, 69796 lrg 100%
c otfs: sub 417, 410 red 98%, 7 irr 2%
c otfs: sub 417, 0 bin 0%, 24 trn 6%, 393 lrg 94%
c phas: 1 computed, 3066 set, 1343 pos (44%), 1723 neg (56%)
c prbs: 3 basic, 6810 probed, 3 failed, 0 lifted
c prbs: 4 simple, 14208 probed, 4 failed, 4 eqs
c prbs: 3 treelook, 7492 probed, 1 failed, 0 lifted
c prom: 871640 locked 17% out of 5252178 tried
c prps: 563879295 props, 18 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 11 count, 2726 quat, 2123 self1, 194 self2, 485 dup
c queu: 13 sorted, 30489830 next (166 steps 0.00)
c queu: 532809227 enq (532809208 steps 1.00), 532765729 deq 100%
c redc: 763 clauses 0%, 529577 tried 10%, 3 sat 0%
c redc: 791 lits 0%, 4430474 tried 1%, 3 sat 0%
c redc: 31 times jump level reduced, 13.2 levels on average
c reds: 80 count, 66496.5 conflicts per reduce
c reds: 0 memlim 0%, 80 arith 100%
c reds: 3543076 collected 71%, 1473024 retired 29%
c rmbd: 50 removed, 31 red 62%
c rsts: 36281 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: 5290874 count (10351307 tried 2.0), 27297 sub out of 5288388 (0.5%)
c swps: 6 count, 16 rounds, 4264 queries (266.5/round)
c swps: 4275 sat calls, 21 unsat (0.8% success rate)
c swps: 155871 decisions 36.5, 3537 conflicts 0.8
c swps; 142.9 avg class size, 178.5 avg environment size
c swps: 0 failed, 23 impls, 10 equivs
c swp0: 1416 type 0 queries, 54 unsat (3.8%), 1415 sat (99.9%)
c swp1: 2848 type 1 queries, 293 unsat (10.3%), 2839 sat (99.7%)
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: 71561696 calls to obtain time
c tops: 902 fixed 22%, 0 its, 0.00 confs/it
c trds: 11 transitive reductions, 177 removed, 0 failed
c trds: 66300 nodes, 6746 edges, 11268 steps
c trim: 210044 words, 0.8 MB
c trnr: 11 count, 110 bin, 1160 trn, 22130405 steps
c unhd: 4 count, 5 rounds, 3238033 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: 1477 tauts, 1 bin 0%, 1156 trn 78%, 305 lrg 21%
c unhd: 1477 tauts, 15 stamp 1%, 958 red 65%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 29996 str, 0 bin 0%, 145 trn 0%, 29851 lrg 100%, 29855 red 100%
c vars: 3022 remaining 73% and 1106 removed 27% out of 4128
c vars: 902 fixed 22%, 108 eliminated 3%, 96 equivalent 2%
c vsts: 36762382663 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 65.2 search visits per propagation, 6908.1 per conflict
c wchs: 10891356069 pushed, 13534961 enlarged, 1176 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        5291114       3543076       1473024     235277225      52434584       2634816
c 
c  0 0        194531   4       434   0         0   0 189237054  80< 37903661  72   1902459  72     6.2
c  1 5        220756   4     91681   3    107871   7  25300596  11   5721924  11<   305555  12<    0.8
c  2 6        724313  14    411505  12    288913  20  10688738   5   3193996   6    160325   6     1.3
c  3 9        782136  15    520975  15    254364  17   3385218   1   1543067   3     64105   2     1.0
c  4 14       699821  13    503976  14    191624  13   2076804   1   1130040   2     48040   2     1.3
c  5 21       599222  11<   442080  12<   153298  10<  1366963   1    812057   2     35664   1     1.9
c  6 30       499122   9    374467  11    121571   8    918394   0    580234   1     27539   1     2.4
c  7 41       418530   8    319221   9     96657   7    671135   0    441599   1     22256   1     3.1
c  8 54       349578   7    270638   8     76455   5    513794   0    348531   1     19139   1     3.7
c  9 69       284754   5    222338   6     59626   4    398890   0    275814   1     16447   1     4.2
c 10 86       374379   7    288613   8     81061   6    519714   0    357128   1     23524   1     8.0
c 11 126      126733   2     88919   3     36051   2    174957   0    111500   0      8654   0     4.3
c 12 230       17239   0      8229   0      5533   0     24968   0     15033   0      1109   0     0.8
c 
c avg                  5.0           5.5           4.6           0.4           0.8           0.8
c std                  2.9           2.7           2.7           1.2           1.8           1.9
c 
c   43.886   4% bump
c   20.776   2% decide
c    2.484   0% cce
c 
c    5.239 < 1% rest (below)
c 
c    2.095   0% sweep
c    1.823   0% elim
c    1.059   0% quatres
c    0.725   0% probe
c    0.530   0% unhide
c    0.431   0% block
c    0.315   0% gauss
c    0.146   0% card
c    0.129   0% ternres
c    0.062   0% bca
c    0.019   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.376   0% preprocessing     3%
c   10.815   1% inprocessing     97%
c ==================================
c   11.191   1% simplifying
c  988.752  99% search
c ==================================
c  999.944 100% all
c 
c       5319719 conflicts,        5320.0 confs/sec
c          2065 ternaries,        2576.1 confs/ternary
c            92 binaries,        57823.0 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            80 reductions,          0.1 redus/sec,  66496.5 confs/reduction
c         36281 restarts,           36.3 rests/sec,    146.6 confs/restart
c      30489830 decisions,       30491.5 decis/sec,      5.7 decis/conflict
c     563879295 propagations,   563910.9 props/sec,     18.5 props/decision
c 
c 999.9 seconds, 108.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
