c launch: /data/cnf/sc2014/app/minandmaxor128.cnf.bz2
c host: atom31
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=6
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] AVG (--score=6)
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 1001 conflicts
c [simpleprobe-2] 14706 schedulable variables 19%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 15772 variables remain 21% (59805 retained 79%)
c [simpleprobe-2] removed 0 variables, found 702 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 38504 literals 25%
c [treelook-1] scheduling used 300024 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 304928 steps
c [treelook-1] 38491 literals remain 25%
c [treelook-1] 35412 variables remain to probed next time 47%
c [treelook-1] removed 0 variables, found 3991 hbrs
c [basicprobe-1] limit 3045600 based on 380700 irredundant clauses
c [basicprobe-1-0] 33498 probes remain 44% after last round
c [basicprobe-1-0] removed 0 variables, found 68498 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 1689 tauts, 0 hbrs, 1662 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 15319 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] 322287 negative 87.0% of 370411 except 48124 13.0%
c [phase-count-2] 299324 positive 80.8% of 370411 except 71087 19.2%
c [phase-2] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-2] sorted 40568 enqueued variables after 1001 conflicts
c [score-dist-2] active 21687 (35%), one 0 (0%), zero 40568 (65%)
c [score-dist-2] max exp 511, different 10 (2%)
c [score-dist-2] median active exp 510, avg 510.3
c [simplification-2] removed 13322 variables 17.6% (62255 remain 25%)
c [simplification-2] removed 10289 irredundant clauses 2.7% (370411 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 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
c 
c [simplification-3] limit of 123 binary hit after 123 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1 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] 1 out of 1 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 7055 not tried 11% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 927 = 1% variables out of 62255 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 320819 negative 87.0% of 368736 except 47917 13.0%
c [phase-count-3] 298132 positive 80.9% of 368736 except 70604 19.1%
c [phase-3] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-3] sorted 36919 enqueued variables after 2510 conflicts
c [score-dist-3] active 24409 (40%), one 0 (0%), zero 36919 (60%)
c [score-dist-3] max exp 513, different 12 (2%)
c [score-dist-3] median active exp 512, avg 512.3
c [simplification-3] removed 927 variables 1.5% (61328 remain 25%)
c [simplification-3] removed 1674 irredundant clauses 0.5% (368736 remain 49%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3001 (hard 13001)
c [simplification-3] new binary interval 1000
c 
c [simplification-4] limit 3001 conflicts (hard 13001) hit after 3001 conflicts
c [decomp-7] removed 8 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 15600 literals 13%
c [treelook-2] scheduling used 162003 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 591571 steps
c [treelook-2] 15598 literals remain 13%
c [treelook-2] 11869 variables remain to probed next time 19%
c [unhide-3] limit 102431 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 180 tauts, 0 hbrs, 2473 literals
c [elim-4] 6843 variables 11% will be scheduled this time
c [elim-4] scheduled 6843 variables 11%
c [elim-4] boosting limit by 20
c [elim-4] limit of 409724060 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 1556 variables 3% in round 1 in 109384942 steps
c [elim-4-1] backward subsumption/strengthening limit 109384900
c [elim-4-1-1] backward checking 3312 touched variables 5%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 890 and strengthened 804 clauses in 27146106 steps
c [elim-4-1] rescheduled 1251 variables 2% by backward subsumption
c [elim-4-2] eliminated 3 variables 0% in round 2 in 5844346 steps
c [elim-4-2] backward subsumption/strengthening limit 5844300
c [elim-4-2-1] backward checking 37 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 5 clauses in 997888 steps
c [elim-4-2] rescheduled 10 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 805120 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 1559 = 23% variables out of 6843 scheduled
c [phase-count-4] 317404 negative 87.0% of 364965 except 47561 13.0%
c [phase-count-4] 295084 positive 80.9% of 364965 except 69881 19.1%
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-4] sorted 36081 enqueued variables after 3001 conflicts
c [score-dist-4] active 23680 (40%), one 0 (0%), zero 36081 (60%)
c [score-dist-4] max exp 513, different 11 (2%)
c [score-dist-4] median active exp 513, avg 512.6
c [simplification-4] removed 1567 variables 2.6% (59761 remain 24%)
c [simplification-4] removed 3770 irredundant clauses 1.0% (364965 remain 49%)
c [simplification-4] maximum reduction of 3% = max (3%, 1%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 5000
c [simplification-4] penalized conflict interval 5000 = 1 * 5000
c [simplification-4] hard conflict limit 18001 (soft 8001 + delta 10000)
c [simplification-4] new conflict limit 8001 (hard 18001)
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   20.5   59760   364964      4974    3146    285 56295   45   167   46  27%     60  161   45    4 1037%
c i   22.9   59759   364963      7209    4652    383 56700   44   192   46  23%     25  180   51    6  922%
c 
c [simplification-5] limit 8001 conflicts (hard 18001) hit after 8015 conflicts
c [quatres-1] found 55255 quaternary clauses 51% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 45 single-self-subsuming ternary resolvents
c [quatres-1-2] added 2567 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 59758 free variables schedulable
c [ternres-1] 64570 ternary resolvents (1 bin, 64569 trn)
c [ternres-1] 11123 variables remain 19% (48635 retained 81%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 14176 xors of average arity 3.0
c [gauss-1] connected 42478 occurrences of 16995 variables (average 2.5)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-8] removed 75 variables
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 68 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 59683 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 924 blocked clauses
c [block-1] 924 < 1/100 * 364400 = 3644 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 30000033 steps
c [cce-1-1] allowing another 15000016 steps for small clauses
c [cce-1-1] scheduling 238134 clauses = 72677 binary + 165457 ternary
c [cce-1-1] tried to eliminate 512 small clauses 0%
c [cce-1-1] eliminated 2 ternary clauses 0%
c [cce-1-1] eliminated 2 small clauses 0%
c [cce-1-1] eliminated 2 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3 covered clauses in round 1
c [cce-1] eliminated 3 covered clauses in TOTAL during 1 rounds
c [cce-1] 3 < 1/100 * 363476 = 3634 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 59683 variables 100%
c [elim-5] limit of 52360047 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 473 not tried 1% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 276 = 0% variables out of 59683 scheduled
c [elim-5] 276 < 1/100 * 59683 = 596 considered unsuccessful
c [bca-1] limit of 10000000 steps and 727138 added (scaled 2)
c [bca-1] 99534 out of 118816 literals actually usable 84%
c [bca-1] added 5168 blocked clauses in 256461 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 23017 pos 38.7% + 36390 neg 61.3% = 59407 sched 100.0% ret 0
c [sweep-1-1] 1161384 steps 17 queries 18951.24 avg class size
c [sweep-1-1] 96 decisions 14 SAT calls 97.21 avg env size
c [sweep-1-1] 59356 variables remain 100% (51 retained 0%)
c [decomp-9] removed 2 variables
c [sweep-1-1] removed 2 vars (0 failed, 2 eqs, 5 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 2 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-5] 315900 negative 86.9% of 363315 except 47415 13.1%
c [phase-count-5] 294097 positive 80.9% of 363315 except 69218 19.1%
c [phase-5] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-5] sorted 27506 enqueued variables after 8015 conflicts
c [score-dist-5] active 31899 (54%), one 0 (0%), zero 27506 (46%)
c [score-dist-5] max exp 514, different 10 (2%)
c [score-dist-5] median active exp 514, avg 513.6
c [simplification-5] removed 353 variables 0.6% (59405 remain 24%)
c [simplification-5] removed 1648 irredundant clauses 0.5% (363315 remain 49%)
c [simplification-5] maximum reduction of 1% = max (1%, 0%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 15000
c [simplification-5] penalized conflict interval 15000 = 1 * 15000
c [simplification-5] hard conflict limit 33015 (soft 23015 + delta 10000)
c [simplification-5] new conflict limit 23015 (hard 33015)
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   31.5   59404   363315      9039    8085  65142 66250   56   225   52  25%     16  208   77    7 1048%
c i   40.9   59402   363315     16646   13615  65309 67192   69   260   55  27%     94  219   64   14  456%
c 
c [simplification-6] limit of 1840 binary hit after 1840 binaries
c [quatres-2] found 58021 quaternary clauses 52% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 15 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1992 quaternary resolvents
c [ternres-2] limit 7155865 with penalty 0 = 0 + 0
c [ternres-2] 11113 schedulable variables 19%
c [ternres-2] 37020 ternary resolvents (10 bin, 37010 trn)
c [ternres-2] 1958 variables remain 3% (57444 retained 97%)
c [card-3] limit 894483 penalty 2 = 2 + 0
c [card-3] no at-most-one constraint found
c [card-3] no at-most-two constraint found
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 11124 xors of average arity 3.0
c [gauss-2] connected 33327 occurrences of 13294 variables (average 2.5)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-10] removed 96 variables
c [basicprobe-2] limit 17889664 penalty 1 = 1 + 0
c [basicprobe-2-0] 29644 probes remain 50% after last round
c [basicprobe-2-0] removed 0 variables, found 131361 hbrs
c [bate-1] eliminated 15 asymmetric tautologies during probing
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 7 transitive binary clauses
c [bca-2] limit of 10000000 steps and 728490 added (scaled 2)
c [bca-2] 83640 out of 118614 literals actually usable 71%
c [bca-2] added 0 blocked clauses in 219890 steps
c [sweep-2] limit 2146759 penalty 0 = 0 + 0
c [sweep-2-1] 26508 pos 44.7% + 32749 neg 55.3% = 59257 sched 99.9% ret 49
c [sweep-2-1] 6634565 steps 18 queries 11938.72 avg class size
c [sweep-2-1] 521 decisions 16 SAT calls 188.88 avg env size
c [sweep-2-1] 59141 variables remain 100% (165 retained 0%)
c [decomp-11] removed 2 variables
c [sweep-2-1] removed 2 vars (0 failed, 1 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 2 vars in TOTAL (1 rounds, 17 queries)
c [phase-count-6] 315284 negative 86.9% of 362697 except 47413 13.1%
c [phase-count-6] 293809 positive 81.0% of 362697 except 68888 19.0%
c [phase-6] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-6] sorted 14258 enqueued variables after 19658 conflicts
c [score-dist-6] active 45046 (76%), one 0 (0%), zero 14258 (24%)
c [score-dist-6] max exp 516, different 12 (2%)
c [score-dist-6] median active exp 516, avg 515.3
c [simplification-6] removed 98 variables 0.2% (59304 remain 24%)
c [simplification-6] removed 618 irredundant clauses 0.2% (362697 remain 49%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] forced so keeping old conflict interval 15000
c [simplification-6] conflict limit remains at 23015 (hard 33015)
c [simplification-6] new binary interval 10000
c 
c [simplification-7] limit 23015 conflicts (hard 33015) hit after 23015 conflicts
c [quatres-3] found 60052 quaternary clauses 52% in total
c [quatres-3-1] removed 4 duplicate quaternary clauses
c [quatres-3-2] added 36 quaternary resolvents
c [ternres-3] limit 8953414 with penalty 0 = 0 + 0
c [ternres-3] 1952 schedulable variables 3%
c [ternres-3] 12247 ternary resolvents (12 bin, 12235 trn)
c [ternres-3] 1 variables remain 0% (59303 retained 100%)
c [decomp-12] removed 9 variables
c [unhide-4] limit 447670 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 2 failed, 2059 tauts, 0 hbrs, 22575 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 68 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 59293 variables 100%
c [block-2] limit of 44767070 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 129 blocked clauses
c [block-2] 129 < 1/100 * 362672 = 3626 considered unsuccessful
c [cce-2] limit of 22383535 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 8 (25%) 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 7 (14%) of length 109
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 108
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 107
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 106
c [cce-2-1] eliminated 1 clauses out of 6 (17%) 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 7 (14%) of length 102
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 101
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 100
c [cce-2-1] eliminated 1 clauses out of 6 (17%) 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 7 (14%) of length 96
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 95
c [cce-2-1] eliminated 1 clauses out of 7 (14%) 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 8 (12%) 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 7 (14%) of length 89
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 88
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 87
c [cce-2-1] eliminated 1 clauses out of 11 (9%) of length 86
c [cce-2-1] eliminated 1 clauses out of 9 (11%) of length 85
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 84
c [cce-2-1] eliminated 1 clauses out of 10 (10%) of length 83
c [cce-2-1] eliminated 1 clauses out of 13 (8%) of length 82
c [cce-2-1] eliminated 1 clauses out of 11 (9%) of length 81
c [cce-2-1] eliminated 1 clauses out of 10 (10%) of length 80
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 38 large clauses in 22386488 steps
c [cce-2-1] allowing another 11193244 steps for small clauses
c [cce-2-1] scheduling 236578 clauses = 72280 binary + 164298 ternary
c [cce-2-1] tried to eliminate 219 small clauses 0%
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 38 covered clauses in round 1
c [cce-2] eliminated 38 covered clauses in TOTAL during 1 rounds
c [cce-2] 38 < 1/100 * 362286 = 3622 considered unsuccessful
c [elim-6] 471 variables 1% will be scheduled this time
c [elim-6] scheduled 471 variables 1%
c [elim-6] limit of 89534141 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 53447074 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 471 scheduled
c [sweep-3] limit 2686024 penalty 0 = 0 + 0
c [sweep-3-1] 36016 pos 60.9% + 23113 neg 39.1% = 59129 sched 99.7% ret 164
c [sweep-3-1] 2818640 steps 19 queries 16722.79 avg class size
c [sweep-3-1] 543 decisions 17 SAT calls 65.35 avg env size
c [sweep-3-1] 58992 variables remain 99% (301 retained 1%)
c [decomp-13] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1 vars in TOTAL (1 rounds, 18 queries)
c [sort-queue-7] sorted 12150 enqueued variables after 23015 conflicts
c [score-dist-7] active 47142 (80%), one 0 (0%), zero 12150 (20%)
c [score-dist-7] max exp 516, different 11 (2%)
c [score-dist-7] median active exp 516, avg 515.5
c [simplification-7] removed 12 variables 0.0% (59292 remain 24%)
c [simplification-7] removed 464 irredundant clauses 0.1% (362233 remain 49%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20000
c [simplification-7] new conflict interval 35000
c [simplification-7] penalized conflict interval 35000 = 1 * 35000
c [simplification-7] hard conflict limit 75515 (soft 58015 + delta 17500)
c [simplification-7] new conflict limit 58015 (hard 75515)
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   79.7   59291   362233     35707   30576 113559 238058   91   252   70  36%    239  158  111   32  348%
c i   79.7   59290   362233     35708   30576 113559 238058   91   252   70  36%    238  158  111   32  347%
c i   88.9   59289   362233     41006   35275 113643 238144   84   287   80  29%     22  179   84   36  233%
c i   98.5   59287   362233     46434   40235 113737 238183   84   308   82  27%     23  185   76   40  190%
c i   98.5   59286   362233     46435   40235 113737 238183   84   308   82  27%     23  185   75   40  190%
c i   98.5   59284   362233     46436   40235 113737 238183   84   308   82  27%     23  185   75   40  189%
c i   98.5   59280   362233     46437   40235 113737 238183   84   308   82  27%     23  185   75   40  188%
c 
c [simplification-8] limit 58055 conflicts (hard 75515) hit after 58056 conflicts
c [quatres-4] found 60475 quaternary clauses 52% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 8 single-self-subsuming ternary resolvents
c [quatres-4-2] added 22 quaternary resolvents
c [ternres-4] limit 26681135 with penalty 0 = 0 + 0
c [ternres-4] 1 schedulable variables 0%
c [ternres-4] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 2668113 penalty 1 = 1 + 0
c [gauss-3] extracted 11259 xors of average arity 3.0
c [gauss-3] connected 33659 occurrences of 12392 variables (average 2.7)
c [gauss-3] limit 2668113 penalty 1 = 1 + 0
c [gauss-3] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-14] removed 246 variables
c [simpleprobe-3] 12212 schedulable variables 21%
c [simpleprobe-3] limit 53362270 penalty 1 = 1 + 0
c [decomp-15] removed 1 variables
c [simpleprobe-3] 7533 variables remain 13% (51466 retained 87%)
c [simpleprobe-3] removed 1 variables, found 22916 hbrs, 0 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 70 transitive binary clauses
c [bca-3] limit of 10000000 steps and 719928 added (scaled 2)
c [bca-3] 63884 out of 118000 literals actually usable 54%
c [bca-3] added 117 blocked clauses in 200642 steps
c [sweep-4] limit 8004340 penalty 0 = 0 + 0
c [sweep-4-1] 24096 pos 41.0% + 34622 neg 59.0% = 58718 sched 99.5% ret 281
c [sweep-4-1] 9306647 steps 51 queries 4698.45 avg class size
c [sweep-4-1] 1586 decisions 42 SAT calls 310.88 avg env size
c [sweep-4-1] 58165 variables remain 99% (834 retained 1%)
c [decomp-16] removed 7 variables
c [sweep-4-1] removed 7 vars (0 failed, 8 eqs, 14 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 7 vars in TOTAL (1 rounds, 50 queries)
c [sort-queue-8] sorted 6648 enqueued variables after 58056 conflicts
c [score-dist-8] active 52344 (89%), one 0 (0%), zero 6648 (11%)
c [score-dist-8] max exp 517, different 11 (2%)
c [score-dist-8] median active exp 517, avg 516.7
c [simplification-8] removed 254 variables 0.4% (58992 remain 24%)
c [simplification-8] removed 3825 irredundant clauses 1.1% (358408 remain 48%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 17500 = 35000 / 2
c [simplification-8] new conflict interval 52500
c [simplification-8] penalized conflict interval 52500 = 1 * 52500
c [simplification-8] hard conflict limit 136806 (soft 110556 + delta 26250)
c [simplification-8] new conflict limit 110556 (hard 136806)
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  118.2   58991   358408     59098   50668 112585 283027   79   273   96  29%    128  122  110   46  239%
c i  118.2   58990   358408     59099   50668 112585 283027   79   273   96  29%    128  122  110   46  238%
c i  118.3   58988   358408     59110   50675 112587 283028   79   273   96  29%    126  121  105   46  228%
c i  125.4   58982   358408     64396   55498 112681 283071   80   293   96  27%     13  131   75   49  153%
c -  130.4   58976   358408     70422   22389 112745 283104   73   226   61  32%     25   60  143   50  288%
c i  147.7   58975   358408     85702   35553 112923 283161   79   235   70  33%    232   53  122   56  218%
c 
c [simplification-9] limit 110566 conflicts (hard 136806) hit after 110566 conflicts
c [quatres-5] found 61327 quaternary clauses 51% in total
c [quatres-5-2] added 14 single-self-subsuming ternary resolvents
c [quatres-5-2] added 44 quaternary resolvents
c [ternres-5] limit 42016579 with penalty 0 = 0 + 0
c [ternres-5] all 58974 free variables schedulable
c [ternres-5] 26726 ternary resolvents (29 bin, 26697 trn)
c [ternres-5] 3812 variables remain 6% (55162 retained 94%)
c [gauss-4] limit 8403315 penalty 0 = 0 + 0
c [gauss-4] extracted 27780 xors of average arity 3.0
c [gauss-4] connected 82958 occurrences of 14729 variables (average 5.6)
c [gauss-4] limit 8403315 penalty 0 = 0 + 0
c [decomp-17] removed 273 variables
c [gauss-4] exported 0 unary, 3 binary and 1 ternary equations
c [unhide-5] limit 2100828 with penalty 2 = 1 + 1
c [unhide-5-5] 0 units, 0 failed, 1208 tauts, 0 hbrs, 158039 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 64 transitive binary clauses
c [bca-4] limit of 10000000 steps and 715588 added (scaled 2)
c [bca-4] 67326 out of 117404 literals actually usable 57%
c [bca-4] added 61 blocked clauses in 218211 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 126049730 penalty 0 = 0 + 0
c [sweep-5-1] 22745 pos 39.3% + 35146 neg 60.7% = 57891 sched 98.6% ret 810
c [sweep-5-1] 127970458 steps 680 queries 524.20 avg class size
c [sweep-5-1] 13355 decisions 577 SAT calls 86.72 avg env size
c [sweep-5-1] 32419 variables remain 55% (26282 retained 45%)
c [decomp-19] removed 148 variables
c [sweep-5-1] removed 148 vars (0 failed, 129 eqs, 215 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 148 vars in TOTAL (1 rounds, 679 queries)
c [sort-queue-9] sorted 4454 enqueued variables after 110566 conflicts
c [score-dist-9] active 54099 (92%), one 0 (0%), zero 4454 (8%)
c [score-dist-9] max exp 518, different 10 (2%)
c [score-dist-9] median active exp 518, avg 517.6
c [simplification-9] removed 421 variables 0.7% (58553 remain 23%)
c [simplification-9] removed 2485 irredundant clauses 0.7% (355923 remain 48%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 26250 = 52500 / 2
c [simplification-9] new conflict interval 78750
c [simplification-9] penalized conflict interval 78750 = 1 * 78750
c [simplification-9] hard conflict limit 228691 (soft 189316 + delta 39375)
c [simplification-9] new conflict limit 189316 (hard 228691)
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 -  190.8   58553   355922    120816   33007 135888 565011   76   261   69  29%    363   62   41   58   71%
c i  220.7   58552   355922    151083   60662 136268 565117   85   255   93  33%    607   68   94   55  170%
c -  239.7   58552   355922    166528   40446 136448 565213   55   184   70  30%   -125   -8   24   57   43%
c i  247.7   58551   355922    188468   60555 136713 565290   46   112   85  41%    202  -57   85   51  167%
c i  259.9   58550   355922    204271   74823 136892 565345   55   187   92  29%    -88   14   83   50  167%
c -  268.5   58550   355922    210394   47949 136940 565367   76   246   71  31%   -217   67   95   53  179%
c 
c [simplification-10] limit 189316 conflicts (hard 228691) hit after 223017 conflicts
c [quatres-6] found 63094 quaternary clauses 47% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-1] added 4 double-self-subsuming ternary resolvents
c [quatres-6-2] added 23 single-self-subsuming ternary resolvents
c [quatres-6-2] added 71 quaternary resolvents
c [ternres-6] limit 77773330 with penalty 0 = 0 + 0
c [ternres-6] 3758 schedulable variables 6%
c [ternres-6] 9949 ternary resolvents (245 bin, 9704 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 4860833 penalty 3 = 3 + 0
c [card-4] found 36 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 4860833 for elimination
c [card-4] 36 out of 36 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 15554666 penalty 0 = 0 + 0
c [gauss-5] extracted 30816 xors of average arity 3.0
c [gauss-5] connected 92250 occurrences of 15889 variables (average 5.8)
c [gauss-5] limit 15554666 penalty 0 = 0 + 0
c [decomp-20] removed 121 variables
c [gauss-5] exported 0 unary, 5 binary and 6 ternary equations
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 104 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 58429 variables 100%
c [block-3] limit of 194433326 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 625 blocked clauses
c [block-3] 625 < 1/100 * 355547 = 3555 considered unsuccessful
c [cce-3] limit of 97216663 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 3 clauses out of 5 (60%) of length 129
c [cce-3-1] eliminated 1 clauses out of 9 (11%) of length 79
c [cce-3-1] eliminated 1 clauses out of 13 (8%) of length 78
c [cce-3-1] eliminated 1 clauses out of 17 (6%) of length 77
c [cce-3-1] eliminated 1 clauses out of 26 (4%) of length 76
c [cce-3-1] eliminated 1 clauses out of 26 (4%) of length 75
c [cce-3-1] eliminated 1 clauses out of 34 (3%) of length 74
c [cce-3-1] eliminated 1 clauses out of 41 (2%) of length 73
c [cce-3-1] eliminated 1 clauses out of 45 (2%) of length 72
c [cce-3-1] eliminated 1 clauses out of 51 (2%) of length 71
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 12 large clauses in 97217834 steps
c [cce-3-1] allowing another 48608917 steps for small clauses
c [cce-3-1] scheduling 87576 clauses = 68792 binary + 18784 ternary
c [cce-3-1] tried to eliminate 1288 small clauses 1%
c [cce-3-1] eliminated 2 binary clauses 0%
c [cce-3-1] eliminated 14 ternary clauses 0%
c [cce-3-1] eliminated 16 small clauses 0%
c [cce-3-1] eliminated 16 small clauses in 97216670 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 28 covered clauses in round 1
c [cce-3] eliminated 28 covered clauses in TOTAL during 1 rounds
c [cce-3] 28 < 1/100 * 354922 = 3549 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 58429 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 259 variables 0% in round 1 in 134962997 steps
c [elim-7-1] backward subsumption/strengthening limit 65037003
c [elim-7-1-1] backward checking 2026 touched variables 3%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 2 and strengthened 2 clauses in 9837416 steps
c [elim-7-1] rescheduled 44 variables 0% by backward subsumption
c [elim-7-2] eliminated 1 variables 0% in round 2 in 663067 steps
c [elim-7-2] backward subsumption/strengthening limit 663000
c [elim-7-2-1] backward checking 7 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 140588 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 261 = 0% variables out of 58429 scheduled
c [elim-7] 261 < 1/100 * 58429 = 584 considered unsuccessful
c [bca-5] limit of 10000000 steps and 711869 added (scaled 2)
c [bca-5] 64184 out of 116338 literals actually usable 55%
c [bca-5] added 105 blocked clauses in 213300 steps
c [sweep-6] limit 23331999 penalty 0 = 0 + 0
c [sweep-6-1] 18403 pos 57.3% + 13735 neg 42.7% = 32138 sched 55.3% ret 26030
c [sweep-6-1] 23483040 steps 155 queries 1121.52 avg class size
c [sweep-6-1] 3612 decisions 137 SAT calls 141.76 avg env size
c [sweep-6-1] 30273 variables remain 52% (27895 retained 48%)
c [decomp-22] removed 39 variables
c [sweep-6-1] removed 39 vars (0 failed, 21 eqs, 37 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 39 vars in TOTAL (1 rounds, 154 queries)
c [sort-queue-10] sorted 2796 enqueued variables after 223017 conflicts
c [score-dist-10] active 55333 (95%), one 0 (0%), zero 2796 (5%)
c [score-dist-10] max exp 519, different 11 (2%)
c [score-dist-10] median active exp 519, avg 518.7
c [simplification-10] removed 421 variables 0.7% (58129 remain 23%)
c [simplification-10] removed 1654 irredundant clauses 0.5% (354268 remain 47%)
c [simplification-10] maximum reduction of 1% = max (1%, 0%)
c [simplification-10] geometric conflict interval increment 39375 = 78750 / 2
c [simplification-10] new conflict interval 118125
c [simplification-10] penalized conflict interval 118125 = 1 * 118125
c [simplification-10] hard conflict limit 400204 (soft 341142 + delta 59062)
c [simplification-10] new conflict limit 341142 (hard 400204)
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 -  318.7   58129   354268    255339   51591 145266 590930   50   271   71  18%    399   68   41   55   74%
c i  328.4   58128   354268    270475   65337 145432 590984   44   135   79  33%    528  -71   74   52  142%
c i  330.9   58126   354268    271808   66144 145460 590995   52   149   81  35%   -206  -55   68   53  128%
c i  332.2   58125   354268    272525   66648 145470 591003   56   152   81  37%   -344  -52   80   53  152%
c i  332.2   58124   354268    272526   66648 145470 591003   56   152   81  37%   -344  -52   80   53  151%
c i  350.9   58114   354268    294142   85870 145715 591061   57   160   95  36%    -77  -30   91   52  176%
c i  359.8   58113   354268    299860   91193 145759 591082   75   252  100  30%   -299   59   69   54  127%
c -  359.9   58108   354268    299880   56037 145759 591082   75   253   72  30%   -300   60   65   54  119%
c 
c [simplification-11] limit of 4401 ternary hit after 4742 ternaries
c [quatres-7] found 64851 quaternary clauses 45% in total
c [quatres-7-2] added 17 single-self-subsuming ternary resolvents
c [quatres-7-2] added 115 quaternary resolvents
c [ternres-7] limit 107658363 with penalty 0 = 0 + 0
c [ternres-7] all 58108 free variables schedulable
c [ternres-7] 5499 ternary resolvents (236 bin, 5263 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-6] limit 21531672 penalty 0 = 0 + 0
c [gauss-6] extracted 41282 xors of average arity 3.0
c [gauss-6] connected 122967 occurrences of 21731 variables (average 5.7)
c [gauss-6] limit 21531672 penalty 0 = 0 + 0
c [decomp-23] removed 426 variables
c [gauss-6] exported 0 unary, 60 binary and 20 ternary equations
c [treelook-3] limit 2691459 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 74812 literals 65%
c [treelook-3] scheduling used 2537382 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 2691459 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 3607256 steps
c [treelook-3] 74632 literals remain 65%
c [treelook-3] 10921 variables remain to probed next time 19%
c [decomp-25] removed 6 variables
c [treelook-3] removed 6 variables, found 2805 hbrs
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 123 transitive binary clauses
c [bca-6] limit of 10000000 steps and 706701 added (scaled 2)
c [bca-6] 55488 out of 115354 literals actually usable 48%
c [bca-6] added 82 blocked clauses in 210951 steps
c [sweep-7] limit 32297509 penalty 0 = 0 + 0
c [sweep-7-1] 15373 pos 51.5% + 14499 neg 48.5% = 29872 sched 51.8% ret 27804
c [sweep-7-1] 32303984 steps 78 queries 3434.74 avg class size
c [sweep-7-1] 1531 decisions 71 SAT calls 86.06 avg env size
c [sweep-7-1] 29074 variables remain 50% (28602 retained 50%)
c [decomp-26] removed 10 variables
c [sweep-7-1] removed 10 vars (0 failed, 7 eqs, 13 impls)
c [sweep-7] 10 < 1/1000 * 57676 = 57 considered unsuccessful
c [sweep-7] removed 10 vars in TOTAL (1 rounds, 77 queries)
c [sort-queue-11] sorted 1563 enqueued variables after 324297 conflicts
c [score-dist-11] active 56103 (97%), one 0 (0%), zero 1563 (3%)
c [score-dist-11] max exp 520, different 11 (2%)
c [score-dist-11] median active exp 520, avg 519.7
c [simplification-11] removed 442 variables 0.8% (57666 remain 23%)
c [simplification-11] removed 2550 irredundant clauses 0.7% (351718 remain 47%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] forced so keeping old conflict interval 118125
c [simplification-11] conflict limit remains at 341152 (hard 400204)
c [simplification-11] 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 i  390.3   57665   351718    331804   84948 147072 691433   29   238   96  12%    155   28   19   49   40%
c i  397.3   57664   351718    338162   90741 147156 691454   57   220   96  26%   -224   10  129   49  262%
c i  398.4   57663   351718    338724   90907 147158 691466   58   209   96  28%   -255   -1   74   49  149%
c i  402.6   57662   351718    343844   95588 147188 691473   51   247  101  20%   -221   37   62   49  127%
c -  407.7   57662   351718    346741   62295 147218 691486   83   268   75  31%   -241   55  151   52  293%
c 
c [simplification-12] limit 341152 conflicts (hard 400204) hit after 366782 conflicts
c [quatres-8] found 65587 quaternary clauses 44% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 17 single-self-subsuming ternary resolvents
c [quatres-8-2] added 32 quaternary resolvents
c [ternres-8] limit 121708216 with penalty 0 = 0 + 0
c [ternres-8] all 57662 free variables schedulable
c [ternres-8] 3725 ternary resolvents (144 bin, 3581 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-7] limit 24341643 penalty 0 = 0 + 0
c [gauss-7] extracted 43818 xors of average arity 3.0
c [gauss-7] connected 131075 occurrences of 20584 variables (average 6.4)
c [gauss-7] limit 24341643 penalty 0 = 0 + 0
c [decomp-27] removed 157 variables
c [gauss-7] exported 0 unary, 9 binary and 10 ternary equations
c [unhide-6] limit 2500000 with penalty 3 = 2 + 1
c [unhide-6-6] 0 units, 4 failed, 39275 tauts, 0 hbrs, 114109 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 92 transitive binary clauses
c [bca-7] limit of 10000000 steps and 704838 added (scaled 2)
c [bca-7] 53823 out of 115010 literals actually usable 47%
c [bca-7] added 0 blocked clauses in 205942 steps
c [sort-queue-12] sorted 1403 enqueued variables after 366782 conflicts
c [score-dist-12] active 56101 (98%), one 0 (0%), zero 1403 (2%)
c [score-dist-12] max exp 520, different 11 (2%)
c [score-dist-12] median active exp 520, avg 519.8
c [simplification-12] removed 158 variables 0.3% (57504 remain 23%)
c [simplification-12] removed 932 irredundant clauses 0.3% (350786 remain 47%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 118125
c [simplification-12] new conflict interval 236250
c [simplification-12] penalized conflict interval 236250 = 1 * 236250
c [simplification-12] hard conflict limit 721157 (soft 603032 + delta 118125)
c [simplification-12] new conflict limit 603032 (hard 721157)
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 -  459.6   57504   350786    392003   66515 145929 624061   60   229   74  26%    388   29   64   55  116%
c -  510.1   57504   350786    439264   71402 146420 624264   68   215   76  32%    715   13   50   55   92%
c i  513.2   57503   350786    442267   74083 146475 624287   68   221   82  31%    728   18  100   55  182%
c i  513.3   57502   350786    442282   74085 146477 624288   68   220   82  31%    706   17   98   55  177%
c i  513.3   57501   350786    442283   74085 146477 624288   68   220   82  31%    705   17   97   55  177%
c i  514.5   57500   350786    443003   74762 146482 624292   72   232   82  31%    -52   28   98   55  177%
c i  528.9   57499   350786    460522   90911 146664 624330   51   222   91  23%   -391   16   67   52  129%
c -  557.7   57499   350786    487045   77298 146940 624417   67   235   76  29%   -106   28   61   53  115%
c i  570.7   57498   350786    497732   87280 147007 624438   60   241   86  25%     64   26   40   54   74%
c i  589.5   57497   350786    524023  111579 147293 624516   53   197  101  27%    -14   -2  103   50  208%
c -  604.1   57496   350786    533670   81507 147396 624554   73   233   75  31%   -232   30   75   54  139%
c i  636.9   57495   350786    572660  117724 147746 624652   56   179   99  32%    331  -19  124   49  253%
c i  644.0   57494   350786    576518  121184 147782 624669   80   228  107  35%   -339   30   94   52  181%
c -  650.4   57493   350786    582433   87331 147832 624680   50   191   77  26%   -294  -10   60   51  118%
c i  650.8   57492   350786    582641   87436 147837 624691   52   191   83  27%   -290  -11   76   51  149%
c i  663.9   57491   350786    594589   98438 147957 624736   51   207   89  25%   -152    3  102   51  201%
c i  686.0   57475   350786    611038  113005 148183 624790   47   173   99  27%    -38  -40   66   54  123%
c i  697.0   57474   350786    622491  123481 148298 624834   51   194  104  26%    -87  -29   84   53  158%
c -  710.3   57474   350786    631825   91043 148372 624859   78   211   77  37%    -97  -10   67   57  118%
c 
c [simplification-13] limit 603042 conflicts (hard 721157) hit after 647093 conflicts
c [quatres-9] found 69034 quaternary clauses 40% in total
c [quatres-9-1] removed 3 duplicate quaternary clauses
c [quatres-9-2] added 38 single-self-subsuming ternary resolvents
c [quatres-9-2] added 235 quaternary resolvents
c [ternres-9] limit 200000000 with penalty 0 = 0 + 0
c [ternres-9] all 57474 free variables schedulable
c [ternres-9] 3706 ternary resolvents (347 bin, 3359 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-8] limit 43109628 penalty 0 = 0 + 0
c [gauss-8] extracted 91109 xors of average arity 2.9
c [gauss-8] connected 268707 occurrences of 22097 variables (average 12.2)
c [gauss-8] limit 43109628 penalty 0 = 0 + 0
c [decomp-29] removed 1150 variables
c [gauss-8] exported 0 unary, 300 binary and 178 ternary equations
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 52 transitive binary clauses
c [sweep-8] limit 32332221 penalty 1 = 1 + 0
c [sweep-8-1] 12644 pos 45.3% + 15295 neg 54.7% = 27939 sched 49.6% ret 28385
c [sweep-8-1] 33644835 steps 128 queries 863.88 avg class size
c [sweep-8-1] 2709 decisions 114 SAT calls 76.07 avg env size
c [sweep-8-1] 25797 variables remain 46% (30526 retained 54%)
c [decomp-31] removed 46 variables
c [sweep-8-1] removed 46 vars (0 failed, 16 eqs, 20 impls)
c [sweep-8] 46 < 1/1000 * 56324 = 56 considered unsuccessful
c [sweep-8] removed 46 vars in TOTAL (1 rounds, 127 queries)
c [sort-queue-13] sorted 356 enqueued variables after 647093 conflicts
c [score-dist-13] active 55922 (99%), one 0 (0%), zero 356 (1%)
c [score-dist-13] max exp 521, different 12 (2%)
c [score-dist-13] median active exp 521, avg 520.9
c [simplification-13] removed 1196 variables 2.1% (56278 remain 23%)
c [simplification-13] removed 5537 irredundant clauses 1.6% (345249 remain 46%)
c [simplification-13] maximum reduction of 2% = max (2%, 2%)
c [simplification-13] geometric conflict interval increment 78750 = 236250 / 3
c [simplification-13] new conflict interval 315000
c [simplification-13] penalized conflict interval 315000 = 1 * 315000
c [simplification-13] hard conflict limit 1119593 (soft 962093 + delta 157500)
c [simplification-13] new conflict limit 962093 (hard 1119593)
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  741.6   56277   345249    667527  123452 140508 574628   44   128   96  35%    374  -59   89   49  182%
c -  758.9   56277   345249    682531   98380 140632 574660   64   192   75  33%    -62    6   94   51  186%
c i  766.7   56276   345249    692293  107564 140703 574671   36   138   85  26%     88  -48   32   49   67%
c i  772.5   56275   345249    697955  112533 140748 574699   52   167   88  31%   -193  -15   75   49  154%
c i  772.5   56274   345249    697956  112533 140748 574699   52   167   88  31%   -193  -15   75   49  153%
c i  772.5   56273   345249    697957  112533 140748 574699   52   167   88  31%   -193  -15   74   49  152%
c i  779.3   56271   345249    702826  117126 140789 574708   59   271   90  22%   -190   86   67   50  136%
c i  779.3   56270   345249    702827  117126 140789 574708   59   271   90  22%   -190   85   67   50  135%
c i  779.3   56266   345249    702849  117144 140790 574708   59   270   90  22%   -191   85   69   50  139%
c -  810.4   56265   345249    730839  101463 140993 574793   40   121   74  33%    181  -68   32   52   61%
c -  857.4   56265   345249    782425  108638 141521 574922   27    62   76  44%    640 -104   44   45   96%
c i  866.3   56264   345249    788845  114698 141568 574930   64   256   85  25%    676   88   82   47  174%
c i  879.8   56263   345249    798864  123795 141663 574952   87   244   91  36%   -446   67  103   51  202%
c i  879.8   56260   345249    798873  123801 141664 574953   87   244   91  36%   -447   66  100   51  195%
c i  910.8   56259   345249    823705  146631 141856 575020   56   192  105  29%    -91   -2   95   53  177%
c -  921.6   56257   345249    832702  110470 141930 575032   67   192   77  35%   -292   -3   44   56   80%
c i  930.0   56256   345249    846329  123172 142036 575056   32   122   88  26%    -45  -64   64   51  124%
c 
c [simplification-14] limit of 52 iterations hit after 55 iterations
c [quatres-10] found 71719 quaternary clauses 37% in total
c [quatres-10-1] removed 6 duplicate quaternary clauses
c [quatres-10-1] added 2 double-self-subsuming ternary resolvents
c [quatres-10-2] added 34 single-self-subsuming ternary resolvents
c [quatres-10-2] added 131 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 56256 free variables schedulable
c [ternres-10] 11461 ternary resolvents (448 bin, 11013 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-9] limit 50000000 penalty 0 = 0 + 0
c [gauss-9] extracted 89741 xors of average arity 3.0
c [gauss-9] connected 266289 occurrences of 21292 variables (average 12.5)
c [gauss-9] limit 50000000 penalty 0 = 0 + 0
c [decomp-32] removed 730 variables
c [gauss-9] exported 0 unary, 282 binary and 192 ternary equations
c [basicprobe-3] limit 100000000 penalty 2 = 2 + 0
c [basicprobe-3-0] 6322 probes remain 11% after last round
c [basicprobe-3-0] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 7 variables, found 238708 hbrs
c [bate-2] eliminated 167 asymmetric tautologies during probing
c [unhide-7] limit 5000000 with penalty 2 = 1 + 1
c [unhide-7-8] 0 units, 0 failed, 52577 tauts, 0 hbrs, 290002 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 92 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 55519 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 3073 blocked clauses
c [block-4] 3073 < 1/100 * 339685 = 3396 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 1771938411 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 49 (2%) of length 70
c [cce-4-1] eliminated 1 clauses out of 59 (2%) of length 69
c [cce-4-1] eliminated 1 clauses out of 54 (2%) of length 68
c [cce-4-1] eliminated 1 clauses out of 51 (2%) of length 67
c [cce-4-1] eliminated 1 clauses out of 72 (1%) of length 66
c [cce-4-1] eliminated 1 clauses out of 70 (1%) of length 65
c [cce-4-1] eliminated 2 clauses out of 74 (3%) of length 64
c [cce-4-1] eliminated 1 clauses out of 77 (1%) of length 63
c [cce-4-1] eliminated 1 clauses out of 87 (1%) of length 62
c [cce-4-1] eliminated 1 clauses out of 103 (1%) of length 61
c [cce-4-1] eliminated 1 clauses out of 92 (1%) of length 60
c [cce-4-1] eliminated 1 clauses out of 106 (1%) of length 59
c [cce-4-1] eliminated 1 clauses out of 109 (1%) of length 58
c [cce-4-1] eliminated 1 clauses out of 118 (1%) of length 57
c [cce-4-1] eliminated 1 clauses out of 136 (1%) of length 56
c [cce-4-1] eliminated 1 clauses out of 122 (1%) of length 55
c [cce-4-1] eliminated 1 clauses out of 149 (1%) of length 54
c [cce-4-1] eliminated 1 clauses out of 197 (1%) of length 53
c [cce-4-1] eliminated 1 clauses out of 183 (1%) of length 52
c [cce-4-1] eliminated 1 clauses out of 189 (1%) of length 51
c [cce-4-1] eliminated 1 clauses out of 228 (0%) of length 50
c [cce-4-1] eliminated 1 clauses out of 225 (0%) of length 49
c [cce-4-1] eliminated 1 clauses out of 261 (0%) of length 48
c [cce-4-1] eliminated 1 clauses out of 240 (0%) of length 47
c [cce-4-1] eliminated 2 clauses out of 260 (1%) of length 46
c [cce-4-1] eliminated 1 clauses out of 280 (0%) of length 45
c [cce-4-1] eliminated 2 clauses out of 351 (1%) of length 44
c [cce-4-1] eliminated 1 clauses out of 289 (0%) of length 43
c [cce-4-1] eliminated 1 clauses out of 360 (0%) of length 42
c [cce-4-1] eliminated 1 clauses out of 309 (0%) of length 41
c [cce-4-1] eliminated 2 clauses out of 313 (1%) of length 40
c [cce-4-1] eliminated 2 clauses out of 394 (1%) of length 39
c [cce-4-1] eliminated 2 clauses out of 303 (1%) of length 38
c [cce-4-1] eliminated 2 clauses out of 411 (0%) of length 37
c [cce-4-1] eliminated 2 clauses out of 440 (0%) of length 36
c [cce-4-1] eliminated 2 clauses out of 391 (1%) of length 35
c [cce-4-1] eliminated 1 clauses out of 444 (0%) of length 34
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 46 large clauses in 1771939406 steps
c [cce-4-1] allowing another 885969703 steps for small clauses
c [cce-4-1] scheduling 83080 clauses = 63086 binary + 19994 ternary
c [cce-4-1] tried to eliminate 28248 small clauses 34%
c [cce-4-1] eliminated 86 binary clauses 0%
c [cce-4-1] eliminated 376 ternary clauses 2%
c [cce-4-1] eliminated 462 small clauses 1%
c [cce-4-1] eliminated 462 small clauses in 1771938442 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 508 covered clauses in round 1
c [cce-4] eliminated 508 covered clauses in TOTAL during 1 rounds
c [cce-4] 508 < 1/100 * 336612 = 3366 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 55518 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2000000000 steps penalty 3 = 3 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 807 variables 1% in round 1 in 130960308 steps
c [elim-8-1] backward subsumption/strengthening limit 130960300
c [elim-8-1-1] backward checking 3134 touched variables 6%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 201 and strengthened 188 clauses in 16565765 steps
c [elim-8-1] rescheduled 681 variables 1% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 22179997 steps
c [elim-8-2] backward subsumption/strengthening limit 22179900
c [elim-8-2-1] backward checking 8 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 166131 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 808 = 1% variables out of 55518 scheduled
c [bca-8] limit of 10000000 steps and 673538 added (scaled 2)
c [bca-8] 35573 out of 109422 literals actually usable 33%
c [bca-8] added 138 blocked clauses in 218469 steps
c [sort-queue-14] sorted 160 enqueued variables after 868704 conflicts
c [score-dist-14] active 54550 (100%), one 0 (0%), zero 160 (0%)
c [score-dist-14] max exp 521, different 10 (2%)
c [score-dist-14] median active exp 521, avg 521.0
c [simplification-14] removed 1546 variables 2.7% (54710 remain 22%)
c [simplification-14] removed 10113 irredundant clauses 2.9% (335136 remain 45%)
c [simplification-14] maximum reduction of 3% = max (3%, 3%)
c [simplification-14] forced so keeping old conflict interval 315000
c [simplification-14] conflict limit remains at 962124 (hard 1119593)
c [simplification-14] new iteration interval 100
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  994.6   54709   335136    869889  136643 138254 676164   65   217  106  30%     27   24   73   55  133%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 182 basic ate = 17 trn 9% + 165 lrg 91% in 2 updates
c bcas: 8 count, 5671 added (20 skipped), 1743866 steps
c bkwd: tried 248383 clauses, 494914 lits, 1.99 lits/clause
c bkwd: checked 34742475 occs, 139.87 occs/clause, 70.20 occs/lit
c bkwd: subsumed 10 binary, 103 ternary, 980 large
c bkwd: strengthened 0 binary, 31 ternary (100% self), 968 large (0% self)
c blkd: 4 bces, 4751 removed, 10459190 resolutions, 26500106 steps
c blkd: 1470 blocking literals 0%, 1 pure
c bump: 859289 bumped seen, 166266186 lits 193.5 on average
c card: 4 count, 0 units, 0 am1, 19582656 steps
c card: 1 rescheduled, 3 eliminated, 1762 resolved, 332 subsumed
c card: 37 at-most-one constraints found, average size 3.00
c card: 37 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: 4 cces, 577 eliminated, 575 ate 100%, 2 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 2488144 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 67 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 33 decompositions, 3553 equivalent 1%
c deco: 20471 decision-only clauses 2%, 57% reduction
c decs: 12060072 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 190881 eliminated 77%, 0 pure 0%
c elms: 14 rounds, 1.8 rounds/bve
c elms: 170676 small 89%, 20204 large 11%
c elms: 353077 tried small, 170676 succeeded 48%, 182401 failed 52%
c elms: 2345 subsumed, 3682 strengthened, 163 blocked
c elms: 9127550 copies, 14493475 resolutions, 11432323 ipos
c elms: 8379269 subchks, 5802123 strchks
c gaus: 9 extractions, 361105 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 659 binary and 410 ternary equations
c gaus: 0 gc, 324756048 steps, 162378024 extr 50%, 170028939 elim 52%
c glue: 54.9 orig avg, 54.9 real avg, 5.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1037139 = 23618 simple 2% + 1013243 trn 98% + 278 lrg 0%, 1810 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 859289 clauses, 111.2 length
c lrnd: 95527522 lits = 122863236 orig - 27335714 removed 22%
c lrnd: 392849 uips 46%, 330497 flips 38%
c mins: 750852 mins 92%, 4159 bin 1%, 38001 size 5%
c mins: 306368540 poisoned searches, 31485643 hits, 10% hit rate
c mins: 366964741 used twice searches, 24208790 hits, 7% hit rate
c move: moved 3237, 515 bin 16%, 2722 trn 84%
c otfs: 16660 driving 62%, 10117 restarting 38%
c otfs: str 26777, 20027 red 75%, 6750 irr 25%
c otfs: str 26777, 0 bin 0%, 7127 trn 27%, 19650 lrg 73%
c otfs: sub 162, 157 red 97%, 5 irr 3%
c otfs: sub 162, 0 bin 0%, 68 trn 42%, 94 lrg 58%
c phas: 6 computed, 75579 set, 23991 pos (32%), 51588 neg (68%)
c prbs: 3 basic, 35276 probed, 7 failed, 0 lifted
c prbs: 3 simple, 476592 probed, 1 failed, 1 eqs
c prbs: 3 treelook, 195 probed, 0 failed, 0 lifted
c prom: 157874 locked 9% out of 1672491 tried
c prps: 1833706151 props, 151 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 10 count, 5245 quat, 211 self1, 9 self2, 33 dup
c queu: 14 sorted, 12060072 next (4604 steps 0.00)
c queu: 166775952 enq (5759091554 steps 34.53), 166266186 deq 100%
c redc: 10690 clauses 8%, 134452 tried 15%, 20 sat 0%
c redc: 14789 lits 1%, 1228140 tried 1%, 20 sat 0%
c redc: 475 times jump level reduced, 16.3 levels on average
c reds: 17 count, 51472.6 conflicts per reduce
c reds: 0 memlim 0%, 17 arith 100%
c reds: 493494 collected 77%, 147613 retired 23%
c rmbd: 24008 removed, 23828 red 99%
c rsts: 18297 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: 14 count, 10 confs 71%, 0 vars 0%
c simp: 1 its 7%, 2 bin 14%, 1 trns 7%
c subl: 859289 count (925805 tried 1.1), 52818 sub out of 844229 (6.3%)
c swps: 8 count, 8 rounds, 1138 queries (142.2/round)
c swps: 988 sat calls, 35 unsat (0.9% success rate)
c swps: 23953 decisions 24.2, 914 conflicts 0.9
c swps; 1760.3 avg class size, 104.0 avg environment size
c swps: 0 failed, 307 impls, 185 equivs
c swp0: 376 type 0 queries, 104 unsat (27.7%), 331 sat (88.0%)
c swp1: 762 type 1 queries, 341 unsat (44.8%), 622 sat (81.6%)
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: 25839027 calls to obtain time
c tops: 184 fixed 0%, 56 its, 15625.62 confs/it
c trds: 10 transitive reductions, 740 removed, 0 failed
c trds: 19115 nodes, 32823 edges, 20011836 steps
c trim: 1110915 words, 4.2 MB
c trnr: 10 count, 1472 bin, 173434 trn, 513931137 steps
c unhd: 7 count, 8 rounds, 29177222 steps
c unhd: 534 non-trivial sccs of average size 2.0
c unhd: 2 units, 2 bin, 0 trn, 0 lrg
c unhd: 19 failed, 19 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 97014 tauts, 422 bin 0%, 11350 trn 12%, 368 lrg 0%
c unhd: 97014 tauts, 84874 stamp 87%, 96554 red 100%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 588863 str, 2 bin 0%, 1535 trn 0%, 587326 lrg 100%, 579149 red 98%
c vars: 54709 remaining 22% and 194618 removed 78% out of 249327
c vars: 184 fixed 0%, 190881 eliminated 77%, 3553 equivalent 1%
c vsts: 28840292288 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 15.7 search visits per propagation, 32700.7 per conflict
c wchs: 1433734734 pushed, 30534560 enlarged, 116 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         849474        493494        147613     154238874       7984206        264664
c 
c  0 0        106815  13     10793   2         0   0  78643727  51   2861444  36     82095  31     3.6
c  1 5         39138   5     22085   4      8526   6  10172692   7    568874   7     17887   7     0.7
c  2 6         80914  10     51990  11     15145  10  17227833  11<   960630  12     30018  11     1.7
c  3 9         76401   9     50693  10     14017   9  13867290   9    749804   9<    23129   9     2.3
c  4 14        66527   8     46440   9     11784   8  10437446   7    619862   8     18662   7<    2.5
c  5 21        66668   8<    47950  10     11302   8   7958361   5    553467   7     17620   7     3.1
c  6 30        68921   8     49118  10<    11302   8   5016721   3    411693   5     15074   6     3.8
c  7 41        69258   8     48941  10     11302   8<  3459511   2    323247   4     13020   5     4.5
c  8 54        60239   7     41611   8     10305   7   2007324   1    210667   3      9832   4     3.2
c  9 69        45250   5     29459   6      8944   6   1880257   1    178241   2      7482   3     2.1
c 10 86        65675   8     40135   8     15357  10   2181478   1    228420   3      9655   4     3.5
c 11 126       63645   7     32596   7     17435  12    862395   1    196306   2     10236   4     4.8
c 12 230       39995   5     21676   4     12179   8    523805   0    121536   2      9954   4     9.6
c 13 534          28   0         7   0        15   0        34   0        15   0         0   0     0.0
c 
c avg                  5.5           6.0           6.7           1.9           3.0           3.7
c std                  3.7           3.2           3.5           2.6           3.3           3.7
c 
c  147.548  15% bump
c   20.797   2% elim
c   17.761   2% gauss
c   17.531   2% cce
c   16.520   2% sweep
c   11.174   1% probe
c    8.481   1% decide
c    6.693   1% unhide
c 
c   14.311 < 1% rest (below)
c 
c    4.504   0% block
c    3.793   0% ternres
c    2.225   0% bca
c    2.060   0% quatres
c    1.498   0% transred
c    0.232   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    4.848   0% preprocessing     4%
c  106.711  11% inprocessing     96%
c ==================================
c  111.558  11% simplifying
c  888.026  89% search
c ==================================
c  999.587 100% all
c 
c        875035 conflicts,         875.4 confs/sec
c         10258 ternaries,          85.3 confs/ternary
c          4540 binaries,          192.7 confs/binary
c            56 iterations,      15625.6 confs/iteration
c 
c            17 reductions,          0.0 redus/sec,  51472.6 confs/reduction
c         18297 restarts,           18.3 rests/sec,     47.8 confs/restart
c      12060072 decisions,       12065.1 decis/sec,     13.8 decis/conflict
c    1833706151 propagations,  1834463.7 props/sec,    152.0 props/decision
c 
c 999.6 seconds, 150.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
