c launch: /data/cnf/sc2014/app/010-22-160.cnf.bz2
c host: atom02
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/010-22-160.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/010-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=3
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 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] SUM (--score=3)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0    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 968 variables
c [simpleprobe-1] all 3160 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 3 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 3 variables, found 16 hbrs, 2 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 789 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 78 variables 2% in round 1 in 2457204 steps
c [elim-1-1] backward subsumption/strengthening limit 2457200
c [elim-1-1-1] backward checking 1327 touched variables 42%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 9 and strengthened 76 clauses in 757363 steps
c [elim-1-1] rescheduled 152 variables 5% by backward subsumption
c [elim-1-2] eliminated 3 variables 0% in round 2 in 109840 steps
c [elim-1-2] backward subsumption/strengthening limit 109800
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 0 and strengthened 1 clauses in 91329 steps
c [elim-1-2] rescheduled 4 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 2273 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 82 = 3% variables out of 3157 scheduled
c [phase-count-1] 56135 negative 99.0% of 56708 except 573 1.0%
c [phase-count-1] 55920 positive 98.6% of 56708 except 788 1.4%
c [phase-1] phase bias: 1349 positive 44%, 1726 negative 56%
c [sort-queue-1] sorted 3075 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 3075 (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 160 variables 4.9% (3075 remain 86%)
c [simplification-1] removed 15551 irredundant clauses 21.5% (56708 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 1001 conflicts
c [simpleprobe-2] all 3075 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1345 variables remain 44% (1730 retained 56%)
c [simpleprobe-2] removed 0 variables, found 10 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6150 literals 100%
c [treelook-1] scheduling used 246154 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300071 steps
c [treelook-1] 4832 literals remain 79%
c [treelook-1] 3063 variables remain to probed next time 100%
c [decomp-5] removed 1 variables
c [treelook-1] removed 4 variables, found 15 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 370 sched 12%, 1 failed, 0 lifted, 14 hbrs
c [decomp-6] removed 2 variables
c [basicprobe-1-1] 371 sched 12%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-1-2] 372 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 2 variables, found 16 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 3069 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 87 blocked clauses
c [block-1] 87 < 1/100 * 56664 = 566 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2832 clauses out of 16847 (17%) of length 7
c [cce-1-1] eliminated 328 clauses out of 16034 (2%) of length 6
c [cce-1-1] eliminated 2142 clauses out of 12299 (17%) of length 5
c [cce-1-1] eliminated 592 clauses out of 6431 (9%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 5894 large clauses in 25478791 steps
c [cce-1-1] allowing another 12739395 steps for small clauses
c [cce-1-1] scheduling 4314 clauses = 248 binary + 4066 ternary
c [cce-1-1] tried to eliminate 4314 small clauses 100%
c [cce-1-1] eliminated 12 binary clauses 5%
c [cce-1-1] eliminated 1040 ternary clauses 26%
c [cce-1-1] eliminated 1052 small clauses 24%
c [cce-1-1] eliminated 1052 small clauses in 13769975 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 6946 covered clauses in round 1
c [cce-1-2] eliminated 36 clauses out of 14015 (0%) of length 7
c [cce-1-2] incomplete large round (ABCE)
c [cce-1-2] eliminated 36 large clauses in 16230061 steps
c [cce-1-2] allowing another 8115030 steps for small clauses
c [cce-1-2] scheduling 3262 clauses = 236 binary + 3026 ternary
c [cce-1-2] tried to eliminate 3262 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 3655098 steps for small clauses
c [cce-1-3] scheduling 3262 clauses = 236 binary + 3026 ternary
c [cce-1-3] tried to eliminate 3262 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 6982 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3069 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 385 not tried 13% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 14 = 0% variables out of 3069 scheduled
c [elim-2] 14 < 1/100 * 3069 = 30 considered unsuccessful
c [bca-1] limit of 10000000 steps and 99150 added (scaled 2)
c [bca-1] 3858 out of 6112 literals actually usable 63%
c [bca-1] added 0 blocked clauses in 24755 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1450 pos 47.5% + 1605 neg 52.5% = 3055 sched 100.0% ret 0
c [sweep-1-1] 447181 steps 556 queries 147.22 avg class size
c [sweep-1-1] 8361 decisions 554 SAT calls 21.29 avg env size
c [sweep-1-1] fully completed sweeping round
c [decomp-8] removed 8 variables
c [sweep-1-1] removed 8 vars (0 failed, 7 eqs, 8 impls)
c [sweep-1-2] 1445 pos 47.4% + 1602 neg 52.6% = 3047 sched 100.0% ret 0
c [sweep-1-2] 398897 steps 522 queries 152.43 avg class size
c [sweep-1-2] 7637 decisions 524 SAT calls 21.17 avg env size
c [sweep-1-2] fully completed sweeping round
c [decomp-9] removed 3 variables
c [sweep-1-2] removed 3 vars (0 failed, 1 eqs, 1 impls)
c [sweep-1-3] 1443 pos 47.4% + 1601 neg 52.6% = 3044 sched 100.0% ret 0
c [sweep-1-3] 154773 steps 161 queries 471.17 avg class size
c [sweep-1-3] 2891 decisions 161 SAT calls 24.99 avg env size
c [sweep-1-3] 1969 variables remain 65% (1075 retained 35%)
c [sweep-1-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] removed 11 vars in TOTAL (3 rounds, 1236 queries)
c [sort-queue-2] sorted 196 enqueued variables after 1001 conflicts
c [score-dist-2] active 2848 (94%), one 0 (0%), zero 196 (6%)
c [score-dist-2] max exp 517, different 14 (3%)
c [score-dist-2] median active exp 514, avg 513.5
c [simplification-2] removed 31 variables 1.0% (3044 remain 85%)
c [simplification-2] removed 7405 irredundant clauses 13.1% (49299 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 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
c 
c [simplification-3] limit 3001 conflicts (hard 13001) hit after 3001 conflicts
c [quatres-1] found 6404 quaternary clauses 14% in total
c [quatres-1-1] added 20 double-self-subsuming ternary resolvents
c [quatres-1-2] added 114 single-self-subsuming ternary resolvents
c [quatres-1-2] added 415 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 3044 free variables schedulable
c [ternres-1] 407 ternary resolvents (29 bin, 378 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 6 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 6 out of 6 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 3244 xors of average arity 5.0
c [gauss-1] connected 16298 occurrences of 752 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 3 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 6071 literals 100%
c [treelook-2] scheduling used 234025 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 300050 steps
c [treelook-2] 4624 literals remain 76%
c [treelook-2] 2466 variables remain to probed next time 81%
c [treelook-2] removed 0 variables, found 39 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 154 tauts, 0 hbrs, 251 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 18 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 180 clauses out of 16101 (1%) of length 6
c [cce-2-1] eliminated 23 clauses out of 10240 (0%) of length 5
c [cce-2-1] eliminated 63 clauses out of 5855 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 266 large clauses in 22469693 steps
c [cce-2-1] allowing another 11234846 steps for small clauses
c [cce-2-1] scheduling 952 clauses = 272 binary + 680 ternary
c [cce-2-1] tried to eliminate 952 small clauses 100%
c [cce-2-1] eliminated 3 binary clauses 1%
c [cce-2-1] eliminated 64 ternary clauses 9%
c [cce-2-1] eliminated 67 small clauses 7%
c [cce-2-1] eliminated 67 small clauses in 11395153 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 333 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 9302445 steps for small clauses
c [cce-2-2] scheduling 885 clauses = 269 binary + 616 ternary
c [cce-2-2] tried to eliminate 885 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 333 covered clauses in TOTAL during 2 rounds
c [cce-2] 333 < 1/100 * 49289 = 492 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 946 pos 48.1% + 1021 neg 51.9% = 1967 sched 64.7% ret 1074
c [sweep-2-1] 365165 steps 405 queries 109.26 avg class size
c [sweep-2-1] 8398 decisions 405 SAT calls 27.91 avg env size
c [sweep-2-1] fully completed sweeping round
c [decomp-13] removed 2 variables
c [sweep-2-1] removed 2 vars (0 failed, 2 eqs, 4 impls)
c [sweep-2-2] 1455 pos 47.9% + 1584 neg 52.1% = 3039 sched 100.0% ret 0
c [sweep-2-2] 439960 steps 456 queries 118.29 avg class size
c [sweep-2-2] 10038 decisions 456 SAT calls 30.86 avg env size
c [sweep-2-2] fully completed sweeping round
c [decomp-14] removed 2 variables
c [sweep-2-2] removed 2 vars (0 failed, 1 eqs, 2 impls)
c [sweep-2-3] 1454 pos 47.9% + 1583 neg 52.1% = 3037 sched 100.0% ret 0
c [sweep-2-3] 195129 steps 160 queries 297.96 avg class size
c [sweep-2-3] 4527 decisions 159 SAT calls 40.94 avg env size
c [sweep-2-3] 1527 variables remain 50% (1510 retained 50%)
c [sweep-2-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 4 vars in TOTAL (3 rounds, 1018 queries)
c [sort-queue-3] sorted 64 enqueued variables after 3001 conflicts
c [score-dist-3] active 2973 (98%), one 0 (0%), zero 64 (2%)
c [score-dist-3] max exp 520, different 14 (3%)
c [score-dist-3] median active exp 517, avg 516.9
c [simplification-3] removed 7 variables 0.2% (3037 remain 85%)
c [simplification-3] removed 351 irredundant clauses 0.7% (48948 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 23001 (soft 13001 + delta 10000)
c [simplification-3] new conflict limit 13001 (hard 23001)
c 
c [simplification-4] limit 13001 conflicts (hard 23001) hit after 13003 conflicts
c [quatres-2] found 6843 quaternary clauses 14% in total
c [quatres-2-1] added 18 double-self-subsuming ternary resolvents
c [quatres-2-2] added 124 single-self-subsuming ternary resolvents
c [quatres-2-2] added 368 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3037 free variables schedulable
c [ternres-2] 273 ternary resolvents (14 bin, 259 trn)
c [ternres-2] fully completed ternary resolution
c [basicprobe-2] limit 2268265 penalty 0 = 0 + 0
c [basicprobe-2-0] 512 sched 17%, 1 failed, 0 lifted, 16 hbrs
c [decomp-17] removed 1 variables
c [basicprobe-2-1] 514 sched 17%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-2-1] removed 1 variables, found 16 hbrs
c [bate-1] eliminated 35 asymmetric tautologies during probing
c [transred-2] limit 453653 with penalty 0 = 0 + 0
c [transred-2] removed 16 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3036 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 [elim-3] 385 variables 13% will be scheduled this time
c [elim-3] scheduled 385 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 107 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 385 scheduled
c [bca-2] limit of 10000000 steps and 98298 added (scaled 2)
c [bca-2] 257 out of 6074 literals actually usable 4%
c [bca-2] added 0 blocked clauses in 15884 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 776 pos 50.8% + 751 neg 49.2% = 1527 sched 50.3% ret 1509
c [sweep-3-1] 391632 steps 245 queries 54.72 avg class size
c [sweep-3-1] 13978 decisions 247 SAT calls 155.81 avg env size
c [sweep-3-1] fully completed sweeping round
c [decomp-18] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3-2] 1510 pos 49.8% + 1525 neg 50.2% = 3035 sched 100.0% ret 0
c [sweep-3-2] 490785 steps 290 queries 88.19 avg class size
c [sweep-3-2] 16181 decisions 291 SAT calls 162.23 avg env size
c [sweep-3-2] fully completed sweeping round
c [sweep-3-2] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-3-3] 1510 pos 49.8% + 1525 neg 50.2% = 3035 sched 100.0% ret 0
c [sweep-3-3] 117967 steps 58 queries 413.26 avg class size
c [sweep-3-3] 4094 decisions 57 SAT calls 199.77 avg env size
c [sweep-3-3] 2071 variables remain 68% (964 retained 32%)
c [sweep-3-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] 1 < 1/1000 * 3036 = 3 considered unsuccessful
c [sweep-3] removed 1 vars in TOTAL (3 rounds, 590 queries)
c [sort-queue-4] sorted 21 enqueued variables after 13003 conflicts
c [score-dist-4] active 3014 (99%), one 0 (0%), zero 21 (1%)
c [score-dist-4] max exp 525, different 17 (3%)
c [score-dist-4] median active exp 523, avg 522.6
c [simplification-4] removed 2 variables 0.1% (3035 remain 85%)
c [simplification-4] removed 51 irredundant clauses 0.1% (48897 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 58003 (soft 43003 + delta 15000)
c [simplification-4] new conflict limit 43003 (hard 58003)
c 
c [simplification-5] limit 43003 conflicts (hard 58003) hit after 43003 conflicts
c [quatres-3] found 7355 quaternary clauses 15% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 16 double-self-subsuming ternary resolvents
c [quatres-3-2] added 76 single-self-subsuming ternary resolvents
c [quatres-3-2] added 272 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3035 free variables schedulable
c [ternres-3] 47 ternary resolvents (4 bin, 43 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1684 xors of average arity 5.0
c [gauss-2] connected 8348 occurrences of 477 variables (average 17.5)
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 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 2 transitive binary clauses
c [transred-3] found 1 units
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500022 steps for small clauses
c [cce-3-1] scheduling 3295 clauses = 292 binary + 3003 ternary
c [cce-3-1] tried to eliminate 3295 small clauses 100%
c [cce-3-1] eliminated 15 ternary clauses 0%
c [cce-3-1] eliminated 15 small clauses 0%
c [cce-3-1] eliminated 20 small clauses in 8370463 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 3314772 steps for small clauses
c [cce-3-2] scheduling 3280 clauses = 292 binary + 2988 ternary
c [cce-3-2] tried to eliminate 3280 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 * 48897 = 488 considered unsuccessful
c [sort-queue-5] sorted 6 enqueued variables after 43003 conflicts
c [score-dist-5] active 3028 (100%), one 0 (0%), zero 6 (0%)
c [score-dist-5] max exp 529, different 16 (3%)
c [score-dist-5] median active exp 527, avg 526.5
c [simplification-5] removed 1 variables 0.0% (3034 remain 85%)
c [simplification-5] removed 20 irredundant clauses 0.0% (48877 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 133003 (soft 103003 + delta 30000)
c [simplification-5] new conflict limit 103003 (hard 133003)
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.3    3034    48877     55571   23478   2352   175  106   387   12  27%    578  185  147   46  323%
c -   22.8    3034    48877     91225   29463   2358   175  118   382   14  31%    765  105   74   77   96%
c 
c [simplification-6] limit 103003 conflicts (hard 133003) hit after 103003 conflicts
c [quatres-4] found 7594 quaternary clauses 15% in total
c [quatres-4-1] added 10 double-self-subsuming ternary resolvents
c [quatres-4-2] added 45 single-self-subsuming ternary resolvents
c [quatres-4-2] added 160 quaternary resolvents
c [ternres-4] limit 6141944 with penalty 0 = 0 + 0
c [ternres-4] all 3034 free variables schedulable
c [ternres-4] 8 ternary resolvents (2 bin, 6 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 767743 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] found 24 at-most-two constraints of average size 4.1
c [card-3] using previous limit 767743 for elimination
c [card-3] 26 out of 27 constraints (96%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 1330 schedulable variables 44%
c [simpleprobe-3] limit 12283888 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 36 hbrs, 0 units
c [unhide-3] limit 307097 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 50 tauts, 0 hbrs, 16858 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 20 transitive binary clauses
c [sweep-4] limit 921291 penalty 1 = 1 + 0
c [sweep-4-1] 1004 pos 48.5% + 1066 neg 51.5% = 2070 sched 68.2% ret 964
c [sweep-4-1] 703299 steps 266 queries 57.36 avg class size
c [sweep-4-1] 19583 decisions 265 SAT calls 248.23 avg env size
c [sweep-4-1] fully completed sweeping round
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4-2] 1460 pos 48.1% + 1574 neg 51.9% = 3034 sched 100.0% ret 0
c [sweep-4-2] 220882 steps 74 queries 253.70 avg class size
c [sweep-4-2] 5889 decisions 73 SAT calls 307.58 avg env size
c [sweep-4-2] 1441 variables remain 47% (1593 retained 53%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 338 queries)
c [score-dist-6] active 3034 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-6] max exp 532, different 17 (3%)
c [score-dist-6] median active exp 530, avg 529.7
c [simplification-6] removed 0 variables 0.0% (3034 remain 85%)
c [simplification-6] removed 1 irredundant clauses 0.0% (48876 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 283003 (soft 223003 + delta 60000)
c [simplification-6] new conflict limit 223003 (hard 283003)
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 -   32.9    3034    48876    125557   30834   2439   212  137   374   14  37%    871   57  155  108  143%
c -   46.0    3034    48876    170001   29093   2444   212  278   354   20  79%    946    9  106  160   66%
c -   52.2    3034    48876    202195   31609   2444   212   87   368   17  24%    976   15   65  136   48%
c 
c [simplification-7] limit 223003 conflicts (hard 283003) hit after 223003 conflicts
c [quatres-5] found 7764 quaternary clauses 15% in total
c [quatres-5-1] added 10 double-self-subsuming ternary resolvents
c [quatres-5-2] added 55 single-self-subsuming ternary resolvents
c [quatres-5-2] added 131 quaternary resolvents
c [ternres-5] limit 13848536 with penalty 0 = 0 + 0
c [ternres-5] all 3034 free variables schedulable
c [ternres-5] 116 ternary resolvents (19 bin, 97 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-26] removed 1 variables
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 13 transitive binary clauses
c [transred-5] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 3032 variables 100%
c [block-3] limit of 34621341 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 3032 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1384853660 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 2 variables 0% in round 1 in 34577191 steps
c [elim-4-1] backward subsumption/strengthening limit 34577100
c [elim-4-1-1] backward checking 495 touched variables 16%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 0 clauses in 265716 steps
c [elim-4-1] rescheduled 3 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 1954 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 2 = 0% variables out of 3032 scheduled
c [elim-4] 2 < 1/100 * 3032 = 30 considered unsuccessful
c [bca-3] limit of 10000000 steps and 98136 added (scaled 2)
c [bca-3] 114 out of 6062 literals actually usable 2%
c [bca-3] added 0 blocked clauses in 52300 steps
c [score-dist-7] active 3030 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-7] max exp 535, different 18 (3%)
c [score-dist-7] median active exp 533, avg 532.2
c [simplification-7] removed 4 variables 0.1% (3030 remain 84%)
c [simplification-7] removed 58 irredundant clauses 0.1% (48818 remain 68%)
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 583003 (soft 463003 + delta 120000)
c [simplification-7] new conflict limit 463003 (hard 583003)
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 -   61.4    3030    48818    237172   31111   2482   193  300   405   14  74%    996   37  263  149  177%
c -  102.6    3030    48818    379797   29380   2488   195  281   326   16  86%   1021  -37  264  310   85%
c -  115.7    3030    48818    426812   31679   2496   196  214   308   22  69%   1022  -31  211  275   77%
c -  123.4    3030    48818    461224   33524   2500   197  124   403   18  31%   1023   42  152  208   73%
c 
c [simplification-8] limit 463003 conflicts (hard 583003) hit after 463005 conflicts
c [quatres-6] found 7871 quaternary clauses 15% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-1] added 4 double-self-subsuming ternary resolvents
c [quatres-6-2] added 45 single-self-subsuming ternary resolvents
c [quatres-6-2] added 100 quaternary resolvents
c [ternres-6] limit 26909620 with penalty 0 = 0 + 0
c [ternres-6] all 3030 free variables schedulable
c [ternres-6] 33 ternary resolvents (3 bin, 30 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1345481 penalty 2 = 2 + 0
c [gauss-3] extracted 3120 xors of average arity 5.0
c [gauss-3] connected 15504 occurrences of 712 variables (average 21.8)
c [gauss-3] limit 1345481 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 1345481 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 4964 literals 82%
c [treelook-3] scheduling used 322411 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1345481 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 1021468 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 16 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 8 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 336370257 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 26 clauses out of 10225 (0%) of length 5
c [cce-4-1] eliminated 30 clauses out of 5715 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 56 large clauses in 22204927 steps
c [cce-4-1] allowing another 11102463 steps for small clauses
c [cce-4-1] scheduling 949 clauses = 298 binary + 651 ternary
c [cce-4-1] tried to eliminate 949 small clauses 100%
c [cce-4-1] eliminated 1 binary clauses 0%
c [cce-4-1] eliminated 6 ternary clauses 1%
c [cce-4-1] eliminated 7 small clauses 1%
c [cce-4-1] eliminated 7 small clauses in 11265497 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 63 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 11103821 steps for small clauses
c [cce-4-2] scheduling 942 clauses = 297 binary + 645 ternary
c [cce-4-2] tried to eliminate 942 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 63 covered clauses in TOTAL during 2 rounds
c [cce-4] 63 < 1/100 * 48818 = 488 considered unsuccessful
c [score-dist-8] active 3030 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-8] max exp 538, different 17 (3%)
c [score-dist-8] median active exp 534, avg 534.1
c [simplification-8] removed 0 variables 0.0% (3030 remain 84%)
c [simplification-8] removed 63 irredundant clauses 0.1% (48755 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 1183005 (soft 943005 + delta 240000)
c [simplification-8] new conflict limit 943005 (hard 1183005)
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 -  133.1    3030    48755    495085   34806   2582   209  121   415   23  29%   1023   32  118  174   68%
c -  140.6    3030    48755    528233   35773   2582   209   86   425   21  20%   1024   28   74  146   51%
c -  148.1    3030    48755    561406   35422   2582   209   96   424   20  23%   1024   16   95  124   77%
c -  156.9    3030    48755    596268   35386   2586   209  128   442   24  29%   1024   22  128  122  105%
c -  167.1    3030    48755    632565   34629   2588   209  129   440   24  29%   1024   11  130  129  100%
c -  177.7    3030    48755    670785   35541   2589   209  137   432   25  32%   1024   -2  149  136  110%
c -  187.7    3030    48755    709646   36698   2600   209  151   406   23  37%   1024  -20  155  142  110%
c -  201.7    3030    48755    758695   36158   2608   209  241   371   19  65%   1024  -34  241  188  128%
c -  243.8    3030    48755    900768   37221   2614   210  262   317   29  83%   1024  -22  248  289   86%
c -  261.5    3030    48755    963541   38194   2637   212  227   299   28  76%   1024  -20  233  262   89%
c -  283.5    3030    48755   1040963   37895   2644   212  247   289   30  86%   1024  -11  249  251   99%
c 
c [simplification-9] limit 943005 conflicts (hard 1183005) hit after 1051636 conflicts
c [quatres-7] found 8073 quaternary clauses 15% in total
c [quatres-7-1] added 12 double-self-subsuming ternary resolvents
c [quatres-7-2] added 63 single-self-subsuming ternary resolvents
c [quatres-7-2] added 143 quaternary resolvents
c [ternres-7] limit 72344829 with penalty 0 = 0 + 0
c [ternres-7] all 3030 free variables schedulable
c [ternres-7] 31 ternary resolvents (3 bin, 28 trn)
c [ternres-7] fully completed ternary resolution
c [basicprobe-3] limit 361724145 penalty 0 = 0 + 0
c [basicprobe-3-0] 559 sched 18%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-1] 560 sched 18%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] removed 0 variables, found 1 hbrs
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 3 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 54258620 penalty 2 = 2 + 0
c [sweep-5-1] 734 pos 51.0% + 706 neg 49.0% = 1440 sched 47.5% ret 1590
c [sweep-5-1] 695568 steps 327 queries 62.62 avg class size
c [sweep-5-1] 16033 decisions 326 SAT calls 148.66 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] 1528 pos 50.4% + 1502 neg 49.6% = 3030 sched 100.0% ret 0
c [sweep-5-2] 767463 steps 356 queries 98.60 avg class size
c [sweep-5-2] 17500 decisions 356 SAT calls 142.67 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] 1528 pos 50.4% + 1502 neg 49.6% = 3030 sched 100.0% ret 0
c [sweep-5-3] 786135 steps 366 queries 76.86 avg class size
c [sweep-5-3] 17075 decisions 367 SAT calls 138.33 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 4 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 1046 queries)
c [score-dist-9] active 3030 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-9] max exp 540, different 15 (3%)
c [score-dist-9] median active exp 536, avg 536.3
c [simplification-9] removed 0 variables 0.0% (3030 remain 84%)
c [simplification-9] removed 0 irredundant clauses 0.0% (48755 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 2491636 (soft 2011636 + delta 480000)
c [simplification-9] new conflict limit 2011636 (hard 2491636)
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 -  298.3    3030    48755   1100977   41384   2875   224  119   372   22  32%   1024   55  119  202   59%
c -  308.6    3030    48755   1141972   42880   2876   224  100   368   27  27%   1024   28  101  159   64%
c -  319.3    3030    48755   1182390   43334   2877   224   98   374   26  26%   1024   20  100  135   74%
c -  331.7    3030    48755   1224367   43132   2879   224  121   381   24  32%   1024   15  122  129   95%
c -  349.6    3030    48755   1269818   43425   2880   224  152   379   30  40%   1024    6  115  137   84%
c -  366.0    3030    48755   1315713   43381   2880   224  165   382   31  43%   1024    5  171  145  118%
c -  376.0    3030    48755   1358890   44133   2881   224   79   407   27  19%   1024   16   86  112   76%
c -  389.1    3030    48755   1403242   45134   2882   224  121   404   27  30%   1024    5  127  112  113%
c -  403.3    3030    48755   1448444   44668   2882   224  152   408   29  37%   1024    7  175  121  145%
c -  420.7    3030    48755   1497336   45320   2882   224  141   408   32  35%   1024    2  133  143   93%
c -  438.4    3030    48755   1546547   46352   2882   224  127   401   34  32%   1024   -3  167  140  119%
c -  455.9    3030    48755   1595450   47056   2887   224  113   388   33  29%   1024  -10  124  134   92%
c -  472.6    3030    48755   1643376   47535   2887   224  135   400   34  34%   1024    4  105  135   78%
c -  488.1    3030    48755   1691715   47518   2895   224  120   384   36  31%   1024   -7  121  141   86%
c -  504.3    3030    48755   1742890   47366   2900   224  159   378   39  42%   1024   -8  156  169   93%
c -  521.2    3030    48755   1795924   48490   2902   224  158   376   43  42%   1024   -7  145  183   79%
c -  541.3    3030    48755   1849837   48159   2905   224  237   362   42  65%   1024  -12  236  220  107%
c -  580.9    3030    48755   1965675   49469   2907   224  280   325   47  86%   1024  -15  295  280  105%
c -  610.0    3030    48755   2046892   51637   2907   224  236   322   46  73%   1024   -4  193  270   72%
c -  629.5    3030    48755   2106752   52034   2907   224  261   319   48  82%   1024   -4  268  263  102%
c 
c [simplification-10] limit 2011636 conflicts (hard 2491636) hit after 2331013 conflicts
c [quatres-8] found 8469 quaternary clauses 15% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-1] added 15 double-self-subsuming ternary resolvents
c [quatres-8-2] added 98 single-self-subsuming ternary resolvents
c [quatres-8-2] added 140 quaternary resolvents
c [ternres-8] limit 199952814 with penalty 0 = 0 + 0
c [ternres-8] all 3030 free variables schedulable
c [ternres-8] 23 ternary resolvents (0 bin, 23 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 12497050 penalty 3 = 3 + 0
c [card-4] found 2 at-most-one constraints of average size 3.0
c [card-4] found 24 at-most-two constraints of average size 4.1
c [card-4] using previous limit 12497050 for elimination
c [card-4] 25 out of 26 constraints (96%) meet size limits
c [card-4] no units found
c [card-4] generated 6 at-most-one constraints, 1 used 17%
c [card-4] exported 1 binary clauses, 1.0 per/constraint
c [unhide-4] limit 312500 with penalty 6 = 3 + 3
c [unhide-4-4] 0 units, 0 failed, 236 tauts, 0 hbrs, 352174 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 8 transitive binary clauses
c [score-dist-10] active 3030 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-10] max exp 542, different 16 (3%)
c [score-dist-10] median active exp 539, avg 538.8
c [simplification-10] removed 0 variables 0.0% (3030 remain 84%)
c [simplification-10] removed 0 irredundant clauses 0.0% (48755 remain 67%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 960000
c [simplification-10] new conflict interval 1920000
c [simplification-10] penalized conflict interval 1920000 = 1 * 1920000
c [simplification-10] hard conflict limit 5211013 (soft 4251013 + delta 960000)
c [simplification-10] new conflict limit 4251013 (hard 5211013)
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 -  697.2    3030    48755   2331959   50926   2846   224  189   292   38  65%   1024   22   49  256   19%
c -  710.2    3030    48755   2384922   54036   2848   224  119   384   32  31%   1024   54  104  175   59%
c -  723.8    3030    48755   2437103   55030   2848   224   92   387   38  24%   1024   26   92  140   66%
c 1  739.1    3030    48755   2485336  100203   2848   224  119   388  109  31%   1024   13  107  132   81%
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 
s SATISFIABLE
c
c bate: 35 basic ate = 35 trn 100% + 0 lrg 0% in 1 updates
c bcas: 3 count, 0 added (0 skipped), 92939 steps
c bkwd: tried 4610 clauses, 9154 lits, 1.99 lits/clause
c bkwd: checked 378558 occs, 82.12 occs/clause, 41.35 occs/lit
c bkwd: subsumed 0 binary, 6 ternary, 4 large
c bkwd: strengthened 0 binary, 5 ternary (100% self), 72 large (0% self)
c blkd: 3 bces, 87 removed, 1888552 resolutions, 3902478 steps
c blkd: 29 blocking literals 0%, 0 pure
c bump: 2481087 bumped seen, 1033433275 lits 416.5 on average
c card: 4 count, 0 units, 1 am1, 17904027 steps
c card: 2 rescheduled, 18 eliminated, 81149 resolved, 3644 subsumed
c card: 8 at-most-one constraints found, average size 3.00
c card: 8 at-most-one constraints used 100%, average size 3.00
c card: 60 at-most-two constraints found, average size 4.07
c card: 58 at-most-two constraints used 97%, average size 4.07
c cces: 4 cces, 7393 eliminated, 7357 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: 44 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 34 decompositions, 97 equivalent 2%
c deco: 750922 decision-only clauses 30%, 41% reduction
c decs: 10273859 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 4 elims, 97 eliminated 2%, 0 pure 0%
c elms: 7 rounds, 1.8 rounds/bve
c elms: 97 small 100%, 0 large 0%
c elms: 1267 tried small, 97 succeeded 8%, 1170 failed 92%
c elms: 2441 subsumed, 2743 strengthened, 1 blocked
c elms: 677553 copies, 1604029 resolutions, 324614 ipos
c elms: 119760 subchks, 81661 strchks
c gaus: 3 extractions, 8048 extracted, 5.0 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8691056 steps, 4345528 extr 50%, 255848 elim 3%
c glue: 194.9 orig avg, 194.9 real avg, 10.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 199 = 62 simple 31% + 118 trn 59% + 19 lrg 10%, 36 sub 18%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2481087 clauses, 270.2 length
c lrnd: 670405386 lits = 864064725 orig - 193659339 removed 22%
c lrnd: 622369 uips 25%, 1383155 flips 56%
c mins: 1223454 mins 62%, 30 bin 0%, 10641 size 1%
c mins: 138198591 poisoned searches, 15029769 hits, 11% hit rate
c mins: 303226748 used twice searches, 86026163 hits, 28% hit rate
c move: moved 1445, 16 bin 1%, 1429 trn 99%
c otfs: 8790 driving 17%, 41492 restarting 83%
c otfs: str 50282, 49790 red 99%, 492 irr 1%
c otfs: str 50282, 0 bin 0%, 103 trn 0%, 50179 lrg 100%
c otfs: sub 508, 504 red 99%, 4 irr 1%
c otfs: sub 508, 0 bin 0%, 10 trn 2%, 498 lrg 98%
c phas: 1 computed, 3075 set, 1349 pos (44%), 1726 neg (56%)
c prbs: 3 basic, 6514 probed, 2 failed, 0 lifted
c prbs: 3 simple, 13693 probed, 2 failed, 2 eqs
c prbs: 3 treelook, 7726 probed, 2 failed, 0 lifted
c prom: 34713 locked 1% out of 4387662 tried
c prps: 484663559 props, 47 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 8 count, 1729 quat, 620 self1, 105 self2, 4 dup
c queu: 5 sorted, 10273859 next (280478 steps 0.03)
c queu: 1033440765 enq (1746174533 steps 1.69), 1033433275 deq 100%
c redc: 38 clauses 0%, 14784 tried 1%, 0 sat 0%
c redc: 42 lits 0%, 118488 tried 0%, 0 sat 0%
c redc: 1 times jump level reduced, 4.0 levels on average
c reds: 43 count, 57798.5 conflicts per reduce
c reds: 0 memlim 0%, 43 arith 100%
c reds: 1527023 collected 90%, 165476 retired 10%
c rmbd: 21 removed, 7 red 33%
c rsts: 11485 restarts 86%, 1880 skipped 14%
c rsts: 1880 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 10 count, 10 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 2481087 count (9204777 tried 3.7), 687846 sub out of 2480242 (27.7%)
c swps: 5 count, 14 rounds, 4228 queries (302.0/round)
c swps: 4241 sat calls, 25 unsat (1.1% success rate)
c swps: 152185 decisions 35.9, 4541 conflicts 1.1
c swps; 133.4 avg class size, 92.9 avg environment size
c swps: 0 failed, 21 impls, 11 equivs
c swp0: 1404 type 0 queries, 50 unsat (3.6%), 1401 sat (99.8%)
c swp1: 2824 type 1 queries, 223 unsat (7.9%), 2816 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: 25510101 calls to obtain time
c tops: 904 fixed 22%, 0 its, 0.00 confs/it
c trds: 8 transitive reductions, 88 removed, 2 failed
c trds: 48281 nodes, 3866 edges, 5823 steps
c trim: 121303 words, 0.5 MB
c trnr: 8 count, 74 bin, 864 trn, 6581371 steps
c unhd: 4 count, 4 rounds, 2122334 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: 1229 tauts, 1 bin 0%, 950 trn 77%, 267 lrg 22%
c unhd: 1229 tauts, 11 stamp 1%, 706 red 57%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 369313 str, 0 bin 0%, 73 trn 0%, 369240 lrg 100%, 369192 red 100%
c vars: 3030 remaining 73% and 1098 removed 27% out of 4128
c vars: 904 fixed 22%, 97 eliminated 2%, 97 equivalent 2%
c vsts: 21321617601 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 44.0 search visits per propagation, 8576.7 per conflict
c wchs: 4871264176 pushed, 2853415 enlarged, 104 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2481971       1527023        165476     178518620      69446977       1198056
c 
c  0 0         12796   1       112   0         0   0  71364833  40  20711414  30    215870  18     0.3
c  1 5          5889   0       140   0      4499   3  25018147  14   8546594  12     89367   7     0.1
c  2 6         10671   0      1549   0      7134   4  17183322  10<  6590316   9     79640   7     0.1
c  3 9         31389   1     11486   1     15147   9  21567790  12   8934132  13<    93621   8     0.5
c  4 14        63232   3     37045   2     18313  11  13134577   7   5857821   8     83513   7     1.1
c  5 21        93790   4     69035   5     14759   9   7343577   4   3801041   5     60513   5     1.7
c  6 30       102711   4     84759   6      9555   6   4773607   3   2366080   3     42561   4<    2.1
c  7 41        96001   4     81907   5      7299   4   3695136   2   2000960   3     37920   3     2.6
c  8 54        93337   4     81930   5      5712   3<  2081949   1   1225252   2     30584   3     2.8
c  9 69       101476   4     90901   6      5090   3   1849634   1   1177666   2     28045   2     3.3
c 10 86       260760  11<   239833  16<     9747   6   2978543   2   2009413   3     57912   5    11.6
c 11 126      463999  19    421754  28     21010  13   4183735   2   3266738   5    159151  13    35.2
c 12 230     1145920  46    406572  27     47211  29   3343770   2   2959550   4    219359  18   255.5
c 
c avg                 10.2           9.8           7.9           2.3           3.3           6.0
c std                  2.6           2.3           3.7           3.0           3.6           4.6
c 
c  182.279  25% bump
c    6.613   1% decide
c    1.914   0% cce
c 
c    4.561 < 1% rest (below)
c 
c    1.381   0% unhide
c    1.296   0% elim
c    1.248   0% sweep
c    0.788   0% probe
c    0.397   0% block
c    0.244   0% card
c    0.210   0% gauss
c    0.173   0% quatres
c    0.149   0% bca
c    0.046   0% ternres
c    0.010   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.379   0% preprocessing     4%
c    9.078   1% inprocessing     96%
c ==================================
c    9.457   1% simplifying
c  729.669  99% search
c ==================================
c  739.127 100% all
c 
c       2485336 conflicts,        3362.5 confs/sec
c           299 ternaries,        8312.2 confs/ternary
c            22 binaries,       112969.8 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            43 reductions,          0.1 redus/sec,  57798.5 confs/reduction
c         11485 restarts,           15.5 rests/sec,    216.4 confs/restart
c      10273859 decisions,       13900.0 decis/sec,      4.1 decis/conflict
c     484663559 propagations,   655724.6 props/sec,     47.2 props/decision
c 
c 739.1 seconds, 401.1 MB
c launch: done
