c launch: /data/cnf/sc2014/app/minandmaxor128.cnf.bz2
c host: atom19
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/minandmaxor128.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/minandmaxor128.cnf.bz2
c no embedded options
c found 'p cnf 249327 746444' header
c read 249327 variables, 746444 clauses, 1741700 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 249325 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  249325   746442         0       0      0     0    0     0   39   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] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 10 variables
c [simpleprobe-1] all 249317 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 2 variables
c [simpleprobe-1] 48777 variables remain 20% (200538 retained 80%)
c [simpleprobe-1] removed 2 variables, found 0 hbrs, 1 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 2 units, 13 failed, 26 tauts, 0 hbrs, 3 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 249305 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 75394 not tried 30% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 173728 = 70% variables out of 249305 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 339408 negative 89.2% of 380700 except 41292 10.8%
c [phase-count-1] 306793 positive 80.6% of 380700 except 73907 19.4%
c [phase-1] phase bias: 23989 positive 32%, 51588 negative 68%
c [sort-queue-1] sorted 75577 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 75577 (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 173740 variables 69.7% (75577 remain 30%)
c [simplification-1] removed 365742 irredundant clauses 49.0% (380700 remain 51%)
c [simplification-1] maximum reduction of 70% = max (70%, 49%)
c [simplification-1] large reduction 70% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [simpleprobe-2] 14706 schedulable variables 19%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 15808 variables remain 21% (59769 retained 79%)
c [simpleprobe-2] removed 0 variables, found 726 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 38939 literals 26%
c [treelook-1] scheduling used 300006 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 439754 steps
c [treelook-1] 38918 literals remain 26%
c [treelook-1] 35767 variables remain to probed next time 47%
c [treelook-1] removed 0 variables, found 6679 hbrs
c [basicprobe-1] limit 3045600 based on 380700 irredundant clauses
c [basicprobe-1-0] 34846 probes remain 46% after last round
c [basicprobe-1-0] removed 0 variables, found 19065 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 1648 tauts, 0 hbrs, 2300 literals
c [elim-2] 75394 variables 100% will be scheduled this time
c [elim-2] scheduled 75394 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 15271 not tried 20% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 13322 = 18% variables out of 75394 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 322456 negative 87.0% of 370574 except 48118 13.0%
c [phase-count-2] 299445 positive 80.8% of 370574 except 71129 19.2%
c [phase-2] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-2] sorted 41294 enqueued variables after 1000 conflicts
c [score-dist-2] active 20961 (34%), one 0 (0%), zero 41294 (66%)
c [score-dist-2] max exp 509, different 12 (2%)
c [score-dist-2] median active exp 501, avg 501.3
c [simplification-2] removed 13322 variables 17.6% (62255 remain 25%)
c [simplification-2] removed 10126 irredundant clauses 2.7% (370574 remain 50%)
c [simplification-2] maximum reduction of 18% = max (18%, 3%)
c [simplification-2] large reduction 18% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 28 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] 28 out of 28 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 62255 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 7061 not tried 11% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 899 = 1% variables out of 62255 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 321124 negative 87.0% of 369035 except 47911 13.0%
c [phase-count-3] 298382 positive 80.9% of 369035 except 70653 19.1%
c [phase-3] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-3] sorted 37801 enqueued variables after 3000 conflicts
c [score-dist-3] active 23555 (38%), one 0 (0%), zero 37801 (62%)
c [score-dist-3] max exp 509, different 20 (4%)
c [score-dist-3] median active exp 503, avg 499.7
c [simplification-3] removed 899 variables 1.4% (61356 remain 25%)
c [simplification-3] removed 1539 irredundant clauses 0.4% (369035 remain 49%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23000 (soft 13000 + delta 10000)
c [simplification-3] new conflict limit 13000 (hard 23000)
c 
c [simplification-4] limit of 136 binary hit after 136 binaries
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 14053 literals 11%
c [treelook-2] scheduling used 150262 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 243133 steps
c [treelook-2] 13975 literals remain 11%
c [treelook-2] 11419 variables remain to probed next time 19%
c [treelook-2] removed 0 variables, found 940 hbrs
c [unhide-3] limit 183030 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 183 tauts, 0 hbrs, 19787 literals
c [elim-4] 6831 variables 11% will be scheduled this time
c [elim-4] scheduled 6831 variables 11%
c [elim-4] boosting limit by 20
c [elim-4] limit of 732123140 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 1389 variables 2% in round 1 in 90617494 steps
c [elim-4-1] backward subsumption/strengthening limit 90617400
c [elim-4-1-1] backward checking 3184 touched variables 5%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 899 and strengthened 352 clauses in 17631961 steps
c [elim-4-1] rescheduled 909 variables 1% by backward subsumption
c [elim-4-2] eliminated 3 variables 0% in round 2 in 2319896 steps
c [elim-4-2] backward subsumption/strengthening limit 2319800
c [elim-4-2-1] backward checking 46 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 7 clauses in 985208 steps
c [elim-4-2] rescheduled 14 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 811120 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 1392 = 20% variables out of 6831 scheduled
c [phase-count-4] 317797 negative 87.0% of 365478 except 47681 13.0%
c [phase-count-4] 295379 positive 80.8% of 365478 except 70099 19.2%
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-4] sorted 35352 enqueued variables after 5909 conflicts
c [score-dist-4] active 24612 (41%), one 0 (0%), zero 35352 (59%)
c [score-dist-4] max exp 509, different 32 (6%)
c [score-dist-4] median active exp 500, avg 498.1
c [simplification-4] removed 1392 variables 2.3% (59964 remain 24%)
c [simplification-4] removed 3557 irredundant clauses 1.0% (365478 remain 49%)
c [simplification-4] maximum reduction of 2% = max (2%, 1%)
c [simplification-4] forced so keeping old conflict interval 10000
c [simplification-4] conflict limit remains at 13000 (hard 23000)
c [simplification-4] new binary interval 1000
c 
c [simplification-5] limit 13000 conflicts (hard 23000) hit after 13001 conflicts
c [quatres-1] found 55579 quaternary clauses 51% in total
c [quatres-1-1] removed 4 duplicate quaternary clauses
c [quatres-1-2] added 28 single-self-subsuming ternary resolvents
c [quatres-1-2] added 2877 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 59964 free variables schedulable
c [ternres-1] 87194 ternary resolvents (0 bin, 87194 trn)
c [ternres-1] 9870 variables remain 16% (50094 retained 84%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 14095 xors of average arity 3.0
c [gauss-1] connected 42270 occurrences of 15129 variables (average 2.8)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 19 variables
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 39 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 59945 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 919 blocked clauses
c [block-1] 919 < 1/100 * 365439 = 3654 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 6 (17%) of length 129
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1 large clauses in 30000952 steps
c [cce-1-1] allowing another 15000476 steps for small clauses
c [cce-1-1] scheduling 91186 clauses = 73238 binary + 17948 ternary
c [cce-1-1] tried to eliminate 442 small clauses 0%
c [cce-1-1] eliminated 1 ternary clauses 0%
c [cce-1-1] eliminated 1 small clauses 0%
c [cce-1-1] eliminated 1 small clauses in 30000005 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2 covered clauses in round 1
c [cce-1] eliminated 2 covered clauses in TOTAL during 1 rounds
c [cce-1] 2 < 1/100 * 364520 = 3645 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 59945 variables 100%
c [elim-5] limit of 77308274 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 355 not tried 1% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 264 = 0% variables out of 59945 scheduled
c [elim-5] 264 < 1/100 * 59945 = 599 considered unsuccessful
c [bca-1] limit of 10000000 steps and 729282 added (scaled 2)
c [bca-1] 96322 out of 119364 literals actually usable 81%
c [bca-1] added 385 blocked clauses in 248958 steps
c [sweep-1] limit 1159624 penalty 0 = 0 + 0
c [sweep-1-1] 28104 pos 47.1% + 31577 neg 52.9% = 59681 sched 100.0% ret 0
c [sweep-1-1] 1352066 steps 15 queries 11631.87 avg class size
c [sweep-1-1] 535 decisions 13 SAT calls 726.54 avg env size
c [sweep-1-1] 59647 variables remain 100% (34 retained 0%)
c [decomp-10] removed 3 variables
c [sweep-1-1] removed 3 vars (0 failed, 3 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 3 vars in TOTAL (1 rounds, 14 queries)
c [sort-queue-5] sorted 28142 enqueued variables after 13001 conflicts
c [score-dist-5] active 31536 (53%), one 0 (0%), zero 28142 (47%)
c [score-dist-5] max exp 510, different 60 (12%)
c [score-dist-5] median active exp 497, avg 492.1
c [simplification-5] removed 286 variables 0.5% (59678 remain 24%)
c [simplification-5] removed 1093 irredundant clauses 0.3% (364385 remain 49%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 20000
c [simplification-5] new conflict interval 30000
c [simplification-5] penalized conflict interval 30000 = 1 * 30000
c [simplification-5] hard conflict limit 58001 (soft 43001 + delta 15000)
c [simplification-5] new conflict limit 43001 (hard 58001)
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   65.5   59677   364385     38976   36476  87843 20606  108   381   75  28%    450  163  188   58  322%
c 
c [simplification-6] limit 43001 conflicts (hard 58001) hit after 48961 conflicts
c [quatres-2] found 58859 quaternary clauses 52% in total
c [quatres-2-2] added 2 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1688 quaternary resolvents
c [ternres-2] limit 15258552 with penalty 0 = 0 + 0
c [ternres-2] 9860 schedulable variables 17%
c [ternres-2] 43281 ternary resolvents (1 bin, 43280 trn)
c [ternres-2] 139 variables remain 0% (59538 retained 100%)
c [card-3] limit 1907319 penalty 2 = 2 + 0
c [card-3] found 67 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1907319 for elimination
c [card-3] 67 out of 67 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 1 variables
c [basicprobe-2] limit 38146380 penalty 1 = 1 + 0
c [basicprobe-2-0] 28102 probes remain 47% after last round
c [basicprobe-2-0] removed 0 variables, found 200176 hbrs
c [bate-1] eliminated 41 asymmetric tautologies during probing
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 91 transitive binary clauses
c [bca-2] limit of 10000000 steps and 729104 added (scaled 2)
c [bca-2] 76995 out of 119356 literals actually usable 65%
c [bca-2] added 0 blocked clauses in 230942 steps
c [sweep-2] limit 4577565 penalty 0 = 0 + 0
c [sweep-2-1] 27919 pos 46.8% + 31727 neg 53.2% = 59646 sched 99.9% ret 31
c [sweep-2-1] 10108427 steps 40 queries 10328.02 avg class size
c [sweep-2-1] 979 decisions 38 SAT calls 92.47 avg env size
c [sweep-2-1] 59287 variables remain 99% (390 retained 1%)
c [decomp-12] removed 1 variables
c [sweep-2-1] removed 1 vars (0 failed, 1 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 1 vars in TOTAL (1 rounds, 39 queries)
c [sort-queue-6] sorted 19594 enqueued variables after 48961 conflicts
c [score-dist-6] active 40082 (67%), one 0 (0%), zero 19594 (33%)
c [score-dist-6] max exp 510, different 191 (37%)
c [score-dist-6] median active exp 489, avg 470.2
c [simplification-6] removed 1 variables 0.0% (59676 remain 24%)
c [simplification-6] removed 181 irredundant clauses 0.0% (364204 remain 49%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 30000
c [simplification-6] new conflict interval 60000
c [simplification-6] penalized conflict interval 60000 = 1 * 60000
c [simplification-6] hard conflict limit 138961 (soft 108961 + delta 30000)
c [simplification-6] new conflict limit 108961 (hard 138961)
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 -   95.2   59676   364204     64075   26838 131372 272096  144   446   62  32%    211  140   90   77  117%
c -  136.7   59676   364204    108912   33625 131765 272499   72   352   62  21%    614  -21  173   89  193%
c 
c [simplification-7] limit 108961 conflicts (hard 138961) hit after 109464 conflicts
c [quatres-3] found 61382 quaternary clauses 50% in total
c [quatres-3-2] added 9 single-self-subsuming ternary resolvents
c [quatres-3-2] added 79 quaternary resolvents
c [ternres-3] limit 34205098 with penalty 0 = 0 + 0
c [ternres-3] 139 schedulable variables 0%
c [ternres-3] 727 ternary resolvents (0 bin, 727 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 3420509 penalty 1 = 1 + 0
c [gauss-2] extracted 11385 xors of average arity 3.0
c [gauss-2] connected 34155 occurrences of 10600 variables (average 3.2)
c [gauss-2] limit 3420509 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 2 variables
c [unhide-4] limit 1710254 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 2852 tauts, 0 hbrs, 16989 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 94 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 59674 variables 100%
c [block-2] limit of 171025490 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 2 blocked clauses
c [block-2] 2 < 1/100 * 364197 = 3641 considered unsuccessful
c [cce-2] limit of 85512745 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 136
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 134
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 133
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 132
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 131
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 130
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 129
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 128
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 127
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 126
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 125
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 124
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 123
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 122
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 121
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 120
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 119
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 118
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 117
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 116
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 115
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 114
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 113
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 112
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 111
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 110
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 109
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 108
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 107
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 106
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 105
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 104
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 103
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 102
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 101
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 100
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 99
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 98
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 97
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 96
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 95
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 94
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 93
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 92
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 91
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 90
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 89
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 88
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 87
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 86
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 85
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 84
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 83
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 82
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 81
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 80
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 79
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 78
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 77
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 76
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 75
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 74
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 73
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 72
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 71
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 70
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 69
c [cce-2-1] eliminated 1 clauses out of 9 (11%) of length 68
c [cce-2-1] eliminated 1 clauses out of 15 (7%) of length 67
c [cce-2-1] eliminated 1 clauses out of 16 (6%) of length 66
c [cce-2-1] eliminated 1 clauses out of 17 (6%) of length 65
c [cce-2-1] eliminated 1 clauses out of 20 (5%) of length 64
c [cce-2-1] eliminated 1 clauses out of 23 (4%) of length 63
c [cce-2-1] eliminated 1 clauses out of 30 (3%) of length 62
c [cce-2-1] eliminated 1 clauses out of 27 (4%) of length 61
c [cce-2-1] eliminated 1 clauses out of 36 (3%) of length 60
c [cce-2-1] eliminated 1 clauses out of 38 (3%) of length 59
c [cce-2-1] eliminated 1 clauses out of 42 (2%) of length 58
c [cce-2-1] eliminated 1 clauses out of 37 (3%) of length 57
c [cce-2-1] eliminated 1 clauses out of 46 (2%) of length 56
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 82 large clauses in 85514867 steps
c [cce-2-1] allowing another 42757433 steps for small clauses
c [cce-2-1] scheduling 90807 clauses = 73275 binary + 17532 ternary
c [cce-2-1] tried to eliminate 1321 small clauses 1%
c [cce-2-1] eliminated 2 binary clauses 0%
c [cce-2-1] eliminated 1 ternary clauses 0%
c [cce-2-1] eliminated 3 small clauses 0%
c [cce-2-1] eliminated 3 small clauses in 85512915 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 85 covered clauses in round 1
c [cce-2] eliminated 85 covered clauses in TOTAL during 1 rounds
c [cce-2] 85 < 1/100 * 364195 = 3641 considered unsuccessful
c [elim-6] 354 variables 1% will be scheduled this time
c [elim-6] scheduled 354 variables 1%
c [elim-6] limit of 342050981 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 24927996 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 354 scheduled
c [sweep-3] limit 10261529 penalty 0 = 0 + 0
c [sweep-3-1] 24361 pos 41.1% + 34925 neg 58.9% = 59286 sched 99.3% ret 388
c [sweep-3-1] 10681440 steps 115 queries 4093.16 avg class size
c [sweep-3-1] 2197 decisions 103 SAT calls 110.86 avg env size
c [sweep-3-1] 57741 variables remain 97% (1933 retained 3%)
c [decomp-14] removed 14 variables
c [sweep-3-1] removed 14 vars (0 failed, 13 eqs, 25 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 14 vars in TOTAL (1 rounds, 114 queries)
c [sort-queue-7] sorted 9986 enqueued variables after 109464 conflicts
c [score-dist-7] active 49674 (83%), one 0 (0%), zero 9986 (17%)
c [score-dist-7] max exp 510, different 376 (74%)
c [score-dist-7] median active exp 458, avg 432.6
c [simplification-7] removed 16 variables 0.0% (59660 remain 24%)
c [simplification-7] removed 123 irredundant clauses 0.0% (364081 remain 49%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 60000
c [simplification-7] new conflict interval 120000
c [simplification-7] penalized conflict interval 120000 = 1 * 120000
c [simplification-7] hard conflict limit 289464 (soft 229464 + delta 60000)
c [simplification-7] new conflict limit 229464 (hard 289464)
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 -  180.3   59660   364081    148890   37888 132490 282685  137   410   62  33%    801  -20  137  117  117%
c -  207.9   59660   364081    188050   41416 132906 282880  107   424   61  25%    901  -54  115  112  102%
c 
c [simplification-8] limit of 2240 ternary hit after 2240 ternaries
c [quatres-4] found 62687 quaternary clauses 48% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 10 single-self-subsuming ternary resolvents
c [quatres-4-2] added 86 quaternary resolvents
c [ternres-4] limit 60084530 with penalty 0 = 0 + 0
c [ternres-4] all 59660 free variables schedulable
c [ternres-4] 15500 ternary resolvents (12 bin, 15488 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-15] removed 1 variables
c [simpleprobe-3] 12371 schedulable variables 21%
c [simpleprobe-3] limit 100000000 penalty 1 = 1 + 0
c [decomp-16] removed 1 variables
c [simpleprobe-3] 2428 variables remain 4% (57230 retained 96%)
c [simpleprobe-3] removed 1 variables, found 33639 hbrs, 1 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 193 transitive binary clauses
c [bca-3] limit of 10000000 steps and 728592 added (scaled 2)
c [bca-3] 64805 out of 119318 literals actually usable 54%
c [bca-3] added 0 blocked clauses in 214998 steps
c [sweep-4] limit 18025359 penalty 0 = 0 + 0
c [sweep-4-1] 27685 pos 48.0% + 30052 neg 52.0% = 57737 sched 96.8% ret 1921
c [sweep-4-1] 18546521 steps 113 queries 4037.85 avg class size
c [sweep-4-1] 2810 decisions 108 SAT calls 110.86 avg env size
c [sweep-4-1] 55490 variables remain 93% (4168 retained 7%)
c [decomp-17] removed 4 variables
c [sweep-4-1] removed 4 vars (0 failed, 4 eqs, 10 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 4 vars in TOTAL (1 rounds, 112 queries)
c [sort-queue-8] sorted 9640 enqueued variables after 210113 conflicts
c [score-dist-8] active 50014 (84%), one 3282 (6%), zero 6358 (11%)
c [score-dist-8] max exp 510, different 456 (89%)
c [score-dist-8] median active exp 492, avg 427.1
c [simplification-8] removed 6 variables 0.0% (59654 remain 24%)
c [simplification-8] removed 139 irredundant clauses 0.0% (363942 remain 49%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] forced so keeping old conflict interval 120000
c [simplification-8] conflict limit remains at 229464 (hard 289464)
c [simplification-8] new ternary interval 10000
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 -  242.7   59654   363942    228623   47111 148737 373813  133   518   66  26%    958   19  130  107  121%
c 
c [simplification-9] limit 229464 conflicts (hard 289464) hit after 229465 conflicts
c [quatres-5] found 63087 quaternary clauses 47% in total
c [quatres-5-2] added 5 single-self-subsuming ternary resolvents
c [quatres-5-2] added 19 quaternary resolvents
c [ternres-5] limit 66602339 with penalty 0 = 0 + 0
c [ternres-5] all 59654 free variables schedulable
c [ternres-5] 316 ternary resolvents (2 bin, 314 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 136 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 199807010 penalty 0 = 0 + 0
c [sweep-5-1] 26275 pos 47.4% + 29215 neg 52.6% = 55490 sched 93.0% ret 4164
c [sweep-5-1] 202366704 steps 955 queries 407.31 avg class size
c [sweep-5-1] 13442 decisions 785 SAT calls 63.38 avg env size
c [sweep-5-1] 28019 variables remain 47% (31634 retained 53%)
c [decomp-19] removed 216 variables
c [sweep-5-1] removed 216 vars (0 failed, 202 eqs, 355 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 216 vars in TOTAL (1 rounds, 954 queries)
c [sort-queue-9] sorted 9384 enqueued variables after 229465 conflicts
c [score-dist-9] active 50054 (84%), one 4187 (7%), zero 5197 (9%)
c [score-dist-9] max exp 509, different 445 (87%)
c [score-dist-9] median active exp 499, avg 452.4
c [simplification-9] removed 216 variables 0.4% (59438 remain 24%)
c [simplification-9] removed 560 irredundant clauses 0.2% (363382 remain 49%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 120000
c [simplification-9] new conflict interval 240000
c [simplification-9] penalized conflict interval 240000 = 1 * 240000
c [simplification-9] hard conflict limit 589465 (soft 469465 + delta 120000)
c [simplification-9] new conflict limit 469465 (hard 589465)
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 -  296.9   59438   363382    268177   50580 147327 680313  102   431   74  24%    988  -65  134  117  115%
c -  339.9   59438   363382    310458   55259 147755 680384   78   508   74  15%   1005    6  108  130   83%
c -  372.8   59438   363382    351634   59797 148108 680454   48   274   74  18%   1014 -194   48  116   42%
c -  411.7   59438   363382    393327   63207 148452 680529  121   466   73  26%   1019    8  119  123   97%
c -  452.7   59438   363382    436054   66423 148707 680607  157   350   75  45%   1021  -76  238  118  201%
c 
c [simplification-10] limit 469465 conflicts (hard 589465) hit after 469465 conflicts
c [quatres-6] found 65673 quaternary clauses 43% in total
c [quatres-6-2] added 14 single-self-subsuming ternary resolvents
c [quatres-6-2] added 188 quaternary resolvents
c [ternres-6] limit 162481670 with penalty 0 = 0 + 0
c [ternres-6] all 59438 free variables schedulable
c [ternres-6] 3795 ternary resolvents (85 bin, 3710 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 10155104 penalty 3 = 3 + 0
c [card-4] found 46 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 10155104 for elimination
c [card-4] 46 out of 46 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 8124083 penalty 2 = 2 + 0
c [gauss-3] extracted 13998 xors of average arity 3.0
c [gauss-3] connected 41976 occurrences of 7854 variables (average 5.3)
c [gauss-3] limit 8124083 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 1 variables
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 243 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 59437 variables 100%
c [block-3] limit of 200000000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-3] limit of 203102088 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 129
c [cce-3-1] eliminated 1 clauses out of 41 (2%) of length 55
c [cce-3-1] eliminated 1 clauses out of 51 (2%) of length 54
c [cce-3-1] eliminated 1 clauses out of 48 (2%) of length 53
c [cce-3-1] eliminated 1 clauses out of 50 (2%) of length 52
c [cce-3-1] eliminated 1 clauses out of 62 (2%) of length 51
c [cce-3-1] eliminated 1 clauses out of 71 (1%) of length 50
c [cce-3-1] eliminated 1 clauses out of 88 (1%) of length 49
c [cce-3-1] eliminated 1 clauses out of 102 (1%) of length 48
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 11 large clauses in 203103824 steps
c [cce-3-1] allowing another 101551912 steps for small clauses
c [cce-3-1] scheduling 238239 clauses = 73408 binary + 164831 ternary
c [cce-3-1] tried to eliminate 3051 small clauses 1%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 23 ternary clauses 0%
c [cce-3-1] eliminated 24 small clauses 0%
c [cce-3-1] eliminated 24 small clauses in 203102093 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 35 covered clauses in round 1
c [cce-3] eliminated 35 covered clauses in TOTAL during 1 rounds
c [cce-3] 35 < 1/100 * 363377 = 3633 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 59437 variables 100%
c [elim-7] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 98 variables 0% in round 1 in 139458559 steps
c [elim-7-1] backward subsumption/strengthening limit 60541441
c [elim-7-1-1] backward checking 1319 touched variables 2%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 1 and strengthened 312 clauses in 26045652 steps
c [elim-7-1] rescheduled 944 variables 2% by backward subsumption
c [elim-7] incomplete 61 not tried 0% in round 2
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 99 = 0% variables out of 59437 scheduled
c [elim-7] 99 < 1/100 * 59437 = 594 considered unsuccessful
c [sweep-6] limit 48744501 penalty 0 = 0 + 0
c [sweep-6-1] 19477 pos 69.7% + 8482 neg 30.3% = 27959 sched 47.1% ret 31379
c [sweep-6-1] 48774032 steps 161 queries 1760.80 avg class size
c [sweep-6-1] 3557 decisions 146 SAT calls 89.32 avg env size
c [sweep-6-1] 26071 variables remain 44% (33266 retained 56%)
c [decomp-21] removed 23 variables
c [sweep-6-1] removed 23 vars (0 failed, 19 eqs, 29 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 23 vars in TOTAL (1 rounds, 160 queries)
c [sort-queue-10] sorted 8956 enqueued variables after 469465 conflicts
c [score-dist-10] active 50359 (85%), one 7247 (12%), zero 1709 (3%)
c [score-dist-10] max exp 510, different 430 (84%)
c [score-dist-10] median active exp 494, avg 446.6
c [simplification-10] removed 123 variables 0.2% (59315 remain 24%)
c [simplification-10] removed 560 irredundant clauses 0.2% (362822 remain 49%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 240000
c [simplification-10] new conflict interval 480000
c [simplification-10] penalized conflict interval 480000 = 1 * 480000
c [simplification-10] hard conflict limit 1189465 (soft 949465 + delta 240000)
c [simplification-10] new conflict limit 949465 (hard 1189465)
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 -  519.7   59315   362822    481754   69013 152332 786891  157   493   79  32%   1023   36  291  146  200%
c -  565.4   59315   362822    527969   74116 152690 786966  112   400   79  28%   1023  -50  102  150   68%
c -  611.8   59315   362822    571560   75946 152943 787004  287   600   80  48%   1024  150  291  160  182%
c -  653.5   59315   362822    621851   81448 153269 787087  192   500   81  38%   1024   76  164  147  112%
c -  693.7   59315   362822    667136   83908 153510 787163  145   404   79  36%   1024  -38  173  143  121%
c -  746.8   59315   362822    717166   88951 153870 787226  125   394   80  32%   1024  -33  178  127  141%
c -  795.9   59315   362822    774345   95005 154440 787341   71   120   81  59%   1024 -184   32  108   30%
c -  845.0   59315   362822    821412   96249 154689 787422  174   506   80  34%   1024  163  161  135  119%
c -  895.7   59315   362822    874480  101754 154960 787494   46   477   81  10%   1024   59    7  141    5%
c -  946.0   59315   362822    920646  104556 155249 787552  273   603   83  45%   1024  157  346  144  241%
c i  975.1   59314   362822    940391  120697 155319 787565  280   630  122  44%   1024  137  268  187  143%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 41 basic ate = 4 trn 10% + 37 lrg 90% in 1 updates
c bcas: 3 count, 385 added (0 skipped), 694898 steps
c bkwd: tried 197383 clauses, 393227 lits, 1.99 lits/clause
c bkwd: checked 36696175 occs, 185.91 occs/clause, 93.32 occs/lit
c bkwd: subsumed 9 binary, 97 ternary, 794 large
c bkwd: strengthened 0 binary, 35 ternary (100% self), 636 large (0% self)
c blkd: 3 bces, 921 removed, 7531272 resolutions, 18147188 steps
c blkd: 337 blocking literals 0%, 0 pure
c bump: 959320 bumped seen, 263353070 lits 274.5 on average
c card: 4 count, 0 units, 0 am1, 36493784 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1914 subsumed
c card: 141 at-most-one constraints found, average size 3.00
c card: 141 at-most-one constraints used 100%, average size 3.00
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: 3 cces, 122 eliminated, 114 ate 93%, 8 abce 7%
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: 2488144 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 39 gcs, 0 rescored clauses, 3747 rescored vars
c dcps: 21 decompositions, 283 equivalent 0%
c deco: 69737 decision-only clauses 7%, 49% reduction
c decs: 16568126 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 7 elims, 189704 eliminated 76%, 0 pure 0%
c elms: 10 rounds, 1.4 rounds/bve
c elms: 169737 small 89%, 19967 large 11%
c elms: 319046 tried small, 169737 succeeded 53%, 149309 failed 47%
c elms: 2356 subsumed, 3596 strengthened, 29 blocked
c elms: 7528449 copies, 11413246 resolutions, 9721517 ipos
c elms: 6814369 subchks, 4721389 strchks
c gaus: 3 extractions, 39478 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 27436920 steps, 13718460 extr 50%, 13594530 elim 50%
c glue: 135.6 orig avg, 135.6 real avg, 7.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 824988 = 34365 simple 4% + 790032 trn 96% + 591 lrg 0%, 857 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 959320 clauses, 184.4 length
c lrnd: 176919848 lits = 207028953 orig - 30109105 removed 15%
c lrnd: 448977 uips 47%, 307462 flips 32%
c mins: 653383 mins 85%, 3213 bin 0%, 46152 size 6%
c mins: 81526631 poisoned searches, 9869920 hits, 12% hit rate
c mins: 134185200 used twice searches, 37796047 hits, 28% hit rate
c move: moved 635, 133 bin 21%, 502 trn 79%
c otfs: 12728 driving 30%, 29337 restarting 70%
c otfs: str 42065, 41499 red 99%, 566 irr 1%
c otfs: str 42065, 0 bin 0%, 623 trn 1%, 41442 lrg 99%
c otfs: sub 314, 314 red 100%, 0 irr 0%
c otfs: sub 314, 0 bin 0%, 1 trn 0%, 313 lrg 100%
c phas: 4 computed, 75579 set, 23991 pos (32%), 51588 neg (68%)
c prbs: 2 basic, 6056 probed, 0 failed, 0 lifted
c prbs: 3 simple, 490751 probed, 2 failed, 0 eqs
c prbs: 2 treelook, 99 probed, 0 failed, 0 lifted
c prom: 119277 locked 8% out of 1416379 tried
c prps: 2107953159 props, 127 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 6 count, 4937 quat, 68 self1, 0 self2, 13 dup
c queu: 10 sorted, 16568126 next (311462 steps 0.02)
c queu: 452132555 enq (743583457 steps 1.64), 263353070 deq 58%
c redc: 9420 clauses 8%, 117190 tried 12%, 27 sat 0%
c redc: 12081 lits 1%, 993061 tried 0%, 27 sat 0%
c redc: 277 times jump level reduced, 15.8 levels on average
c reds: 20 count, 48546.1 conflicts per reduce
c reds: 0 memlim 0%, 20 arith 100%
c reds: 595539 collected 83%, 120159 retired 17%
c rmbd: 2176 removed, 2124 red 98%
c rsts: 16442 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 10 count, 8 confs 80%, 0 vars 0%
c simp: 0 its 0%, 1 bin 10%, 1 trns 10%
c subl: 959320 count (1316330 tried 1.4), 85560 sub out of 947944 (9.0%)
c swps: 6 count, 6 rounds, 1393 queries (232.2/round)
c swps: 1193 sat calls, 42 unsat (0.9% success rate)
c swps: 23520 decisions 19.7, 1127 conflicts 0.9
c swps; 1570.0 avg class size, 83.1 avg environment size
c swps: 0 failed, 424 impls, 242 equivs
c swp0: 463 type 0 queries, 133 unsat (28.7%), 403 sat (87.0%)
c swp1: 930 type 1 queries, 439 unsat (47.2%), 748 sat (80.4%)
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: 35062560 calls to obtain time
c tops: 26 fixed 0%, 2 its, 485460.50 confs/it
c trds: 6 transitive reductions, 796 removed, 0 failed
c trds: 17416 nodes, 25983 edges, 12008441 steps
c trim: 1015458 words, 3.9 MB
c trnr: 6 count, 100 bin, 150713 trn, 235007853 steps
c unhd: 4 count, 4 rounds, 11308708 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 2 units, 2 bin, 0 trn, 0 lrg
c unhd: 13 failed, 13 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 4709 tauts, 0 bin 0%, 260 trn 6%, 94 lrg 2%
c unhd: 4709 tauts, 4355 stamp 92%, 4539 red 96%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 39079 str, 2 bin 0%, 1021 trn 3%, 38056 lrg 97%, 34136 red 87%
c vars: 59314 remaining 24% and 190013 removed 76% out of 249327
c vars: 26 fixed 0%, 189704 eliminated 76%, 283 equivalent 0%
c vsts: 36535572173 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 17.3 search visits per propagation, 37422.9 per conflict
c wchs: 1072366286 pushed, 21035670 enlarged, 71 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         952881        595539        120159     181108251      12931895        395194
c 
c  0 0         82137   9      2785   0         0   0  77865351  43   4066513  31     98036  25     2.7
c  1 5         32194   3     19488   3      6042   5  10902455   6    929535   7     22596   6     0.6
c  2 6         69304   7     44814   8     12182  10  19178874  11   1511012  12     38872  10     1.7
c  3 9         63197   7     42137   7      9884   8  15165596   8<  1082530   8     29681   8     2.0
c  4 14        46837   5     33070   6      6930   6   8721618   5    603811   5<    17042   4     1.1
c  5 21        32769   3     23641   4      4676   4   8509105   5    442875   3     10649   3     1.1
c  6 30        30727   3     22716   4      3940   3   6444221   4    409354   3     10343   3<    1.4
c  7 41        28969   3     22558   4      3605   3   6204374   3    386941   3     10049   3     1.5
c  8 54        33613   4<    26958   5<     3710   3<  4923771   3    357657   3      9945   3     2.3
c  9 69        41023   4     32879   6      4302   4   3848856   2    318344   2     10573   3     2.9
c 10 86        87587   9     66946  11      9561   8   9808938   5    924909   7     22766   6     6.4
c 11 126      198489  21    142806  24     25403  21   6571315   4   1120496   9     47717  12    13.7
c 12 230      182458  19    105305  18     27068  23   2885888   2    734372   6     61424  16    26.0
c 13 534       23577   2      9436   2      2856   2     77889   0     43546   0      5501   1    13.8
c 
c avg                  7.7           8.3           8.0           3.0           4.2           5.5
c std                  4.3           3.7           4.0           3.6           4.3           4.8
c 
c   50.732   5% bump
c   24.896   2% rescore
c   16.450   2% elim
c   16.354   2% sweep
c   11.716   1% decide
c    6.474   1% probe
c    4.558   0% cce
c 
c   10.793 < 1% rest (below)
c 
c    2.650   0% block
c    1.950   0% ternres
c    1.645   0% gauss
c    1.492   0% unhide
c    1.028   0% quatres
c    0.897   0% transred
c    0.804   0% bca
c    0.326   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    4.841   0% preprocessing     8%
c   54.521   5% inprocessing     92%
c ==================================
c   59.362   6% simplifying
c  940.247  94% search
c ==================================
c  999.612 100% all
c 
c        970921 conflicts,         971.3 confs/sec
c          7706 ternaries,         126.0 confs/ternary
c          3317 binaries,          292.7 confs/binary
c             2 iterations,     485460.5 confs/iteration
c 
c            20 reductions,          0.0 redus/sec,  48546.1 confs/reduction
c         16442 restarts,           16.4 rests/sec,     59.1 confs/restart
c      16568126 decisions,       16574.5 decis/sec,     17.1 decis/conflict
c    2107953159 propagations,  2108770.4 props/sec,    127.2 props/decision
c 
c 999.6 seconds, 164.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
