c launch: /data/cnf/sc2014/app/9dlx_vliw_at_b_iq4.cnf.bz2
c host: atom01
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/9dlx_vliw_at_b_iq4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/9dlx_vliw_at_b_iq4.cnf.bz2
c no embedded options
c found 'p cnf 106013 1598301' header
c read 106013 variables, 1598301 clauses, 4617403 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=4
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 106012 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] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
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  106012  1598300         0       0      0     0    0     0   48   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 19 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 19 out of 19 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 7 variables
c [simpleprobe-1] all 106006 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 533 variables
c [simpleprobe-1] 74690 variables remain 71% (30783 retained 29%)
c [simpleprobe-1] removed 533 variables, found 15999 hbrs, 532 units
c [unhide-1] limit 99313 based on 1589016 irredundant clauses
c [unhide-1-1] 27 units, 2 failed, 2334 tauts, 0 hbrs, 16640 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 105445 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 99852 not tried 95% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 5593 = 5% variables out of 105445 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 1574931 negative 100.0% of 1575313 except 382 0.0%
c [phase-count-1] 433508 positive 27.5% of 1575313 except 1141805 72.5%
c [phase-count-1] less non-negative clauses 382 than limit 157500 (10.0%)
c [phase-count-1] non-pos/non-neg = 1141805/382 = 2989.02 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 99852 negative 100%
c [sort-queue-1] sorted 99852 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 99852 (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 6154 variables 5.8% (99852 remain 94%)
c [simplification-1] removed 22987 irredundant clauses 1.4% (1575313 remain 99%)
c [simplification-1] maximum reduction of 6% = max (6%, 1%)
c [simplification-1] large reduction 6% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [simpleprobe-2] 70968 schedulable variables 71%
c [simpleprobe-2] limit 3150626 based on 1575313 irredundant clauses
c [decomp-4] removed 176 variables
c [simpleprobe-2] 71814 variables remain 72% (27862 retained 28%)
c [simpleprobe-2] removed 176 variables, found 3313 hbrs, 176 units
c [treelook-1] limit 392949 based on 1571798 irredundant clauses
c [treelook-1] scheduled 74104 literals 37%
c [treelook-1] scheduling used 392953 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 392949 based on 1571798 irredundant clauses
c [treelook-1] used 438689 steps
c [treelook-1] 74099 literals remain 37%
c [treelook-1] 71912 variables remain to probed next time 72%
c [treelook-1] removed 0 variables, found 11 hbrs
c [basicprobe-1] limit 12574384 based on 1571798 irredundant clauses
c [basicprobe-1-0] 93527 probes remain 98% after last round
c [basicprobe-1-0] 36 units = 36 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 4288 variables, found 10551 hbrs
c [unhide-2] limit 98237 based on 1571798 irredundant clauses
c [unhide-2-2] 2768 units, 0 failed, 603 tauts, 0 hbrs, 29881 literals
c [elim-2] 92620 variables 100% will be scheduled this time
c [elim-2] scheduled 92620 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 82959 not tried 90% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 9661 = 10% variables out of 92620 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 74859 enqueued variables after 1001 conflicts
c [score-dist-2] active 8100 (10%), one 0 (0%), zero 74859 (90%)
c [score-dist-2] max exp 509, different 12 (2%)
c [score-dist-2] median active exp 502, avg 502.4
c [simplification-2] removed 16893 variables 16.9% (82959 remain 78%)
c [simplification-2] removed 132269 irredundant clauses 8.4% (1443044 remain 90%)
c [simplification-2] maximum reduction of 17% = max (17%, 8%)
c [simplification-2] large reduction 17% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
c 
c  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   10.8   82958  1443044      1296    1008     10 21045    8   489   52   2%      9  484   31    1 5657%
c 
c [simplification-3] limit 3001 conflicts (hard 13001) hit after 3001 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 18 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 18 out of 18 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 370 variables
c [unhide-3] limit 90143 based on 1442299 irredundant clauses
c [unhide-3-3] 0 units, 1 failed, 4927 tauts, 0 hbrs, 8555 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 82588 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 66310 not tried 80% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 8011 = 10% variables out of 82588 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 60722 enqueued variables after 3001 conflicts
c [score-dist-3] active 13855 (19%), one 0 (0%), zero 60722 (81%)
c [score-dist-3] max exp 509, different 20 (4%)
c [score-dist-3] median active exp 501, avg 499.7
c [simplification-3] removed 8381 variables 10.1% (74577 remain 70%)
c [simplification-3] removed 21012 irredundant clauses 1.5% (1422032 remain 89%)
c [simplification-3] maximum reduction of 10% = max (10%, 1%)
c [simplification-3] large reduction 10% >= 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 15001 (soft 5001 + delta 10000)
c [simplification-3] new conflict limit 5001 (hard 15001)
c 
c [simplification-4] limit 5001 conflicts (hard 15001) hit after 5013 conflicts
c [decomp-7] removed 5 variables
c [treelook-2] limit 355454 based on 1421818 irredundant clauses
c [treelook-2] scheduled 58744 literals 39%
c [treelook-2] scheduling used 356398 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 355454 based on 1421818 irredundant clauses
c [treelook-2] used 1266728 steps
c [treelook-2] 58740 literals remain 39%
c [treelook-2] 52455 variables remain to probed next time 70%
c [treelook-2] removed 0 variables, found 337 hbrs
c [unhide-4] limit 88863 based on 1421818 irredundant clauses
c [unhide-4-4] 479 units, 2 failed, 168 tauts, 0 hbrs, 17480 literals
c [elim-4] 65264 variables 89% will be scheduled this time
c [elim-4] scheduled 65264 variables 89%
c [elim-4] boosting limit by 20
c [elim-4] limit of 502039140 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 5870 variables 8% in round 1 in 306358627 steps
c [elim-4-1] backward subsumption/strengthening limit 195680513
c [elim-4-1-1] backward checking 47486 touched variables 65%
c [elim-4-1-1] incomplete backward checking 47665 remain 100%
c [elim-4-1] subsumed 327 and strengthened 123 clauses in 195682006 steps
c [elim-4] incomplete 1201 not tried 2% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 5870 = 9% variables out of 65264 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 49715 enqueued variables after 5013 conflicts
c [score-dist-4] active 17938 (27%), one 0 (0%), zero 49715 (73%)
c [score-dist-4] max exp 509, different 27 (5%)
c [score-dist-4] median active exp 499, avg 498.0
c [simplification-4] removed 6924 variables 9.3% (67653 remain 64%)
c [simplification-4] removed 95353 irredundant clauses 6.7% (1326679 remain 83%)
c [simplification-4] maximum reduction of 9% = max (9%, 7%)
c [simplification-4] large reduction 9% >= 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 17013 (soft 7013 + delta 10000)
c [simplification-4] new conflict limit 7013 (hard 17013)
c 
c [simplification-5] limit 7013 conflicts (hard 17013) hit after 7013 conflicts
c [quatres-1] found 16100 quaternary clauses 16% in total
c [quatres-1-2] added 109 single-self-subsuming ternary resolvents
c [quatres-1-2] added 806 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 67653 free variables schedulable
c [ternres-1] 33611 ternary resolvents (1 bin, 33610 trn)
c [ternres-1] 923 variables remain 1% (66730 retained 99%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 5 xors of average arity 2.0
c [gauss-1] connected 10 occurrences of 9 variables (average 1.1)
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 42 variables
c [basicprobe-2] limit 10611936 based on 1326492 irredundant clauses
c [basicprobe-2-0] 63151 probes remain 93% after last round
c [basicprobe-2-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 9 variables, found 10673 hbrs
c [bate-1] eliminated 2 asymmetric tautologies during probing
c [unhide-5] limit 88113 with penalty 2 = 0 + 2
c [unhide-5-5] 84 units, 10 failed, 14448 tauts, 0 hbrs, 13335 literals
c [transred-1] limit 1762265 with penalty 0 = 0 + 0
c [transred-1] removed 4 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 67509 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 125511 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 5 (40%) of length 113
c [cce-1-1] eliminated 1 clauses out of 7 (14%) of length 111
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 110
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 109
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 108
c [cce-1-1] eliminated 3 clauses out of 6 (50%) of length 106
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 105
c [cce-1-1] eliminated 7 clauses out of 13 (54%) of length 104
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 103
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 102
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 101
c [cce-1-1] eliminated 3 clauses out of 7 (43%) of length 100
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 99
c [cce-1-1] eliminated 11 clauses out of 23 (48%) of length 98
c [cce-1-1] eliminated 17 clauses out of 29 (59%) of length 97
c [cce-1-1] eliminated 3 clauses out of 11 (27%) of length 96
c [cce-1-1] eliminated 15 clauses out of 47 (32%) of length 95
c [cce-1-1] eliminated 5 clauses out of 21 (24%) of length 94
c [cce-1-1] eliminated 1 clauses out of 19 (5%) of length 93
c [cce-1-1] eliminated 4 clauses out of 43 (9%) of length 92
c [cce-1-1] eliminated 3 clauses out of 39 (8%) of length 91
c [cce-1-1] eliminated 3 clauses out of 42 (7%) of length 90
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 96 large clauses in 30000037 steps
c [cce-1-1] allowing another 15000018 steps for small clauses
c [cce-1-1] scheduling 1078734 clauses = 1039939 binary + 38795 ternary
c [cce-1-1] tried to eliminate 305 small clauses 0%
c [cce-1-1] eliminated 171 binary clauses 0%
c [cce-1-1] eliminated 171 small clauses 0%
c [cce-1-1] eliminated 171 small clauses in 30002257 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 267 covered clauses in round 1
c [cce-1] eliminated 267 covered clauses in TOTAL during 1 rounds
c [cce-1] 267 < 1/100 * 1184626 = 11846 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 65375 variables 100%
c [elim-5] limit of 35245310 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 29469 not tried 45% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 3407 = 5% variables out of 65375 scheduled
c [bca-1] limit of 10000000 steps and 2361124 added (scaled 2)
c [bca-1] 107904 out of 123938 literals actually usable 87%
c [bca-1] added 12255 blocked clauses in 393564 steps
c [sweep-1] limit 2360624 based on 1180312 irredundant clauses
c [sweep-1-1] 5076 pos 8.2% + 56892 neg 91.8% = 61968 sched 100.0% ret 0
c [sweep-1-1] 2486466 steps 12 queries 7172.25 avg class size
c [sweep-1-1] 438 decisions 10 SAT calls 561.80 avg env size
c [sweep-1-1] 61930 variables remain 100% (38 retained 0%)
c [decomp-10] removed 15 variables
c [sweep-1-1] removed 15 vars (0 failed, 3 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 15 vars in TOTAL (1 rounds, 11 queries)
c [sort-queue-5] sorted 39273 enqueued variables after 7013 conflicts
c [score-dist-5] active 22680 (37%), one 0 (0%), zero 39273 (63%)
c [score-dist-5] max exp 509, different 35 (7%)
c [score-dist-5] median active exp 498, avg 496.1
c [simplification-5] removed 5700 variables 8.4% (61953 remain 58%)
c [simplification-5] removed 146452 irredundant clauses 11.0% (1180227 remain 74%)
c [simplification-5] maximum reduction of 11% = max (8%, 11%)
c [simplification-5] large reduction 11% >= 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 19013 (soft 9013 + delta 10000)
c [simplification-5] new conflict limit 9013 (hard 19013)
c 
c [simplification-6] limit 9013 conflicts (hard 19013) hit after 9013 conflicts
c [quatres-2] found 15579 quaternary clauses 16% in total
c [quatres-2-2] added 3 single-self-subsuming ternary resolvents
c [quatres-2-2] added 398 quaternary resolvents
c [ternres-2] limit 4720840 based on 1180210 irredundant clauses
c [ternres-2] 896 schedulable variables 1%
c [ternres-2] 4008 ternary resolvents (3 bin, 4005 trn)
c [ternres-2] 358 variables remain 1% (61595 retained 99%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 9 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 9 out of 9 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 45144 schedulable variables 73%
c [simpleprobe-3] limit 9047327 penalty 0 = 0 + 0
c [simpleprobe-3] 47153 variables remain 76% (14800 retained 24%)
c [simpleprobe-3] removed 0 variables, found 11608 hbrs, 0 units
c [unhide-6] limit 113091 with penalty 2 = 0 + 2
c [unhide-6-6] 21 units, 23 failed, 520 tauts, 0 hbrs, 20396 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 7 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 61912 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 18506 blocked clauses
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 61904 variables 100%
c [elim-6] limit of 45236639 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 19295 not tried 31% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 677 = 1% variables out of 61904 scheduled
c [bca-2] limit of 10000000 steps and 2322189 added (scaled 2)
c [bca-2] 102207 out of 122456 literals actually usable 83%
c [bca-2] added 934 blocked clauses in 353423 steps
c [sweep-2] limit 2315562 based on 1157781 irredundant clauses
c [sweep-2-1] 5645 pos 9.2% + 55545 neg 90.8% = 61190 sched 99.9% ret 37
c [sweep-2-1] 2513228 steps 37 queries 10719.41 avg class size
c [sweep-2-1] 1038 decisions 30 SAT calls 84.37 avg env size
c [sweep-2-1] 60811 variables remain 99% (416 retained 1%)
c [decomp-13] removed 8 variables
c [sweep-2-1] removed 8 vars (0 failed, 6 eqs, 10 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 8 vars in TOTAL (1 rounds, 36 queries)
c [sort-queue-6] sorted 33965 enqueued variables after 9013 conflicts
c [score-dist-6] active 27254 (45%), one 0 (0%), zero 33965 (55%)
c [score-dist-6] max exp 509, different 43 (8%)
c [score-dist-6] median active exp 494, avg 492.7
c [simplification-6] removed 734 variables 1.2% (61219 remain 58%)
c [simplification-6] removed 22452 irredundant clauses 1.9% (1157775 remain 72%)
c [simplification-6] maximum reduction of 2% = max (1%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 6666
c [simplification-6] penalized conflict interval 6666 = 1 * 6666
c [simplification-6] hard conflict limit 25679 (soft 15679 + delta 10000)
c [simplification-6] new conflict limit 15679 (hard 25679)
c 
c [simplification-7] limit 15679 conflicts (hard 25679) hit after 15679 conflicts
c [quatres-3] found 15070 quaternary clauses 17% in total
c [quatres-3-2] added 4 single-self-subsuming ternary resolvents
c [quatres-3-2] added 149 quaternary resolvents
c [ternres-3] limit 4630752 based on 1157688 irredundant clauses
c [ternres-3] 358 schedulable variables 1%
c [ternres-3] 3141 ternary resolvents (7 bin, 3134 trn)
c [ternres-3] 119 variables remain 0% (61100 retained 100%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-7] limit 183830 with penalty 2 = 0 + 2
c [unhide-7-7] 99 units, 2 failed, 12423 tauts, 0 hbrs, 25646 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 3 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 61118 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 35335 blocked clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 8 (25%) of length 110
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 108
c [cce-2-1] eliminated 1 clauses out of 59 (2%) of length 89
c [cce-2-1] eliminated 13 clauses out of 42 (31%) of length 88
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 17 large clauses in 15001034 steps
c [cce-2-1] allowing another 7500517 steps for small clauses
c [cce-2-1] scheduling 984263 clauses = 966313 binary + 17950 ternary
c [cce-2-1] tried to eliminate 170 small clauses 0%
c [cce-2-1] eliminated 13 binary clauses 0%
c [cce-2-1] eliminated 13 small clauses 0%
c [cce-2-1] eliminated 13 small clauses in 15000519 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 30 covered clauses in round 1
c [cce-2] eliminated 30 covered clauses in TOTAL during 1 rounds
c [cce-2] 30 < 1/100 * 1109233 = 11092 considered unsuccessful
c [elim-7] 19287 variables 32% will be scheduled this time
c [elim-7] scheduled 19287 variables 32%
c [elim-7] limit of 73532076 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 4696 not tried 8% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 505 = 3% variables out of 19287 scheduled
c [elim-7] 505 < 1/100 * 19287 = 192 considered unsuccessful
c [bca-3] limit of 10000000 steps and 2218256 added (scaled 2)
c [bca-3] 96098 out of 121222 literals actually usable 79%
c [bca-3] added 1160 blocked clauses in 321647 steps
c [sweep-3] limit 2211162 based on 1105581 irredundant clauses
c [sweep-3-1] 5623 pos 9.3% + 54588 neg 90.7% = 60211 sched 99.3% ret 399
c [sweep-3-1] 2414073 steps 17 queries 14057.76 avg class size
c [sweep-3-1] 674 decisions 15 SAT calls 370.93 avg env size
c [sweep-3-1] 59516 variables remain 99% (450 retained 1%)
c [decomp-15] removed 654 variables
c [sweep-3-1] removed 654 vars (0 failed, 3 eqs, 4 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 654 vars in TOTAL (1 rounds, 16 queries)
c [sort-queue-7] sorted 27539 enqueued variables after 15679 conflicts
c [score-dist-7] active 32417 (54%), one 0 (0%), zero 27539 (46%)
c [score-dist-7] max exp 509, different 68 (13%)
c [score-dist-7] median active exp 490, avg 486.7
c [simplification-7] removed 1263 variables 2.1% (59956 remain 57%)
c [simplification-7] removed 66947 irredundant clauses 5.8% (1090826 remain 68%)
c [simplification-7] maximum reduction of 6% = max (2%, 6%)
c [simplification-7] large reduction 6% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 27679 (soft 17679 + delta 10000)
c [simplification-7] new conflict limit 17679 (hard 27679)
c 
c [simplification-8] limit 17679 conflicts (hard 27679) hit after 17679 conflicts
c [quatres-4] found 12886 quaternary clauses 15% in total
c [quatres-4-2] added 19 single-self-subsuming ternary resolvents
c [quatres-4-2] added 212 quaternary resolvents
c [ternres-4] limit 4363300 based on 1090825 irredundant clauses
c [ternres-4] 119 schedulable variables 0%
c [ternres-4] 1738 ternary resolvents (4 bin, 1734 trn)
c [ternres-4] 29 variables remain 0% (59927 retained 100%)
c [unhide-8] limit 201851 with penalty 2 = 0 + 2
c [unhide-8-8] 40 units, 5 failed, 1750 tauts, 0 hbrs, 17468 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 15 transitive binary clauses
c [transred-4] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 59913 variables 100%
c [block-4] limit of 50000000 steps penalty 0 = 0 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 32066 blocked clauses
c [bca-4] limit of 10000000 steps and 2121468 added (scaled 2)
c [bca-4] 92921 out of 118698 literals actually usable 78%
c [bca-4] added 4406 blocked clauses in 320958 steps
c [sweep-4] limit 2113794 based on 1056897 irredundant clauses
c [sweep-4-1] 5319 pos 9.0% + 53585 neg 91.0% = 58904 sched 99.3% ret 444
c [sweep-4-1] 2169648 steps 12 queries 14219.25 avg class size
c [sweep-4-1] 613 decisions 11 SAT calls 205.91 avg env size
c [sweep-4-1] 58843 variables remain 99% (505 retained 1%)
c [decomp-17] removed 3 variables
c [sweep-4-1] removed 3 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 3 vars in TOTAL (1 rounds, 11 queries)
c [sort-queue-8] sorted 26133 enqueued variables after 17679 conflicts
c [score-dist-8] active 33212 (56%), one 0 (0%), zero 26133 (44%)
c [score-dist-8] max exp 509, different 76 (15%)
c [score-dist-8] median active exp 487, avg 482.8
c [simplification-8] removed 611 variables 1.0% (59345 remain 56%)
c [simplification-8] removed 33936 irredundant clauses 3.1% (1056890 remain 66%)
c [simplification-8] maximum reduction of 3% = max (1%, 3%)
c [simplification-8] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-8] new conflict interval 11666
c [simplification-8] penalized conflict interval 11666 = 1 * 11666
c [simplification-8] hard conflict limit 39345 (soft 29345 + delta 10000)
c [simplification-8] new conflict limit 29345 (hard 39345)
c 
c [simplification-9] limit 29345 conflicts (hard 39345) hit after 29345 conflicts
c [quatres-5] found 13067 quaternary clauses 16% in total
c [quatres-5-2] added 2 single-self-subsuming ternary resolvents
c [quatres-5-2] added 27 quaternary resolvents
c [ternres-5] limit 6028937 with penalty 0 = 0 + 0
c [ternres-5] 29 schedulable variables 0%
c [ternres-5] 1300 ternary resolvents (2 bin, 1298 trn)
c [ternres-5] 8 variables remain 0% (59337 retained 100%)
c [treelook-3] limit 264221 based on 1056884 irredundant clauses
c [treelook-3] scheduled 41335 literals 35%
c [treelook-3] scheduling used 268203 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 264221 based on 1056884 irredundant clauses
c [treelook-3] used 664472 steps
c [treelook-3] 41331 literals remain 35%
c [treelook-3] 35938 variables remain to probed next time 61%
c [treelook-3] removed 0 variables, found 58 hbrs
c [unhide-9] limit 301446 with penalty 2 = 0 + 2
c [unhide-9-9] 4 units, 8 failed, 8234 tauts, 0 hbrs, 26814 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 5 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 59337 variables 100%
c [block-5] limit of 60289374 steps penalty 0 = 0 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 2608 blocked clauses
c [block-5] 2608 < 1/100 * 1049476 = 10494 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 59265 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1205787480 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1658 variables 3% in round 1 in 516282927 steps
c [elim-8-1] backward subsumption/strengthening limit 516282900
c [elim-8-1-1] backward checking 13761 touched variables 23%
c [elim-8-1-1] incomplete backward checking 13775 remain 100%
c [elim-8-1] subsumed 0 and strengthened 11 clauses in 516287581 steps
c [elim-8-1] rescheduled 24 variables 0% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 965993 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1658 = 3% variables out of 59265 scheduled
c [bca-5] limit of 10000000 steps and 2068061 added (scaled 2)
c [bca-5] 88282 out of 115216 literals actually usable 77%
c [bca-5] added 312 blocked clauses in 311921 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 18086810 penalty 0 = 0 + 0
c [sweep-5-1] 4250 pos 7.4% + 52860 neg 92.6% = 57110 sched 99.1% ret 497
c [sweep-5-1] 18180942 steps 169 queries 2409.50 avg class size
c [sweep-5-1] 5302 decisions 157 SAT calls 201.06 avg env size
c [sweep-5-1] 51884 variables remain 91% (5141 retained 9%)
c [decomp-20] removed 1068 variables
c [sweep-5-1] removed 1068 vars (0 failed, 18 eqs, 29 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1068 vars in TOTAL (1 rounds, 168 queries)
c [sort-queue-9] sorted 23827 enqueued variables after 29345 conflicts
c [score-dist-9] active 32712 (58%), one 0 (0%), zero 23827 (42%)
c [score-dist-9] max exp 510, different 122 (24%)
c [score-dist-9] median active exp 459, avg 461.2
c [simplification-9] removed 2806 variables 4.7% (56539 remain 53%)
c [simplification-9] removed 42547 irredundant clauses 4.0% (1014337 remain 63%)
c [simplification-9] maximum reduction of 5% = max (5%, 4%)
c [simplification-9] large reduction 5% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 41345 (soft 31345 + delta 10000)
c [simplification-9] new conflict limit 31345 (hard 41345)
c 
c [simplification-10] limit 31345 conflicts (hard 41345) hit after 31346 conflicts
c [quatres-6] found 11389 quaternary clauses 15% in total
c [quatres-6-2] added 91 quaternary resolvents
c [ternres-6] limit 6331696 with penalty 0 = 0 + 0
c [ternres-6] 8 schedulable variables 0%
c [ternres-6] 41 ternary resolvents (0 bin, 41 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 395731 penalty 3 = 3 + 0
c [card-4] found 10 at-most-one constraints of average size 3.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 395731 for elimination
c [card-4] 10 out of 10 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 507167 based on 1014335 irredundant clauses
c [gauss-3] extracted 1 xors of average arity 3.0
c [gauss-3] connected 3 occurrences of 3 variables (average 1.0)
c [gauss-3] limit 507167 based on 1014335 irredundant clauses
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 31658484 penalty 0 = 0 + 0
c [basicprobe-3-0] 51225 probes remain 91% after last round
c [basicprobe-3-0] 60 units = 60 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 60 variables, found 8776 hbrs
c [bate-2] eliminated 5 asymmetric tautologies during probing
c [unhide-10] limit 316584 with penalty 2 = 0 + 2
c [unhide-10-10] 561 units, 10 failed, 2401 tauts, 0 hbrs, 61943 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 14 transitive binary clauses
c [transred-6] found 1 units
c [cce-3] limit of 7914621 steps penalty 2 = 2 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 3957311 steps for small clauses
c [cce-3-1] scheduling 916223 clauses = 882396 binary + 33827 ternary
c [cce-3-1] tried to eliminate 30 small clauses 0%
c [cce-3-1] eliminated 13 binary clauses 0%
c [cce-3-1] eliminated 13 small clauses 0%
c [cce-3-1] eliminated 9035 small clauses in 7914634 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 9035 covered clauses in round 1
c [cce-3] eliminated 9035 covered clauses in TOTAL during 1 rounds
c [cce-3] 9035 < 1/100 * 1012859 = 10128 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 55902 variables 100%
c [elim-9] limit of 126633938 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 2762 not tried 5% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 762 = 1% variables out of 55902 scheduled
c [bca-6] limit of 10000000 steps and 2007007 added (scaled 2)
c [bca-6] 83760 out of 110282 literals actually usable 76%
c [bca-6] added 9114 blocked clauses in 308253 steps
c [sweep-6] limit 1996974 based on 998487 irredundant clauses
c [sweep-6-1] 3330 pos 6.7% + 46726 neg 93.3% = 50056 sched 90.8% ret 5084
c [sweep-6-1] 2251486 steps 18 queries 7709.44 avg class size
c [sweep-6-1] 779 decisions 14 SAT calls 311.14 avg env size
c [sweep-6-1] 49972 variables remain 91% (5168 retained 9%)
c [decomp-22] removed 6 variables
c [sweep-6-1] removed 6 vars (0 failed, 3 eqs, 6 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 6 vars in TOTAL (1 rounds, 17 queries)
c [sort-queue-10] sorted 22790 enqueued variables after 31346 conflicts
c [score-dist-10] active 32344 (59%), one 0 (0%), zero 22790 (41%)
c [score-dist-10] max exp 510, different 130 (25%)
c [score-dist-10] median active exp 461, avg 457.8
c [simplification-10] removed 1405 variables 2.5% (55134 remain 52%)
c [simplification-10] removed 15854 irredundant clauses 1.6% (998483 remain 62%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-10] new conflict interval 18332
c [simplification-10] penalized conflict interval 18332 = 1 * 18332
c [simplification-10] hard conflict limit 59678 (soft 49678 + delta 10000)
c [simplification-10] new conflict limit 49678 (hard 59678)
c 
c [simplification-11] limit 49678 conflicts (hard 59678) hit after 49681 conflicts
c [quatres-7] found 11990 quaternary clauses 16% in total
c [quatres-7-2] added 3 single-self-subsuming ternary resolvents
c [quatres-7-2] added 78 quaternary resolvents
c [ternres-7] limit 9471324 with penalty 0 = 0 + 0
c [ternres-7] all 55134 free variables schedulable
c [ternres-7] 1522 ternary resolvents (0 bin, 1522 trn)
c [ternres-7] 32968 variables remain 60% (22166 retained 40%)
c [unhide-11] limit 473566 with penalty 2 = 0 + 2
c [unhide-11-11] 4 units, 2 failed, 6908 tauts, 0 hbrs, 45584 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 7 transitive binary clauses
c [transred-7] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 55127 variables 100%
c [block-6] limit of 47356623 steps penalty 1 = 1 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 13513 blocked clauses
c [elim-10] 2761 variables 5% will be scheduled this time
c [elim-10] scheduled 2761 variables 5%
c [elim-10] limit of 189426495 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 556 not tried 1% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 1 = 0% variables out of 2761 scheduled
c [elim-10] 1 < 1/100 * 2761 = 27 considered unsuccessful
c [bca-7] limit of 10000000 steps and 1971552 added (scaled 2)
c [bca-7] 75409 out of 109334 literals actually usable 69%
c [bca-7] added 338 blocked clauses in 260071 steps
c [sweep-7] limit 2841397 penalty 0 = 0 + 0
c [sweep-7-1] 3169 pos 6.4% + 46390 neg 93.6% = 49559 sched 90.7% ret 5107
c [sweep-7-1] 3055053 steps 27 queries 5279.96 avg class size
c [sweep-7-1] 1092 decisions 23 SAT calls 227.04 avg env size
c [sweep-7-1] 49333 variables remain 90% (5332 retained 10%)
c [decomp-24] removed 13 variables
c [sweep-7-1] removed 13 vars (0 failed, 3 eqs, 7 impls)
c [sweep-7] 13 < 1/1000 * 54666 = 54 considered unsuccessful
c [sweep-7] removed 13 vars in TOTAL (1 rounds, 26 queries)
c [sort-queue-11] sorted 16787 enqueued variables after 49681 conflicts
c [score-dist-11] active 37866 (69%), one 0 (0%), zero 16787 (31%)
c [score-dist-11] max exp 509, different 199 (39%)
c [score-dist-11] median active exp 478, avg 455.1
c [simplification-11] removed 481 variables 0.9% (54653 remain 52%)
c [simplification-11] removed 21621 irredundant clauses 2.2% (976836 remain 61%)
c [simplification-11] maximum reduction of 2% = max (1%, 2%)
c [simplification-11] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-11] new conflict interval 24998
c [simplification-11] penalized conflict interval 24998 = 1 * 24998
c [simplification-11] hard conflict limit 87178 (soft 74679 + delta 12499)
c [simplification-11] new conflict limit 74679 (hard 87178)
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 -  127.1   54653   976836     66979   22007  29122 60448   93   319   54  29%    642   60  106   52  204%
c 
c [simplification-12] limit 74679 conflicts (hard 87178) hit after 75155 conflicts
c [quatres-8] found 12296 quaternary clauses 16% in total
c [quatres-8-2] added 25 quaternary resolvents
c [ternres-8] limit 11202940 with penalty 0 = 0 + 0
c [ternres-8] 32663 schedulable variables 60%
c [ternres-8] 801 ternary resolvents (0 bin, 801 trn)
c [ternres-8] 19651 variables remain 36% (35002 retained 64%)
c [simpleprobe-4] 41501 schedulable variables 76%
c [simpleprobe-4] limit 22405881 penalty 1 = 1 + 0
c [decomp-26] removed 36 variables
c [simpleprobe-4] 33133 variables remain 61% (21484 retained 39%)
c [simpleprobe-4] removed 36 variables, found 19498 hbrs, 35 units
c [unhide-12] limit 560147 with penalty 2 = 0 + 2
c [unhide-12-12] 917 units, 13 failed, 1362 tauts, 0 hbrs, 54902 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 4 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 53152 variables 100%
c [block-7] limit of 112029407 steps penalty 0 = 0 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 29720 blocked clauses
c [bca-8] limit of 10000000 steps and 1872807 added (scaled 2)
c [bca-8] 74891 out of 105508 literals actually usable 71%
c [bca-8] added 611 blocked clauses in 247034 steps
c [sort-queue-12] sorted 15593 enqueued variables after 75155 conflicts
c [score-dist-12] active 37160 (70%), one 0 (0%), zero 15593 (30%)
c [score-dist-12] max exp 510, different 297 (58%)
c [score-dist-12] median active exp 408, avg 405.0
c [simplification-12] removed 1900 variables 3.5% (52753 remain 50%)
c [simplification-12] removed 47812 irredundant clauses 4.9% (929024 remain 58%)
c [simplification-12] maximum reduction of 5% = max (3%, 5%)
c [simplification-12] large reduction 5% >= 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 87155 (soft 77155 + delta 10000)
c [simplification-12] new conflict limit 77155 (hard 87155)
c 
c [simplification-13] limit 77155 conflicts (hard 87155) hit after 77156 conflicts
c [quatres-9] found 11406 quaternary clauses 16% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-2] added 16 single-self-subsuming ternary resolvents
c [quatres-9-2] added 17 quaternary resolvents
c [ternres-9] limit 11232088 with penalty 0 = 0 + 0
c [ternres-9] 18956 schedulable variables 36%
c [ternres-9] 1422 ternary resolvents (0 bin, 1422 trn)
c [ternres-9] 58 variables remain 0% (52695 retained 100%)
c [decomp-27] removed 236 variables
c [unhide-13] limit 561604 with penalty 2 = 0 + 2
c [unhide-13-13] 3 units, 1 failed, 7211 tauts, 0 hbrs, 15109 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 17 transitive binary clauses
c [transred-9] found 2 units
c [block-8] scheduling all variables this time
c [block-8] scheduled 52511 variables 100%
c [block-8] limit of 112320883 steps penalty 0 = 0 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 110 blocked clauses
c [block-8] 110 < 1/100 * 921393 = 9213 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 52500 variables 100%
c [elim-11] limit of 112320883 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 3089 not tried 6% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 2115 = 4% variables out of 52500 scheduled
c [bca-9] limit of 10000000 steps and 1805621 added (scaled 2)
c [bca-9] 71187 out of 100772 literals actually usable 71%
c [bca-9] added 164 blocked clauses in 242961 steps
c [sweep-8] limit 1790556 based on 895278 irredundant clauses
c [sweep-8-1] 2519 pos 5.6% + 42834 neg 94.4% = 45353 sched 90.0% ret 5032
c [sweep-8-1] 2433610 steps 17 queries 6188.65 avg class size
c [sweep-8-1] 250 decisions 13 SAT calls 45.85 avg env size
c [sweep-8-1] 45288 variables remain 90% (5097 retained 10%)
c [decomp-28] removed 2 variables
c [sweep-8-1] removed 2 vars (0 failed, 1 eqs, 0 impls)
c [sweep-8] 2 < 1/1000 * 50385 = 50 considered unsuccessful
c [sweep-8] removed 2 vars in TOTAL (1 rounds, 16 queries)
c [sort-queue-13] sorted 13937 enqueued variables after 77156 conflicts
c [score-dist-13] active 36446 (72%), one 0 (0%), zero 13937 (28%)
c [score-dist-13] max exp 510, different 305 (60%)
c [score-dist-13] median active exp 402, avg 399.0
c [simplification-13] removed 2370 variables 4.5% (50383 remain 48%)
c [simplification-13] removed 33750 irredundant clauses 3.6% (895274 remain 56%)
c [simplification-13] maximum reduction of 4% = max (4%, 4%)
c [simplification-13] geometric conflict interval increment 4999 = 24998 / 5
c [simplification-13] new conflict interval 29997
c [simplification-13] penalized conflict interval 29997 = 1 * 29997
c [simplification-13] hard conflict limit 122151 (soft 107153 + delta 14998)
c [simplification-13] new conflict limit 107153 (hard 122151)
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 -  143.9   50383   895271    104325   26517  29744 56558   31   132   51  23%    808 -105   30   48   62%
c 
c [simplification-14] limit 107153 conflicts (hard 122151) hit after 122152 conflicts
c [quatres-10] found 11943 quaternary clauses 17% in total
c [quatres-10-2] added 51 quaternary resolvents
c [ternres-10] limit 12041035 with penalty 0 = 0 + 0
c [ternres-10] 57 schedulable variables 0%
c [ternres-10] 113 ternary resolvents (0 bin, 113 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 447635 based on 895271 irredundant clauses
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-14] limit 602051 with penalty 2 = 0 + 2
c [unhide-14-14] 234 units, 0 failed, 638 tauts, 0 hbrs, 280557 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 16 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 75256473 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 5 clauses out of 8 (62%) of length 108
c [cce-4-1] eliminated 4 clauses out of 36 (11%) of length 90
c [cce-4-1] eliminated 4 clauses out of 32 (12%) of length 88
c [cce-4-1] eliminated 8 clauses out of 44 (18%) of length 87
c [cce-4-1] eliminated 8 clauses out of 33 (24%) of length 85
c [cce-4-1] eliminated 4 clauses out of 45 (9%) of length 82
c [cce-4-1] eliminated 2 clauses out of 69 (3%) of length 81
c [cce-4-1] eliminated 7 clauses out of 96 (7%) of length 80
c [cce-4-1] eliminated 4 clauses out of 55 (7%) of length 79
c [cce-4-1] eliminated 11 clauses out of 110 (10%) of length 78
c [cce-4-1] eliminated 14 clauses out of 146 (10%) of length 77
c [cce-4-1] eliminated 8 clauses out of 91 (9%) of length 76
c [cce-4-1] eliminated 14 clauses out of 132 (11%) of length 75
c [cce-4-1] eliminated 10 clauses out of 120 (8%) of length 73
c [cce-4-1] eliminated 3 clauses out of 145 (2%) of length 72
c [cce-4-1] eliminated 2 clauses out of 188 (1%) of length 71
c [cce-4-1] eliminated 7 clauses out of 135 (5%) of length 70
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 115 large clauses in 75256891 steps
c [cce-4-1] allowing another 37628445 steps for small clauses
c [cce-4-1] scheduling 810266 clauses = 779501 binary + 30765 ternary
c [cce-4-1] tried to eliminate 681 small clauses 0%
c [cce-4-1] eliminated 66 binary clauses 0%
c [cce-4-1] eliminated 66 small clauses 0%
c [cce-4-1] eliminated 2381 small clauses in 75256498 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 2496 covered clauses in round 1
c [cce-4] eliminated 2496 covered clauses in TOTAL during 1 rounds
c [cce-4] 2496 < 1/100 * 895148 = 8951 considered unsuccessful
c [elim-12] 548 variables 1% will be scheduled this time
c [elim-12] scheduled 548 variables 1%
c [elim-12] limit of 240820719 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 77 not tried 0% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 1 = 0% variables out of 548 scheduled
c [elim-12] 1 < 1/100 * 548 = 5 considered unsuccessful
c [bca-10] limit of 10000000 steps and 1795745 added (scaled 2)
c [bca-10] 73191 out of 100296 literals actually usable 73%
c [bca-10] added 861 blocked clauses in 269274 steps
c [sort-queue-14] sorted 12419 enqueued variables after 122152 conflicts
c [score-dist-14] active 37728 (75%), one 0 (0%), zero 12419 (25%)
c [score-dist-14] max exp 510, different 431 (84%)
c [score-dist-14] median active exp 264, avg 270.0
c [simplification-14] removed 236 variables 0.5% (50147 remain 47%)
c [simplification-14] removed 4972 irredundant clauses 0.6% (890299 remain 56%)
c [simplification-14] maximum reduction of 1% = max (0%, 1%)
c [simplification-14] geometric conflict interval increment 14998 = 29997 / 2
c [simplification-14] new conflict interval 44995
c [simplification-14] penalized conflict interval 44995 = 1 * 44995
c [simplification-14] hard conflict limit 189644 (soft 167147 + delta 22497)
c [simplification-14] new conflict limit 167147 (hard 189644)
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 -  153.4   50147   890298    134700   27550  29847 55801   32   138   51  23%    888  -77   31   43   72%
c -  158.1   50147   890298    165691   26124  29874 55806   24   119   52  20%    939  -62   22   37   60%
c 
c [simplification-15] limit 167147 conflicts (hard 189644) hit after 189644 conflicts
c [quatres-11] found 11596 quaternary clauses 17% in total
c [quatres-11-2] added 5 single-self-subsuming ternary resolvents
c [quatres-11-2] added 33 quaternary resolvents
c [ternres-11] limit 14005566 with penalty 0 = 0 + 0
c [ternres-11] all 50147 free variables schedulable
c [ternres-11] 253 ternary resolvents (1 bin, 252 trn)
c [ternres-11] 26490 variables remain 53% (23657 retained 47%)
c [card-5] limit 437673 penalty 4 = 4 + 0
c [card-5] found 12 at-most-one constraints of average size 3.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 437673 for elimination
c [card-5] 12 out of 12 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-30] removed 3 variables
c [unhide-15] limit 700278 with penalty 2 = 0 + 2
c [unhide-15-15] 0 units, 0 failed, 4044 tauts, 0 hbrs, 335773 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 13 transitive binary clauses
c [transred-11] found 2 units
c [block-9] scheduling all variables this time
c [block-9] scheduled 50142 variables 100%
c [block-9] limit of 70027834 steps penalty 1 = 1 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 10245 blocked clauses
c [bca-11] limit of 10000000 steps and 1767357 added (scaled 2)
c [bca-11] 76040 out of 100116 literals actually usable 76%
c [bca-11] added 2496 blocked clauses in 287738 steps
c [sort-queue-15] sorted 30027 enqueued variables after 189644 conflicts
c [score-dist-15] active 20030 (40%), one 17729 (35%), zero 12298 (25%)
c [score-dist-15] max exp 510, different 349 (68%)
c [score-dist-15] median active exp 73, avg 198.0
c [simplification-15] removed 90 variables 0.2% (50057 remain 47%)
c [simplification-15] removed 14408 irredundant clauses 1.6% (875890 remain 55%)
c [simplification-15] maximum reduction of 2% = max (0%, 2%)
c [simplification-15] geometric conflict interval increment 14998 = 44995 / 3
c [simplification-15] new conflict interval 59993
c [simplification-15] penalized conflict interval 59993 = 1 * 59993
c [simplification-15] hard conflict limit 279633 (soft 249637 + delta 29996)
c [simplification-15] new conflict limit 249637 (hard 279633)
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 -  167.6   50057   875889    199894   26521  30710 66263   40   117   51  34%    974  -42   36   34  107%
c -  180.8   50057   875881    236039   25962  30733 66286   73   461   51  16%    995  198   61   49  123%
c 
c [simplification-16] limit 249637 conflicts (hard 279633) hit after 266944 conflicts
c [quatres-12] found 11666 quaternary clauses 17% in total
c [quatres-12-2] added 2 single-self-subsuming ternary resolvents
c [ternres-12] limit 18579599 with penalty 0 = 0 + 0
c [ternres-12] 26440 schedulable variables 53%
c [ternres-12] 250 ternary resolvents (0 bin, 250 trn)
c [ternres-12] 1479 variables remain 3% (48578 retained 97%)
c [decomp-31] removed 1 variables
c [treelook-4] limit 232244 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 33778 literals 34%
c [treelook-4] scheduling used 234761 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 232244 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 1765869 steps
c [treelook-4] 33774 literals remain 34%
c [treelook-4] 28313 variables remain to probed next time 57%
c [treelook-4] removed 0 variables, found 60 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 23 transitive binary clauses
c [block-10] scheduling all variables this time
c [block-10] scheduled 50056 variables 100%
c [block-10] limit of 185795991 steps penalty 0 = 0 + 0
c [block-10] fully completed
c [block-10] transition to [ all 0 rem 0 ] state
c [block-10] eliminated 0 blocked clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 50056 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 1281 variables 3% in round 1 in 1094936849 steps
c [elim-13-1] backward subsumption/strengthening limit 1094936800
c [elim-13-1-1] backward checking 11003 touched variables 22%
c [elim-13-1-1] incomplete backward checking 11032 remain 100%
c [elim-13-1] subsumed 0 and strengthened 24 clauses in 1094943999 steps
c [elim-13-1] rescheduled 44 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 53450640 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 1281 = 3% variables out of 50056 scheduled
c [bca-12] limit of 10000000 steps and 1743731 added (scaled 2)
c [bca-12] 66581 out of 97552 literals actually usable 68%
c [bca-12] added 868 blocked clauses in 262247 steps
c [sweep-9] limit 1726906 based on 863453 irredundant clauses
c [sweep-9-1] 2174 pos 5.0% + 41619 neg 95.0% = 43793 sched 89.8% ret 4982
c [sweep-9-1] 1748989 steps 19 queries 4795.42 avg class size
c [sweep-9-1] 509 decisions 16 SAT calls 78.94 avg env size
c [sweep-9-1] 43699 variables remain 90% (5076 retained 10%)
c [decomp-33] removed 3 variables
c [sweep-9-1] removed 3 vars (0 failed, 1 eqs, 1 impls)
c [sweep-9] 3 < 1/1000 * 48775 = 48 considered unsuccessful
c [sweep-9] removed 3 vars in TOTAL (1 rounds, 18 queries)
c [sort-queue-16] sorted 13287 enqueued variables after 266944 conflicts
c [score-dist-16] active 35485 (73%), one 3126 (6%), zero 10161 (21%)
c [score-dist-16] max exp 510, different 299 (59%)
c [score-dist-16] median active exp 376, avg 371.3
c [simplification-16] removed 1285 variables 2.6% (48772 remain 46%)
c [simplification-16] removed 12435 irredundant clauses 1.4% (863445 remain 54%)
c [simplification-16] maximum reduction of 3% = max (3%, 1%)
c [simplification-16] geometric conflict interval increment 14998 = 59993 / 4
c [simplification-16] new conflict interval 74991
c [simplification-16] penalized conflict interval 74991 = 1 * 74991
c [simplification-16] hard conflict limit 379430 (soft 341935 + delta 37495)
c [simplification-16] new conflict limit 341935 (hard 379430)
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 -  219.7   48772   863445    271004   28795  30381 55291   36   695   51   5%   1007  413   50   45  109%
c -  229.5   48772   863432    307874   27364  30385 55302   63   236   51  27%   1014  -84   43   56   76%
c -  236.2   48772   863431    344582   28667  30399 55327   49   243   52  20%   1018 -248   35   54   65%
c 
c [simplification-17] limit 341935 conflicts (hard 379430) hit after 379431 conflicts
c [quatres-13] found 11695 quaternary clauses 18% in total
c [quatres-13-1] removed 4 duplicate quaternary clauses
c [quatres-13-2] added 22 single-self-subsuming ternary resolvents
c [quatres-13-2] added 41 quaternary resolvents
c [ternres-13] limit 24271174 with penalty 0 = 0 + 0
c [ternres-13] 1447 schedulable variables 3%
c [ternres-13] 103 ternary resolvents (0 bin, 103 trn)
c [ternres-13] fully completed ternary resolution
c [basicprobe-4] limit 121355872 penalty 0 = 0 + 0
c [basicprobe-4-0] 38672 probes remain 80% after last round
c [basicprobe-4-0] 69 units = 69 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 170 variables, found 29975 hbrs
c [bate-3] eliminated 82 asymmetric tautologies during probing
c [unhide-16] limit 606779 with penalty 3 = 1 + 2
c [unhide-16-16] 0 units, 4 failed, 1049 tauts, 0 hbrs, 82628 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 11 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 48601 variables 100%
c [elim-14] limit of 485423491 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14] incomplete 85 not tried 0% in round 1
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 382 = 1% variables out of 48601 scheduled
c [elim-14] 382 < 1/100 * 48601 = 486 considered unsuccessful
c [bca-13] limit of 10000000 steps and 1725411 added (scaled 2)
c [bca-13] 62165 out of 96440 literals actually usable 64%
c [bca-13] added 2579 blocked clauses in 241727 steps
c [sort-queue-17] sorted 15393 enqueued variables after 379431 conflicts
c [score-dist-17] active 32826 (68%), one 5823 (12%), zero 9570 (20%)
c [score-dist-17] max exp 510, different 405 (79%)
c [score-dist-17] median active exp 408, avg 394.2
c [simplification-17] removed 553 variables 1.1% (48219 remain 45%)
c [simplification-17] removed 9353 irredundant clauses 1.1% (854076 remain 53%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 37495 = 74991 / 2
c [simplification-17] new conflict interval 112486
c [simplification-17] penalized conflict interval 112486 = 1 * 112486
c [simplification-17] hard conflict limit 548160 (soft 491917 + delta 56243)
c [simplification-17] new conflict limit 491917 (hard 548160)
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 -  262.6   48219   854076    389967   27290  29673 82459   99   186   52  53%   1021 -175  108   70  154%
c -  275.1   48219   854064    436687   28088  29683 82467   79   184   52  43%   1023 -157   41   83   50%
c -  281.3   48219   854064    479443   31626  29684 82469   60   631   54  10%   1023  198   59   75   79%
c 
c [simplification-18] limit 491917 conflicts (hard 548160) hit after 491918 conflicts
c [quatres-14] found 11986 quaternary clauses 18% in total
c [quatres-14-2] added 14 quaternary resolvents
c [ternres-14] limit 28677619 with penalty 0 = 0 + 0
c [ternres-14] all 48219 free variables schedulable
c [ternres-14] 549 ternary resolvents (0 bin, 549 trn)
c [ternres-14] 15 variables remain 0% (48204 retained 100%)
c [decomp-35] removed 12 variables
c [simpleprobe-5] 29044 schedulable variables 60%
c [simpleprobe-5] limit 114710478 penalty 0 = 0 + 0
c [decomp-36] removed 624 variables
c [simpleprobe-5] 22160 variables remain 47% (25423 retained 53%)
c [simpleprobe-5] removed 624 variables, found 124671 hbrs, 86 units
c [unhide-17] limit 1433880 with penalty 2 = 0 + 2
c [unhide-17-17] 27 units, 0 failed, 4026 tauts, 0 hbrs, 25955 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 14 transitive binary clauses
c [block-11] scheduling all variables this time
c [block-11] scheduled 47556 variables 100%
c [block-11] limit of 143388098 steps penalty 1 = 1 + 0
c [block-11] fully completed
c [block-11] transition to [ all 0 rem 0 ] state
c [block-11] eliminated 9430 blocked clauses
c [bca-14] limit of 10000000 steps and 1684547 added (scaled 2)
c [bca-14] 64577 out of 94804 literals actually usable 68%
c [bca-14] added 736 blocked clauses in 243255 steps
c [sort-queue-18] sorted 17688 enqueued variables after 491918 conflicts
c [score-dist-18] active 29713 (63%), one 8373 (18%), zero 9315 (20%)
c [score-dist-18] max exp 510, different 398 (78%)
c [score-dist-18] median active exp 280, avg 277.0
c [simplification-18] removed 818 variables 1.7% (47401 remain 45%)
c [simplification-18] removed 21065 irredundant clauses 2.5% (832999 remain 52%)
c [simplification-18] maximum reduction of 2% = max (2%, 2%)
c [simplification-18] geometric conflict interval increment 37495 = 112486 / 3
c [simplification-18] new conflict interval 149981
c [simplification-18] penalized conflict interval 149981 = 1 * 149981
c [simplification-18] hard conflict limit 716889 (soft 641899 + delta 74990)
c [simplification-18] new conflict limit 641899 (hard 716889)
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 -  292.5   47401   832999    516729   31438  27902 204403   57   301   54  19%   1024 -179   45   69   65%
c -  299.9   47401   832999    554452   30609  27915 204409   79   534   55  15%   1024  122  144   68  212%
c -  308.6   47401   832998    599319   30980  27931 204421   59   185   54  32%   1024 -167   57   70   82%
c -  320.3   47401   832998    649066   30895  27952 204447  102   239   55  43%   1024 -105  114   80  142%
c -  336.5   47401   832998    715505   29920  27979 204476  118   169   55  70%   1024  -85  116  100  116%
c 
c [simplification-19] limit 641899 conflicts (hard 716889) hit after 716890 conflicts
c [quatres-15] found 11959 quaternary clauses 18% in total
c [quatres-15-2] added 1 single-self-subsuming ternary resolvents
c [quatres-15-2] added 6 quaternary resolvents
c [ternres-15] limit 37293046 with penalty 0 = 0 + 0
c [ternres-15] 13 schedulable variables 0%
c [ternres-15] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 466163 penalty 4 = 4 + 0
c [gauss-5] extracted 0 xors of average arity 0.0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-18] limit 3729304 with penalty 1 = 0 + 1
c [unhide-18-19] 0 units, 0 failed, 17815 tauts, 0 hbrs, 70817 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 13 transitive binary clauses
c [block-12] scheduling all variables this time
c [block-12] scheduled 47401 variables 100%
c [block-12] limit of 372930465 steps penalty 0 = 0 + 0
c [block-12] fully completed
c [block-12] transition to [ all 0 rem 0 ] state
c [block-12] eliminated 38 blocked clauses
c [block-12] 38 < 1/100 * 830771 = 8307 considered unsuccessful
c [cce-5] limit of 11654077 steps penalty 4 = 4 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 123
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1 large clauses in 11655945 steps
c [cce-5-1] allowing another 5827972 steps for small clauses
c [cce-5-1] scheduling 755993 clauses = 727368 binary + 28625 ternary
c [cce-5-1] tried to eliminate 114 small clauses 0%
c [cce-5-1] eliminated 67 binary clauses 0%
c [cce-5-1] eliminated 67 small clauses 0%
c [cce-5-1] eliminated 67 small clauses in 11654162 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 68 covered clauses in round 1
c [cce-5] eliminated 68 covered clauses in TOTAL during 1 rounds
c [cce-5] 68 < 1/100 * 830733 = 8307 considered unsuccessful
c [elim-15] 85 variables 0% will be scheduled this time
c [elim-15] scheduled 85 variables 0%
c [elim-15] limit of 372930465 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15] incomplete 11 not tried 0% in round 1
c [elim-15] transition to [ all 0 rem 1 ] state
c [elim-15] eliminated 0 = 0% variables out of 85 scheduled
c [bca-15] limit of 10000000 steps and 1679123 added (scaled 2)
c [bca-15] 63709 out of 94802 literals actually usable 67%
c [bca-15] added 351 blocked clauses in 224798 steps
c [sort-queue-19] sorted 20845 enqueued variables after 716890 conflicts
c [score-dist-19] active 26555 (56%), one 11551 (24%), zero 9294 (20%)
c [score-dist-19] max exp 510, different 443 (87%)
c [score-dist-19] median active exp 473, avg 402.2
c [simplification-19] removed 1 variables 0.0% (47400 remain 45%)
c [simplification-19] removed 2895 irredundant clauses 0.3% (830103 remain 52%)
c [simplification-19] maximum reduction of 0% = max (0%, 0%)
c [simplification-19] full geometric conflict interval increment 149981
c [simplification-19] new conflict interval 299962
c [simplification-19] penalized conflict interval 299962 = 1 * 299962
c [simplification-19] hard conflict limit 1166833 (soft 1016852 + delta 149981)
c [simplification-19] new conflict limit 1016852 (hard 1166833)
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 -  364.7   47400   830099    821619   24285  27934 187976  116   122   55  96%   1024  -43  115  113  102%
c -  394.9   47400   830099    974247   23513  27936 187983  113   118   60  96%   1024  -12  105  113   93%
c 
c [simplification-20] limit 1016852 conflicts (hard 1166833) hit after 1045767 conflicts
c [quatres-16] found 11833 quaternary clauses 18% in total
c [quatres-16-2] added 3 single-self-subsuming ternary resolvents
c [quatres-16-2] added 14 quaternary resolvents
c [ternres-16] limit 46781814 with penalty 0 = 0 + 0
c [ternres-16] all 47400 free variables schedulable
c [ternres-16] 120 ternary resolvents (1 bin, 119 trn)
c [ternres-16] fully completed ternary resolution
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 21 transitive binary clauses
c [transred-16] found 1 units
c [bca-16] limit of 10000000 steps and 1679264 added (scaled 2)
c [bca-16] 65330 out of 94800 literals actually usable 69%
c [bca-16] added 14 blocked clauses in 249748 steps
c [sweep-10] limit 1754318 penalty 3 = 3 + 0
c [sweep-10-1] 2080 pos 4.9% + 40344 neg 95.1% = 42424 sched 89.5% ret 4975
c [sweep-10-1] 1800034 steps 25 queries 4328.84 avg class size
c [sweep-10-1] 792 decisions 24 SAT calls 103.62 avg env size
c [sweep-10-1] 42237 variables remain 89% (5162 retained 11%)
c [decomp-39] removed 1 variables
c [sweep-10-1] removed 1 vars (0 failed, 0 eqs, 2 impls)
c [sweep-10] 1 < 1/1000 * 47399 = 47 considered unsuccessful
c [sweep-10] removed 1 vars in TOTAL (1 rounds, 24 queries)
c [sort-queue-20] sorted 31310 enqueued variables after 1045767 conflicts
c [score-dist-20] active 16088 (34%), one 22028 (46%), zero 9282 (20%)
c [score-dist-20] max exp 509, different 291 (57%)
c [score-dist-20] median active exp 376, avg 366.0
c [simplification-20] removed 2 variables 0.0% (47398 remain 45%)
c [simplification-20] removed 13 irredundant clauses 0.0% (830086 remain 52%)
c [simplification-20] maximum reduction of 0% = max (0%, 0%)
c [simplification-20] full geometric conflict interval increment 299962
c [simplification-20] new conflict interval 599924
c [simplification-20] penalized conflict interval 599924 = 1 * 599924
c [simplification-20] hard conflict limit 1945653 (soft 1645691 + delta 299962)
c [simplification-20] new conflict limit 1645691 (hard 1945653)
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 -  424.2   47398   830086   1107696   21047  28060 188010  111   118   56  94%   1024  -12  109  113   96%
c -  457.7   47398   830086   1275175   27395  28060 188017  106   109   64  97%   1024   -9  104  107   98%
c -  476.5   47398   830086   1372068   32598  28059 188025   98   106   67  93%   1024  -11   96  103   93%
c -  487.9   47398   830086   1425117   36536  28060 188028   94   105   69  90%   1024   -9   93   98   95%
c -  498.1   47398   830086   1473432   36582  28060 188028   91   102   69  90%   1024   -8   89   95   93%
c -  508.3   47398   830086   1523221   36580  28059 188029   97   106   69  92%   1024   -1  103   94  109%
c -  520.1   47398   830086   1585007   36449  28063 188031   96   107   69  90%   1024   -1   99   95  104%
c -  530.5   47398   830086   1635974   37785  28063 188031   92   100   70  92%   1024   -5   96   93  102%
c 
c [simplification-21] limit 1645691 conflicts (hard 1945653) hit after 1665680 conflicts
c [quatres-17] found 11903 quaternary clauses 18% in total
c [quatres-17-2] added 1 single-self-subsuming ternary resolvents
c [quatres-17-2] added 1 quaternary resolvents
c [ternres-17] limit 70289012 with penalty 0 = 0 + 0
c [ternres-17] all 47398 free variables schedulable
c [ternres-17] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 2196531 penalty 4 = 4 + 0
c [card-6] found 66 at-most-one constraints of average size 3.1
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2196531 for elimination
c [card-6] 66 out of 66 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [unhide-19] limit 1757225 with penalty 3 = 1 + 2
c [unhide-19-20] 0 units, 0 failed, 2067 tauts, 0 hbrs, 70266 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 19 transitive binary clauses
c [block-13] scheduling all variables this time
c [block-13] scheduled 47398 variables 100%
c [block-13] limit of 351445061 steps penalty 1 = 1 + 0
c [block-13] fully completed
c [block-13] transition to [ all 0 rem 0 ] state
c [block-13] eliminated 788 blocked clauses
c [block-13] 788 < 1/100 * 828068 = 8280 considered unsuccessful
c [bca-17] limit of 10000000 steps and 1673659 added (scaled 2)
c [bca-17] 70283 out of 94720 literals actually usable 74%
c [bca-17] added 202 blocked clauses in 283043 steps
c [sort-queue-21] sorted 34055 enqueued variables after 1665680 conflicts
c [score-dist-21] active 13304 (28%), one 24883 (53%), zero 9172 (19%)
c [score-dist-21] max exp 510, different 267 (52%)
c [score-dist-21] median active exp 501, avg 460.5
c [simplification-21] removed 39 variables 0.1% (47359 remain 45%)
c [simplification-21] removed 2806 irredundant clauses 0.3% (827280 remain 52%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 599924
c [simplification-21] conflict interval soft limit 1000000 reached
c [simplification-21] new conflict interval 1000000
c [simplification-21] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-21] hard conflict limit 3165680 (soft 2665680 + delta 500000)
c [simplification-21] new conflict limit 2665680 (hard 3165680)
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 -  545.7   47359   827280   1691208   37782  28167 188618   76   180   61  42%   1024   41   78   89   88%
c -  554.7   47359   827280   1742815   38968  28188 188639   54   605   60   9%   1024  403   78   76  103%
c -  574.3   47359   827280   1829802   37960  28196 188653  109   134   60  82%   1024 -102   83   94   88%
c -  598.2   47359   827280   1943769   36217  28207 188693  100   108   62  92%   1024  -35   95  103   92%
c -  616.8   47359   827280   2036439   36972  28209 188705   82    97   63  84%   1024  -31   86   95   90%
c -  629.0   47359   827280   2090009   40692  28209 188706   82    92   65  88%   1024  -20   82   87   94%
c -  647.5   47359   827280   2173150   38361  28212 188710  102   104   64  98%   1024  -18  101   96  106%
c -  674.4   47359   827280   2296465   34611  28210 188717  108   121   63  90%   1024   -4  109  105  104%
c -  710.1   47359   827280   2474522   34475  28213 188724  103   107   63  96%   1024   -8  106  106  100%
c 
c [simplification-22] limit of 418 binary hit after 418 binaries
c [quatres-18] found 12178 quaternary clauses 19% in total
c [quatres-18-2] added 2 single-self-subsuming ternary resolvents
c [quatres-18-2] added 2 quaternary resolvents
c [ternres-18] limit 105813642 with penalty 0 = 0 + 0
c [ternres-18] all 47359 free variables schedulable
c [ternres-18] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-41] removed 1 variables
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 32 transitive binary clauses
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 47358 variables 100%
c [elim-16] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16] incomplete 831 not tried 2% in round 1
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 491 = 1% variables out of 47358 scheduled
c [bca-18] limit of 10000000 steps and 1669932 added (scaled 2)
c [bca-18] 64603 out of 93736 literals actually usable 69%
c [bca-18] added 730 blocked clauses in 264219 steps
c [sort-queue-22] sorted 32203 enqueued variables after 2547391 conflicts
c [score-dist-22] active 14664 (31%), one 23355 (50%), zero 8848 (19%)
c [score-dist-22] max exp 510, different 279 (55%)
c [score-dist-22] median active exp 493, avg 433.5
c [simplification-22] removed 492 variables 1.0% (46867 remain 44%)
c [simplification-22] removed 1914 irredundant clauses 0.2% (825366 remain 52%)
c [simplification-22] maximum reduction of 1% = max (1%, 0%)
c [simplification-22] forced so keeping old conflict interval 1000000
c [simplification-22] conflict limit remains at 2665680 (hard 3165680)
c [simplification-22] new binary interval 1000
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 -  742.9   46867   825366   2605043   37267  27705 183480  107   111   62  97%   1024   -2  103  104   99%
c 
c [simplification-23] limit 2665680 conflicts (hard 3165680) hit after 2665682 conflicts
c [quatres-19] found 12845 quaternary clauses 19% in total
c [quatres-19-2] added 5 quaternary resolvents
c [ternres-19] limit 111275532 with penalty 0 = 0 + 0
c [ternres-19] all 46867 free variables schedulable
c [ternres-19] 67 ternary resolvents (0 bin, 67 trn)
c [ternres-19] fully completed ternary resolution
c [treelook-5] limit 695472 penalty 4 = 4 + 0 boost 1
c [treelook-5] scheduled 45096 literals 48%
c [treelook-5] scheduling used 699158 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 695472 penalty 4 = 4 + 0 boost 1
c [treelook-5] used 698153 steps
c [treelook-5] 45092 literals remain 48%
c [treelook-5] 25906 variables remain to probed next time 55%
c [treelook-5] removed 0 variables, found 54 hbrs
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 15 transitive binary clauses
c [bca-19] limit of 10000000 steps and 1670291 added (scaled 2)
c [bca-19] 64887 out of 93736 literals actually usable 69%
c [bca-19] added 2 blocked clauses in 265829 steps
c [sort-queue-23] sorted 30634 enqueued variables after 2665682 conflicts
c [score-dist-23] active 16233 (35%), one 21796 (47%), zero 8838 (19%)
c [score-dist-23] max exp 510, different 342 (67%)
c [score-dist-23] median active exp 482, avg 425.5
c [simplification-23] removed 0 variables 0.0% (46867 remain 44%)
c [simplification-23] removed 3 irredundant clauses 0.0% (825363 remain 52%)
c [simplification-23] maximum reduction of 0% = max (0%, 0%)
c [simplification-23] full geometric conflict interval increment 1000000
c [simplification-23] conflict interval soft limit 1000000 reached
c [simplification-23] new conflict interval 1000000
c [simplification-23] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-23] hard conflict limit 4165682 (soft 3665682 + delta 500000)
c [simplification-23] new conflict limit 3665682 (hard 4165682)
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 -  766.3   46867   825363   2710527   40552  27772 183529   99   105   63  94%   1024   -9   97  101   96%
c -  786.4   46867   825363   2809045   40825  27771 183530  104   106   64  98%   1024   -8  103  102  101%
c -  803.0   46867   825363   2890181   42980  27772 183532   98   107   65  92%   1024   -6   92   97   95%
c -  819.3   46867   825363   2962130   43929  27773 183538   94   102   65  92%   1024  -18   98   94  104%
c -  828.7   46867   825363   3018719   46647  27778 183547   66    91   64  73%   1024  -41   66   78   84%
c -  836.4   46867   825363   3069359   48555  27780 183549   66    73   65  90%   1024  -31   65   72   91%
c -  844.6   46867   825363   3119670   48630  27781 183554   64    74   65  86%   1024  -15   64   68   94%
c -  854.5   46867   825363   3171619   46696  27782 183563   60    68   64  87%   1024  -10   60   64   93%
c -  863.5   46867   825363   3227120   47946  27787 183564   60    67   64  90%   1024   -8   59   62   95%
c -  872.4   46867   825363   3281740   48183  27787 183565   58    65   65  90%   1024   -5   58   61   95%
c -  881.6   46867   825363   3338247   48441  27787 183565   59    70   65  85%   1024    2   62   60  104%
c -  891.2   46867   825363   3395224   48363  27789 183565   58    67   65  86%   1024   -3   57   59   96%
c -  900.6   46867   825363   3455017   48728  27790 183565   57    62   65  91%   1024   -5   57   59   96%
c -  909.9   46867   825363   3514354   49905  27792 183565   60    65   66  93%   1024   -3   58   59   98%
c -  919.2   46867   825363   3574417   49769  27792 183565   59    64   65  92%   1024   -2   60   59  101%
c -  929.2   46867   825363   3635930   50925  27800 183569   46   113   95  40%   1024   15   46   56   82%
c 
c [simplification-24] limit 3665682 conflicts (hard 4165682) hit after 3665683 conflicts
c [quatres-20] found 13011 quaternary clauses 19% in total
c [quatres-20-2] added 4 single-self-subsuming ternary resolvents
c [quatres-20-2] added 4 quaternary resolvents
c [ternres-20] limit 159603275 with penalty 0 = 0 + 0
c [ternres-20] all 46867 free variables schedulable
c [ternres-20] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-20] fully completed ternary resolution
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 22912 probes remain 49% after last round
c [basicprobe-5-0] 462 units = 462 failed (100%) + 0 lifted (0%)
c [basicprobe-5-0] removed 462 variables, found 19898 hbrs
c [bate-4] eliminated 189 asymmetric tautologies during probing
c [unhide-20] limit 1250000 with penalty 4 = 2 + 2
c [unhide-20-21] 0 units, 0 failed, 7989 tauts, 0 hbrs, 259785 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 21 transitive binary clauses
c [block-14] scheduling all variables this time
c [block-14] scheduled 46405 variables 100%
c [block-14] limit of 200000000 steps penalty 2 = 2 + 0
c [block-14] fully completed
c [block-14] transition to [ all 0 rem 0 ] state
c [block-14] eliminated 456 blocked clauses
c [block-14] 456 < 1/100 * 820347 = 8203 considered unsuccessful
c [elim-17] 11 variables 0% will be scheduled this time
c [elim-17] scheduled 11 variables 0%
c [elim-17] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17] incomplete 2 not tried 0% in round 1
c [elim-17] transition to [ all 0 rem 1 ] state
c [elim-17] eliminated 0 = 0% variables out of 11 scheduled
c [bca-20] limit of 10000000 steps and 1658408 added (scaled 2)
c [bca-20] 65862 out of 92810 literals actually usable 71%
c [bca-20] added 899 blocked clauses in 290421 steps
c [sort-queue-24] sorted 24309 enqueued variables after 3665683 conflicts
c [score-dist-24] active 22095 (48%), one 15749 (34%), zero 8560 (18%)
c [score-dist-24] max exp 510, different 269 (53%)
c [score-dist-24] median active exp 483, avg 463.0
c [simplification-24] removed 463 variables 1.0% (46404 remain 44%)
c [simplification-24] removed 5942 irredundant clauses 0.7% (819421 remain 51%)
c [simplification-24] maximum reduction of 1% = max (1%, 1%)
c [simplification-24] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-24] conflict interval soft limit 1000000 reached
c [simplification-24] new conflict interval 1000000
c [simplification-24] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-24] hard conflict limit 5165683 (soft 4665683 + delta 500000)
c [simplification-24] new conflict limit 4665683 (hard 5165683)
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 -  960.5   46404   819421   3707579   49579  27357 176498   88   192   62  46%   1024    6   85   71  120%
c -  976.2   46404   819421   3780672   50485  27371 176521   66   366   62  18%   1024  110   31   75   41%
c -  986.6   46404   819421   3850452   54043  27400 176527   50   923   62   5%   1024  672   44   56   78%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 278 basic ate = 218 trn 78% + 60 lrg 22% in 4 updates
c bcas: 20 count, 39032 added (11919 skipped), 5642131 steps
c bkwd: tried 286304 clauses, 572123 lits, 2.00 lits/clause
c bkwd: checked 1542000088 occs, 5385.88 occs/clause, 2695.22 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 325 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 158 large (0% self)
c blkd: 14 bces, 278326 removed, 68120467 resolutions, 178071454 steps
c blkd: 19733 blocking literals 9%, 3933 pure
c bump: 3801356 bumped seen, 1027534059 lits 270.3 on average
c card: 6 count, 0 units, 0 am1, 30260803 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1510 subsumed
c card: 134 at-most-one constraints found, average size 3.05
c card: 134 at-most-one constraints used 100%, average size 3.05
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: 5 cces, 559 eliminated, 548 ate 98%, 11 abce 2%
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: 6215704 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 122 gcs, 0 rescored clauses, 14830 rescored vars
c dcps: 44 decompositions, 1462 equivalent 1%
c deco: 1369855 decision-only clauses 36%, 64% reduction
c decs: 46964571 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 17 elims, 44348 eliminated 42%, 400 pure 1%
c elms: 20 rounds, 1.2 rounds/bve
c elms: 17388 small 39%, 22627 large 51%
c elms: 30296 tried small, 17388 succeeded 57%, 12908 failed 43%
c elms: 54965 subsumed, 279934 strengthened, 19937 blocked
c elms: 19810456 copies, 33190121 resolutions, 603554 ipos
c elms: 149241893 subchks, 195799720 strchks
c gaus: 5 extractions, 6 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8915880 steps, 4457940 extr 50%, 20 elim 0%
c glue: 85.8 orig avg, 85.8 real avg, 8.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 264309 = 175089 simple 66% + 89092 trn 34% + 128 lrg 0%, 4051 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3801356 clauses, 112.4 length
c lrnd: 427373091 lits = 873142447 orig - 445769356 removed 51%
c lrnd: 1697319 uips 45%, 1536372 flips 40%
c mins: 2426098 mins 64%, 111 bin 0%, 3724 size 0%
c mins: 268242944 poisoned searches, 46199743 hits, 17% hit rate
c mins: 622658012 used twice searches, 119986531 hits, 19% hit rate
c move: moved 243684, 233724 bin 96%, 9960 trn 4%
c otfs: 110046 driving 52%, 100226 restarting 48%
c otfs: str 210272, 209804 red 100%, 468 irr 0%
c otfs: str 210272, 0 bin 0%, 82 trn 0%, 210190 lrg 100%
c otfs: sub 4994, 4913 red 98%, 81 irr 2%
c otfs: sub 4994, 0 bin 0%, 0 trn 0%, 4994 lrg 100%
c phas: 1 computed, 99852 set, 0 pos (0%), 99852 neg (100%)
c prbs: 5 basic, 32236 probed, 636 failed, 0 lifted
c prbs: 5 simple, 232928 probed, 829 failed, 196 eqs
c prbs: 5 treelook, 21 probed, 0 failed, 0 lifted
c prom: 108325 locked 1% out of 15636635 tried
c prps: 2073359997 props, 43 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 20 count, 1974 quat, 196 self1, 0 self2, 125 dup
c queu: 24 sorted, 46964571 next (2091906 steps 0.04)
c queu: 1323429695 enq (1576886941 steps 1.19), 1027534059 deq 78%
c redc: 2593 clauses 39%, 6679 tried 0%, 87 sat 1%
c redc: 14363 lits 16%, 91444 tried 0%, 87 sat 0%
c redc: 447 times jump level reduced, 80.0 levels on average
c reds: 56 count, 69844.3 conflicts per reduce
c reds: 0 memlim 0%, 56 arith 100%
c reds: 2170276 collected 89%, 281815 retired 11%
c rmbd: 15753 removed, 11134 red 71%
c rsts: 14479 restarts 97%, 515 skipped 3%
c rsts: 515 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 24 count, 23 confs 96%, 0 vars 0%
c simp: 0 its 0%, 1 bin 4%, 0 trns 0%
c subl: 3801356 count (8401527 tried 2.2), 1230481 sub out of 3800109 (32.4%)
c swps: 10 count, 10 rounds, 343 queries (34.3/round)
c swps: 313 sat calls, 11 unsat (0.4% success rate)
c swps: 11487 decisions 36.7, 120 conflicts 0.4
c swps; 5496.7 avg class size, 196.4 avg environment size
c swps: 0 failed, 61 impls, 38 equivs
c swp0: 111 type 0 queries, 10 unsat (9.0%), 108 sat (97.3%)
c swp1: 232 type 1 queries, 91 unsat (39.2%), 197 sat (84.9%)
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: 101561997 calls to obtain time
c tops: 13799 fixed 13%, 1 its, 3911282.00 confs/it
c trds: 20 transitive reductions, 274 removed, 10 failed
c trds: 4859 nodes, 30523 edges, 39825188 steps
c trim: 10674347 words, 40.7 MB
c trnr: 20 count, 19 bin, 49052 trn, 338846286 steps
c unhd: 20 count, 21 rounds, 63350773 steps
c unhd: 1016 non-trivial sccs of average size 2.7
c unhd: 5268 units, 5268 bin, 0 trn, 0 lrg
c unhd: 83 failed, 81 stamp, 0 lits, 2 bin, 0 trn, 0 lrg
c unhd: 100917 tauts, 728 bin 1%, 8714 trn 9%, 8536 lrg 8%
c unhd: 100917 tauts, 82939 stamp 82%, 37232 red 37%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1479534 str, 5268 bin 0%, 6870 trn 0%, 1467396 lrg 99%, 1337248 red 90%
c vars: 46404 remaining 44% and 59609 removed 56% out of 106013
c vars: 13799 fixed 13%, 44348 eliminated 42%, 1462 equivalent 1%
c vsts: 17343060686 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 8.4 search visits per propagation, 4317.3 per conflict
c wchs: 1964550805 pushed, 102060025 enlarged, 190 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3802083       2170276        281815     138259630      77952069       2701657
c 
c  0 0          6391   0       494   0         0   0  13078702   9   1578670   2     25693   1     0.2
c  1 5          2807   0       496   0      1585   1   6307274   5   2061809   3     40653   2     0.1
c  2 6         17331   0      4523   0      8602   3  24384026  18  12017719  15    174701   6     0.4
c  3 9         52659   1     19987   1     21203   8  30878962  22  22045574  28    240078   9     1.3
c  4 14        81044   2     43943   2     18866   7  17793098  13< 13629231  17<   175746   7     2.7
c  5 21       131115   3     88735   4     13176   5   9043679   7   6433536   8    152041   6     6.9
c  6 30       149217   4    109630   5     20397   7   7620844   6   4357020   6    208876   8     5.2
c  7 41       279614   7    235469  11     18207   6   7716349   6   4039641   5    273417  10<    7.2
c  8 54       633590  17    564717  26<    22805   8<  8530900   6   4338691   6    390659  14    20.8
c  9 69       356541   9<   305675  14     13576   5   4686971   3   2340330   3    292303  11    11.8
c 10 86      1763361  46    749245  35    115049  41   7505399   5   4770949   6    691691  26    68.2
c 11 126      320649   8     46464   2     27066  10    702591   1    333172   0     35615   1    20.6
c 12 230        7723   0       883   0      1274   0     10778   0      5694   0       184   0     0.8
c 13 534          41   0        15   0         9   0        57   0        33   0         0   0     0.1
c 
c avg                  8.8           8.4           8.0           4.0           4.4           7.0
c std                  1.9           1.7           2.8           2.8           2.5           2.8
c 
c  156.112  16% bump
c  100.398  10% elim
c   41.827   4% rescore
c   31.107   3% decide
c   27.270   3% block
c   24.465   2% probe
c   14.279   1% unhide
c    5.296   1% bca
c    4.694   0% sweep
c 
c   11.497 < 1% rest (below)
c 
c    4.561   0% quatres
c    3.007   0% cce
c    1.678   0% ternres
c    1.054   0% gauss
c    1.019   0% transred
c    0.178   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    5.103   1% preprocessing     3%
c  193.993  19% inprocessing     97%
c ==================================
c  199.096  20% simplifying
c  800.046  80% search
c ==================================
c  999.144 100% all
c 
c       3911282 conflicts,        3914.6 confs/sec
c           674 ternaries,        5803.1 confs/ternary
c           515 binaries,         7594.7 confs/binary
c             1 iterations,    3911282.0 confs/iteration
c 
c            56 reductions,          0.1 redus/sec,  69844.3 confs/reduction
c         14479 restarts,           14.5 rests/sec,    270.1 confs/restart
c      46964571 decisions,       47004.8 decis/sec,     12.0 decis/conflict
c    2073359997 propagations,  2075136.4 props/sec,     44.1 props/decision
c 
c 999.1 seconds, 204.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
