c launch: /data/cnf/sc2014/app/q_query_3_L90_coli.sat.cnf.bz2
c host: atom18
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/q_query_3_L90_coli.sat.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/q_query_3_L90_coli.sat.cnf.bz2
c no embedded options
c found 'p cnf 282842 1350458' header
c read 282842 variables, 1350458 clauses, 3903824 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 243248 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  243248  1268704         0       0      0     0    0     0   98   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 2389 at-most-one constraints of average size 4.1
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 2389 out of 2389 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 99068 variables
c [simpleprobe-1] all 183774 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 17603 variables
c [simpleprobe-1] 141586 variables remain 85% (24585 retained 15%)
c [simpleprobe-1] removed 17603 variables, found 10618 hbrs, 68 units
c [unhide-1] limit 52218 based on 835497 irredundant clauses
c [unhide-1-1] 88 units, 130 failed, 58 tauts, 0 hbrs, 223 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 165810 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 93991 not tried 57% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 71831 = 43% variables out of 165810 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 610926 negative 97.2% of 628528 except 17602 2.8%
c [phase-count-1] 485472 positive 77.2% of 628528 except 143056 22.8%
c [phase-count-1] less non-negative clauses 17602 than limit 62800 (10.0%)
c [phase-count-1] non-pos/non-neg = 143056/17602 = 8.13 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 93979 negative 100%
c [sort-queue-1] sorted 93979 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 93979 (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 126206 variables 57.3% (93979 remain 39%)
c [simplification-1] removed 640176 irredundant clauses 50.5% (628528 remain 50%)
c [simplification-1] maximum reduction of 57% = max (57%, 50%)
c [simplification-1] large reduction 57% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    3.4   93978   628528         1       0      0   133    0     0   50   0%      0    0    0    0    0%
c i    3.4   93643   628528       352     272     47   151    0     4   50  10%      1    4    3    0 13273%
c i    3.5   93642   628528       594     472     73   162    1     5   50  12%      1    5    4    0 9964%
c 
c [simplification-2] limit 1010 conflicts (hard 11000) hit after 1011 conflicts
c [decomp-3] removed 4631 variables
c [simpleprobe-2] 76374 schedulable variables 85%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 78 variables
c [simpleprobe-2] 76461 variables remain 86% (12809 retained 14%)
c [simpleprobe-2] removed 78 variables, found 4856 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 29151 literals 16%
c [treelook-1] scheduling used 300071 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 301134 steps
c [treelook-1] 28886 literals remain 16%
c [treelook-1] 27970 variables remain to probed next time 31%
c [decomp-5] removed 80 variables
c [treelook-1] removed 88 variables, found 1726 hbrs
c [basicprobe-1] limit 4503672 based on 562959 irredundant clauses
c [basicprobe-1-0] 38911 probes remain 44% after last round
c [basicprobe-1-0] 187 units = 151 failed (81%) + 36 lifted (19%)
c [basicprobe-1-0] removed 275 variables, found 71917 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 3 units, 24 failed, 4707 tauts, 0 hbrs, 387 literals
c [elim-2] 88858 variables 100% will be scheduled this time
c [elim-2] scheduled 88858 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 14314 not tried 16% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 47480 = 53% variables out of 88858 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 419433 negative 98.2% of 427336 except 7903 1.8%
c [phase-count-2] 316614 positive 74.1% of 427336 except 110722 25.9%
c [phase-count-2] less non-negative clauses 7903 than limit 42700 (10.0%)
c [phase-count-2] non-pos/non-neg = 110722/7903 = 14.01 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 14730 negative 100%
c [sort-queue-2] sorted 41378 enqueued variables after 1011 conflicts
c [score-dist-2] active 0 (0%), one 2882 (7%), zero 38496 (93%)
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 52264 variables 55.8% (41378 remain 17%)
c [simplification-2] removed 201192 irredundant clauses 32.0% (427336 remain 34%)
c [simplification-2] maximum reduction of 56% = max (56%, 32%)
c [simplification-2] large reduction 56% >= 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 13011 (soft 3011 + delta 10000)
c [simplification-2] new conflict limit 3011 (hard 13011)
c 
c [simplification-3] limit 3011 conflicts (hard 13011) hit after 3012 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 2381 at-most-one constraints of average size 3.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 2381 out of 2381 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 13 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 10333 literals 12%
c [treelook-2] scheduling used 300012 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 302676 steps
c [treelook-2] 10209 literals remain 12%
c [treelook-2] 6413 variables remain to probed next time 16%
c [treelook-2] removed 0 variables, found 785 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 3 failed, 1719 tauts, 0 hbrs, 4940 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 41363 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 4274 not tried 10% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2151 = 5% variables out of 41363 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 409074 negative 98.2% of 416712 except 7638 1.8%
c [phase-count-3] 314904 positive 75.6% of 416712 except 101808 24.4%
c [phase-count-3] less non-negative clauses 7638 than limit 41600 (10.0%)
c [phase-count-3] non-pos/non-neg = 101808/7638 = 13.33 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 13080 negative 100%
c [sort-queue-3] sorted 39212 enqueued variables after 3012 conflicts
c [score-dist-3] active 0 (0%), one 5259 (13%), zero 33953 (87%)
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 2166 variables 5.2% (39212 remain 16%)
c [simplification-3] removed 10549 irredundant clauses 2.5% (416712 remain 33%)
c [simplification-3] maximum reduction of 5% = max (5%, 2%)
c [simplification-3] large reduction 5% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15012 (soft 5012 + delta 10000)
c [simplification-3] new conflict limit 5012 (hard 15012)
c 
c [simplification-4] limit 5012 conflicts (hard 15012) hit after 5014 conflicts
c [decomp-8] removed 1 variables
c [basicprobe-2] limit 3333472 based on 416684 irredundant clauses
c [basicprobe-2-0] 12201 probes remain 32% after last round
c [basicprobe-2-0] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 945 variables, found 4660 hbrs
c [unhide-4] limit 103522 with penalty 0 = 0 + 0
c [unhide-4-4] 2 units, 3 failed, 206 tauts, 0 hbrs, 3381 literals
c [elim-4] 4066 variables 11% will be scheduled this time
c [elim-4] scheduled 4066 variables 11%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 275030587 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 84 = 2% variables out of 4066 scheduled
c [elim-4] 84 < 1/100 * 4066 = 40 considered unsuccessful
c [phase-count-4] 357569 negative 97.9% of 365166 except 7597 2.1%
c [phase-count-4] 266635 positive 73.0% of 365166 except 98531 27.0%
c [phase-count-4] less non-negative clauses 7597 than limit 36500 (10.0%)
c [phase-count-4] non-pos/non-neg = 98531/7597 = 12.97 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 12116 negative 100%
c [sort-queue-4] sorted 38164 enqueued variables after 5014 conflicts
c [score-dist-4] active 0 (0%), one 5865 (15%), zero 32299 (85%)
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 1048 variables 2.7% (38164 remain 16%)
c [simplification-4] removed 51530 irredundant clauses 12.4% (365166 remain 29%)
c [simplification-4] maximum reduction of 12% = max (3%, 12%)
c [simplification-4] large reduction 12% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 17014 (soft 7014 + delta 10000)
c [simplification-4] new conflict limit 7014 (hard 17014)
c 
c [simplification-5] limit 7014 conflicts (hard 17014) hit after 7014 conflicts
c [quatres-1] found 13566 quaternary clauses 25% in total
c [quatres-1-1] removed 3 duplicate quaternary clauses
c [quatres-1-1] added 2 double-self-subsuming ternary resolvents
c [quatres-1-2] added 34 single-self-subsuming ternary resolvents
c [quatres-1-2] added 2689 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 38164 free variables schedulable
c [ternres-1] 2908 ternary resolvents (0 bin, 2908 trn)
c [ternres-1] 23463 variables remain 61% (14701 retained 39%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 257 xors of average arity 2.3
c [gauss-1] connected 584 occurrences of 429 variables (average 1.4)
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-9] removed 201 variables
c [simpleprobe-3] 31948 schedulable variables 84%
c [simpleprobe-3] limit 3080267 penalty 0 = 0 + 0
c [decomp-10] removed 1 variables
c [simpleprobe-3] 32194 variables remain 85% (5768 retained 15%)
c [simpleprobe-3] removed 1 variables, found 1810 hbrs, 0 units
c [unhide-5] limit 154013 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 10 failed, 2216 tauts, 0 hbrs, 1492 literals
c [transred-1] limit 770066 with penalty 0 = 0 + 0
c [transred-1] removed 1587 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 37948 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 18086 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 12
c [cce-1-1] eliminated 1 clauses out of 172 (1%) of length 11
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 10
c [cce-1-1] eliminated 1 clauses out of 91 (1%) of length 9
c [cce-1-1] eliminated 1040 clauses out of 2141 (49%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1049 large clauses in 30000000 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 174607 clauses = 29595 binary + 145012 ternary
c [cce-1-1] tried to eliminate 9856 small clauses 6%
c [cce-1-1] eliminated 540 binary clauses 2%
c [cce-1-1] eliminated 7077 ternary clauses 5%
c [cce-1-1] eliminated 7617 small clauses 4%
c [cce-1-1] eliminated 7617 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 8666 covered clauses in round 1
c [cce-1] eliminated 8666 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 669538 added (scaled 2)
c [bca-1] 67579 out of 75872 literals actually usable 89%
c [bca-1] added 0 blocked clauses in 156445 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 10775 pos 28.4% + 27160 neg 71.6% = 37935 sched 100.0% ret 0
c [sweep-1-1] 1019533 steps 30 queries 6342.00 avg class size
c [sweep-1-1] 840 decisions 27 SAT calls 95.04 avg env size
c [sweep-1-1] 36636 variables remain 99% (400 retained 1%)
c [decomp-11] removed 902 variables
c [sweep-1-1] removed 902 vars (0 failed, 2 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 902 vars in TOTAL (1 rounds, 29 queries)
c [phase-count-5] 313512 negative 97.7% of 320839 except 7327 2.3%
c [phase-count-5] 234100 positive 73.0% of 320839 except 86739 27.0%
c [phase-count-5] less non-negative clauses 7327 than limit 32000 (10.0%)
c [phase-count-5] non-pos/non-neg = 86739/7327 = 11.84 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 10794 negative 100%
c [sort-queue-5] sorted 37033 enqueued variables after 7014 conflicts
c [score-dist-5] active 0 (0%), one 6456 (17%), zero 30577 (83%)
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 1131 variables 3.0% (37033 remain 15%)
c [simplification-5] removed 44327 irredundant clauses 12.1% (320839 remain 25%)
c [simplification-5] maximum reduction of 12% = max (3%, 12%)
c [simplification-5] large reduction 12% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 19014 (soft 9014 + delta 10000)
c [simplification-5] new conflict limit 9014 (hard 19014)
c 
c [simplification-6] limit 9014 conflicts (hard 19014) hit after 9014 conflicts
c [quatres-2] found 14881 quaternary clauses 32% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-1] added 2 double-self-subsuming ternary resolvents
c [quatres-2-2] added 18 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1454 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 22728 schedulable variables 61%
c [ternres-2] 961 ternary resolvents (2 bin, 959 trn)
c [ternres-2] 21025 variables remain 57% (16008 retained 43%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1135 at-most-one constraints of average size 3.4
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 1135 out of 1135 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-6] limit 204868 with penalty 0 = 0 + 0
c [unhide-6-6] 1 units, 0 failed, 1014 tauts, 0 hbrs, 4775 literals
c [transred-2] limit 1024341 with penalty 0 = 0 + 0
c [transred-2] removed 153 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 37032 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 173 (1%) of length 9
c [cce-2-1] eliminated 58 clauses out of 809 (7%) of length 8
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 59 large clauses in 30000025 steps
c [cce-2-1] allowing another 15000012 steps for small clauses
c [cce-2-1] scheduling 167109 clauses = 32211 binary + 134898 ternary
c [cce-2-1] tried to eliminate 4844 small clauses 3%
c [cce-2-1] eliminated 335 binary clauses 1%
c [cce-2-1] eliminated 2979 ternary clauses 2%
c [cce-2-1] eliminated 3314 small clauses 2%
c [cce-2-1] eliminated 3314 small clauses in 30000014 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 3373 covered clauses in round 1
c [cce-2] eliminated 3373 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 37031 variables 100%
c [elim-5] limit of 10243412 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 2849 not tried 8% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1587 = 4% variables out of 37031 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 11471 pos 32.7% + 23595 neg 67.3% = 35066 sched 98.9% ret 378
c [sweep-2-1] 1030270 steps 33 queries 8888.82 avg class size
c [sweep-2-1] 1096 decisions 28 SAT calls 253.29 avg env size
c [sweep-2-1] 34867 variables remain 98% (577 retained 2%)
c [decomp-13] removed 4 variables
c [sweep-2-1] removed 4 vars (0 failed, 4 eqs, 8 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 4 vars in TOTAL (1 rounds, 32 queries)
c [phase-count-6] 308049 negative 97.7% of 315223 except 7174 2.3%
c [phase-count-6] 228378 positive 72.4% of 315223 except 86845 27.6%
c [phase-count-6] less non-negative clauses 7174 than limit 31500 (10.0%)
c [phase-count-6] non-pos/non-neg = 86845/7174 = 12.11 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 7348 negative 100%
c [sort-queue-6] sorted 35440 enqueued variables after 9014 conflicts
c [score-dist-6] active 0 (0%), one 6750 (19%), zero 28690 (81%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 1593 variables 4.3% (35440 remain 15%)
c [simplification-6] removed 5616 irredundant clauses 1.8% (315223 remain 25%)
c [simplification-6] maximum reduction of 4% = max (4%, 2%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 4000
c [simplification-6] penalized conflict interval 4000 = 1 * 4000
c [simplification-6] hard conflict limit 23014 (soft 13014 + delta 10000)
c [simplification-6] new conflict limit 13014 (hard 23014)
c 
c [simplification-7] limit 13014 conflicts (hard 23014) hit after 13014 conflicts
c [quatres-3] found 17887 quaternary clauses 35% in total
c [quatres-3-1] removed 14 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 155 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1837 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 20173 schedulable variables 57%
c [ternres-3] 1076 ternary resolvents (4 bin, 1072 trn)
c [ternres-3] 18574 variables remain 52% (16866 retained 48%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 55 xors of average arity 3.0
c [gauss-2] connected 165 occurrences of 100 variables (average 1.6)
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 [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 5110 literals 7%
c [treelook-3] scheduling used 150085 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 165237 steps
c [treelook-3] 5074 literals remain 7%
c [treelook-3] 2264 variables remain to probed next time 6%
c [treelook-3] removed 0 variables, found 167 hbrs
c [unhide-7] limit 309735 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 0 failed, 2957 tauts, 0 hbrs, 2514 literals
c [transred-3] limit 1548679 with penalty 0 = 0 + 0
c [transred-3] removed 140 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 27 clauses out of 34 (79%) of length 12
c [cce-3-1] eliminated 21 clauses out of 168 (12%) of length 11
c [cce-3-1] eliminated 3 clauses out of 37 (8%) of length 10
c [cce-3-1] eliminated 1 clauses out of 746 (0%) of length 8
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 52 large clauses in 30000068 steps
c [cce-3-1] allowing another 15000034 steps for small clauses
c [cce-3-1] scheduling 140013 clauses = 29251 binary + 110762 ternary
c [cce-3-1] tried to eliminate 3664 small clauses 3%
c [cce-3-1] eliminated 294 binary clauses 1%
c [cce-3-1] eliminated 744 ternary clauses 1%
c [cce-3-1] eliminated 1038 small clauses 1%
c [cce-3-1] eliminated 1038 small clauses in 30000150 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1090 covered clauses in round 1
c [cce-3] eliminated 1090 covered clauses in TOTAL during 1 rounds
c [cce-3] 1090 < 1/100 * 312407 = 3124 considered unsuccessful
c [elim-6] 2849 variables 8% will be scheduled this time
c [elim-6] scheduled 2849 variables 8%
c [elim-6] limit of 30973593 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 1151 not tried 3% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 2849 scheduled
c [bca-2] limit of 10000000 steps and 622382 added (scaled 2)
c [bca-2] 60092 out of 70882 literals actually usable 85%
c [bca-2] added 410 blocked clauses in 145096 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 12519 pos 35.9% + 22348 neg 64.1% = 34867 sched 98.4% ret 573
c [sweep-3-1] 1010082 steps 56 queries 6454.41 avg class size
c [sweep-3-1] 904 decisions 50 SAT calls 64.54 avg env size
c [sweep-3-1] 34504 variables remain 97% (936 retained 3%)
c [decomp-16] removed 6 variables
c [sweep-3-1] removed 6 vars (0 failed, 6 eqs, 12 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 6 vars in TOTAL (1 rounds, 55 queries)
c [phase-count-7] 303774 negative 97.7% of 310941 except 7167 2.3%
c [phase-count-7] 224773 positive 72.3% of 310941 except 86168 27.7%
c [phase-count-7] less non-negative clauses 7167 than limit 31000 (10.0%)
c [phase-count-7] non-pos/non-neg = 86168/7167 = 12.02 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 6916 negative 100%
c [sort-queue-7] sorted 35434 enqueued variables after 13014 conflicts
c [score-dist-7] active 0 (0%), one 7445 (21%), zero 27989 (79%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 6 variables 0.0% (35434 remain 15%)
c [simplification-7] removed 4281 irredundant clauses 1.4% (310941 remain 25%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-7] new conflict interval 14000
c [simplification-7] penalized conflict interval 14000 = 1 * 14000
c [simplification-7] hard conflict limit 37014 (soft 27014 + delta 10000)
c [simplification-7] new conflict limit 27014 (hard 37014)
c 
c [simplification-8] limit 27014 conflicts (hard 37014) hit after 27014 conflicts
c [quatres-4] found 20515 quaternary clauses 36% in total
c [quatres-4-1] removed 24 duplicate quaternary clauses
c [quatres-4-1] added 6 double-self-subsuming ternary resolvents
c [quatres-4-2] added 59 single-self-subsuming ternary resolvents
c [quatres-4-2] added 636 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 18572 schedulable variables 52%
c [ternres-4] 1297 ternary resolvents (2 bin, 1295 trn)
c [ternres-4] 16176 variables remain 46% (19258 retained 54%)
c [basicprobe-3] limit 17285040 penalty 0 = 0 + 0
c [basicprobe-3-0] 11946 probes remain 34% after last round
c [basicprobe-3-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1 variables, found 80265 hbrs
c [bate-1] eliminated 4 asymmetric tautologies during probing
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1008 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 35433 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 19 blocked clauses
c [block-3] 19 < 1/100 * 310862 = 3108 considered unsuccessful
c [bca-3] limit of 10000000 steps and 622379 added (scaled 2)
c [bca-3] 58059 out of 70868 literals actually usable 82%
c [bca-3] added 97 blocked clauses in 154790 steps
c [sweep-4] limit 1037102 penalty 0 = 0 + 0
c [sweep-4-1] 13314 pos 38.6% + 21189 neg 61.4% = 34503 sched 97.4% ret 930
c [sweep-4-1] 1156259 steps 28 queries 8711.04 avg class size
c [sweep-4-1] 255 decisions 26 SAT calls 34.00 avg env size
c [sweep-4-1] 34366 variables remain 97% (1067 retained 3%)
c [decomp-18] removed 1 variables
c [sweep-4-1] removed 1 vars (0 failed, 1 eqs, 3 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 1 vars in TOTAL (1 rounds, 27 queries)
c [phase-count-8] 303670 negative 97.7% of 310837 except 7167 2.3%
c [phase-count-8] 224703 positive 72.3% of 310837 except 86134 27.7%
c [phase-count-8] less non-negative clauses 7167 than limit 31000 (10.0%)
c [phase-count-8] non-pos/non-neg = 86134/7167 = 12.02 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 6744 negative 100%
c [sort-queue-8] sorted 35432 enqueued variables after 27014 conflicts
c [score-dist-8] active 0 (0%), one 8862 (25%), zero 26570 (75%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 2 variables 0.0% (35432 remain 15%)
c [simplification-8] removed 99 irredundant clauses 0.0% (310837 remain 25%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 20000
c [simplification-8] new conflict interval 34000
c [simplification-8] penalized conflict interval 34000 = 1 * 34000
c [simplification-8] hard conflict limit 78014 (soft 61014 + delta 17000)
c [simplification-8] new conflict limit 61014 (hard 78014)
c 
c [simplification-9] limit of 334 binary hit after 334 binaries
c [quatres-5] found 21621 quaternary clauses 36% in total
c [quatres-5-1] removed 6 duplicate quaternary clauses
c [quatres-5-1] added 46 double-self-subsuming ternary resolvents
c [quatres-5-2] added 205 single-self-subsuming ternary resolvents
c [quatres-5-2] added 262 quaternary resolvents
c [ternres-5] limit 6181967 with penalty 0 = 0 + 0
c [ternres-5] 16174 schedulable variables 46%
c [ternres-5] 1886 ternary resolvents (11 bin, 1875 trn)
c [ternres-5] 13724 variables remain 39% (21708 retained 61%)
c [decomp-19] removed 1 variables
c [simpleprobe-4] 29970 schedulable variables 85%
c [simpleprobe-4] limit 24727870 penalty 0 = 0 + 0
c [decomp-20] removed 1 variables
c [simpleprobe-4] 14999 variables remain 42% (20431 retained 58%)
c [simpleprobe-4] removed 1 variables, found 4199 hbrs, 0 units
c [unhide-8] limit 618196 with penalty 1 = 1 + 0
c [unhide-8-8] 0 units, 0 failed, 12252 tauts, 0 hbrs, 32016 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 365 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 154549185 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 20 clauses out of 737 (3%) of length 8
c [cce-4-1] eliminated 1647 clauses out of 4502 (37%) of length 7
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 1667 large clauses in 154549195 steps
c [cce-4-1] allowing another 77274597 steps for small clauses
c [cce-4-1] scheduling 162629 clauses = 33976 binary + 128653 ternary
c [cce-4-1] tried to eliminate 14231 small clauses 9%
c [cce-4-1] eliminated 656 binary clauses 2%
c [cce-4-1] eliminated 5445 ternary clauses 4%
c [cce-4-1] eliminated 6101 small clauses 4%
c [cce-4-1] eliminated 6101 small clauses in 154549256 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 7768 covered clauses in round 1
c [cce-4] eliminated 7768 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 35430 variables 100%
c [elim-7] limit of 61819675 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 828 not tried 2% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 356 = 1% variables out of 35430 scheduled
c [bca-4] limit of 10000000 steps and 603933 added (scaled 2)
c [bca-4] 56632 out of 70150 literals actually usable 81%
c [bca-4] added 443 blocked clauses in 161207 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 18545900 penalty 0 = 0 + 0
c [sweep-5-1] 11790 pos 34.6% + 22255 neg 65.4% = 34045 sched 97.1% ret 1029
c [sweep-5-1] 18758515 steps 224 queries 1838.55 avg class size
c [sweep-5-1] 4966 decisions 205 SAT calls 91.24 avg env size
c [sweep-5-1] 29638 variables remain 85% (5433 retained 15%)
c [decomp-21] removed 58 variables
c [sweep-5-1] removed 58 vars (0 failed, 19 eqs, 40 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 58 vars in TOTAL (1 rounds, 223 queries)
c [phase-count-9] 292409 negative 97.6% of 299476 except 7067 2.4%
c [phase-count-9] 212580 positive 71.0% of 299476 except 86896 29.0%
c [phase-count-9] less non-negative clauses 7067 than limit 29900 (10.0%)
c [phase-count-9] non-pos/non-neg = 86896/7067 = 12.30 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 5959 negative 100%
c [sort-queue-9] sorted 35016 enqueued variables after 41054 conflicts
c [score-dist-9] active 0 (0%), one 9779 (28%), zero 25237 (72%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 416 variables 1.2% (35016 remain 14%)
c [simplification-9] removed 11357 irredundant clauses 3.7% (299476 remain 24%)
c [simplification-9] maximum reduction of 4% = max (1%, 4%)
c [simplification-9] forced so keeping old conflict interval 34000
c [simplification-9] conflict limit remains at 61014 (hard 78014)
c [simplification-9] new binary interval 1000
c 
c [simplification-10] limit 61014 conflicts (hard 78014) hit after 61014 conflicts
c [quatres-6] found 21940 quaternary clauses 36% in total
c [quatres-6-1] removed 26 duplicate quaternary clauses
c [quatres-6-1] added 25 double-self-subsuming ternary resolvents
c [quatres-6-2] added 445 single-self-subsuming ternary resolvents
c [quatres-6-2] added 391 quaternary resolvents
c [ternres-6] limit 10160843 with penalty 0 = 0 + 0
c [ternres-6] 13585 schedulable variables 39%
c [ternres-6] 3300 ternary resolvents (8 bin, 3292 trn)
c [ternres-6] 8496 variables remain 24% (26520 retained 76%)
c [card-4] limit 635052 penalty 3 = 3 + 0
c [card-4] found 268 at-most-one constraints of average size 3.4
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 635052 for elimination
c [card-4] 268 out of 268 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 508042 penalty 2 = 2 + 0
c [gauss-3] extracted 90 xors of average arity 3.0
c [gauss-3] connected 270 occurrences of 99 variables (average 2.7)
c [gauss-3] limit 508042 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 2 variables
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 804 transitive binary clauses
c [cce-5] limit of 50804217 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 4 clauses out of 17 (24%) of length 12
c [cce-5-1] eliminated 31 clauses out of 129 (24%) of length 11
c [cce-5-1] eliminated 4 clauses out of 98 (4%) of length 10
c [cce-5-1] eliminated 2 clauses out of 188 (1%) of length 9
c [cce-5-1] eliminated 366 clauses out of 3100 (12%) of length 7
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 407 large clauses in 50804297 steps
c [cce-5-1] allowing another 25402148 steps for small clauses
c [cce-5-1] scheduling 157555 clauses = 36716 binary + 120839 ternary
c [cce-5-1] tried to eliminate 4359 small clauses 3%
c [cce-5-1] eliminated 545 binary clauses 1%
c [cce-5-1] eliminated 2494 ternary clauses 2%
c [cce-5-1] eliminated 3039 small clauses 2%
c [cce-5-1] eliminated 3039 small clauses in 50804226 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 3446 covered clauses in round 1
c [cce-5] eliminated 3446 covered clauses in TOTAL during 1 rounds
c [elim-8] 825 variables 2% will be scheduled this time
c [elim-8] scheduled 825 variables 2%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4064337400 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 142506701 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 825 scheduled
c [bca-5] limit of 10000000 steps and 590075 added (scaled 2)
c [bca-5] 55713 out of 70030 literals actually usable 80%
c [bca-5] added 65 blocked clauses in 174235 steps
c [sweep-6] limit 3048253 penalty 0 = 0 + 0
c [sweep-6-1] 11799 pos 39.9% + 17801 neg 60.1% = 29600 sched 84.5% ret 5414
c [sweep-6-1] 3059031 steps 73 queries 7034.18 avg class size
c [sweep-6-1] 978 decisions 65 SAT calls 67.05 avg env size
c [sweep-6-1] 29237 variables remain 84% (5777 retained 16%)
c [decomp-23] removed 8 variables
c [sweep-6-1] removed 8 vars (0 failed, 8 eqs, 15 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 8 vars in TOTAL (1 rounds, 72 queries)
c [phase-count-10] 287492 negative 97.6% of 294547 except 7055 2.4%
c [phase-count-10] 207929 positive 70.6% of 294547 except 86618 29.4%
c [phase-count-10] less non-negative clauses 7055 than limit 29400 (10.0%)
c [phase-count-10] non-pos/non-neg = 86618/7055 = 12.28 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 5500 negative 100%
c [sort-queue-10] sorted 35006 enqueued variables after 61014 conflicts
c [score-dist-10] active 0 (0%), one 10344 (30%), zero 24662 (70%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 10 variables 0.0% (35006 remain 14%)
c [simplification-10] removed 4924 irredundant clauses 1.6% (294547 remain 23%)
c [simplification-10] maximum reduction of 2% = max (0%, 2%)
c [simplification-10] geometric conflict interval increment 11333 = 34000 / 3
c [simplification-10] new conflict interval 45333
c [simplification-10] penalized conflict interval 45333 = 1 * 45333
c [simplification-10] hard conflict limit 129013 (soft 106347 + delta 22666)
c [simplification-10] new conflict limit 106347 (hard 129013)
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 -   55.6   35006   294546     83249   35161  36655 93747    8    25   40  31%    729    6    8    5  157%
c 
c [simplification-11] limit 106347 conflicts (hard 129013) hit after 106348 conflicts
c [quatres-7] found 22776 quaternary clauses 35% in total
c [quatres-7-1] removed 30 duplicate quaternary clauses
c [quatres-7-1] added 6 double-self-subsuming ternary resolvents
c [quatres-7-2] added 271 single-self-subsuming ternary resolvents
c [quatres-7-2] added 223 quaternary resolvents
c [ternres-7] limit 19537992 with penalty 0 = 0 + 0
c [ternres-7] 8494 schedulable variables 24%
c [ternres-7] 5929 ternary resolvents (11 bin, 5918 trn)
c [ternres-7] 1169 variables remain 3% (33837 retained 97%)
c [decomp-24] removed 2 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 685 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 35004 variables 100%
c [block-4] limit of 48844980 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 12 blocked clauses
c [block-4] 12 < 1/100 * 294400 = 2944 considered unsuccessful
c [cce-6] limit of 97689960 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 70 clauses out of 2678 (3%) of length 7
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 70 large clauses in 97689964 steps
c [cce-6-1] allowing another 48844982 steps for small clauses
c [cce-6-1] scheduling 154600 clauses = 36356 binary + 118244 ternary
c [cce-6-1] tried to eliminate 13392 small clauses 9%
c [cce-6-1] eliminated 832 binary clauses 2%
c [cce-6-1] eliminated 6056 ternary clauses 5%
c [cce-6-1] eliminated 6888 small clauses 4%
c [cce-6-1] eliminated 6888 small clauses in 97690083 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 6958 covered clauses in round 1
c [cce-6] eliminated 6958 covered clauses in TOTAL during 1 rounds
c [bca-6] limit of 10000000 steps and 575867 added (scaled 2)
c [bca-6] 55749 out of 70010 literals actually usable 80%
c [bca-6] added 57 blocked clauses in 176059 steps
c [sweep-7] limit 5861397 penalty 0 = 0 + 0
c [sweep-7-1] 11562 pos 39.5% + 17673 neg 60.5% = 29235 sched 83.5% ret 5769
c [sweep-7-1] 5876415 steps 251 queries 6665.46 avg class size
c [sweep-7-1] 2335 decisions 202 SAT calls 42.33 avg env size
c [sweep-7-1] 27973 variables remain 80% (7024 retained 20%)
c [decomp-25] removed 67 variables
c [sweep-7-1] removed 67 vars (1 failed, 52 eqs, 107 impls)
c [sweep-7] removed 67 vars in TOTAL (1 rounds, 250 queries)
c [phase-count-11] 280203 negative 97.5% of 287263 except 7060 2.5%
c [phase-count-11] 201241 positive 70.1% of 287263 except 86022 29.9%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 729 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 34937 enqueued variables after 106348 conflicts
c [score-dist-11] active 0 (0%), one 14317 (41%), zero 20620 (59%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 69 variables 0.2% (34937 remain 14%)
c [simplification-11] removed 7282 irredundant clauses 2.5% (287263 remain 23%)
c [simplification-11] maximum reduction of 2% = max (0%, 2%)
c [simplification-11] geometric conflict interval increment 15111 = 45333 / 3
c [simplification-11] new conflict interval 60444
c [simplification-11] penalized conflict interval 60444 = 1 * 60444
c [simplification-11] hard conflict limit 197014 (soft 166792 + delta 30222)
c [simplification-11] new conflict limit 166792 (hard 197014)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   69.0   34936   287263    110236   60895  49226 98126    9    29   46  31%    829    7    8    6  135%
c -   78.6   34936   287262    133857   45376  49546 98249    9    28   41  31%   -326    4    8    7  115%
c i   79.0   34935   287262    134990   46466  49557 98258    9    29   43  30%   -303    5    9    7  123%
c 
c [simplification-12] limit 166792 conflicts (hard 197014) hit after 169852 conflicts
c [quatres-8] found 23786 quaternary clauses 33% in total
c [quatres-8-1] removed 252 duplicate quaternary clauses
c [quatres-8-1] added 5 double-self-subsuming ternary resolvents
c [quatres-8-2] added 165 single-self-subsuming ternary resolvents
c [quatres-8-2] added 131 quaternary resolvents
c [ternres-8] limit 32799080 with penalty 0 = 0 + 0
c [ternres-8] 1167 schedulable variables 3%
c [ternres-8] 7792 ternary resolvents (30 bin, 7762 trn)
c [ternres-8] 155 variables remain 0% (34780 retained 100%)
c [decomp-26] removed 8 variables
c [treelook-4] limit 819977 penalty 2 = 2 + 0 boost 1
c [treelook-4] scheduled 13528 literals 19%
c [treelook-4] scheduling used 820105 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 819977 penalty 2 = 2 + 0 boost 1
c [treelook-4] used 839082 steps
c [treelook-4] 13350 literals remain 19%
c [treelook-4] 2183 variables remain to probed next time 6%
c [decomp-27] removed 1 variables
c [treelook-4] removed 2 variables, found 1354 hbrs
c [unhide-9] limit 1639954 with penalty 2 = 2 + 0
c [unhide-9-9] 0 units, 15 failed, 4593 tauts, 0 hbrs, 65977 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 718 transitive binary clauses
c [cce-7] limit of 163995402 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 100 (1%) of length 10
c [cce-7-1] eliminated 30 clauses out of 2573 (1%) of length 7
c [cce-7-1] eliminated 5078 clauses out of 13833 (37%) of length 6
c [cce-7-1] eliminated 464 clauses out of 8336 (6%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 5573 large clauses in 163995443 steps
c [cce-7-1] allowing another 81997721 steps for small clauses
c [cce-7-1] scheduling 135322 clauses = 33093 binary + 102229 ternary
c [cce-7-1] tried to eliminate 20573 small clauses 15%
c [cce-7-1] eliminated 994 binary clauses 3%
c [cce-7-1] eliminated 6204 ternary clauses 6%
c [cce-7-1] eliminated 7198 small clauses 5%
c [cce-7-1] eliminated 7319 small clauses in 163995473 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 12892 covered clauses in round 1
c [cce-7] eliminated 12892 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 34914 variables 100%
c [elim-9] limit of 327990805 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 533 variables 2% in round 1 in 160462712 steps
c [elim-9-1] backward subsumption/strengthening limit 160462700
c [elim-9-1-1] backward checking 3109 touched variables 9%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 101 and strengthened 42 clauses in 17817660 steps
c [elim-9-1] rescheduled 239 variables 1% by backward subsumption
c [elim-9-2] eliminated 3 variables 0% in round 2 in 9464338 steps
c [elim-9-2] backward subsumption/strengthening limit 9464300
c [elim-9-2-1] backward checking 36 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 1 and strengthened 0 clauses in 186549 steps
c [elim-9-2] rescheduled 5 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 12653 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 536 = 2% variables out of 34914 scheduled
c [bca-7] limit of 10000000 steps and 538812 added (scaled 2)
c [bca-7] 53573 out of 68758 literals actually usable 78%
c [bca-7] added 103 blocked clauses in 189309 steps
c [sweep-8] limit 9839724 penalty 0 = 0 + 0
c [sweep-8-1] 11165 pos 40.3% + 16517 neg 59.7% = 27682 sched 80.5% ret 6696
c [sweep-8-1] 10012875 steps 222 queries 3259.83 avg class size
c [sweep-8-1] 3013 decisions 157 SAT calls 74.07 avg env size
c [sweep-8-1] 26449 variables remain 77% (7929 retained 23%)
c [decomp-28] removed 75 variables
c [sweep-8-1] removed 75 vars (0 failed, 67 eqs, 127 impls)
c [sweep-8] removed 75 vars in TOTAL (1 rounds, 221 queries)
c [phase-count-12] 261860 negative 97.4% of 268781 except 6921 2.6%
c [phase-count-12] 184386 positive 68.6% of 268781 except 84395 31.4%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 83 positive 83%, 17 negative 17%
c [sort-queue-12] sorted 34303 enqueued variables after 169852 conflicts
c [score-dist-12] active 0 (0%), one 15567 (45%), zero 18736 (55%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 632 variables 1.8% (34303 remain 14%)
c [simplification-12] removed 18481 irredundant clauses 6.4% (268781 remain 21%)
c [simplification-12] maximum reduction of 6% = max (2%, 6%)
c [simplification-12] large reduction 6% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 181852 (soft 171852 + delta 10000)
c [simplification-12] new conflict limit 171852 (hard 181852)
c 
c [simplification-13] limit 171852 conflicts (hard 181852) hit after 171853 conflicts
c [quatres-9] found 22691 quaternary clauses 35% in total
c [quatres-9-1] removed 291 duplicate quaternary clauses
c [quatres-9-1] added 3 double-self-subsuming ternary resolvents
c [quatres-9-2] added 84 single-self-subsuming ternary resolvents
c [quatres-9-2] added 197 quaternary resolvents
c [ternres-9] limit 33263037 with penalty 0 = 0 + 0
c [ternres-9] 154 schedulable variables 0%
c [ternres-9] 7252 ternary resolvents (42 bin, 7210 trn)
c [ternres-9] 8 variables remain 0% (34295 retained 100%)
c [decomp-29] removed 5 variables
c [basicprobe-4] limit 166315189 penalty 0 = 0 + 0
c [basicprobe-4-0] 10106 sched 30%, 46 failed, 0 lifted, 94855 hbrs
c [decomp-30] removed 96 variables
c [basicprobe-4-1] 10098 probes remain 30% after last round
c [basicprobe-4-1] 54 units = 54 failed (100%) + 0 lifted (0%)
c [basicprobe-4-1] removed 104 variables, found 95857 hbrs
c [bate-2] eliminated 142 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1846 transitive binary clauses
c [transred-9] found 1 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 1663151890 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 2 clauses out of 11 (18%) of length 12
c [cce-8-1] eliminated 10 clauses out of 62 (16%) of length 11
c [cce-8-1] eliminated 10 clauses out of 132 (8%) of length 10
c [cce-8-1] eliminated 7 clauses out of 234 (3%) of length 9
c [cce-8-1] eliminated 2 clauses out of 23 (9%) of length 8
c [cce-8-1] eliminated 3 clauses out of 2444 (0%) of length 7
c [cce-8-1] eliminated 86 clauses out of 8561 (1%) of length 6
c [cce-8-1] eliminated 231 clauses out of 7791 (3%) of length 5
c [cce-8-1] eliminated 1528 clauses out of 10777 (14%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 1879 large clauses in 173414186 steps
c [cce-8-1] allowing another 86707093 steps for small clauses
c [cce-8-1] scheduling 145516 clauses = 34306 binary + 111210 ternary
c [cce-8-1] tried to eliminate 145516 small clauses 100%
c [cce-8-1] eliminated 4467 binary clauses 13%
c [cce-8-1] eliminated 29738 ternary clauses 27%
c [cce-8-1] eliminated 34205 small clauses 24%
c [cce-8-1] eliminated 34303 small clauses in 631028847 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] completed small and large (ATE)
c [cce-8-1] eliminated 36182 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 32862891 steps for small clauses
c [cce-8-2] scheduling 111311 clauses = 29839 binary + 81472 ternary
c [cce-8-2] tried to eliminate 111311 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 36182 covered clauses in TOTAL during 2 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 34193 variables 100%
c [elim-10] limit of 665260756 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 2530 variables 7% in round 1 in 127750217 steps
c [elim-10-1] backward subsumption/strengthening limit 127750200
c [elim-10-1-1] backward checking 10650 touched variables 31%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 154 and strengthened 52 clauses in 14202378 steps
c [elim-10-1] rescheduled 275 variables 1% by backward subsumption
c [elim-10-2] eliminated 2 variables 0% in round 2 in 16141341 steps
c [elim-10-2] backward subsumption/strengthening limit 16141300
c [elim-10-2-1] backward checking 28 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 1 and strengthened 2 clauses in 187635 steps
c [elim-10-2] rescheduled 6 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 2487837 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 2532 = 7% variables out of 34193 scheduled
c [bca-8] limit of 10000000 steps and 460693 added (scaled 2)
c [bca-8] 50267 out of 63324 literals actually usable 79%
c [bca-8] added 196 blocked clauses in 170407 steps
c [sweep-9] limit 9978911 penalty 0 = 0 + 0
c [sweep-9-1] 9824 pos 39.9% + 14797 neg 60.1% = 24621 sched 77.8% ret 7040
c [sweep-9-1] 10011200 steps 214 queries 3423.75 avg class size
c [sweep-9-1] 2492 decisions 171 SAT calls 45.28 avg env size
c [sweep-9-1] 23411 variables remain 74% (8246 retained 26%)
c [decomp-31] removed 60 variables
c [sweep-9-1] removed 60 vars (0 failed, 42 eqs, 80 impls)
c [sweep-9] removed 60 vars in TOTAL (1 rounds, 213 queries)
c [phase-count-13] 224983 negative 98.0% of 229474 except 4491 2.0%
c [phase-count-13] 154114 positive 67.2% of 229474 except 75360 32.8%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 10 positive 12%, 72 negative 88%
c [sort-queue-13] sorted 31601 enqueued variables after 171853 conflicts
c [score-dist-13] active 0 (0%), one 16714 (53%), zero 14887 (47%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 2702 variables 7.9% (31601 remain 13%)
c [simplification-13] removed 39307 irredundant clauses 14.6% (229474 remain 18%)
c [simplification-13] maximum reduction of 15% = max (8%, 15%)
c [simplification-13] large reduction 15% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 183853 (soft 173853 + delta 10000)
c [simplification-13] new conflict limit 173853 (hard 183853)
c 
c [simplification-14] limit 173853 conflicts (hard 183853) hit after 173853 conflicts
c [quatres-10] found 20588 quaternary clauses 32% in total
c [quatres-10-1] removed 173 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 78 single-self-subsuming ternary resolvents
c [quatres-10-2] added 545 quaternary resolvents
c [ternres-10] limit 33489219 with penalty 0 = 0 + 0
c [ternres-10] 8 schedulable variables 0%
c [ternres-10] 5577 ternary resolvents (25 bin, 5552 trn)
c [ternres-10] 1 variables remain 0% (31600 retained 100%)
c [gauss-4] limit 837230 penalty 3 = 3 + 0
c [gauss-4] extracted 87 xors of average arity 3.0
c [gauss-4] connected 258 occurrences of 117 variables (average 2.2)
c [gauss-4] limit 837230 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 4 variables
c [simpleprobe-5] 13087 schedulable variables 41%
c [simpleprobe-5] limit 133956877 penalty 0 = 0 + 0
c [decomp-33] removed 141 variables
c [simpleprobe-5] 1018 variables remain 3% (30438 retained 97%)
c [simpleprobe-5] removed 141 variables, found 16749 hbrs, 9 units
c [unhide-10] limit 3348921 with penalty 1 = 1 + 0
c [unhide-10-12] 1 units, 2 failed, 34363 tauts, 0 hbrs, 65583 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 1523 transitive binary clauses
c [transred-10] found 2 units
c [cce-9] limit of 167446096 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 36 (3%) of length 11
c [cce-9-1] eliminated 10 clauses out of 140 (7%) of length 10
c [cce-9-1] eliminated 5 clauses out of 249 (2%) of length 9
c [cce-9-1] eliminated 4 clauses out of 33 (12%) of length 8
c [cce-9-1] eliminated 2 clauses out of 2394 (0%) of length 7
c [cce-9-1] eliminated 42 clauses out of 8837 (0%) of length 6
c [cce-9-1] eliminated 41 clauses out of 11133 (0%) of length 5
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 105 large clauses in 167446169 steps
c [cce-9-1] allowing another 83723084 steps for small clauses
c [cce-9-1] scheduling 116027 clauses = 24406 binary + 91621 ternary
c [cce-9-1] tried to eliminate 36904 small clauses 32%
c [cce-9-1] eliminated 423 binary clauses 2%
c [cce-9-1] eliminated 5261 ternary clauses 6%
c [cce-9-1] eliminated 5684 small clauses 5%
c [cce-9-1] eliminated 5712 small clauses in 167446144 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 5817 covered clauses in round 1
c [cce-9] eliminated 5817 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 31452 variables 100%
c [elim-11] limit of 669784387 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 428 variables 1% in round 1 in 120412709 steps
c [elim-11-1] backward subsumption/strengthening limit 120412700
c [elim-11-1-1] backward checking 2353 touched variables 7%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 88 and strengthened 6 clauses in 6467186 steps
c [elim-11-1] rescheduled 238 variables 1% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 14846465 steps
c [elim-11-2] backward subsumption/strengthening limit 14846400
c [elim-11-2-1] backward checking 27 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 165772 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 429 = 1% variables out of 31452 scheduled
c [bca-9] limit of 10000000 steps and 442171 added (scaled 2)
c [bca-9] 49240 out of 62048 literals actually usable 79%
c [bca-9] added 668 blocked clauses in 163989 steps
c [sweep-10] limit 10046765 penalty 0 = 0 + 0
c [sweep-10-1] 9473 pos 41.0% + 13616 neg 59.0% = 23089 sched 74.4% ret 7934
c [sweep-10-1] 11820078 steps 138 queries 3380.64 avg class size
c [sweep-10-1] 2009 decisions 122 SAT calls 57.99 avg env size
c [sweep-10-1] 22283 variables remain 72% (8740 retained 28%)
c [decomp-34] removed 21 variables
c [sweep-10-1] removed 21 vars (0 failed, 17 eqs, 36 impls)
c [sweep-10] 21 < 1/1000 * 31023 = 31 considered unsuccessful
c [sweep-10] removed 21 vars in TOTAL (1 rounds, 137 queries)
c [phase-count-14] 215920 negative 97.9% of 220489 except 4569 2.1%
c [phase-count-14] 145855 positive 66.2% of 220489 except 74634 33.8%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 63 positive 95%, 3 negative 5%
c [sort-queue-14] sorted 31002 enqueued variables after 173853 conflicts
c [score-dist-14] active 0 (0%), one 16506 (53%), zero 14496 (47%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 599 variables 1.9% (31002 remain 13%)
c [simplification-14] removed 8985 irredundant clauses 3.9% (220489 remain 17%)
c [simplification-14] maximum reduction of 4% = max (2%, 4%)
c [simplification-14] geometric conflict interval increment 12088 = 60444 / 5
c [simplification-14] new conflict interval 72532
c [simplification-14] penalized conflict interval 72532 = 1 * 72532
c [simplification-14] hard conflict limit 282651 (soft 246385 + delta 36266)
c [simplification-14] new conflict limit 246385 (hard 282651)
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 -  136.5   31002   220489    203185   55814  94672 51301    8    21   41  38%    417   -4   10    8  123%
c -  144.7   31002   220489    243090   63717  95022 51345    8    18   41  45%    694   -5    7    8   88%
c 
c [simplification-15] limit 246385 conflicts (hard 282651) hit after 253821 conflicts
c [quatres-11] found 21701 quaternary clauses 30% in total
c [quatres-11-1] removed 161 duplicate quaternary clauses
c [quatres-11-1] added 5 double-self-subsuming ternary resolvents
c [quatres-11-2] added 105 single-self-subsuming ternary resolvents
c [quatres-11-2] added 283 quaternary resolvents
c [ternres-11] limit 42481349 with penalty 0 = 0 + 0
c [ternres-11] 1 schedulable variables 0%
c [ternres-11] 10681 ternary resolvents (13 bin, 10668 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1327542 penalty 4 = 4 + 0
c [card-5] found 927 at-most-one constraints of average size 3.9
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1327542 for elimination
c [card-5] 927 out of 927 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 3 variables
c [unhide-11] limit 8496269 with penalty 0 = 0 + 0
c [unhide-11-18] 4 units, 26 failed, 13523 tauts, 0 hbrs, 173262 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 743 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 30990 variables 100%
c [block-5] limit of 53101687 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 15 blocked clauses
c [block-5] 15 < 1/100 * 219815 = 2198 considered unsuccessful
c [cce-10] limit of 212406748 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 11 (9%) of length 12
c [cce-10-1] eliminated 1 clauses out of 23 (4%) of length 11
c [cce-10-1] eliminated 3 clauses out of 142 (2%) of length 10
c [cce-10-1] eliminated 5 clauses out of 256 (2%) of length 9
c [cce-10-1] eliminated 1 clauses out of 33 (3%) of length 8
c [cce-10-1] eliminated 35 clauses out of 2420 (1%) of length 7
c [cce-10-1] eliminated 35 clauses out of 8859 (0%) of length 6
c [cce-10-1] eliminated 85 clauses out of 10811 (1%) of length 5
c [cce-10-1] eliminated 234 clauses out of 9457 (2%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 400 large clauses in 188232664 steps
c [cce-10-1] allowing another 94116332 steps for small clauses
c [cce-10-1] scheduling 108877 clauses = 24613 binary + 84264 ternary
c [cce-10-1] tried to eliminate 47463 small clauses 44%
c [cce-10-1] eliminated 227 binary clauses 1%
c [cce-10-1] eliminated 2852 ternary clauses 3%
c [cce-10-1] eliminated 3079 small clauses 3%
c [cce-10-1] eliminated 3079 small clauses in 212406750 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 3479 covered clauses in round 1
c [cce-10] eliminated 3479 covered clauses in TOTAL during 1 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 30990 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 178 variables 1% in round 1 in 116416723 steps
c [elim-12-1] backward subsumption/strengthening limit 116416700
c [elim-12-1-1] backward checking 1697 touched variables 5%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 3 and strengthened 3 clauses in 4217815 steps
c [elim-12-1] rescheduled 9 variables 0% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 160527 steps
c [elim-12-2] backward subsumption/strengthening limit 160500
c [elim-12-2-1] backward checking 14 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 0 clauses in 39197 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 179 = 1% variables out of 30990 scheduled
c [elim-12] 179 < 1/100 * 30990 = 309 considered unsuccessful
c [bca-10] limit of 10000000 steps and 432963 added (scaled 2)
c [bca-10] 46745 out of 61624 literals actually usable 76%
c [bca-10] added 599 blocked clauses in 171578 steps
c [phase-count-15] 211146 negative 97.9% of 215722 except 4576 2.1%
c [phase-count-15] 141452 positive 65.6% of 215722 except 74270 34.4%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 4 positive 100%, 0 negative 0%
c [sort-queue-15] sorted 30811 enqueued variables after 253821 conflicts
c [score-dist-15] active 0 (0%), one 19634 (64%), zero 11177 (36%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 191 variables 0.6% (30811 remain 13%)
c [simplification-15] removed 4767 irredundant clauses 2.2% (215722 remain 17%)
c [simplification-15] maximum reduction of 2% = max (1%, 2%)
c [simplification-15] geometric conflict interval increment 24177 = 72532 / 3
c [simplification-15] new conflict interval 96709
c [simplification-15] penalized conflict interval 96709 = 1 * 96709
c [simplification-15] hard conflict limit 398884 (soft 350530 + delta 48354)
c [simplification-15] new conflict limit 350530 (hard 398884)
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 -  161.8   30811   215722    279888   66518 105556 40210    9    23   42  39%    836    1    9    8  109%
c i  167.6   30810   215722    303998   89705 105687 40252    9    18   49  48%    894   -3   10    8  120%
c -  170.7   30807   215722    316716   69678 105729 40269    9    21   42  41%  -1293    0    8    8   99%
c -  179.7   30807   215722    354240   74026 105860 40318    8    24   43  35%   -283    4    9    8  107%
c i  183.5   30806   215722    370480   89271 105918 40346    8    14   48  57%      4   -7    5    8   65%
c i  186.1   30786   215722    382547  100951 105962 40365    8    16   52  47%   -702   -4    6    8   68%
c -  188.0   30753   215722    391111   77125 105998 40372    8    25   43  34%   -659    5    8    8  102%
c 
c [simplification-16] limit 350530 conflicts (hard 398884) hit after 398885 conflicts
c [quatres-12] found 17366 quaternary clauses 31% in total
c [quatres-12-1] removed 33 duplicate quaternary clauses
c [quatres-12-1] added 1 double-self-subsuming ternary resolvents
c [quatres-12-2] added 101 single-self-subsuming ternary resolvents
c [quatres-12-2] added 960 quaternary resolvents
c [ternres-12] limit 60186630 with penalty 0 = 0 + 0
c [ternres-12] all 30753 free variables schedulable
c [ternres-12] 6392 ternary resolvents (35 bin, 6357 trn)
c [ternres-12] 1147 variables remain 4% (29606 retained 96%)
c [decomp-36] removed 88 variables
c [treelook-5] limit 3009331 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 17359 literals 28%
c [treelook-5] scheduling used 929660 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 3009331 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 3013322 steps
c [treelook-5] 17241 literals remain 28%
c [treelook-5] 1952 variables remain to probed next time 6%
c [decomp-37] removed 2 variables
c [treelook-5] removed 4 variables, found 11834 hbrs
c [unhide-12] limit 12037326 with penalty 0 = 0 + 0
c [unhide-12-26] 16 units, 88 failed, 31251 tauts, 0 hbrs, 252664 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 940 transitive binary clauses
c [transred-12] found 1 units
c [cce-11] limit of 300933152 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 1 clauses out of 19 (5%) of length 11
c [cce-11-1] eliminated 3 clauses out of 151 (2%) of length 10
c [cce-11-1] eliminated 10 clauses out of 255 (4%) of length 9
c [cce-11-1] eliminated 1 clauses out of 19 (5%) of length 8
c [cce-11-1] eliminated 34 clauses out of 1003 (3%) of length 7
c [cce-11-1] eliminated 85 clauses out of 6579 (1%) of length 6
c [cce-11-1] eliminated 260 clauses out of 11317 (2%) of length 5
c [cce-11-1] eliminated 891 clauses out of 7966 (11%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 1285 large clauses in 208065369 steps
c [cce-11-1] allowing another 104032684 steps for small clauses
c [cce-11-1] scheduling 101307 clauses = 31242 binary + 70065 ternary
c [cce-11-1] tried to eliminate 42913 small clauses 42%
c [cce-11-1] eliminated 1304 binary clauses 4%
c [cce-11-1] eliminated 3063 ternary clauses 4%
c [cce-11-1] eliminated 4367 small clauses 4%
c [cce-11-1] eliminated 4417 small clauses in 300933284 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 5702 covered clauses in round 1
c [cce-11] eliminated 5702 covered clauses in TOTAL during 1 rounds
c [bca-11] limit of 10000000 steps and 398905 added (scaled 2)
c [bca-11] 45224 out of 61110 literals actually usable 74%
c [bca-11] added 365 blocked clauses in 151066 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 90279945 penalty 1 = 1 + 0
c [sweep-11-1] 10187 pos 46.1% + 11913 neg 53.9% = 22100 sched 72.3% ret 8454
c [sweep-11-1] 90366605 steps 2070 queries 680.53 avg class size
c [sweep-11-1] 17491 decisions 1854 SAT calls 26.09 avg env size
c [sweep-11-1] 6818 variables remain 23% (23450 retained 77%)
c [decomp-38] removed 712 variables
c [sweep-11-1] removed 712 vars (1 failed, 274 eqs, 540 impls)
c [sweep-11] removed 712 vars in TOTAL (1 rounds, 2069 queries)
c [phase-count-16] 185215 negative 97.4% of 190206 except 4991 2.6%
c [phase-count-16] 121913 positive 64.1% of 190206 except 68293 35.9%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 3 positive 23%, 10 negative 77%
c [sort-queue-16] sorted 29842 enqueued variables after 398885 conflicts
c [score-dist-16] active 0 (0%), one 21241 (71%), zero 8601 (29%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 911 variables 3.0% (29842 remain 12%)
c [simplification-16] removed 25516 irredundant clauses 11.8% (190206 remain 15%)
c [simplification-16] maximum reduction of 12% = max (3%, 12%)
c [simplification-16] large reduction 12% >= 5% limit
c [simplification-16] next conflict interval 3988 = min (398885/100, 96709)
c [simplification-16] penalized conflict interval 3988 = 1 * 3988
c [simplification-16] hard conflict limit 412873 (soft 402873 + delta 10000)
c [simplification-16] new conflict limit 402873 (hard 412873)
c 
c [simplification-17] limit 402873 conflicts (hard 412873) hit after 412873 conflicts
c [quatres-13] found 18096 quaternary clauses 31% in total
c [quatres-13-1] removed 921 duplicate quaternary clauses
c [quatres-13-1] added 28 double-self-subsuming ternary resolvents
c [quatres-13-2] added 820 single-self-subsuming ternary resolvents
c [quatres-13-2] added 615 quaternary resolvents
c [ternres-13] limit 61428577 with penalty 0 = 0 + 0
c [ternres-13] 1094 schedulable variables 4%
c [ternres-13] 9185 ternary resolvents (212 bin, 8973 trn)
c [ternres-13] 73 variables remain 0% (29769 retained 100%)
c [decomp-39] removed 57 variables
c [basicprobe-5] limit 307142887 penalty 0 = 0 + 0
c [basicprobe-5-0] 11006 sched 37%, 217 failed, 43 lifted, 50903 hbrs
c [decomp-40] removed 569 variables
c [basicprobe-5-1] 12160 sched 42%, 127 failed, 22 lifted, 10074 hbrs
c [decomp-41] removed 389 variables
c [basicprobe-5-2] 1367 probes remain 5% after last round
c [basicprobe-5-2] 520 units = 437 failed (84%) + 83 lifted (16%)
c [basicprobe-5-2] removed 1207 variables, found 61507 hbrs
c [bate-3] eliminated 138 asymmetric tautologies during probing
c [unhide-13] limit 12285715 with penalty 0 = 0 + 0
c [unhide-13-34] 17 units, 47 failed, 55333 tauts, 0 hbrs, 432642 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 354 transitive binary clauses
c [cce-12] limit of 307142887 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 77 (1%) of length 8
c [cce-12-1] eliminated 36 clauses out of 412 (9%) of length 7
c [cce-12-1] eliminated 101 clauses out of 4568 (2%) of length 6
c [cce-12-1] eliminated 71 clauses out of 10637 (1%) of length 5
c [cce-12-1] eliminated 104 clauses out of 5388 (2%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 313 large clauses in 153292749 steps
c [cce-12-1] allowing another 76646374 steps for small clauses
c [cce-12-1] scheduling 87799 clauses = 33337 binary + 54462 ternary
c [cce-12-1] tried to eliminate 53922 small clauses 61%
c [cce-12-1] eliminated 1084 binary clauses 3%
c [cce-12-1] eliminated 1018 ternary clauses 2%
c [cce-12-1] eliminated 2102 small clauses 2%
c [cce-12-1] eliminated 2174 small clauses in 307143006 steps
c [cce-12-1] incomplete small round (ATE)
c [cce-12-1] eliminated 2487 covered clauses in round 1
c [cce-12] eliminated 2487 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 28507 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 5297 variables 19% in round 1 in 73551661 steps
c [elim-13-1] backward subsumption/strengthening limit 73551600
c [elim-13-1-1] backward checking 17244 touched variables 61%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 142 and strengthened 85 clauses in 11582852 steps
c [elim-13-1] rescheduled 459 variables 2% by backward subsumption
c [elim-13-2] eliminated 27 variables 0% in round 2 in 12211048 steps
c [elim-13-2] backward subsumption/strengthening limit 12211000
c [elim-13-2-1] backward checking 305 touched variables 1%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 12 and strengthened 29 clauses in 1143755 steps
c [elim-13-2] rescheduled 135 variables 0% by backward subsumption
c [elim-13-3] eliminated 8 variables 0% in round 3 in 1088517 steps
c [elim-13-3] backward subsumption/strengthening limit 1088500
c [elim-13-3-1] backward checking 79 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 3 and strengthened 9 clauses in 144167 steps
c [elim-13] incomplete 49 not tried 0% in round 3
c [gc-119] reconnected 55224 binary clauses (produced 0 empty 2 units)
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 5474 = 19% variables out of 28507 scheduled
c [bca-12] limit of 10000000 steps and 330565 added (scaled 2)
c [bca-12] 35583 out of 46068 literals actually usable 77%
c [bca-12] added 149 blocked clauses in 116175 steps
c [sweep-12] limit 18428573 penalty 0 = 0 + 0
c [sweep-12-1] 4427 pos 70.8% + 1825 neg 29.2% = 6252 sched 27.1% ret 16781
c [sweep-12-1] 18469977 steps 860 queries 882.70 avg class size
c [sweep-12-1] 6112 decisions 846 SAT calls 17.04 avg env size
c [sweep-12-1] 3875 variables remain 18% (17265 retained 82%)
c [decomp-42] removed 1950 variables
c [sweep-12-1] removed 1950 vars (0 failed, 22 eqs, 46 impls)
c [sweep-12] removed 1950 vars in TOTAL (1 rounds, 859 queries)
c [phase-count-17] 150037 negative 98.0% of 153137 except 3100 2.0%
c [phase-count-17] 95269 positive 62.2% of 153137 except 57868 37.8%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-17] sorted 21083 enqueued variables after 412873 conflicts
c [score-dist-17] active 0 (0%), one 15576 (74%), zero 5507 (26%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 8759 variables 29.4% (21083 remain 9%)
c [simplification-17] removed 37067 irredundant clauses 19.5% (153137 remain 12%)
c [simplification-17] maximum reduction of 29% = max (29%, 19%)
c [simplification-17] large reduction 29% >= 5% limit
c [simplification-17] next conflict interval 4128 = min (412873/100, 96709)
c [simplification-17] penalized conflict interval 4128 = 1 * 4128
c [simplification-17] hard conflict limit 427001 (soft 417001 + delta 10000)
c [simplification-17] new conflict limit 417001 (hard 427001)
c 
c [simplification-18] limit 417001 conflicts (hard 427001) hit after 423670 conflicts
c [quatres-14] found 11235 quaternary clauses 22% in total
c [quatres-14-1] removed 28 duplicate quaternary clauses
c [quatres-14-1] added 15 double-self-subsuming ternary resolvents
c [quatres-14-2] added 124 single-self-subsuming ternary resolvents
c [quatres-14-2] added 1024 quaternary resolvents
c [ternres-14] limit 62391125 with penalty 0 = 0 + 0
c [ternres-14] 68 schedulable variables 0%
c [ternres-14] 5817 ternary resolvents (43 bin, 5774 trn)
c [ternres-14] 3 variables remain 0% (21080 retained 100%)
c [decomp-43] removed 14 variables
c [simpleprobe-6] 803 schedulable variables 4%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-44] removed 49 variables
c [simpleprobe-6] 145 variables remain 1% (20875 retained 99%)
c [simpleprobe-6] removed 49 variables, found 29351 hbrs, 13 units
c [unhide-14] limit 12478225 with penalty 0 = 0 + 0
c [unhide-14-44] 3 units, 23 failed, 38334 tauts, 0 hbrs, 162135 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 134 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 3119556250 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 2 clauses out of 11 (18%) of length 11
c [cce-13-1] eliminated 4 clauses out of 50 (8%) of length 10
c [cce-13-1] eliminated 13 clauses out of 219 (6%) of length 9
c [cce-13-1] eliminated 32 clauses out of 154 (21%) of length 8
c [cce-13-1] eliminated 40 clauses out of 376 (11%) of length 7
c [cce-13-1] eliminated 126 clauses out of 3383 (4%) of length 6
c [cce-13-1] eliminated 569 clauses out of 16894 (3%) of length 5
c [cce-13-1] eliminated 292 clauses out of 4208 (7%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 1078 large clauses in 285590808 steps
c [cce-13-1] allowing another 142795404 steps for small clauses
c [cce-13-1] scheduling 79069 clauses = 20158 binary + 58911 ternary
c [cce-13-1] tried to eliminate 79069 small clauses 100%
c [cce-13-1] eliminated 1205 binary clauses 6%
c [cce-13-1] eliminated 34377 ternary clauses 58%
c [cce-13-1] eliminated 35582 small clauses 45%
c [cce-13-1] eliminated 35582 small clauses in 427727114 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] completed small and large (ACCE)
c [cce-13-1] eliminated 36660 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 122 (1%) of length 8
c [cce-13-2] eliminated 27 clauses out of 336 (8%) of length 7
c [cce-13-2] eliminated 41 clauses out of 3257 (1%) of length 6
c [cce-13-2] eliminated 86 clauses out of 16325 (1%) of length 5
c [cce-13-2] eliminated 45 clauses out of 3916 (1%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 200 large clauses in 123633227 steps
c [cce-13-2] allowing another 61816613 steps for small clauses
c [cce-13-2] scheduling 43487 clauses = 18953 binary + 24534 ternary
c [cce-13-2] tried to eliminate 43487 small clauses 100%
c [cce-13-2] eliminated 55 binary clauses 0%
c [cce-13-2] eliminated 148 ternary clauses 1%
c [cce-13-2] eliminated 203 small clauses 0%
c [cce-13-2] eliminated 203 small clauses in 173499808 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 403 covered clauses in round 2
c [cce-13-3] eliminated 1 clauses out of 121 (1%) of length 8
c [cce-13-3] eliminated 3 clauses out of 309 (1%) of length 7
c [cce-13-3] eliminated 4 clauses out of 3216 (0%) of length 6
c [cce-13-3] eliminated 4 clauses out of 16239 (0%) of length 5
c [cce-13-3] eliminated 4 clauses out of 3871 (0%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 16 large clauses in 122989682 steps
c [cce-13-3] allowing another 61494841 steps for small clauses
c [cce-13-3] scheduling 43284 clauses = 18898 binary + 24386 ternary
c [cce-13-3] tried to eliminate 43284 small clauses 100%
c [cce-13-3] eliminated 6 binary clauses 0%
c [cce-13-3] eliminated 20 ternary clauses 0%
c [cce-13-3] eliminated 26 small clauses 0%
c [cce-13-3] eliminated 26 small clauses in 172866592 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 42 covered clauses in round 3
c [cce-13] eliminated 37105 covered clauses in TOTAL during 3 rounds
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 21001 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 727 variables 3% in round 1 in 39447232 steps
c [elim-14-1] backward subsumption/strengthening limit 39447200
c [elim-14-1-1] backward checking 3304 touched variables 16%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 6 and strengthened 8 clauses in 4803822 steps
c [elim-14-1] rescheduled 42 variables 0% by backward subsumption
c [elim-14-2] eliminated 1 variables 0% in round 2 in 494469 steps
c [elim-14-2] backward subsumption/strengthening limit 494400
c [elim-14-2-1] backward checking 13 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 3 and strengthened 0 clauses in 35557 steps
c [elim-14-2] rescheduled 5 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 9240 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 728 = 3% variables out of 21001 scheduled
c [bca-13] limit of 10000000 steps and 227820 added (scaled 2)
c [bca-13] 30079 out of 40548 literals actually usable 74%
c [bca-13] added 65 blocked clauses in 105902 steps
c [sweep-13] limit 18717337 penalty 0 = 0 + 0
c [sweep-13-1] 2976 pos 77.2% + 879 neg 22.8% = 3855 sched 19.0% ret 16418
c [sweep-13-1] 18798683 steps 1037 queries 648.66 avg class size
c [sweep-13-1] 8786 decisions 1033 SAT calls 17.01 avg env size
c [sweep-13-1] 1553 variables remain 8% (18719 retained 92%)
c [decomp-45] removed 12 variables
c [sweep-13-1] removed 12 vars (0 failed, 5 eqs, 10 impls)
c [sweep-13] 12 < 1/1000 * 20273 = 20 considered unsuccessful
c [sweep-13] removed 12 vars in TOTAL (1 rounds, 1036 queries)
c [phase-count-18] 110011 negative 97.5% of 112842 except 2831 2.5%
c [phase-count-18] 57494 positive 51.0% of 112842 except 55348 49.0%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 20261 enqueued variables after 423670 conflicts
c [score-dist-18] active 0 (0%), one 15025 (74%), zero 5236 (26%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 822 variables 3.9% (20261 remain 8%)
c [simplification-18] removed 40295 irredundant clauses 26.3% (112842 remain 9%)
c [simplification-18] maximum reduction of 26% = max (4%, 26%)
c [simplification-18] large reduction 26% >= 5% limit
c [simplification-18] next conflict interval 4236 = min (423670/100, 96709)
c [simplification-18] penalized conflict interval 4236 = 1 * 4236
c [simplification-18] hard conflict limit 437906 (soft 427906 + delta 10000)
c [simplification-18] new conflict limit 427906 (hard 437906)
c 
c [simplification-19] limit 427906 conflicts (hard 437906) hit after 427908 conflicts
c [quatres-15] found 11296 quaternary clauses 23% in total
c [quatres-15-1] removed 6 duplicate quaternary clauses
c [quatres-15-1] added 4 double-self-subsuming ternary resolvents
c [quatres-15-2] added 69 single-self-subsuming ternary resolvents
c [quatres-15-2] added 151 quaternary resolvents
c [ternres-15] limit 62760736 with penalty 0 = 0 + 0
c [ternres-15] 3 schedulable variables 0%
c [ternres-15] 2165 ternary resolvents (19 bin, 2146 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 784509 penalty 4 = 4 + 0
c [gauss-5] extracted 159 xors of average arity 3.0
c [gauss-5] connected 477 occurrences of 167 variables (average 2.9)
c [gauss-5] limit 784509 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-46] removed 2 variables
c [treelook-6] limit 6276073 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 10993 literals 27%
c [treelook-6] scheduling used 640080 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 6276073 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 6289243 steps
c [treelook-6] 10173 literals remain 25%
c [treelook-6] 991 variables remain to probed next time 5%
c [treelook-6] removed 1 variables, found 3609 hbrs
c [unhide-15] limit 12552147 with penalty 0 = 0 + 0
c [unhide-15-55] 0 units, 0 failed, 11580 tauts, 0 hbrs, 49017 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 532 transitive binary clauses
c [cce-14] limit of 313803684 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 55 (2%) of length 10
c [cce-14-1] eliminated 1 clauses out of 206 (0%) of length 9
c [cce-14-1] eliminated 3 clauses out of 148 (2%) of length 8
c [cce-14-1] eliminated 11 clauses out of 325 (3%) of length 7
c [cce-14-1] eliminated 11 clauses out of 3020 (0%) of length 6
c [cce-14-1] eliminated 18 clauses out of 16766 (0%) of length 5
c [cce-14-1] eliminated 32 clauses out of 3917 (1%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 77 large clauses in 124932189 steps
c [cce-14-1] allowing another 62466094 steps for small clauses
c [cce-14-1] scheduling 64041 clauses = 18139 binary + 45902 ternary
c [cce-14-1] tried to eliminate 64041 small clauses 100%
c [cce-14-1] eliminated 56 binary clauses 0%
c [cce-14-1] eliminated 519 ternary clauses 1%
c [cce-14-1] eliminated 575 small clauses 1%
c [cce-14-1] eliminated 575 small clauses in 191579890 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 652 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 60829437 steps for small clauses
c [cce-14-2] scheduling 63466 clauses = 18083 binary + 45383 ternary
c [cce-14-2] tried to eliminate 27921 small clauses 44%
c [cce-14-2] incomplete small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 652 covered clauses in TOTAL during 2 rounds
c [cce-14] 652 < 1/100 * 112796 = 1127 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 20258 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 63 variables 0% in round 1 in 38655747 steps
c [elim-15-1] backward subsumption/strengthening limit 38655700
c [elim-15-1-1] backward checking 548 touched variables 3%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 4 clauses in 682352 steps
c [elim-15-1] rescheduled 6 variables 0% by backward subsumption
c [elim-15-2] eliminated 2 variables 0% in round 2 in 1970 steps
c [elim-15-2] backward subsumption/strengthening limit 1900
c [elim-15-2-1] backward checking 15 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 1901 steps
c [elim-15-2] fully rescheduled 20193 variables 100%
c [elim-15-3] eliminated 12 variables 0% in round 3 in 38587683 steps
c [elim-15-3] backward subsumption/strengthening limit 38587600
c [elim-15-3-1] backward checking 102 touched variables 1%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 1 and strengthened 0 clauses in 226816 steps
c [elim-15] incomplete 4 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 77 = 0% variables out of 20258 scheduled
c [elim-15] 77 < 1/100 * 20258 = 202 considered unsuccessful
c [bca-14] limit of 10000000 steps and 225974 added (scaled 2)
c [bca-14] 29605 out of 40364 literals actually usable 73%
c [bca-14] added 54 blocked clauses in 108920 steps
c [phase-count-19] 109079 negative 97.5% of 111933 except 2854 2.5%
c [phase-count-19] 56781 positive 50.7% of 111933 except 55152 49.3%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-19] sorted 20181 enqueued variables after 427908 conflicts
c [score-dist-19] active 0 (0%), one 15028 (74%), zero 5153 (26%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 80 variables 0.4% (20181 remain 8%)
c [simplification-19] removed 909 irredundant clauses 0.8% (111933 remain 9%)
c [simplification-19] maximum reduction of 1% = max (0%, 1%)
c [simplification-19] geometric conflict interval increment 48354 = 96709 / 2
c [simplification-19] new conflict interval 145063
c [simplification-19] penalized conflict interval 145063 = 1 * 145063
c [simplification-19] hard conflict limit 645502 (soft 572971 + delta 72531)
c [simplification-19] new conflict limit 572971 (hard 645502)
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 -  257.5   20181   111933    467550   53046  96435 20456    8    17   33  47%    500   -5    8    8   95%
c i  263.1   20180   111933    499571   83935  96549 20476    8    16   41  46%    702   -5    5    8   63%
c i  263.8   20179   111933    502432   86619  96564 20483    8    15   41  49%   -949   -5    6    8   77%
c -  264.5   20172   111933    507143   58547  96569 20483    8    24   34  33%   -958    4    7    8   87%
c i  270.7   20171   111933    543525   94027  96638 20491    8    24   43  32%   -115    1    6    8   74%
c -  271.0   20171   111933    544877   62490  96640 20492    8    23   34  34%   -556    1    9    8  112%
c 
c [simplification-20] limit 572971 conflicts (hard 645502) hit after 580158 conflicts
c [quatres-16] found 11427 quaternary clauses 20% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-1] added 2 double-self-subsuming ternary resolvents
c [quatres-16-2] added 60 single-self-subsuming ternary resolvents
c [quatres-16-2] added 371 quaternary resolvents
c [ternres-16] limit 75795396 with penalty 0 = 0 + 0
c [ternres-16] all 20171 free variables schedulable
c [ternres-16] 3989 ternary resolvents (33 bin, 3956 trn)
c [ternres-16] 188 variables remain 1% (19983 retained 99%)
c [decomp-48] removed 26 variables
c [basicprobe-6] limit 378976980 penalty 0 = 0 + 0
c [basicprobe-6-0] 1279 sched 6%, 14 failed, 0 lifted, 1058 hbrs
c [decomp-49] removed 20 variables
c [basicprobe-6-1] 7829 sched 39%, 63 failed, 0 lifted, 1516 hbrs
c [decomp-50] removed 128 variables
c [basicprobe-6-2] 7665 sched 39%, 27 failed, 0 lifted, 138 hbrs
c [decomp-51] removed 137 variables
c [basicprobe-6-3] 7559 sched 38%, 29 failed, 0 lifted, 110 hbrs
c [decomp-52] removed 85 variables
c [basicprobe-6-4] 7479 sched 38%, 71 failed, 0 lifted, 220 hbrs
c [decomp-53] removed 254 variables
c [basicprobe-6-5] 7288 sched 37%, 28 failed, 1 lifted, 220 hbrs
c [decomp-54] removed 78 variables
c [basicprobe-6-6] 7216 sched 37%, 8 failed, 0 lifted, 143 hbrs
c [decomp-55] removed 12 variables
c [basicprobe-6-7] 7182 sched 37%, 8 failed, 0 lifted, 68 hbrs
c [decomp-56] removed 26 variables
c [basicprobe-6-8] 7156 sched 37%, 9 failed, 0 lifted, 134 hbrs
c [basicprobe-6-8] round limit 8 hit
c [basicprobe-6-8] 258 units = 257 failed (100%) + 1 lifted (0%)
c [basicprobe-6-8] removed 751 variables, found 3607 hbrs
c [bate-4] eliminated 55 asymmetric tautologies during probing
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 983 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 19404 variables 100%
c [block-6] limit of 47372122 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 182 blocked clauses
c [block-6] 182 < 1/100 * 105914 = 1059 considered unsuccessful
c [bca-15] limit of 10000000 steps and 213415 added (scaled 2)
c [bca-15] 26028 out of 38798 literals actually usable 67%
c [bca-15] added 3 blocked clauses in 142169 steps
c [sweep-14] limit 11369309 penalty 1 = 1 + 0
c [sweep-14-1] 1256 pos 81.0% + 294 neg 19.0% = 1550 sched 8.0% ret 17848
c [sweep-14-1] 11381105 steps 364 queries 366.59 avg class size
c [sweep-14-1] 3937 decisions 364 SAT calls 21.91 avg env size
c [sweep-14-1] 779 variables remain 4% (18619 retained 96%)
c [decomp-57] removed 3 variables
c [sweep-14-1] removed 3 vars (0 failed, 0 eqs, 0 impls)
c [sweep-14] 3 < 1/1000 * 19398 = 19 considered unsuccessful
c [sweep-14] removed 3 vars in TOTAL (1 rounds, 363 queries)
c [phase-count-20] 102979 negative 97.5% of 105627 except 2648 2.5%
c [phase-count-20] 51721 positive 49.0% of 105627 except 53906 51.0%
c [phase-count-20] skipping relative phase luck test
c [phase-20] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-20] sorted 19395 enqueued variables after 580158 conflicts
c [score-dist-20] active 0 (0%), one 15529 (80%), zero 3866 (20%)
c [score-dist-20] max exp 1, different 2 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 776 variables 3.8% (19395 remain 8%)
c [simplification-20] removed 6306 irredundant clauses 5.6% (105627 remain 8%)
c [simplification-20] maximum reduction of 6% = max (4%, 6%)
c [simplification-20] large reduction 6% >= 5% limit
c [simplification-20] next conflict interval 5801 = min (580158/100, 145063)
c [simplification-20] penalized conflict interval 5801 = 1 * 5801
c [simplification-20] hard conflict limit 595959 (soft 585959 + delta 10000)
c [simplification-20] new conflict limit 585959 (hard 595959)
c 
c [simplification-21] limit 585959 conflicts (hard 595959) hit after 585961 conflicts
c [quatres-17] found 10712 quaternary clauses 19% in total
c [quatres-17-1] removed 15 duplicate quaternary clauses
c [quatres-17-1] added 11 double-self-subsuming ternary resolvents
c [quatres-17-2] added 51 single-self-subsuming ternary resolvents
c [quatres-17-2] added 193 quaternary resolvents
c [ternres-17] limit 76452190 with penalty 0 = 0 + 0
c [ternres-17] 170 schedulable variables 1%
c [ternres-17] 3337 ternary resolvents (17 bin, 3320 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 2389130 penalty 4 = 4 + 0
c [card-6] found 1208 at-most-one constraints of average size 3.7
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2389130 for elimination
c [card-6] 1208 out of 1208 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-58] removed 1 variables
c [simpleprobe-7] 128 schedulable variables 1%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-59] removed 4 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 4 variables, found 13640 hbrs, 0 units
c [unhide-16] limit 7645219 with penalty 1 = 1 + 0
c [unhide-16-60] 0 units, 1 failed, 16321 tauts, 0 hbrs, 753887 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 547 transitive binary clauses
c [cce-15] limit of 191130476 steps penalty 1 = 1 + 0
c [cce-15-1] eliminated 3 clauses out of 139 (2%) of length 9
c [cce-15-1] eliminated 5 clauses out of 101 (5%) of length 8
c [cce-15-1] eliminated 9 clauses out of 105 (9%) of length 7
c [cce-15-1] eliminated 43 clauses out of 1731 (2%) of length 6
c [cce-15-1] eliminated 171 clauses out of 16380 (1%) of length 5
c [cce-15-1] eliminated 105 clauses out of 2593 (4%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 336 large clauses in 111482162 steps
c [cce-15-1] allowing another 55741081 steps for small clauses
c [cce-15-1] scheduling 60693 clauses = 17156 binary + 43537 ternary
c [cce-15-1] tried to eliminate 60693 small clauses 100%
c [cce-15-1] eliminated 361 binary clauses 2%
c [cce-15-1] eliminated 900 ternary clauses 2%
c [cce-15-1] eliminated 1261 small clauses 2%
c [cce-15-1] eliminated 1261 small clauses in 181264787 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 1597 covered clauses in round 1
c [cce-15-2] eliminated 2 clauses out of 16209 (0%) of length 5
c [cce-15-2] incomplete large round (ACCE)
c [cce-15-2] eliminated 2 large clauses in 9865697 steps
c [cce-15-2] allowing another 4932848 steps for small clauses
c [cce-15-2] scheduling 59432 clauses = 16795 binary + 42637 ternary
c [cce-15-2] tried to eliminate 2045 small clauses 3%
c [cce-15-2] eliminated 4 binary clauses 0%
c [cce-15-2] eliminated 4 small clauses 0%
c [cce-15-2] eliminated 4 small clauses in 9865689 steps
c [cce-15-2] incomplete small round (ACCE)
c [cce-15-2] eliminated 6 covered clauses in round 2
c [cce-15] eliminated 1603 covered clauses in TOTAL during 2 rounds
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 19388 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 687 variables 4% in round 1 in 32809948 steps
c [elim-16-1] backward subsumption/strengthening limit 32809900
c [elim-16-1-1] backward checking 2474 touched variables 13%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 45 and strengthened 28 clauses in 5417870 steps
c [elim-16-1] rescheduled 149 variables 1% by backward subsumption
c [elim-16-2] eliminated 19 variables 0% in round 2 in 1225452 steps
c [elim-16-2] backward subsumption/strengthening limit 1225400
c [elim-16-2-1] backward checking 148 touched variables 1%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 8 and strengthened 13 clauses in 728261 steps
c [elim-16-2] rescheduled 36 variables 0% by backward subsumption
c [elim-16-3] eliminated 4 variables 0% in round 3 in 378062 steps
c [elim-16-3] backward subsumption/strengthening limit 378000
c [elim-16-3-1] backward checking 43 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 1 and strengthened 2 clauses in 223367 steps
c [elim-16] incomplete 5 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 711 = 4% variables out of 19388 scheduled
c [bca-16] limit of 10000000 steps and 207097 added (scaled 2)
c [bca-16] 25123 out of 37356 literals actually usable 67%
c [bca-16] added 6 blocked clauses in 139990 steps
c [phase-count-21] 99955 negative 97.5% of 102480 except 2525 2.5%
c [phase-count-21] 49171 positive 48.0% of 102480 except 53309 52.0%
c [phase-count-21] skipping relative phase luck test
c [phase-21] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-21] sorted 18677 enqueued variables after 585961 conflicts
c [score-dist-21] active 0 (0%), one 14877 (80%), zero 3800 (20%)
c [score-dist-21] max exp 1, different 2 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 718 variables 3.7% (18677 remain 8%)
c [simplification-21] removed 3147 irredundant clauses 3.0% (102480 remain 8%)
c [simplification-21] maximum reduction of 4% = max (4%, 3%)
c [simplification-21] geometric conflict interval increment 29012 = 145063 / 5
c [simplification-21] new conflict interval 174075
c [simplification-21] penalized conflict interval 174075 = 1 * 174075
c [simplification-21] hard conflict limit 847073 (soft 760036 + delta 87037)
c [simplification-21] new conflict limit 760036 (hard 847073)
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 -  294.4   18677   102480    592560   60738  96858 18356    8    18   34  44%    177   -5    7    8   87%
c -  302.2   18677   102480    631810   64586  96910 18358    8    17   35  48%    558   -5   10    8  118%
c i  303.1   18676   102480    635972   68634  96920 18359    8    16   39  49%    587   -6    7    8   89%
c i  310.8   18664   102480    669201  100619  97000 18365    8    17   44  47%   -123   -4    6    8   70%
c -  311.3   18419   102480    671262   66998  97001 18365    8    17   36  46%   -528   -3    7    8   91%
c i  319.2   18418   102480    707540  102142  97055 18377    8    20   46  38%     91   -0    6    8   81%
c i  319.2   18415   102480    707770  102338  97062 18381    7    19   46  39%    -26   -1    6    8   70%
c -  320.8   18125   102480    713516   72283  97069 18382    7    15   36  50%   -385   -5    6    8   80%
c i  323.2   18124   102480    726739   84752  97102 18388    7    11   40  61%   -129   -8    6    8   78%
c i  323.3   16329   102480    727006   84972  97110 18393    7    11   40  62%   -192   -8    5    8   70%
c i  323.4   16321   102480    727401   85309  97118 18399    6    10   40  62%   -259   -8    5    8   65%
c i  323.4   16308   102480    727403   85309  97118 18400    6    10   40  62%   -259   -8    5    8   65%
c i  323.4   16302   102480    727584   85440  97129 18405    6    10   40  62%   -282   -8    5    8   59%
c 0  323.4   14459   102480    727584   85440  97129 18405    6    10   40  62%   -282   -8    5    8   59%
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 UNSATISFIABLE
c
c bate: 339 basic ate = 204 trn 60% + 135 lrg 40% in 4 updates
c bcas: 16 count, 3280 added (4652 skipped), 2427337 steps
c bkwd: tried 580346 clauses, 1159961 lits, 2.00 lits/clause
c bkwd: checked 55344205 occs, 95.36 occs/clause, 47.71 occs/lit
c bkwd: subsumed 0 binary, 369 ternary, 200 large
c bkwd: strengthened 7 binary, 56 ternary (100% self), 220 large (0% self)
c blkd: 6 bces, 18314 removed, 6055370 resolutions, 17391566 steps
c blkd: 22080 blocking literals 4%, 20 pure
c bump: 726988 bumped seen, 51166724 lits 70.4 on average
c card: 6 count, 0 units, 0 am1, 129683645 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 34167 subsumed
c card: 8308 at-most-one constraints found, average size 3.72
c card: 8308 at-most-one constraints used 100%, average size 3.72
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 15 cces, 136851 eliminated, 110496 ate 81%, 26355 abce 19%
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: 5254282 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 164 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 59 decompositions, 59841 equivalent 21%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1629009 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 133309 eliminated 47%, 593 pure 0%
c elms: 35 rounds, 2.2 rounds/bve
c elms: 128173 small 96%, 4523 large 3%
c elms: 276369 tried small, 128173 succeeded 46%, 148196 failed 54%
c elms: 13592 subsumed, 36841 strengthened, 705 blocked
c elms: 11486939 copies, 12250437 resolutions, 6580613 ipos
c elms: 26848295 subchks, 7620100 strchks
c gaus: 5 extractions, 648 extracted, 2.7 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10267742 steps, 5133871 extr 50%, 13449 elim 0%
c glue: 8.0 orig avg, 8.0 real avg, 2.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 493361 = 81223 simple 16% + 411828 trn 83% + 310 lrg 0%, 21116 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 726988 clauses, 33.4 length
c lrnd: 24250934 lits = 34544584 orig - 10293650 removed 30%
c lrnd: 157806 uips 22%, 495470 flips 68%
c mins: 711512 mins 98%, 1093 bin 0%, 14383 size 2%
c mins: 62184530 poisoned searches, 11371008 hits, 18% hit rate
c mins: 84575953 used twice searches, 2153510 hits, 3% hit rate
c move: moved 144369, 23761 bin 16%, 120608 trn 84%
c otfs: 3979 driving 27%, 10605 restarting 73%
c otfs: str 14584, 13728 red 94%, 856 irr 6%
c otfs: str 14584, 0 bin 0%, 353 trn 2%, 14231 lrg 98%
c otfs: sub 381, 266 red 70%, 115 irr 30%
c otfs: sub 381, 0 bin 0%, 49 trn 13%, 332 lrg 87%
c phas: 21 computed, 178162 set, 894 pos (1%), 177268 neg (99%)
c prbs: 6 basic, 230248 probed, 906 failed, 120 lifted
c prbs: 7 simple, 227969 probed, 90 failed, 21065 eqs
c prbs: 6 treelook, 1530 probed, 8 failed, 0 lifted
c prom: 174987 locked 17% out of 1026232 tried
c prps: 392602740 props, 226 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 17 count, 11962 quat, 2844 self1, 163 self2, 2822 dup
c queu: 21 sorted, 1629009 next (14 steps 0.00)
c queu: 52167753 enq (52167710 steps 1.00), 51166724 deq 98%
c redc: 51045 clauses 24%, 212486 tried 29%, 51 sat 0%
c redc: 83114 lits 3%, 2805631 tried 8%, 52 sat 0%
c redc: 1312 times jump level reduced, 2.2 levels on average
c reds: 15 count, 48505.6 conflicts per reduce
c reds: 0 memlim 0%, 15 arith 100%
c reds: 427527 collected 84%, 80125 retired 16%
c rmbd: 93259 removed, 90972 red 98%
c rsts: 18088 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: 21 count, 20 confs 95%, 0 vars 0%
c simp: 0 its 0%, 1 bin 5%, 0 trns 0%
c subl: 726988 count (359994 tried 0.5), 17311 sub out of 718947 (2.4%)
c swps: 14 count, 14 rounds, 5586 queries (399.0/round)
c swps: 5150 sat calls, 115 unsat (0.7% success rate)
c swps: 55214 decisions 10.7, 3383 conflicts 0.7
c swps; 1536.7 avg class size, 31.1 avg environment size
c swps: 2 failed, 1028 impls, 519 equivs
c swp0: 1857 type 0 queries, 137 unsat (7.4%), 1816 sat (97.8%)
c swp1: 3729 type 1 queries, 1169 unsat (31.3%), 3251 sat (87.2%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 4712434 calls to obtain time
c tops: 75233 fixed 27%, 20 its, 36379.20 confs/it
c trds: 17 transitive reductions, 13062 removed, 4 failed
c trds: 265860 nodes, 199151 edges, 31000138 steps
c trim: 270270 words, 1.0 MB
c trnr: 17 count, 507 bin, 79037 trn, 586159214 steps
c unhd: 16 count, 60 rounds, 89525960 steps
c unhd: 3175 non-trivial sccs of average size 3.0
c unhd: 135 units, 131 bin, 3 trn, 1 lrg
c unhd: 372 failed, 335 stamp, 0 lits, 2 bin, 29 trn, 1 lrg
c unhd: 230427 tauts, 4370 bin 2%, 28207 trn 12%, 8836 lrg 4%
c unhd: 230427 tauts, 189014 stamp 82%, 212414 red 92%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 2004895 str, 131 bin 0%, 28526 trn 1%, 1976238 lrg 99%, 1974138 red 98%
c vars: 14459 remaining 5% and 268383 removed 95% out of 282842
c vars: 75233 fixed 27%, 133309 eliminated 47%, 59841 equivalent 21%
c vsts: 9802671459 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 24.8 search visits per propagation, 12554.0 per conflict
c wchs: 1154651986 pushed, 29931788 enlarged, 244 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         730909        427527         80125      16997843       5196090        346943
c 
c  0 0        114966  16     17507   4         0   0  12532592  74<  2972172  57    142461  41     1.9
c  1 5         78121  11     40932  10     10799  13   1794984  11    707511  14<    52054  15<    1.0
c  2 6        254606  35<   172806  40<    28899  36   1991056  12   1048127  20    100784  29     3.3
c  3 9        226467  31    160668  38     29206  36<   589692   3    406640   8     45138  13     3.7
c  4 14        52110   7     33484   8      9818  12     83026   0     57829   1      6056   2     0.8
c  5 21         4310   1      2001   0      1292   2      6059   0      3582   0       426   0     0.1
c  6 30          312   0       123   0       108   0       416   0       218   0        23   0     0.0
c  7 41           17   0         6   0         3   0        18   0        11   0         1   0     0.0
c 
c avg                  2.1           2.4           2.5           0.5           0.8           1.2
c std                  1.2           0.9           0.9           0.9           1.1           1.2
c 
c   61.672  19% cce
c   22.336   7% probe
c   21.556   7% elim
c   14.152   4% unhide
c    8.923   3% sweep
c    5.291   2% ternres
c    3.190   1% bump
c    2.983   1% transred
c    1.986   1% quatres
c    1.646   1% bca
c 
c    3.455 < 1% rest (below)
c 
c    1.566   0% block
c    0.982   0% decide
c    0.529   0% gauss
c    0.378   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    3.349   1% preprocessing     2%
c  146.866  45% inprocessing     98%
c ==================================
c  150.215  46% simplifying
c  173.187  54% search
c ==================================
c  323.407 100% all
c 
c        727584 conflicts,        2249.7 confs/sec
c          5855 ternaries,         124.3 confs/ternary
c          1314 binaries,          553.7 confs/binary
c            20 iterations,      36379.2 confs/iteration
c 
c            15 reductions,          0.0 redus/sec,  48505.6 confs/reduction
c         18088 restarts,           55.9 rests/sec,     40.2 confs/restart
c       1629009 decisions,        5037.0 decis/sec,      2.2 decis/conflict
c     392602740 propagations,  1213958.8 props/sec,    241.0 props/decision
c 
c 323.4 seconds, 128.6 MB
c launch: done
