c launch: /data/cnf/sc2014/app/dated-10-17-u.cnf.bz2
c host: atom28
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/dated-10-17-u.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/dated-10-17-u.cnf.bz2
c no embedded options
c found 'p cnf 229544 1070757' header
c read 229544 variables, 1070757 clauses, 2471122 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=0
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 219948 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] STATIC (--score=0)
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  219948  1051601         0       0      0     0    0     0   55   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 8728 at-most-one constraints of average size 5.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 8728 out of 8728 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 108248 variables
c [simpleprobe-1] all 121296 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 81213 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 81213 variables, found 15936 hbrs, 1687 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 2 units, 833 failed, 14136 tauts, 0 hbrs, 1203 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 38854 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 13368 variables 34% in round 1 in 18985445 steps
c [elim-1-1] backward subsumption/strengthening limit 1014555
c [elim-1-1-1] backward checking 23632 touched variables 61%
c [elim-1-1-1] incomplete backward checking 18135 remain 77%
c [elim-1-1] subsumed 90 and strengthened 273 clauses in 1014589 steps
c [elim-1] incomplete 684 not tried 2% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 13502 = 35% variables out of 38854 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 200172 negative 99.1% of 202008 except 1836 0.9%
c [phase-count-1] 173023 positive 85.7% of 202008 except 28985 14.3%
c [phase-count-1] less non-negative clauses 1836 than limit 20200 (10.0%)
c [phase-count-1] non-pos/non-neg = 28985/1836 = 15.79 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 25352 negative 100%
c [sort-queue-1] sorted 25352 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 25352 (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 151707 variables 85.7% (25352 remain 12%)
c [simplification-1] removed 849593 irredundant clauses 80.8% (202008 remain 19%)
c [simplification-1] maximum reduction of 86% = max (86%, 81%)
c [simplification-1] large reduction 86% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    2.4   25351   202008         1       0      0  9216    0     0   18   0%      0    0    0    0    0%
c i    2.4   25247   202008        89      62      5  9234    0     6   18   2%      0    6    2    0 21376%
c i    2.5   25244   202008       248     167     15  9267    0     8   19   3%      0    8    2    0 15784%
c i    2.5   25243   202008       261     177     16  9268    0     9   19   3%      0    9    2    0 15424%
c i    2.5   25242   202008       264     179     16  9268    0     9   19   3%      0    9    2    0 15391%
c i    2.5   25241   202008       279     191     16  9270    0     9   19   3%      0    9    2    0 14953%
c i    2.6   25240   202008       428     320     22  9280    1    21   19   3%      0   21    6    0 14490%
c i    2.9   25236   202008       782     602     46  9315    1    45   19   3%      1   44    9    0 9786%
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [decomp-3] removed 174 variables
c [simpleprobe-2] all 25178 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 501 variables
c [simpleprobe-2] 17033 variables remain 69% (7644 retained 31%)
c [simpleprobe-2] removed 501 variables, found 2399 hbrs, 163 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 32199 literals 65%
c [treelook-1] scheduling used 300427 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 518702 steps
c [treelook-1] 32187 literals remain 65%
c [treelook-1] 24007 variables remain to probed next time 97%
c [decomp-5] removed 1 variables
c [treelook-1] removed 2 variables, found 1109 hbrs
c [basicprobe-1] limit 1560568 based on 195071 irredundant clauses
c [basicprobe-1-0] 2834 probes remain 11% after last round
c [basicprobe-1-0] 11 units = 11 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 27 variables, found 6562 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 3 units, 724 failed, 5609 tauts, 0 hbrs, 2959 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 23980 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 973 variables 4% in round 1 in 15998932 steps
c [elim-2-1] backward subsumption/strengthening limit 4001068
c [elim-2-1-1] backward checking 4123 touched variables 17%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 70 and strengthened 101 clauses in 1049032 steps
c [elim-2-1] rescheduled 331 variables 1% by backward subsumption
c [elim-2-2] eliminated 50 variables 0% in round 2 in 216664 steps
c [elim-2-2] backward subsumption/strengthening limit 216600
c [elim-2-2-1] backward checking 271 touched variables 1%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 37 and strengthened 11 clauses in 109080 steps
c [elim-2-2] rescheduled 85 variables 0% by backward subsumption
c [elim-2-3] eliminated 15 variables 0% in round 3 in 49744 steps
c [elim-2-3] backward subsumption/strengthening limit 49700
c [elim-2-3-1] backward checking 68 touched variables 0%
c [elim-2-3-1] incomplete backward checking 21 remain 31%
c [elim-2-3] subsumed 26 and strengthened 5 clauses in 49711 steps
c [elim-2] incomplete 56 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 1126 = 5% variables out of 23980 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 22854 enqueued variables after 789 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 22854 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 2380 variables 9.4% (22854 remain 10%)
c [simplification-2] removed 18433 irredundant clauses 9.1% (183575 remain 17%)
c [simplification-2] maximum reduction of 9% = max (9%, 9%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1013 (hard 11000)
c [simplification-2] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    4.1   22853   183575       827     593     40 10067    1    47   17   3%      1   47    8    0 8937%
c 
c [simplification-3] limit 1013 conflicts (hard 11000) hit after 1013 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4985 at-most-one constraints of average size 3.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4985 out of 4985 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 51 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 31629 literals 69%
c [treelook-2] scheduling used 300330 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 523044 steps
c [treelook-2] 31619 literals remain 69%
c [treelook-2] 22083 variables remain to probed next time 97%
c [treelook-2] removed 3 variables, found 1421 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 265 failed, 9155 tauts, 0 hbrs, 641 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 22530 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 552 variables 2% in round 1 in 14621652 steps
c [elim-3-1] backward subsumption/strengthening limit 5378348
c [elim-3-1-1] backward checking 2746 touched variables 12%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 58 and strengthened 44 clauses in 660064 steps
c [elim-3-1] rescheduled 191 variables 1% by backward subsumption
c [elim-3-2] eliminated 34 variables 0% in round 2 in 167699 steps
c [elim-3-2] backward subsumption/strengthening limit 167600
c [elim-3-2-1] backward checking 161 touched variables 1%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 23 and strengthened 3 clauses in 102360 steps
c [elim-3-2] rescheduled 45 variables 0% by backward subsumption
c [elim-3-3] eliminated 12 variables 0% in round 3 in 68593 steps
c [elim-3-3] backward subsumption/strengthening limit 68500
c [elim-3-3-1] backward checking 52 touched variables 0%
c [elim-3-3-1] fully completed backward checking in 1 rounds
c [elim-3-3] subsumed 2 and strengthened 3 clauses in 39755 steps
c [elim-3] incomplete 13 not tried 0% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 645 = 3% variables out of 22530 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 21885 enqueued variables after 1013 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 21885 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 968 variables 4.2% (21885 remain 10%)
c [simplification-3] removed 13822 irredundant clauses 7.5% (169753 remain 16%)
c [simplification-3] maximum reduction of 8% = max (4%, 8%)
c [simplification-3] large reduction 8% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13013 (soft 3013 + delta 10000)
c [simplification-3] new conflict limit 3013 (hard 13013)
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    5.9   21884   169753      2378    1929     98 10007    5    99   17   5%     12   97   14    0 3655%
c i    6.1   21883   169753      2655    2170    103 10025    6   106   18   5%     10  103   16    0 3535%
c i    6.3   21882   169753      2877    2364    108 10039    7   112   18   6%      8  109   22    1 4227%
c 
c [simplification-4] limit 3013 conflicts (hard 13013) hit after 3014 conflicts
c [decomp-8] removed 54 variables
c [basicprobe-2] limit 4181357 penalty 0 = 0 + 0
c [basicprobe-2-0] 2862 probes remain 13% after last round
c [basicprobe-2-0] 36 units = 36 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 52 variables, found 10447 hbrs
c [unhide-4] limit 167254 with penalty 0 = 0 + 0
c [unhide-4-4] 8 units, 205 failed, 2307 tauts, 0 hbrs, 4958 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 21538 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 410 variables 2% in round 1 in 13964892 steps
c [elim-4-1] backward subsumption/strengthening limit 13964800
c [elim-4-1-1] backward checking 1636 touched variables 8%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 51 and strengthened 42 clauses in 366309 steps
c [elim-4-1] rescheduled 162 variables 1% by backward subsumption
c [elim-4-2] eliminated 55 variables 0% in round 2 in 122912 steps
c [elim-4-2] backward subsumption/strengthening limit 122900
c [elim-4-2-1] backward checking 225 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 40 and strengthened 2 clauses in 78690 steps
c [elim-4-2] rescheduled 79 variables 0% by backward subsumption
c [elim-4-3] eliminated 27 variables 0% in round 3 in 55363 steps
c [elim-4-3] backward subsumption/strengthening limit 55300
c [elim-4-3-1] backward checking 127 touched variables 1%
c [elim-4-3-1] incomplete backward checking 40 remain 31%
c [elim-4-3] subsumed 37 and strengthened 1 clauses in 55410 steps
c [elim-4] incomplete 53 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 546 = 3% variables out of 21538 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 20992 enqueued variables after 3014 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 20992 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 890 variables 4.1% (20992 remain 10%)
c [simplification-4] removed 5944 irredundant clauses 3.5% (163809 remain 16%)
c [simplification-4] maximum reduction of 4% = max (4%, 4%)
c [simplification-4] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-4] new conflict interval 4000
c [simplification-4] penalized conflict interval 4000 = 1 * 4000
c [simplification-4] hard conflict limit 17014 (soft 7014 + delta 10000)
c [simplification-4] new conflict limit 7014 (hard 17014)
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    7.3   20991   163809      3044    2441     90 13582    7   117   18   6%      7  114   21    1 3701%
c i    8.6   20990   163809      5144    4425    121 13626   13   151   18   9%     19  144   26    1 2092%
c i    8.7   20988   163809      5372    4628    126 13639   13   150   19   9%     16  143   17    1 1352%
c i    9.7   20987   163809      6914    6101    146 13661   16   173   20   9%     14  162   24    2 1363%
c 
c [simplification-5] limit 7014 conflicts (hard 17014) hit after 7014 conflicts
c [quatres-1] found 8704 quaternary clauses 68% in total
c [quatres-1-2] added 13 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 20987 free variables schedulable
c [ternres-1] 285 ternary resolvents (1 bin, 284 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 117 xors of average arity 2.8
c [gauss-1] connected 322 occurrences of 156 variables (average 2.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 40 variables
c [simpleprobe-3] 14458 schedulable variables 69%
c [simpleprobe-3] limit 7121447 penalty 0 = 0 + 0
c [decomp-10] removed 261 variables
c [simpleprobe-3] 2656 variables remain 13% (18030 retained 87%)
c [simpleprobe-3] removed 261 variables, found 9839 hbrs, 89 units
c [unhide-5] limit 356072 with penalty 0 = 0 + 0
c [unhide-5-5] 3 units, 96 failed, 4015 tauts, 0 hbrs, 19268 literals
c [transred-1] limit 1780361 with penalty 0 = 0 + 0
c [transred-1] removed 476 transitive binary clauses
c [transred-1] found 16 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 20588 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 526 blocked clauses
c [block-1] 526 < 1/100 * 159001 = 1590 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 8
c [cce-1-1] eliminated 5 clauses out of 75 (7%) of length 7
c [cce-1-1] eliminated 44 clauses out of 925 (5%) of length 6
c [cce-1-1] eliminated 273 clauses out of 1866 (15%) of length 5
c [cce-1-1] eliminated 1033 clauses out of 7921 (13%) of length 4
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1357 large clauses in 30000002 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 104798 clauses = 76609 binary + 28189 ternary
c [cce-1-1] tried to eliminate 702 small clauses 1%
c [cce-1-1] eliminated 197 binary clauses 0%
c [cce-1-1] eliminated 23 ternary clauses 0%
c [cce-1-1] eliminated 220 small clauses 0%
c [cce-1-1] eliminated 220 small clauses in 30000011 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1577 covered clauses in round 1
c [cce-1] eliminated 1577 covered clauses in TOTAL during 1 rounds
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 20583 variables 100%
c [elim-5] limit of 35607238 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 709 variables 3% in round 1 in 12970269 steps
c [elim-5-1] backward subsumption/strengthening limit 12970200
c [elim-5-1-1] backward checking 2945 touched variables 14%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 45 and strengthened 30 clauses in 558051 steps
c [elim-5-1] rescheduled 194 variables 1% by backward subsumption
c [elim-5-2] eliminated 25 variables 0% in round 2 in 105506 steps
c [elim-5-2] backward subsumption/strengthening limit 105500
c [elim-5-2-1] backward checking 184 touched variables 1%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 36 and strengthened 8 clauses in 58440 steps
c [elim-5-2] rescheduled 70 variables 0% by backward subsumption
c [elim-5-3] eliminated 19 variables 0% in round 3 in 37587 steps
c [elim-5-3] backward subsumption/strengthening limit 37500
c [elim-5-3-1] backward checking 97 touched variables 0%
c [elim-5-3-1] incomplete backward checking 0 remain 0%
c [elim-5-3] subsumed 12 and strengthened 5 clauses in 37501 steps
c [elim-5] incomplete 33 not tried 0% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 761 = 4% variables out of 20583 scheduled
c [bca-1] limit of 10000000 steps and 308208 added (scaled 2)
c [bca-1] 32385 out of 39646 literals actually usable 82%
c [bca-1] added 9 blocked clauses in 71499 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3366 pos 17.0% + 16456 neg 83.0% = 19822 sched 100.0% ret 0
c [sweep-1-1] 1047139 steps 19 queries 5465.58 avg class size
c [sweep-1-1] 207 decisions 14 SAT calls 39.86 avg env size
c [sweep-1-1] 18242 variables remain 100% (33 retained 0%)
c [decomp-11] removed 1777 variables
c [sweep-1-1] removed 1777 vars (0 failed, 4 eqs, 9 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1777 vars in TOTAL (1 rounds, 18 queries)
c [sort-queue-5] sorted 18045 enqueued variables after 7014 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 18045 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 2942 variables 14.0% (18045 remain 8%)
c [simplification-5] removed 27809 irredundant clauses 17.0% (136000 remain 13%)
c [simplification-5] maximum reduction of 17% = max (14%, 17%)
c [simplification-5] large reduction 17% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 19014 (soft 9014 + delta 10000)
c [simplification-5] new conflict limit 9014 (hard 19014)
c 
c  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   12.3   18044   136000      7362    5362    343 17573   17   178   17   9%     10  166   21    2 1085%
c i   12.7   18039   136000      8134    6105    356 17582   18   190   17  10%      8  176   26    2 1214%
c i   13.1   18038   136000      8787    6732    366 17589   20   192   18  10%      6  175   29    2 1217%
c 
c [simplification-6] limit 9014 conflicts (hard 19014) hit after 9015 conflicts
c [quatres-2] found 5884 quaternary clauses 65% in total
c [quatres-2-2] added 4 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 18038 free variables schedulable
c [ternres-2] 104 ternary resolvents (1 bin, 103 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2405 at-most-one constraints of average size 3.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2405 out of 2405 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 13 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 29170 literals 81%
c [treelook-3] scheduling used 300016 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 414806 steps
c [treelook-3] 29136 literals remain 81%
c [treelook-3] 17749 variables remain to probed next time 99%
c [decomp-13] removed 2 variables
c [treelook-3] removed 18 variables, found 3152 hbrs
c [unhide-6] limit 437742 with penalty 0 = 0 + 0
c [unhide-6-6] 21 units, 637 failed, 4328 tauts, 0 hbrs, 26539 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 702 transitive binary clauses
c [transred-2] found 16 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 15 clauses out of 674 (2%) of length 6
c [cce-2-1] eliminated 35 clauses out of 1344 (3%) of length 5
c [cce-2-1] eliminated 1132 clauses out of 5518 (21%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 1182 large clauses in 30000000 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2-1] scheduling 100837 clauses = 69410 binary + 31427 ternary
c [cce-2-1] tried to eliminate 872 small clauses 1%
c [cce-2-1] eliminated 275 binary clauses 0%
c [cce-2-1] eliminated 44 ternary clauses 0%
c [cce-2-1] eliminated 319 small clauses 0%
c [cce-2-1] eliminated 5085 small clauses in 30000005 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 6267 covered clauses in round 1
c [cce-2] eliminated 6267 covered clauses in TOTAL during 1 rounds
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 17591 variables 100%
c [elim-6] limit of 43774206 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 1018 variables 6% in round 1 in 10139670 steps
c [elim-6-1] backward subsumption/strengthening limit 10139600
c [elim-6-1-1] backward checking 3678 touched variables 21%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 19 and strengthened 32 clauses in 605561 steps
c [elim-6-1] rescheduled 141 variables 1% by backward subsumption
c [elim-6-2] eliminated 18 variables 0% in round 2 in 77645 steps
c [elim-6-2] backward subsumption/strengthening limit 77600
c [elim-6-2-1] backward checking 109 touched variables 1%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 9 and strengthened 9 clauses in 34673 steps
c [elim-6-2] rescheduled 36 variables 0% by backward subsumption
c [elim-6-3] eliminated 1 variables 0% in round 3 in 23047 steps
c [elim-6-3] backward subsumption/strengthening limit 23000
c [elim-6-3-1] backward checking 13 touched variables 0%
c [elim-6-3-1] fully completed backward checking in 1 rounds
c [elim-6-3] subsumed 0 and strengthened 5 clauses in 16891 steps
c [elim-6] incomplete 10 not tried 0% in round 3
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 1055 = 6% variables out of 17591 scheduled
c [bca-2] limit of 10000000 steps and 254194 added (scaled 2)
c [bca-2] 26193 out of 33074 literals actually usable 79%
c [bca-2] added 7 blocked clauses in 59226 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2923 pos 17.7% + 13591 neg 82.3% = 16514 sched 99.9% ret 22
c [sweep-2-1] 1110348 steps 10 queries 2489.50 avg class size
c [sweep-2-1] 93 decisions 7 SAT calls 44.71 avg env size
c [sweep-2-1] 16495 variables remain 100% (33 retained 0%)
c [decomp-14] removed 14 variables
c [sweep-2-1] removed 14 vars (1 failed, 2 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 14 vars in TOTAL (1 rounds, 9 queries)
c [sort-queue-6] sorted 16522 enqueued variables after 9015 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 16522 (100%)
c [score-dist-6] max exp 0, different 1 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 1516 variables 8.4% (16522 remain 8%)
c [simplification-6] removed 9282 irredundant clauses 6.8% (126718 remain 12%)
c [simplification-6] maximum reduction of 8% = max (8%, 7%)
c [simplification-6] large reduction 8% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 21015 (soft 11015 + delta 10000)
c [simplification-6] new conflict limit 11015 (hard 21015)
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   15.4   16521   126718      9444    6348    378 13880   20   199   17  10%      5  181   22    3  841%
c 
c [simplification-7] limit 11015 conflicts (hard 21015) hit after 11015 conflicts
c [quatres-3] found 4930 quaternary clauses 58% in total
c [quatres-3-1] removed 3 duplicate quaternary clauses
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 16519 free variables schedulable
c [ternres-3] 244 ternary resolvents (1 bin, 243 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 28 xors of average arity 3.0
c [gauss-2] connected 84 occurrences of 45 variables (average 1.9)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 12805856 penalty 0 = 0 + 0
c [basicprobe-3-0] 2171 probes remain 13% after last round
c [basicprobe-3-0] 129 units = 127 failed (98%) + 2 lifted (2%)
c [basicprobe-3-0] removed 163 variables, found 24635 hbrs
c [bate-1] eliminated 25 asymmetric tautologies during probing
c [unhide-7] limit 512234 with penalty 0 = 0 + 0
c [unhide-7-7] 1 units, 141 failed, 5678 tauts, 0 hbrs, 13756 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 412 transitive binary clauses
c [transred-3] found 13 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 16217 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 196 blocked clauses
c [block-2] 196 < 1/100 * 118936 = 1189 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 10
c [cce-3-1] eliminated 1 clauses out of 7 (14%) of length 8
c [cce-3-1] eliminated 1 clauses out of 65 (2%) of length 7
c [cce-3-1] eliminated 18 clauses out of 616 (3%) of length 6
c [cce-3-1] eliminated 61 clauses out of 1433 (4%) of length 5
c [cce-3-1] eliminated 449 clauses out of 4524 (10%) of length 4
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 531 large clauses in 30000000 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3-1] scheduling 90363 clauses = 60890 binary + 29473 ternary
c [cce-3-1] tried to eliminate 782 small clauses 1%
c [cce-3-1] eliminated 243 binary clauses 0%
c [cce-3-1] eliminated 44 ternary clauses 0%
c [cce-3-1] eliminated 287 small clauses 0%
c [cce-3-1] eliminated 287 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 818 covered clauses in round 1
c [cce-3] eliminated 818 covered clauses in TOTAL during 1 rounds
c [cce-3] 818 < 1/100 * 117399 = 1173 considered unsuccessful
c [elim-7] no untried remaining variables left
c [elim-7] scheduled 16211 variables 100%
c [elim-7] limit of 51223424 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 491 variables 3% in round 1 in 9009261 steps
c [elim-7-1] backward subsumption/strengthening limit 9009200
c [elim-7-1-1] backward checking 2869 touched variables 18%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 4 and strengthened 27 clauses in 516083 steps
c [elim-7-1] rescheduled 79 variables 0% by backward subsumption
c [elim-7-2] eliminated 10 variables 0% in round 2 in 33403 steps
c [elim-7-2] backward subsumption/strengthening limit 33400
c [elim-7-2-1] backward checking 75 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 10 and strengthened 1 clauses in 22835 steps
c [elim-7-2] rescheduled 8 variables 0% by backward subsumption
c [elim-7-3] eliminated 2 variables 0% in round 3 in 3671 steps
c [elim-7-3] backward subsumption/strengthening limit 3600
c [elim-7-3-1] backward checking 11 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 3601 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 511 = 3% variables out of 16211 scheduled
c [bca-3] limit of 10000000 steps and 232338 added (scaled 2)
c [bca-3] 24451 out of 31402 literals actually usable 78%
c [bca-3] added 19 blocked clauses in 56291 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2837 pos 18.1% + 12839 neg 81.9% = 15676 sched 99.8% ret 24
c [sweep-3-1] 1183298 steps 11 queries 3252.91 avg class size
c [sweep-3-1] 110 decisions 10 SAT calls 118.60 avg env size
c [sweep-3-1] 15633 variables remain 100% (67 retained 0%)
c [decomp-16] removed 2 variables
c [sweep-3-1] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 2 vars in TOTAL (1 rounds, 10 queries)
c [sort-queue-7] sorted 15698 enqueued variables after 11015 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 15698 (100%)
c [score-dist-7] max exp 0, different 1 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 821 variables 5.0% (15698 remain 7%)
c [simplification-7] removed 10807 irredundant clauses 8.5% (115911 remain 11%)
c [simplification-7] maximum reduction of 9% = max (5%, 9%)
c [simplification-7] large reduction 9% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 23015 (soft 13015 + delta 10000)
c [simplification-7] new conflict limit 13015 (hard 23015)
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   18.8   15697   115911     11504    7104    592 24313   22   197   17  11%     18  173   30    3  906%
c i   18.8   15694   115911     11505    7104    592 24313   22   197   17  11%     18  173   30    3  903%
c i   18.9   15693   115911     11830    7398    600 24313   22   195   17  11%     13  171   24    3  694%
c 
c [simplification-8] limit 13025 conflicts (hard 23015) hit after 13027 conflicts
c [quatres-4] found 4192 quaternary clauses 57% in total
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 15480 free variables schedulable
c [ternres-4] 196 ternary resolvents (0 bin, 196 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 255 variables
c [simpleprobe-4] 1860 schedulable variables 12%
c [simpleprobe-4] limit 11676200 penalty 0 = 0 + 0
c [decomp-18] removed 101 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 101 variables, found 4886 hbrs, 41 units
c [unhide-8] limit 583810 with penalty 0 = 0 + 0
c [unhide-8-8] 7 units, 110 failed, 4830 tauts, 0 hbrs, 12239 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 576 transitive binary clauses
c [transred-4] found 12 units
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 15146 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1167620040 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 252 variables 2% in round 1 in 8435440 steps
c [elim-8-1] backward subsumption/strengthening limit 8435400
c [elim-8-1-1] backward checking 1295 touched variables 9%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 7 and strengthened 15 clauses in 230600 steps
c [elim-8-1] rescheduled 68 variables 0% by backward subsumption
c [elim-8-2] eliminated 4 variables 0% in round 2 in 39219 steps
c [elim-8-2] backward subsumption/strengthening limit 39200
c [elim-8-2-1] backward checking 34 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 5 and strengthened 0 clauses in 17679 steps
c [elim-8-2] rescheduled 10 variables 0% by backward subsumption
c [elim-8-3] eliminated 1 variables 0% in round 3 in 12734 steps
c [elim-8-3] backward subsumption/strengthening limit 12700
c [elim-8-3-1] backward checking 9 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 9401 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 257 = 2% variables out of 15146 scheduled
c [bca-4] limit of 10000000 steps and 219705 added (scaled 2)
c [bca-4] 22663 out of 29780 literals actually usable 76%
c [bca-4] added 14 blocked clauses in 53673 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 2681 pos 18.1% + 12143 neg 81.9% = 14824 sched 99.6% ret 65
c [sweep-4-1] 1074303 steps 19 queries 3057.89 avg class size
c [sweep-4-1] 140 decisions 8 SAT calls 42.88 avg env size
c [sweep-4-1] 14802 variables remain 99% (87 retained 1%)
c [decomp-19] removed 14 variables
c [sweep-4-1] removed 14 vars (0 failed, 11 eqs, 15 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 14 vars in TOTAL (1 rounds, 18 queries)
c [sort-queue-8] sorted 14875 enqueued variables after 13027 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 14875 (100%)
c [score-dist-8] max exp 0, different 1 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 605 variables 3.9% (14875 remain 7%)
c [simplification-8] removed 6375 irredundant clauses 5.5% (109536 remain 10%)
c [simplification-8] maximum reduction of 5% = max (4%, 5%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 25027 (soft 15027 + delta 10000)
c [simplification-8] new conflict limit 15027 (hard 25027)
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.8   14874   109536     13688    8464    692 23372   24   200   18  12%     16  171   26    4  652%
c i   20.9   14873   109536     13817    8587    694 23372   24   200   18  12%     14  171   26    4  645%
c i   21.1   14872   109536     14365    9104    704 23379   24   193   18  12%      9  163   20    4  481%
c i   21.2   14871   109536     14407    9144    704 23379   24   194   18  12%      9  163   22    4  524%
c i   21.3   14867   109536     14674    9399    706 23382   24   194   18  12%      7  162   26    4  590%
c 
c [simplification-9] limit 15027 conflicts (hard 25027) hit after 15029 conflicts
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 14867 free variables schedulable
c [ternres-5] 67 ternary resolvents (0 bin, 67 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-20] removed 11 variables
c [treelook-4] limit 325292 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 27638 literals 93%
c [treelook-4] scheduling used 325309 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 325292 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 357339 steps
c [treelook-4] 27613 literals remain 93%
c [treelook-4] 14683 variables remain to probed next time 99%
c [treelook-4] removed 8 variables, found 1591 hbrs
c [unhide-9] limit 650584 with penalty 0 = 0 + 0
c [unhide-9-10] 11 units, 269 failed, 5219 tauts, 0 hbrs, 35909 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 337 transitive binary clauses
c [transred-5] found 9 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 150000000 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 9
c [cce-4-1] eliminated 2 clauses out of 92 (2%) of length 7
c [cce-4-1] eliminated 11 clauses out of 520 (2%) of length 6
c [cce-4-1] eliminated 33 clauses out of 1417 (2%) of length 5
c [cce-4-1] eliminated 309 clauses out of 4055 (8%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 356 large clauses in 26621677 steps
c [cce-4-1] allowing another 13310838 steps for small clauses
c [cce-4-1] scheduling 81236 clauses = 54915 binary + 26321 ternary
c [cce-4-1] tried to eliminate 8320 small clauses 10%
c [cce-4-1] eliminated 2089 binary clauses 4%
c [cce-4-1] eliminated 361 ternary clauses 1%
c [cce-4-1] eliminated 2450 small clauses 3%
c [cce-4-1] eliminated 3243 small clauses in 150000008 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 3599 covered clauses in round 1
c [cce-4] eliminated 3599 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 14716 variables 100%
c [elim-9] limit of 65058485 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 389 variables 3% in round 1 in 7778439 steps
c [elim-9-1] backward subsumption/strengthening limit 7778400
c [elim-9-1-1] backward checking 2320 touched variables 16%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 1 and strengthened 15 clauses in 402227 steps
c [elim-9-1] rescheduled 60 variables 0% by backward subsumption
c [elim-9-2] eliminated 2 variables 0% in round 2 in 24904 steps
c [elim-9-2] backward subsumption/strengthening limit 24900
c [elim-9-2-1] backward checking 17 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 2 and strengthened 0 clauses in 12886 steps
c [elim-9-2] rescheduled 4 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 2078 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 391 = 3% variables out of 14716 scheduled
c [bca-5] limit of 10000000 steps and 205268 added (scaled 2)
c [bca-5] 21488 out of 28652 literals actually usable 75%
c [bca-5] added 16 blocked clauses in 51334 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 2555 pos 17.9% + 11699 neg 82.1% = 14254 sched 99.5% ret 71
c [sweep-5-1] 10096131 steps 102 queries 627.07 avg class size
c [sweep-5-1] 1436 decisions 76 SAT calls 114.53 avg env size
c [sweep-5-1] 10106 variables remain 71% (4077 retained 29%)
c [decomp-22] removed 185 variables
c [sweep-5-1] removed 185 vars (0 failed, 33 eqs, 44 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 185 vars in TOTAL (1 rounds, 101 queries)
c [sort-queue-9] sorted 14140 enqueued variables after 15029 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 14140 (100%)
c [score-dist-9] max exp 0, different 1 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 727 variables 4.9% (14140 remain 6%)
c [simplification-9] removed 8708 irredundant clauses 7.9% (100828 remain 10%)
c [simplification-9] maximum reduction of 8% = max (5%, 8%)
c [simplification-9] large reduction 8% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 27029 (soft 17029 + delta 10000)
c [simplification-9] new conflict limit 17029 (hard 27029)
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   26.1   14139   100828     15702    8558    885 25826   25   197   17  13%      7  163   30    5  639%
c i   26.1   14138   100828     15715    8568    886 25826   25   197   17  13%      7  163   30    5  625%
c i   26.3   14137   100828     16219    9055    893 25827   25   197   17  13%      5  161   28    5  581%
c i   26.5   14116   100828     16733    9554    894 25828   27   197   17  14%      4  161   42    5  805%
c i   26.6   14115   100828     16811    9630    894 25828   27   197   17  14%      4  160   36    5  703%
c 
c [simplification-10] limit 17029 conflicts (hard 27029) hit after 17029 conflicts
c [quatres-5] found 3852 quaternary clauses 53% in total
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 14114 free variables schedulable
c [ternres-6] 56 ternary resolvents (0 bin, 56 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 1289 at-most-one constraints of average size 3.4
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 250000 for elimination
c [card-4] 1289 out of 1289 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 10 xors of average arity 2.9
c [gauss-3] connected 29 occurrences of 26 variables (average 1.1)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-4] limit 17787848 penalty 0 = 0 + 0
c [basicprobe-4-0] 1704 probes remain 12% after last round
c [basicprobe-4-0] 309 units = 282 failed (91%) + 27 lifted (9%)
c [basicprobe-4-0] removed 437 variables, found 24389 hbrs
c [bate-2] eliminated 40 asymmetric tautologies during probing
c [unhide-10] limit 711513 with penalty 0 = 0 + 0
c [unhide-10-12] 39 units, 258 failed, 4993 tauts, 0 hbrs, 30052 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 398 transitive binary clauses
c [transred-6] found 16 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 13330 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 128 blocked clauses
c [block-3] 128 < 1/100 * 90101 = 901 considered unsuccessful
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 5 (20%) of length 9
c [cce-5-1] eliminated 3 clauses out of 27 (11%) of length 8
c [cce-5-1] eliminated 4 clauses out of 77 (5%) of length 7
c [cce-5-1] eliminated 8 clauses out of 379 (2%) of length 6
c [cce-5-1] eliminated 47 clauses out of 1212 (4%) of length 5
c [cce-5-1] eliminated 144 clauses out of 3292 (4%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 207 large clauses in 16547350 steps
c [cce-5-1] allowing another 8273675 steps for small clauses
c [cce-5-1] scheduling 68874 clauses = 47690 binary + 21184 ternary
c [cce-5-1] tried to eliminate 1736 small clauses 3%
c [cce-5-1] eliminated 459 binary clauses 1%
c [cce-5-1] eliminated 84 ternary clauses 0%
c [cce-5-1] eliminated 543 small clauses 1%
c [cce-5-1] eliminated 543 small clauses in 30000010 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 750 covered clauses in round 1
c [cce-5] eliminated 750 covered clauses in TOTAL during 1 rounds
c [cce-5] 750 < 1/100 * 89332 = 893 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 13329 variables 100%
c [elim-10] limit of 71151395 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 826 variables 6% in round 1 in 6550900 steps
c [elim-10-1] backward subsumption/strengthening limit 6550900
c [elim-10-1-1] backward checking 3608 touched variables 27%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 6 and strengthened 16 clauses in 548069 steps
c [elim-10-1] rescheduled 72 variables 1% by backward subsumption
c [elim-10-2] eliminated 7 variables 0% in round 2 in 31931 steps
c [elim-10-2] backward subsumption/strengthening limit 31900
c [elim-10-2-1] backward checking 45 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 2 clauses in 19807 steps
c [elim-10-2] rescheduled 11 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 5541 steps
c [elim-10-3] backward subsumption/strengthening limit 5500
c [elim-10-3-1] backward checking 11 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 0 and strengthened 0 clauses in 5501 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 835 = 6% variables out of 13329 scheduled
c [bca-6] limit of 10000000 steps and 175906 added (scaled 2)
c [bca-6] 18819 out of 24990 literals actually usable 75%
c [bca-6] added 5 blocked clauses in 44415 steps
c [sweep-6] limit 1067270 penalty 0 = 0 + 0
c [sweep-6-1] 2192 pos 24.2% + 6848 neg 75.8% = 9040 sched 72.4% ret 3454
c [sweep-6-1] 1072303 steps 8 queries 2167.38 avg class size
c [sweep-6-1] 164 decisions 7 SAT calls 76.71 avg env size
c [sweep-6-1] 9023 variables remain 72% (3471 retained 28%)
c [decomp-24] removed 2 variables
c [sweep-6-1] removed 2 vars (0 failed, 0 eqs, 1 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 2 vars in TOTAL (1 rounds, 7 queries)
c [sort-queue-10] sorted 12492 enqueued variables after 17029 conflicts
c [score-dist-10] active 0 (0%), one 0 (0%), zero 12492 (100%)
c [score-dist-10] max exp 0, different 1 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 1622 variables 11.5% (12492 remain 6%)
c [simplification-10] removed 13144 irredundant clauses 13.0% (87684 remain 8%)
c [simplification-10] maximum reduction of 13% = max (11%, 13%)
c [simplification-10] large reduction 13% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 29029 (soft 19029 + delta 10000)
c [simplification-10] new conflict limit 19029 (hard 29029)
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   29.4   12491    87684     17923    7188    712 26907   26   190   15  14%      6  151   24    6  436%
c i   29.4   12490    87684     17931    7195    712 26907   26   190   15  14%      6  151   24    6  429%
c i   29.7   12489    87684     18575    7803    724 26913   25   188   15  14%      5  147   22    6  393%
c 
c [simplification-11] limit 19030 conflicts (hard 29029) hit after 19031 conflicts
c [quatres-6] found 3439 quaternary clauses 53% in total
c [quatres-6-2] added 6 quaternary resolvents
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 12489 free variables schedulable
c [ternres-7] 82 ternary resolvents (0 bin, 82 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 4 variables
c [simpleprobe-5] all 12488 free variables schedulable
c [simpleprobe-5] limit 15309154 penalty 0 = 0 + 0
c [decomp-26] removed 192 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 192 variables, found 4755 hbrs, 67 units
c [unhide-11] limit 765457 with penalty 0 = 0 + 0
c [unhide-11-14] 7 units, 111 failed, 5285 tauts, 0 hbrs, 15153 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 436 transitive binary clauses
c [transred-7] found 17 units
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 12186 variables 100%
c [elim-11] limit of 76545770 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 206 variables 2% in round 1 in 6116466 steps
c [elim-11-1] backward subsumption/strengthening limit 6116400
c [elim-11-1-1] backward checking 1209 touched variables 10%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 8 clauses in 194605 steps
c [elim-11-1] rescheduled 25 variables 0% by backward subsumption
c [elim-11-2] eliminated 3 variables 0% in round 2 in 9949 steps
c [elim-11-2] backward subsumption/strengthening limit 9900
c [elim-11-2-1] backward checking 25 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 1 and strengthened 0 clauses in 9901 steps
c [elim-11-2] rescheduled 3 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 808 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 209 = 2% variables out of 12186 scheduled
c [bca-7] limit of 10000000 steps and 167137 added (scaled 2)
c [bca-7] 17461 out of 23956 literals actually usable 73%
c [bca-7] added 5 blocked clauses in 42556 steps
c [sweep-7] limit 1148186 penalty 0 = 0 + 0
c [sweep-7-1] 2062 pos 23.7% + 6634 neg 76.3% = 8696 sched 72.6% ret 3281
c [sweep-7-1] 1247508 steps 11 queries 1837.91 avg class size
c [sweep-7-1] 175 decisions 10 SAT calls 94.00 avg env size
c [sweep-7-1] 8660 variables remain 72% (3312 retained 28%)
c [decomp-27] removed 6 variables
c [sweep-7-1] removed 6 vars (0 failed, 1 eqs, 0 impls)
c [sweep-7] 6 < 1/1000 * 11977 = 11 considered unsuccessful
c [sweep-7] removed 6 vars in TOTAL (1 rounds, 10 queries)
c [sort-queue-11] sorted 11971 enqueued variables after 19031 conflicts
c [score-dist-11] active 0 (0%), one 0 (0%), zero 11971 (100%)
c [score-dist-11] max exp 0, different 1 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 518 variables 4.1% (11971 remain 5%)
c [simplification-11] removed 4472 irredundant clauses 5.1% (83212 remain 8%)
c [simplification-11] maximum reduction of 5% = max (4%, 5%)
c [simplification-11] large reduction 5% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 31031 (soft 21031 + delta 10000)
c [simplification-11] new conflict limit 21031 (hard 31031)
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.0   11970    83212     19328    7540    601 24939   27   192   15  14%      5  150   32    6  537%
c 
c [simplification-12] limit 21031 conflicts (hard 31031) hit after 21031 conflicts
c [quatres-7] found 3393 quaternary clauses 51% in total
c [ternres-8] limit 4077721 with penalty 0 = 0 + 0
c [ternres-8] all 11968 free variables schedulable
c [ternres-8] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 4 variables
c [treelook-5] limit 407772 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 23912 literals 100%
c [treelook-5] scheduling used 328142 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 407772 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 476098 steps
c [treelook-5] 23877 literals remain 100%
c [treelook-5] 11837 variables remain to probed next time 99%
c [decomp-29] removed 4 variables
c [treelook-5] removed 18 variables, found 3090 hbrs
c [unhide-12] limit 815544 with penalty 0 = 0 + 0
c [unhide-12-16] 5 units, 82 failed, 2407 tauts, 0 hbrs, 27591 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 363 transitive binary clauses
c [transred-8] found 13 units
c [cce-6] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 12
c [cce-6-1] eliminated 1 clauses out of 7 (14%) of length 10
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 9
c [cce-6-1] eliminated 3 clauses out of 41 (7%) of length 8
c [cce-6-1] eliminated 3 clauses out of 129 (2%) of length 7
c [cce-6-1] eliminated 10 clauses out of 430 (2%) of length 6
c [cce-6-1] eliminated 44 clauses out of 1321 (3%) of length 5
c [cce-6-1] eliminated 165 clauses out of 3119 (5%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 229 large clauses in 15000000 steps
c [cce-6-1] allowing another 7500000 steps for small clauses
c [cce-6-1] scheduling 62240 clauses = 43348 binary + 18892 ternary
c [cce-6-1] tried to eliminate 672 small clauses 1%
c [cce-6-1] eliminated 138 binary clauses 0%
c [cce-6-1] eliminated 19 ternary clauses 0%
c [cce-6-1] eliminated 157 small clauses 0%
c [cce-6-1] eliminated 470 small clauses in 15000014 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 699 covered clauses in round 1
c [cce-6] eliminated 699 covered clauses in TOTAL during 1 rounds
c [cce-6] 699 < 1/100 * 81320 = 813 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 11864 variables 100%
c [elim-12] limit of 81554432 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 127 variables 1% in round 1 in 5809421 steps
c [elim-12-1] backward subsumption/strengthening limit 5809400
c [elim-12-1-1] backward checking 799 touched variables 7%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 10 clauses in 140100 steps
c [elim-12-1] rescheduled 36 variables 0% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 22416 steps
c [elim-12-2] backward subsumption/strengthening limit 22400
c [elim-12-2-1] backward checking 4 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 3 clauses in 8228 steps
c [elim-12-2] rescheduled 6 variables 0% by backward subsumption
c [elim-12-3] eliminated 1 variables 0% in round 3 in 3083 steps
c [elim-12-3] backward subsumption/strengthening limit 3000
c [elim-12-3-1] backward checking 0 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 0 and strengthened 0 clauses in 3001 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 129 = 1% variables out of 11864 scheduled
c [bca-8] limit of 10000000 steps and 161389 added (scaled 2)
c [bca-8] 16668 out of 23472 literals actually usable 71%
c [bca-8] added 2 blocked clauses in 42204 steps
c [sort-queue-12] sorted 11735 enqueued variables after 21031 conflicts
c [score-dist-12] active 0 (0%), one 0 (0%), zero 11735 (100%)
c [score-dist-12] max exp 0, different 1 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 233 variables 1.9% (11735 remain 5%)
c [simplification-12] removed 2786 irredundant clauses 3.3% (80426 remain 8%)
c [simplification-12] maximum reduction of 3% = max (2%, 3%)
c [simplification-12] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-12] new conflict interval 9000
c [simplification-12] penalized conflict interval 9000 = 1 * 9000
c [simplification-12] hard conflict limit 40031 (soft 30031 + delta 10000)
c [simplification-12] new conflict limit 30031 (hard 40031)
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   34.2   11734    80426     24694   12080    643 22437   27   186   17  14%     63  132   29    8  387%
c i   34.6   11733    80426     25783   13134    653 22440   27   183   18  15%     25  127   30    8  374%
c i   34.8   11732    80426     26336   13675    654 22442   28   186   18  15%     14  129   30    8  363%
c i   34.8   11731    80426     26366   13701    655 22442   28   186   18  15%     14  129   29    8  361%
c i   34.8   11069    80426     26371   13703    657 22442   28   186   18  15%     13  129   29    8  355%
c i   35.5   10369    80426     28510   15790    668 22454   27   178   19  15%     16  117   26    9  298%
c 
c [simplification-13] limit 30033 conflicts (hard 40031) hit after 30033 conflicts
c [ternres-9] limit 5204342 with penalty 0 = 0 + 0
c [ternres-9] all 10366 free variables schedulable
c [ternres-9] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 1701 variables
c [basicprobe-5] limit 26021710 penalty 0 = 0 + 0
c [basicprobe-5-0] 37 probes remain 0% after last round
c [basicprobe-5-0] 730 units = 513 failed (70%) + 217 lifted (30%)
c [basicprobe-5-0] removed 2369 variables, found 28975 hbrs
c [bate-3] eliminated 100 asymmetric tautologies during probing
c [unhide-13] limit 1040868 with penalty 0 = 0 + 0
c [unhide-13-19] 6 units, 335 failed, 6052 tauts, 0 hbrs, 60659 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 729 transitive binary clauses
c [transred-9] found 26 units
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 7296 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 1707 variables 23% in round 1 in 2663885 steps
c [elim-13-1] backward subsumption/strengthening limit 2663800
c [elim-13-1-1] backward checking 3465 touched variables 47%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 6 and strengthened 17 clauses in 392178 steps
c [elim-13-1] rescheduled 91 variables 1% by backward subsumption
c [elim-13-2] eliminated 9 variables 0% in round 2 in 41492 steps
c [elim-13-2] backward subsumption/strengthening limit 41400
c [elim-13-2-1] backward checking 36 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 2 and strengthened 1 clauses in 16181 steps
c [elim-13-2] rescheduled 9 variables 0% by backward subsumption
c [elim-13-3] eliminated 1 variables 0% in round 3 in 4471 steps
c [elim-13-3] backward subsumption/strengthening limit 4400
c [elim-13-3-1] backward checking 2 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 0 and strengthened 0 clauses in 4401 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 1717 = 24% variables out of 7296 scheduled
c [bca-9] limit of 10000000 steps and 75114 added (scaled 2)
c [bca-9] 7172 out of 11160 literals actually usable 64%
c [bca-9] added 4 blocked clauses in 20733 steps
c [sweep-8] limit 780651 penalty 1 = 1 + 0
c [sweep-8-1] 912 pos 23.6% + 2945 neg 76.4% = 3857 sched 69.1% ret 1722
c [sweep-8-1] 807731 steps 36 queries 380.00 avg class size
c [sweep-8-1] 268 decisions 29 SAT calls 78.59 avg env size
c [sweep-8-1] 3286 variables remain 59% (2286 retained 41%)
c [decomp-31] removed 29 variables
c [sweep-8-1] removed 29 vars (0 failed, 7 eqs, 11 impls)
c [sweep-8] removed 29 vars in TOTAL (1 rounds, 35 queries)
c [sort-queue-13] sorted 5550 enqueued variables after 30033 conflicts
c [score-dist-13] active 0 (0%), one 0 (0%), zero 5550 (100%)
c [score-dist-13] max exp 0, different 1 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 4816 variables 46.5% (5550 remain 3%)
c [simplification-13] removed 43261 irredundant clauses 53.8% (37165 remain 4%)
c [simplification-13] maximum reduction of 54% = max (46%, 54%)
c [simplification-13] large reduction 54% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 42033 (soft 32033 + delta 10000)
c [simplification-13] new conflict limit 32033 (hard 42033)
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   38.3    5549    37165     31968    8138    276 16498   25   160   12  16%     33   93   21   10  222%
c i   38.3    5543    37165     32017    8177    279 16504   25   159   12  16%     31   92   18   10  193%
c 
c [simplification-14] limit 32033 conflicts (hard 42033) hit after 32036 conflicts
c [quatres-8] found 1623 quaternary clauses 50% in total
c [quatres-8-1] removed 4 duplicate quaternary clauses
c [quatres-8-2] added 3 single-self-subsuming ternary resolvents
c [quatres-8-2] added 2 quaternary resolvents
c [ternres-10] limit 5333196 with penalty 0 = 0 + 0
c [ternres-10] all 5509 free variables schedulable
c [ternres-10] 130 ternary resolvents (0 bin, 130 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] extracted 19 xors of average arity 2.5
c [gauss-4] connected 48 occurrences of 36 variables (average 1.3)
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 9 variables
c [simpleprobe-6] all 5500 free variables schedulable
c [simpleprobe-6] limit 21332784 penalty 0 = 0 + 0
c [decomp-33] removed 96 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 96 variables, found 3204 hbrs, 35 units
c [unhide-14] limit 1066639 with penalty 0 = 0 + 0
c [unhide-14-23] 12 units, 261 failed, 4882 tauts, 0 hbrs, 15311 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 631 transitive binary clauses
c [transred-10] found 29 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 5307 variables 100%
c [block-4] limit of 6666495 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 56 blocked clauses
c [block-4] 56 < 1/100 * 33915 = 339 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 5307 variables 100%
c [elim-14] limit of 106663924 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 211 variables 4% in round 1 in 2255392 steps
c [elim-14-1] backward subsumption/strengthening limit 2255300
c [elim-14-1-1] backward checking 1075 touched variables 20%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 2 and strengthened 3 clauses in 156693 steps
c [elim-14-1] rescheduled 24 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 11554 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 211 = 4% variables out of 5307 scheduled
c [bca-10] limit of 10000000 steps and 66966 added (scaled 2)
c [bca-10] 6085 out of 10194 literals actually usable 60%
c [bca-10] added 2 blocked clauses in 19021 steps
c [sweep-9] limit 1599958 penalty 0 = 0 + 0
c [sweep-9-1] 781 pos 26.2% + 2202 neg 73.8% = 2983 sched 58.5% ret 2113
c [sweep-9-1] 1649006 steps 50 queries 196.48 avg class size
c [sweep-9-1] 802 decisions 44 SAT calls 105.34 avg env size
c [sweep-9-1] 2116 variables remain 42% (2939 retained 58%)
c [decomp-34] removed 56 variables
c [sweep-9-1] removed 56 vars (0 failed, 7 eqs, 13 impls)
c [sweep-9] removed 56 vars in TOTAL (1 rounds, 49 queries)
c [sort-queue-14] sorted 5040 enqueued variables after 32036 conflicts
c [score-dist-14] active 0 (0%), one 0 (0%), zero 5040 (100%)
c [score-dist-14] max exp 0, different 1 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 469 variables 8.5% (5040 remain 2%)
c [simplification-14] removed 4382 irredundant clauses 11.8% (32783 remain 3%)
c [simplification-14] maximum reduction of 12% = max (9%, 12%)
c [simplification-14] large reduction 12% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 44036 (soft 34036 + delta 10000)
c [simplification-14] new conflict limit 34036 (hard 44036)
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   39.2    5039    32783     32800    7495    340 12556   24   155   11  15%     14   87   19   10  201%
c i   39.3    5038    32783     33016    7705    343 12557   23   154   11  15%     11   85   20   10  203%
c 
c [simplification-15] limit 34036 conflicts (hard 44036) hit after 34038 conflicts
c [quatres-9] found 1596 quaternary clauses 48% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-2] added 3 quaternary resolvents
c [ternres-11] limit 5452920 with penalty 0 = 0 + 0
c [ternres-11] all 5036 free variables schedulable
c [ternres-11] 39 ternary resolvents (0 bin, 39 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 170403 penalty 4 = 4 + 0
c [card-5] found 802 at-most-one constraints of average size 3.4
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 170403 for elimination
c [card-5] 802 out of 802 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 5 variables
c [treelook-6] limit 545292 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 10056 literals 100%
c [treelook-6] scheduling used 145734 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 545292 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 548969 steps
c [treelook-6] 9977 literals remain 100%
c [treelook-6] 4949 variables remain to probed next time 99%
c [decomp-36] removed 6 variables
c [treelook-6] removed 35 variables, found 5563 hbrs
c [unhide-15] limit 1090584 with penalty 0 = 0 + 0
c [unhide-15-27] 1 units, 29 failed, 1818 tauts, 0 hbrs, 13273 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 466 transitive binary clauses
c [transred-11] found 13 units
c [cce-7] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 24
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 20
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 15
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 11
c [cce-7-1] eliminated 1 clauses out of 44 (2%) of length 7
c [cce-7-1] eliminated 19 clauses out of 150 (13%) of length 6
c [cce-7-1] eliminated 45 clauses out of 460 (10%) of length 5
c [cce-7-1] eliminated 226 clauses out of 1274 (18%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 295 large clauses in 4428537 steps
c [cce-7-1] allowing another 2214268 steps for small clauses
c [cce-7-1] scheduling 22319 clauses = 17613 binary + 4706 ternary
c [cce-7-1] tried to eliminate 1058 small clauses 5%
c [cce-7-1] eliminated 312 binary clauses 2%
c [cce-7-1] eliminated 36 ternary clauses 1%
c [cce-7-1] eliminated 348 small clauses 2%
c [cce-7-1] eliminated 594 small clauses in 7500000 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 889 covered clauses in round 1
c [cce-7] eliminated 889 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 4955 variables 100%
c [elim-15] limit of 109058411 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 196 variables 4% in round 1 in 2018532 steps
c [elim-15-1] backward subsumption/strengthening limit 2018500
c [elim-15-1-1] backward checking 947 touched variables 19%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 3 clauses in 125559 steps
c [elim-15-1] rescheduled 15 variables 0% by backward subsumption
c [elim-15-2] eliminated 1 variables 0% in round 2 in 6383 steps
c [elim-15-2] backward subsumption/strengthening limit 6300
c [elim-15-2-1] backward checking 10 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 4986 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 198 = 4% variables out of 4955 scheduled
c [bca-11] limit of 10000000 steps and 61317 added (scaled 2)
c [bca-11] 5540 out of 9516 literals actually usable 58%
c [bca-11] added 4 blocked clauses in 18314 steps
c [sweep-10] limit 1635876 penalty 0 = 0 + 0
c [sweep-10-1] 684 pos 34.6% + 1295 neg 65.4% = 1979 sched 41.6% ret 2778
c [sweep-10-1] 1642489 steps 53 queries 62.94 avg class size
c [sweep-10-1] 852 decisions 50 SAT calls 106.34 avg env size
c [sweep-10-1] 1491 variables remain 31% (3263 retained 69%)
c [decomp-37] removed 12 variables
c [sweep-10-1] removed 12 vars (0 failed, 3 eqs, 3 impls)
c [sweep-10] removed 12 vars in TOTAL (1 rounds, 52 queries)
c [sort-queue-15] sorted 4745 enqueued variables after 34038 conflicts
c [score-dist-15] active 0 (0%), one 0 (0%), zero 4745 (100%)
c [score-dist-15] max exp 0, different 1 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 291 variables 5.8% (4745 remain 2%)
c [simplification-15] removed 2437 irredundant clauses 7.4% (30346 remain 3%)
c [simplification-15] maximum reduction of 7% = max (6%, 7%)
c [simplification-15] large reduction 7% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 46038 (soft 36038 + delta 10000)
c [simplification-15] new conflict limit 36038 (hard 46038)
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   40.4    4744    30346     34355    7447    339 12159   23   153   11  15%      7   83   20   10  206%
c i   40.6    4741    30346     35203    8267    348 12163   22   150   11  15%      3   79   24   10  240%
c i   40.6    4740    30346     35223    8283    348 12165   22   150   11  15%      3   79   23   10  234%
c i   40.6    4739    30346     35228    8287    348 12165   22   150   11  15%      3   79   23   10  230%
c 
c [simplification-16] limit 36040 conflicts (hard 46038) hit after 36041 conflicts
c [quatres-10] found 1359 quaternary clauses 44% in total
c [quatres-10-1] removed 1 duplicate quaternary clauses
c [ternres-12] limit 5568601 with penalty 0 = 0 + 0
c [ternres-12] all 4739 free variables schedulable
c [ternres-12] 42 ternary resolvents (0 bin, 42 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-38] removed 10 variables
c [basicprobe-6] limit 27843005 penalty 0 = 0 + 0
c [basicprobe-6-0] 430 sched 10%, 236 failed, 38 lifted, 7288 hbrs
c [decomp-39] removed 540 variables
c [basicprobe-6-1] 701 sched 18%, 162 failed, 31 lifted, 23215 hbrs
c [decomp-40] removed 360 variables
c [basicprobe-6-2] 48 probes remain 1% after last round
c [basicprobe-6-2] 577 units = 500 failed (87%) + 77 lifted (13%)
c [basicprobe-6-2] removed 1055 variables, found 41184 hbrs
c [bate-4] eliminated 105 asymmetric tautologies during probing
c [unhide-16] limit 1113720 with penalty 0 = 0 + 0
c [unhide-16-32] 3 units, 39 failed, 8197 tauts, 0 hbrs, 16755 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 610 transitive binary clauses
c [transred-12] found 1 units
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 3664 variables 100%
c [elim-16] limit of 111372021 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 383 variables 10% in round 1 in 1284300 steps
c [elim-16-1] backward subsumption/strengthening limit 1284300
c [elim-16-1-1] backward checking 1254 touched variables 34%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 1 and strengthened 3 clauses in 148556 steps
c [elim-16-1] rescheduled 19 variables 1% by backward subsumption
c [elim-16-2] no variable eliminated in round 2 in 8436 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 383 = 10% variables out of 3664 scheduled
c [bca-12] limit of 10000000 steps and 40381 added (scaled 2)
c [bca-12] 3337 out of 6564 literals actually usable 51%
c [bca-12] added 15 blocked clauses in 12658 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 16705800 penalty 0 = 0 + 0
c [sweep-11-1] 456 pos 43.0% + 605 neg 57.0% = 1061 sched 32.3% ret 2220
c [sweep-11-1] 4368010 steps 349 queries 9.59 avg class size
c [sweep-11-1] 2612 decisions 296 SAT calls 41.56 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-41] removed 25 variables
c [sweep-11-1] removed 25 vars (0 failed, 54 eqs, 41 impls)
c [sweep-11-2] 731 pos 22.5% + 2525 neg 77.5% = 3256 sched 100.0% ret 0
c [sweep-11-2] 5741213 steps 425 queries 29.62 avg class size
c [sweep-11-2] 3310 decisions 342 SAT calls 57.73 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-42] removed 47 variables
c [sweep-11-2] removed 47 vars (0 failed, 91 eqs, 41 impls)
c [sweep-11-3] 718 pos 22.4% + 2491 neg 77.6% = 3209 sched 100.0% ret 0
c [sweep-11-3] 5551041 steps 430 queries 16.17 avg class size
c [sweep-11-3] 3358 decisions 358 SAT calls 59.46 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-43] removed 23 variables
c [sweep-11-3] removed 23 vars (0 failed, 73 eqs, 24 impls)
c [sweep-11] removed 95 vars in TOTAL (3 rounds, 1201 queries)
c [sort-queue-16] sorted 3186 enqueued variables after 36041 conflicts
c [score-dist-16] active 0 (0%), one 0 (0%), zero 3186 (100%)
c [score-dist-16] max exp 0, different 1 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 1553 variables 32.8% (3186 remain 1%)
c [simplification-16] removed 10892 irredundant clauses 35.9% (19454 remain 2%)
c [simplification-16] maximum reduction of 36% = max (33%, 36%)
c [simplification-16] large reduction 36% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 48041 (soft 38041 + delta 10000)
c [simplification-16] new conflict limit 38041 (hard 48041)
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   42.7    3185    19454     36054    6202    219 21693   22   150   10  15%      2   78   21   10  211%
c i   42.7    3184    19454     36228    6372    220 21693   22   149   10  15%      0   77   21   10  202%
c i   42.8    3183    19454     36999    7120    226 21697   22   142   10  15%      0   69   16   10  160%
c i   42.9    3182    19454     37271    7385    227 21698   22   142   10  15%     -1   69   22   10  216%
c i   42.9    3180    19454     37383    7490    231 21699   22   141   10  15%     -2   67   20   10  191%
c 
c [simplification-17] limit 38041 conflicts (hard 48041) hit after 38288 conflicts
c [ternres-13] limit 5656939 with penalty 0 = 0 + 0
c [ternres-13] all 3180 free variables schedulable
c [ternres-13] 76 ternary resolvents (0 bin, 76 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-44] removed 12 variables
c [simpleprobe-7] all 3174 free variables schedulable
c [simpleprobe-7] limit 22627757 penalty 0 = 0 + 0
c [decomp-45] removed 64 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 64 variables, found 2664 hbrs, 25 units
c [unhide-17] limit 1131387 with penalty 0 = 0 + 0
c [unhide-17-38] 0 units, 2 failed, 4292 tauts, 0 hbrs, 14558 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 648 transitive binary clauses
c [transred-13] found 4 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 150000000 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-8-1] eliminated 1 clauses out of 7 (14%) of length 8
c [cce-8-1] eliminated 1 clauses out of 18 (6%) of length 7
c [cce-8-1] eliminated 17 clauses out of 105 (16%) of length 6
c [cce-8-1] eliminated 27 clauses out of 286 (9%) of length 5
c [cce-8-1] eliminated 68 clauses out of 822 (8%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 115 large clauses in 2342595 steps
c [cce-8-1] allowing another 1171297 steps for small clauses
c [cce-8-1] scheduling 14534 clauses = 10906 binary + 3628 ternary
c [cce-8-1] tried to eliminate 14534 small clauses 100%
c [cce-8-1] eliminated 1734 binary clauses 16%
c [cce-8-1] eliminated 160 ternary clauses 4%
c [cce-8-1] eliminated 1894 small clauses 13%
c [cce-8-1] eliminated 1947 small clauses in 49260157 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] completed small and large (ATE)
c [cce-8-1] eliminated 2062 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 974728 steps for small clauses
c [cce-8-2] scheduling 12640 clauses = 9172 binary + 3468 ternary
c [cce-8-2] tried to eliminate 12640 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 2062 covered clauses in TOTAL during 2 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 3103 variables 100%
c [elim-17] limit of 113138788 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 282 variables 9% in round 1 in 998908 steps
c [elim-17-1] backward subsumption/strengthening limit 998900
c [elim-17-1-1] backward checking 1013 touched variables 33%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 3 clauses in 103866 steps
c [elim-17-1] rescheduled 18 variables 1% by backward subsumption
c [elim-17-2] no variable eliminated in round 2 in 6772 steps
c [elim-17] fully completed in 2 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 282 = 9% variables out of 3103 scheduled
c [bca-13] limit of 10000000 steps and 32315 added (scaled 2)
c [bca-13] 2842 out of 5644 literals actually usable 50%
c [bca-13] added 5 blocked clauses in 11405 steps
c [sweep-12] limit 1697081 penalty 0 = 0 + 0
c [sweep-12-1] 523 pos 18.5% + 2298 neg 81.5% = 2821 sched 100.0% ret 0
c [sweep-12-1] 1775180 steps 90 queries 52.13 avg class size
c [sweep-12-1] 1451 decisions 90 SAT calls 82.03 avg env size
c [sweep-12-1] 814 variables remain 29% (2007 retained 71%)
c [sweep-12-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-12] removed 0 vars in TOTAL (1 rounds, 89 queries)
c [sort-queue-17] sorted 2821 enqueued variables after 38288 conflicts
c [score-dist-17] active 0 (0%), one 0 (0%), zero 2821 (100%)
c [score-dist-17] max exp 0, different 1 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 359 variables 11.3% (2821 remain 1%)
c [simplification-17] removed 3572 irredundant clauses 18.4% (15882 remain 2%)
c [simplification-17] maximum reduction of 18% = max (11%, 18%)
c [simplification-17] large reduction 18% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 50288 (soft 40288 + delta 10000)
c [simplification-17] new conflict limit 40288 (hard 50288)
c 
c [simplification-18] limit 40288 conflicts (hard 50288) hit after 40290 conflicts
c [quatres-11] found 898 quaternary clauses 38% in total
c [quatres-11-1] removed 1 duplicate quaternary clauses
c [ternres-14] limit 5726769 with penalty 0 = 0 + 0
c [ternres-14] all 2821 free variables schedulable
c [ternres-14] 17 ternary resolvents (0 bin, 17 trn)
c [ternres-14] fully completed ternary resolution
c [treelook-7] limit 572676 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 5629 literals 100%
c [treelook-7] scheduling used 103500 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 572676 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 573081 steps
c [treelook-7] 5572 literals remain 99%
c [treelook-7] 2785 variables remain to probed next time 99%
c [treelook-7] removed 2 variables, found 5191 hbrs
c [unhide-18] limit 1145353 with penalty 0 = 0 + 0
c [unhide-18-44] 0 units, 3 failed, 3033 tauts, 0 hbrs, 8466 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 347 transitive binary clauses
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 21
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 15
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 13
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 12
c [cce-9-1] eliminated 2 clauses out of 6 (33%) of length 9
c [cce-9-1] eliminated 2 clauses out of 11 (18%) of length 8
c [cce-9-1] eliminated 6 clauses out of 33 (18%) of length 7
c [cce-9-1] eliminated 4 clauses out of 113 (4%) of length 6
c [cce-9-1] eliminated 9 clauses out of 270 (3%) of length 5
c [cce-9-1] eliminated 29 clauses out of 637 (5%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 59 large clauses in 2112065 steps
c [cce-9-1] allowing another 1056032 steps for small clauses
c [cce-9-1] scheduling 11255 clauses = 8874 binary + 2381 ternary
c [cce-9-1] tried to eliminate 8989 small clauses 80%
c [cce-9-1] eliminated 542 binary clauses 6%
c [cce-9-1] eliminated 150 ternary clauses 6%
c [cce-9-1] eliminated 692 small clauses 6%
c [cce-9-1] eliminated 692 small clauses in 30000003 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 751 covered clauses in round 1
c [cce-9] eliminated 751 covered clauses in TOTAL during 1 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 2817 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 2290707940 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 131 variables 5% in round 1 in 917184 steps
c [elim-18-1] backward subsumption/strengthening limit 917100
c [elim-18-1-1] backward checking 577 touched variables 20%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 1 and strengthened 11 clauses in 67750 steps
c [elim-18-1] rescheduled 34 variables 1% by backward subsumption
c [elim-18-2] eliminated 3 variables 0% in round 2 in 17641 steps
c [elim-18-2] backward subsumption/strengthening limit 17600
c [elim-18-2-1] backward checking 15 touched variables 1%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 0 and strengthened 0 clauses in 4975 steps
c [elim-18] fully completed in 2 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 134 = 5% variables out of 2817 scheduled
c [bca-14] limit of 10000000 steps and 30323 added (scaled 2)
c [bca-14] 2605 out of 5368 literals actually usable 49%
c [bca-14] added 7 blocked clauses in 11433 steps
c [sort-queue-18] sorted 2683 enqueued variables after 40290 conflicts
c [score-dist-18] active 0 (0%), one 0 (0%), zero 2683 (100%)
c [score-dist-18] max exp 0, different 1 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 138 variables 4.9% (2683 remain 1%)
c [simplification-18] removed 997 irredundant clauses 6.3% (14885 remain 1%)
c [simplification-18] maximum reduction of 6% = max (5%, 6%)
c [simplification-18] large reduction 6% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 52290 (soft 42290 + delta 10000)
c [simplification-18] new conflict limit 42290 (hard 52290)
c 
c [simplification-19] limit 42290 conflicts (hard 52290) hit after 42291 conflicts
c [ternres-15] limit 5795256 with penalty 0 = 0 + 0
c [ternres-15] all 2683 free variables schedulable
c [ternres-15] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 125000 penalty 4 = 4 + 0
c [gauss-5] extracted 0 xors of average arity 0.0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-7] limit 28976281 penalty 0 = 0 + 0
c [basicprobe-7-0] 263 sched 10%, 42 failed, 1 lifted, 2171 hbrs
c [decomp-50] removed 46 variables
c [basicprobe-7-1] 688 sched 26%, 23 failed, 0 lifted, 3403 hbrs
c [decomp-51] removed 25 variables
c [basicprobe-7-2] 678 sched 26%, 9 failed, 0 lifted, 659 hbrs
c [decomp-52] removed 10 variables
c [basicprobe-7-3] 682 sched 26%, 1 failed, 0 lifted, 153 hbrs
c [decomp-53] removed 1 variables
c [basicprobe-7-4] 680 sched 26%, 0 failed, 0 lifted, 62 hbrs
c [basicprobe-7-5] 114 probes remain 4% after last round
c [basicprobe-7-5] 76 units = 75 failed (99%) + 1 lifted (1%)
c [basicprobe-7-5] removed 82 variables, found 6457 hbrs
c [bate-5] eliminated 25 asymmetric tautologies during probing
c [unhide-19] limit 1159051 with penalty 0 = 0 + 0
c [unhide-19-50] 0 units, 0 failed, 1319 tauts, 0 hbrs, 9053 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 327 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 2601 variables 100%
c [block-5] limit of 3622035 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 10 blocked clauses
c [block-5] 10 < 1/100 * 14277 = 142 considered unsuccessful
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 11
c [cce-10-1] eliminated 1 clauses out of 12 (8%) of length 8
c [cce-10-1] eliminated 2 clauses out of 264 (1%) of length 5
c [cce-10-1] eliminated 10 clauses out of 604 (2%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 14 large clauses in 1780417 steps
c [cce-10-1] allowing another 890208 steps for small clauses
c [cce-10-1] scheduling 10185 clauses = 8200 binary + 1985 ternary
c [cce-10-1] tried to eliminate 10185 small clauses 100%
c [cce-10-1] eliminated 285 binary clauses 3%
c [cce-10-1] eliminated 45 ternary clauses 2%
c [cce-10-1] eliminated 330 small clauses 3%
c [cce-10-1] eliminated 330 small clauses in 29715398 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 344 covered clauses in round 1
c [cce-10-2] incomplete large round (ATE)
c [cce-10-2] allowing another 142303 steps for small clauses
c [cce-10-2] scheduling 9855 clauses = 7915 binary + 1940 ternary
c [cce-10-2] tried to eliminate 54 small clauses 1%
c [cce-10-2] incomplete small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 344 covered clauses in TOTAL during 2 rounds
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 2601 variables 100%
c [elim-19] limit of 115905126 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 54 variables 2% in round 1 in 838770 steps
c [elim-19-1] backward subsumption/strengthening limit 838700
c [elim-19-1-1] backward checking 394 touched variables 15%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 1 and strengthened 1 clauses in 43693 steps
c [elim-19-1] rescheduled 12 variables 0% by backward subsumption
c [elim-19-2] no variable eliminated in round 2 in 4129 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 54 = 2% variables out of 2601 scheduled
c [bca-15] limit of 10000000 steps and 28307 added (scaled 2)
c [bca-15] 2209 out of 5096 literals actually usable 43%
c [bca-15] added 7 blocked clauses in 11919 steps
c [sweep-13] limit 869288 penalty 1 = 1 + 0
c [sweep-13-1] 232 pos 32.1% + 491 neg 67.9% = 723 sched 28.4% ret 1824
c [sweep-13-1] 878326 steps 47 queries 24.04 avg class size
c [sweep-13-1] 875 decisions 46 SAT calls 69.35 avg env size
c [sweep-13-1] 465 variables remain 18% (2082 retained 82%)
c [sweep-13-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-13] removed 0 vars in TOTAL (1 rounds, 46 queries)
c [sort-queue-19] sorted 2547 enqueued variables after 42291 conflicts
c [score-dist-19] active 0 (0%), one 0 (0%), zero 2547 (100%)
c [score-dist-19] max exp 0, different 1 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 136 variables 5.1% (2547 remain 1%)
c [simplification-19] removed 1010 irredundant clauses 6.8% (13875 remain 1%)
c [simplification-19] maximum reduction of 7% = max (5%, 7%)
c [simplification-19] large reduction 7% >= 5% limit
c [simplification-19] next conflict interval 2000 = 2000/1
c [simplification-19] penalized conflict interval 2000 = 1 * 2000
c [simplification-19] hard conflict limit 54291 (soft 44291 + delta 10000)
c [simplification-19] new conflict limit 44291 (hard 54291)
c 
c [simplification-20] limit 44291 conflicts (hard 54291) hit after 44294 conflicts
c [ternres-16] limit 5866090 with penalty 0 = 0 + 0
c [ternres-16] all 2547 free variables schedulable
c [ternres-16] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-16] fully completed ternary resolution
c [simpleprobe-8] all 2547 free variables schedulable
c [simpleprobe-8] limit 23464360 penalty 0 = 0 + 0
c [decomp-57] removed 1 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 1 variables, found 941 hbrs, 0 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 568 transitive binary clauses
c [cce-11] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-11-1] eliminated 1 clauses out of 7 (14%) of length 9
c [cce-11-1] eliminated 1 clauses out of 32 (3%) of length 7
c [cce-11-1] eliminated 7 clauses out of 273 (3%) of length 5
c [cce-11-1] eliminated 12 clauses out of 604 (2%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 22 large clauses in 2049264 steps
c [cce-11-1] allowing another 1024632 steps for small clauses
c [cce-11-1] scheduling 10833 clauses = 7794 binary + 3039 ternary
c [cce-11-1] tried to eliminate 10345 small clauses 95%
c [cce-11-1] eliminated 180 binary clauses 2%
c [cce-11-1] eliminated 132 ternary clauses 4%
c [cce-11-1] eliminated 312 small clauses 3%
c [cce-11-1] eliminated 312 small clauses in 30000008 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 334 covered clauses in round 1
c [cce-11] eliminated 334 covered clauses in TOTAL during 1 rounds
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 2546 variables 100%
c [elim-20] limit of 117321800 steps penalty 0 = 0 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 38 variables 1% in round 1 in 809314 steps
c [elim-20-1] backward subsumption/strengthening limit 809300
c [elim-20-1-1] backward checking 256 touched variables 10%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 1 and strengthened 0 clauses in 26503 steps
c [elim-20-1] rescheduled 2 variables 0% by backward subsumption
c [elim-20-2] no variable eliminated in round 2 in 482 steps
c [elim-20] fully completed in 2 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 38 = 1% variables out of 2546 scheduled
c [bca-16] limit of 10000000 steps and 27558 added (scaled 2)
c [bca-16] 2042 out of 5018 literals actually usable 41%
c [bca-16] added 0 blocked clauses in 13262 steps
c [sort-queue-20] sorted 2508 enqueued variables after 44294 conflicts
c [score-dist-20] active 0 (0%), one 0 (0%), zero 2508 (100%)
c [score-dist-20] max exp 0, different 1 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 39 variables 1.5% (2508 remain 1%)
c [simplification-20] removed 376 irredundant clauses 2.7% (13499 remain 1%)
c [simplification-20] maximum reduction of 3% = max (2%, 3%)
c [simplification-20] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-20] new conflict interval 14000
c [simplification-20] penalized conflict interval 14000 = 1 * 14000
c [simplification-20] hard conflict limit 68294 (soft 58294 + delta 10000)
c [simplification-20] new conflict limit 58294 (hard 68294)
c 
c [simplification-21] limit 58294 conflicts (hard 68294) hit after 58295 conflicts
c [quatres-12] found 909 quaternary clauses 33% in total
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [ternres-17] limit 6418490 with penalty 0 = 0 + 0
c [ternres-17] all 2508 free variables schedulable
c [ternres-17] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 200577 penalty 4 = 4 + 0
c [card-6] found 374 at-most-one constraints of average size 3.5
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 200577 for elimination
c [card-6] 374 out of 374 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [treelook-8] limit 641849 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 5005 literals 100%
c [treelook-8] scheduling used 130580 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 641849 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 642971 steps
c [treelook-8] 4937 literals remain 98%
c [treelook-8] 2483 variables remain to probed next time 99%
c [treelook-8] removed 0 variables, found 5564 hbrs
c [unhide-20] limit 641849 with penalty 1 = 1 + 0
c [unhide-20-52] 0 units, 0 failed, 1935 tauts, 0 hbrs, 38112 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 279 transitive binary clauses
c [cce-12] limit of 32092450 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 3 clauses out of 593 (1%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 3 large clauses in 1885137 steps
c [cce-12-1] allowing another 942568 steps for small clauses
c [cce-12-1] scheduling 10468 clauses = 7575 binary + 2893 ternary
c [cce-12-1] tried to eliminate 10468 small clauses 100%
c [cce-12-1] eliminated 7 binary clauses 0%
c [cce-12-1] eliminated 3 ternary clauses 0%
c [cce-12-1] eliminated 10 small clauses 0%
c [cce-12-1] eliminated 10 small clauses in 29094652 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 13 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 941096 steps for small clauses
c [cce-12-2] scheduling 10458 clauses = 7568 binary + 2890 ternary
c [cce-12-2] tried to eliminate 755 small clauses 7%
c [cce-12-2] incomplete small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 13 covered clauses in TOTAL during 2 rounds
c [cce-12] 13 < 1/100 * 13495 = 134 considered unsuccessful
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 2508 variables 100%
c [elim-21] limit of 128369803 steps penalty 0 = 0 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 2 variables 0% in round 1 in 805470 steps
c [elim-21-1] backward subsumption/strengthening limit 805400
c [elim-21-1-1] backward checking 28 touched variables 1%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 0 and strengthened 0 clauses in 4582 steps
c [elim-21] fully completed in 1 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 2 = 0% variables out of 2508 scheduled
c [elim-21] 2 < 1/100 * 2508 = 25 considered unsuccessful
c [sort-queue-21] sorted 2506 enqueued variables after 58295 conflicts
c [score-dist-21] active 0 (0%), one 0 (0%), zero 2506 (100%)
c [score-dist-21] max exp 0, different 1 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 2 variables 0.1% (2506 remain 1%)
c [simplification-21] removed 24 irredundant clauses 0.2% (13475 remain 1%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 20000
c [simplification-21] new conflict interval 34000
c [simplification-21] penalized conflict interval 34000 = 1 * 34000
c [simplification-21] hard conflict limit 109295 (soft 92295 + delta 17000)
c [simplification-21] new conflict limit 92295 (hard 109295)
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   54.2    2505    13475     64530   28638    516 21702   25   126   17  20%    332   35   26   15  175%
c -   58.8    2505    13475     88474   15777    559 21715   26   124   15  21%    245   22   23   18  128%
c 
c [simplification-22] limit 92295 conflicts (hard 109295) hit after 92295 conflicts
c [ternres-18] limit 8348938 with penalty 0 = 0 + 0
c [ternres-18] all 2505 free variables schedulable
c [ternres-18] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-60] removed 1 variables
c [basicprobe-8] limit 41744694 penalty 0 = 0 + 0
c [basicprobe-8-0] 151 sched 6%, 2 failed, 0 lifted, 218 hbrs
c [decomp-61] removed 2 variables
c [basicprobe-8-1] 690 sched 28%, 11 failed, 0 lifted, 729 hbrs
c [decomp-62] removed 13 variables
c [basicprobe-8-2] 689 sched 28%, 5 failed, 0 lifted, 415 hbrs
c [decomp-63] removed 6 variables
c [basicprobe-8-3] 684 sched 28%, 1 failed, 0 lifted, 410 hbrs
c [decomp-64] removed 1 variables
c [basicprobe-8-4] 683 sched 28%, 5 failed, 1 lifted, 56 hbrs
c [decomp-65] removed 9 variables
c [basicprobe-8-5] 681 sched 28%, 1 failed, 0 lifted, 98 hbrs
c [decomp-66] removed 1 variables
c [basicprobe-8-6] 681 sched 28%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-8-7] 259 probes remain 10% after last round
c [basicprobe-8-7] 26 units = 25 failed (96%) + 1 lifted (4%)
c [basicprobe-8-7] removed 32 variables, found 1934 hbrs
c [bate-6] eliminated 10 asymmetric tautologies during probing
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 350 transitive binary clauses
c [bca-17] limit of 10000000 steps and 26920 added (scaled 2)
c [bca-17] 1599 out of 4948 literals actually usable 32%
c [bca-17] added 5 blocked clauses in 22918 steps
c [sweep-14] limit 626170 penalty 2 = 2 + 0
c [sweep-14-1] 139 pos 30.6% + 315 neg 69.4% = 454 sched 18.4% ret 2019
c [sweep-14-1] 781317 steps 36 queries 26.28 avg class size
c [sweep-14-1] 609 decisions 35 SAT calls 105.46 avg env size
c [sweep-14-1] 335 variables remain 14% (2138 retained 86%)
c [sweep-14-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-14] removed 0 vars in TOTAL (1 rounds, 35 queries)
c [sort-queue-22] sorted 2473 enqueued variables after 92295 conflicts
c [score-dist-22] active 0 (0%), one 0 (0%), zero 2473 (100%)
c [score-dist-22] max exp 0, different 1 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 32 variables 1.3% (2473 remain 1%)
c [simplification-22] removed 295 irredundant clauses 2.2% (13180 remain 1%)
c [simplification-22] maximum reduction of 2% = max (1%, 2%)
c [simplification-22] geometric conflict interval increment 11333 = 34000 / 3
c [simplification-22] new conflict interval 45333
c [simplification-22] penalized conflict interval 45333 = 1 * 45333
c [simplification-22] hard conflict limit 160294 (soft 137628 + delta 22666)
c [simplification-22] new conflict limit 137628 (hard 160294)
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 -   66.3    2473    13180    126993   20799    554 21881   27   113   16  24%    591    7   30   22  137%
c 
c [simplification-23] limit 137628 conflicts (hard 160294) hit after 137629 conflicts
c [quatres-13] found 1090 quaternary clauses 28% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [ternres-19] limit 10743654 with penalty 0 = 0 + 0
c [ternres-19] all 2473 free variables schedulable
c [ternres-19] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-19] fully completed ternary resolution
c [simpleprobe-9] all 2473 free variables schedulable
c [simpleprobe-9] limit 42974616 penalty 0 = 0 + 0
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 0 variables, found 1001 hbrs, 0 units
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 424 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 268591350 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 1 clauses out of 33 (3%) of length 7
c [cce-13-1] eliminated 1 clauses out of 121 (1%) of length 6
c [cce-13-1] eliminated 3 clauses out of 262 (1%) of length 5
c [cce-13-1] eliminated 4 clauses out of 571 (1%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 9 large clauses in 1879113 steps
c [cce-13-1] allowing another 939556 steps for small clauses
c [cce-13-1] scheduling 9467 clauses = 7583 binary + 1884 ternary
c [cce-13-1] tried to eliminate 9467 small clauses 100%
c [cce-13-1] eliminated 132 binary clauses 2%
c [cce-13-1] eliminated 78 ternary clauses 4%
c [cce-13-1] eliminated 210 small clauses 2%
c [cce-13-1] eliminated 210 small clauses in 26278880 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] completed small and large (ACCE)
c [cce-13-1] eliminated 219 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 32 (3%) of length 7
c [cce-13-2] eliminated 1 clauses out of 120 (1%) of length 6
c [cce-13-2] eliminated 1 clauses out of 259 (0%) of length 5
c [cce-13-2] eliminated 2 clauses out of 567 (0%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 5 large clauses in 1853010 steps
c [cce-13-2] allowing another 926505 steps for small clauses
c [cce-13-2] scheduling 9257 clauses = 7451 binary + 1806 ternary
c [cce-13-2] tried to eliminate 9257 small clauses 100%
c [cce-13-2] eliminated 5 binary clauses 0%
c [cce-13-2] eliminated 8 ternary clauses 0%
c [cce-13-2] eliminated 13 small clauses 0%
c [cce-13-2] eliminated 13 small clauses in 25690171 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 18 covered clauses in round 2
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] allowing another 920442 steps for small clauses
c [cce-13-3] scheduling 9244 clauses = 7446 binary + 1798 ternary
c [cce-13-3] tried to eliminate 9244 small clauses 100%
c [cce-13-3] eliminated 3 binary clauses 0%
c [cce-13-3] eliminated 1 ternary clauses 0%
c [cce-13-3] eliminated 4 small clauses 0%
c [cce-13-3] eliminated 4 small clauses in 25597923 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 4 covered clauses in round 3
c [cce-13] eliminated 241 covered clauses in TOTAL during 3 rounds
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 2473 variables 100%
c [elim-22] limit of 107436541 steps penalty 1 = 1 + 0
c [elim-22] rescheduling of touched variables disabled
c [elim-22-1] eliminated 22 variables 1% in round 1 in 758177 steps
c [elim-22-1] backward subsumption/strengthening limit 758100
c [elim-22-1-1] backward checking 169 touched variables 7%
c [elim-22-1-1] fully completed backward checking in 1 rounds
c [elim-22-1] subsumed 0 and strengthened 0 clauses in 20001 steps
c [elim-22] fully completed in 1 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 22 = 1% variables out of 2473 scheduled
c [elim-22] 22 < 1/100 * 2473 = 24 considered unsuccessful
c [bca-18] limit of 10000000 steps and 26401 added (scaled 2)
c [bca-18] 1453 out of 4904 literals actually usable 30%
c [bca-18] added 0 blocked clauses in 33017 steps
c [sort-queue-23] sorted 2451 enqueued variables after 137629 conflicts
c [score-dist-23] active 0 (0%), one 0 (0%), zero 2451 (100%)
c [score-dist-23] max exp 0, different 1 (100%)
c [score-dist-23] median active exp 0, avg 0.0
c [simplification-23] removed 22 variables 0.9% (2451 remain 1%)
c [simplification-23] removed 261 irredundant clauses 2.0% (12919 remain 1%)
c [simplification-23] maximum reduction of 2% = max (1%, 2%)
c [simplification-23] geometric conflict interval increment 15111 = 45333 / 3
c [simplification-23] new conflict interval 60444
c [simplification-23] penalized conflict interval 60444 = 1 * 60444
c [simplification-23] hard conflict limit 228295 (soft 198073 + delta 30222)
c [simplification-23] new conflict limit 198073 (hard 228295)
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 -   73.2    2451    12919    163245   23519    650 22099   21    66   16  33%    775  -39   18   23   77%
c -   77.8    2451    12919    196594   24265    662 22105   28   113   17  25%    874   18   27   24  114%
c 
c [simplification-24] limit 198073 conflicts (hard 228295) hit after 198074 conflicts
c [ternres-20] limit 13906045 with penalty 0 = 0 + 0
c [ternres-20] all 2451 free variables schedulable
c [ternres-20] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-20] fully completed ternary resolution
c [unhide-21] limit 695302 with penalty 2 = 2 + 0
c [unhide-21-54] 0 units, 0 failed, 1213 tauts, 0 hbrs, 31042 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 272 transitive binary clauses
c [cce-14] limit of 69530229 steps penalty 0 = 0 + 0
c [cce-14-1] completed large round (ATE)
c [cce-14-1] allowing another 914015 steps for small clauses
c [cce-14-1] scheduling 10084 clauses = 7399 binary + 2685 ternary
c [cce-14-1] tried to eliminate 10084 small clauses 100%
c [cce-14-1] eliminated 2 binary clauses 0%
c [cce-14-1] eliminated 6 ternary clauses 0%
c [cce-14-1] eliminated 8 small clauses 0%
c [cce-14-1] eliminated 8 small clauses in 26698959 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 8 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 913078 steps for small clauses
c [cce-14-2] scheduling 10076 clauses = 7397 binary + 2679 ternary
c [cce-14-2] tried to eliminate 10076 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 8 covered clauses in TOTAL during 2 rounds
c [cce-14] 8 < 1/100 * 12917 = 129 considered unsuccessful
c [sort-queue-24] sorted 2451 enqueued variables after 198074 conflicts
c [score-dist-24] active 0 (0%), one 0 (0%), zero 2451 (100%)
c [score-dist-24] max exp 0, different 1 (100%)
c [score-dist-24] median active exp 0, avg 0.0
c [simplification-24] removed 0 variables 0.0% (2451 remain 1%)
c [simplification-24] removed 10 irredundant clauses 0.1% (12909 remain 1%)
c [simplification-24] maximum reduction of 0% = max (0%, 0%)
c [simplification-24] full geometric conflict interval increment 60444
c [simplification-24] new conflict interval 120888
c [simplification-24] penalized conflict interval 120888 = 1 * 120888
c [simplification-24] hard conflict limit 379406 (soft 318962 + delta 60444)
c [simplification-24] new conflict limit 318962 (hard 379406)
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 -   83.9    2451    12909    230581   25386    678 20674   24    73   15  33%    935  -17   23   24   94%
c -   88.0    2451    12909    264535   27128    681 20676   23    80   15  29%    971   -4   21   24   90%
c -   92.4    2451    12909    297986   26509    692 20681   25    90   17  28%    992    9   23   24   96%
c 
c [simplification-25] limit 318962 conflicts (hard 379406) hit after 319635 conflicts
c [gauss-6] limit 254495 penalty 4 = 4 + 0
c [gauss-6] extracted 3 xors of average arity 3.0
c [gauss-6] connected 9 occurrences of 6 variables (average 1.5)
c [gauss-6] limit 254495 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-9] limit 1017980 penalty 1 = 1 + 0 boost 1
c [treelook-9] scheduled 4892 literals 100%
c [treelook-9] scheduling used 187621 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 1017980 penalty 1 = 1 + 0 boost 1
c [treelook-9] used 1024274 steps
c [treelook-9] 4760 literals remain 97%
c [treelook-9] 2427 variables remain to probed next time 99%
c [treelook-9] removed 0 variables, found 7695 hbrs
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 394 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 2451 variables 100%
c [block-6] limit of 12724756 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 0 blocked clauses
c [bca-19] limit of 10000000 steps and 26381 added (scaled 2)
c [bca-19] 1504 out of 4904 literals actually usable 31%
c [bca-19] added 3 blocked clauses in 50908 steps
c [sort-queue-25] sorted 2451 enqueued variables after 319635 conflicts
c [score-dist-25] active 0 (0%), one 0 (0%), zero 2451 (100%)
c [score-dist-25] max exp 0, different 1 (100%)
c [score-dist-25] median active exp 0, avg 0.0
c [simplification-25] removed 0 variables 0.0% (2451 remain 1%)
c [simplification-25] removed 0 irredundant clauses 0.0% (12909 remain 1%)
c [simplification-25] maximum reduction of 0% = max (0%, 0%)
c [simplification-25] full geometric conflict interval increment 120888
c [simplification-25] new conflict interval 241776
c [simplification-25] penalized conflict interval 241776 = 1 * 241776
c [simplification-25] hard conflict limit 682299 (soft 561411 + delta 120888)
c [simplification-25] new conflict limit 561411 (hard 682299)
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 -   97.9    2451    12909    333199   27371    696 27988   25    67   16  37%   1005   -8   31   23  133%
c -  102.7    2451    12909    368867   27573    706 27993   24    65   17  36%   1013  -13   23   24   95%
c -  108.3    2451    12909    405632   27943    720 27997   28   100   14  28%   1018   24   30   25  123%
c -  112.8    2451    12909    442992   29772    724 27999   26    93   18  28%   1021   17   31   25  126%
c -  118.2    2451    12909    479674   29701    736 28003   23    53   17  43%   1022  -28   23   25   93%
c -  123.6    2451    12909    517899   30352    740 28004   20    46   18  44%   1023  -29   19   24   78%
c -  129.2    2451    12909    556725   31340    747 28006   23    64   18  35%   1023   -7   20   24   85%
c 
c [simplification-26] limit 561411 conflicts (hard 682299) hit after 570341 conflicts
c [quatres-14] found 1316 quaternary clauses 21% in total
c [quatres-14-1] removed 3 duplicate quaternary clauses
c [quatres-14-2] added 1 single-self-subsuming ternary resolvents
c [ternres-21] limit 17333539 with penalty 1 = 1 + 0
c [ternres-21] all 2451 free variables schedulable
c [ternres-21] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-21] fully completed ternary resolution
c [basicprobe-9] limit 173335392 penalty 0 = 0 + 0
c [basicprobe-9-0] 266 sched 11%, 4 failed, 1 lifted, 1262 hbrs
c [decomp-75] removed 5 variables
c [basicprobe-9-1] 680 sched 28%, 7 failed, 0 lifted, 2125 hbrs
c [decomp-76] removed 7 variables
c [basicprobe-9-2] 671 sched 28%, 1 failed, 0 lifted, 263 hbrs
c [decomp-77] removed 1 variables
c [basicprobe-9-3] 669 sched 27%, 1 failed, 0 lifted, 58 hbrs
c [decomp-78] removed 1 variables
c [basicprobe-9-4] 671 sched 28%, 0 failed, 0 lifted, 27 hbrs
c [basicprobe-9-5] 671 sched 28%, 0 failed, 0 lifted, 16 hbrs
c [basicprobe-9-6] 671 sched 28%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-9-7] 671 sched 28%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-9-8] 671 sched 28%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-9-8] round limit 8 hit
c [basicprobe-9-8] 14 units = 13 failed (93%) + 1 lifted (7%)
c [basicprobe-9-8] removed 14 variables, found 3793 hbrs
c [bate-7] eliminated 3 asymmetric tautologies during probing
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 422 transitive binary clauses
c [cce-15] limit of 86667696 steps penalty 1 = 1 + 0
c [cce-15-1] eliminated 1 clauses out of 39 (3%) of length 7
c [cce-15-1] eliminated 1 clauses out of 260 (0%) of length 5
c [cce-15-1] eliminated 4 clauses out of 569 (1%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 6 large clauses in 1822171 steps
c [cce-15-1] allowing another 911085 steps for small clauses
c [cce-15-1] scheduling 9173 clauses = 7417 binary + 1756 ternary
c [cce-15-1] tried to eliminate 9173 small clauses 100%
c [cce-15-1] eliminated 49 binary clauses 1%
c [cce-15-1] eliminated 13 ternary clauses 1%
c [cce-15-1] eliminated 62 small clauses 1%
c [cce-15-1] eliminated 62 small clauses in 25235271 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 68 covered clauses in round 1
c [cce-15-2] eliminated 1 clauses out of 16 (6%) of length 8
c [cce-15-2] eliminated 1 clauses out of 109 (1%) of length 6
c [cce-15-2] eliminated 3 clauses out of 565 (1%) of length 4
c [cce-15-2] completed large round (ACCE)
c [cce-15-2] eliminated 5 large clauses in 1810725 steps
c [cce-15-2] allowing another 905362 steps for small clauses
c [cce-15-2] scheduling 9111 clauses = 7368 binary + 1743 ternary
c [cce-15-2] tried to eliminate 9111 small clauses 100%
c [cce-15-2] eliminated 2 binary clauses 0%
c [cce-15-2] eliminated 2 small clauses 0%
c [cce-15-2] eliminated 2 small clauses in 25036990 steps
c [cce-15-2] completed small round (ACCE)
c [cce-15-2] eliminated 7 covered clauses in round 2
c [cce-15-3] completed large round (ACCE)
c [cce-15-3] allowing another 899695 steps for small clauses
c [cce-15-3] scheduling 9109 clauses = 7366 binary + 1743 ternary
c [cce-15-3] tried to eliminate 9109 small clauses 100%
c [cce-15-3] completed small round (ACCE)
c [cce-15-3] eliminated 0 covered clauses in round 3
c [cce-15] eliminated 75 covered clauses in TOTAL during 3 rounds
c [cce-15] 75 < 1/100 * 12815 = 128 considered unsuccessful
c [elim-23] scheduling all variables this time
c [elim-23] scheduled 2437 variables 100%
c [elim-23] almost no limit of 100000000000 steps
c [elim-23] rescheduling of touched variables disabled
c [elim-23-1] eliminated 29 variables 1% in round 1 in 747405 steps
c [elim-23-1] backward subsumption/strengthening limit 747400
c [elim-23-1-1] backward checking 172 touched variables 7%
c [elim-23-1-1] fully completed backward checking in 1 rounds
c [elim-23-1] subsumed 0 and strengthened 0 clauses in 17687 steps
c [elim-23] fully completed in 1 rounds
c [elim-23] transition to [ all 0 rem 0 ] state
c [elim-23] eliminated 29 = 1% variables out of 2437 scheduled
c [bca-20] limit of 10000000 steps and 26006 added (scaled 2)
c [bca-20] 1411 out of 4818 literals actually usable 29%
c [bca-20] added 0 blocked clauses in 46883 steps
c [sweep-15] limit 1300015 penalty 3 = 3 + 0
c [sweep-15-1] 110 pos 33.2% + 221 neg 66.8% = 331 sched 13.7% ret 2077
c [sweep-15-1] 1471200 steps 26 queries 33.00 avg class size
c [sweep-15-1] 596 decisions 25 SAT calls 117.92 avg env size
c [sweep-15-1] 272 variables remain 11% (2136 retained 89%)
c [sweep-15-1] removed 0 vars (0 failed, 1 eqs, 0 impls)
c [sweep-15] removed 0 vars in TOTAL (1 rounds, 25 queries)
c [sort-queue-26] sorted 2408 enqueued variables after 570341 conflicts
c [score-dist-26] active 0 (0%), one 0 (0%), zero 2408 (100%)
c [score-dist-26] max exp 0, different 1 (100%)
c [score-dist-26] median active exp 0, avg 0.0
c [simplification-26] removed 43 variables 1.8% (2408 remain 1%)
c [simplification-26] removed 188 irredundant clauses 1.5% (12721 remain 1%)
c [simplification-26] maximum reduction of 2% = max (2%, 1%)
c [simplification-26] geometric conflict interval increment 80592 = 241776 / 3
c [simplification-26] new conflict interval 322368
c [simplification-26] penalized conflict interval 322368 = 1 * 322368
c [simplification-26] hard conflict limit 1053893 (soft 892709 + delta 161184)
c [simplification-26] new conflict limit 892709 (hard 1053893)
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 -  139.3    2408    12721    596106   31370    672 29252   24    62   17  39%   1024  -10   24   24   99%
c -  145.8    2408    12721    636420   33217    673 29254   18    40   17  46%   1024  -22   20   22   93%
c -  153.3    2408    12721    675740   31607    686 29257   27    90   19  30%   1024   18   23   24   96%
c -  159.6    2408    12721    717835   33523    692 29260   23    80   19  29%   1024    4   23   24   95%
c -  165.5    2408    12721    759343   35316    703 29262   17    34   19  49%   1024  -36   16   23   69%
c -  173.6    2408    12721    800334   34329    707 29264   28   112   18  25%   1024   55   28   21  130%
c -  181.9    2408    12721    843005   32181    725 29270   27   103   19  26%   1024   20   28   25  115%
c -  189.6    2408    12721    889769   37472    725 29270   20    37   21  55%   1024  -26   19   22   85%
c 
c [simplification-27] limit 892709 conflicts (hard 1053893) hit after 895438 conflicts
c [ternres-22] limit 56794194 with penalty 0 = 0 + 0
c [ternres-22] all 2408 free variables schedulable
c [ternres-22] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-22] fully completed ternary resolution
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 291 transitive binary clauses
c [sort-queue-27] sorted 2408 enqueued variables after 895438 conflicts
c [score-dist-27] active 0 (0%), one 0 (0%), zero 2408 (100%)
c [score-dist-27] max exp 0, different 1 (100%)
c [score-dist-27] median active exp 0, avg 0.0
c [simplification-27] removed 0 variables 0.0% (2408 remain 1%)
c [simplification-27] removed 0 irredundant clauses 0.0% (12721 remain 1%)
c [simplification-27] maximum reduction of 0% = max (0%, 0%)
c [simplification-27] full geometric conflict interval increment 322368
c [simplification-27] new conflict interval 644736
c [simplification-27] penalized conflict interval 644736 = 1 * 644736
c [simplification-27] hard conflict limit 1862542 (soft 1540174 + delta 322368)
c [simplification-27] new conflict limit 1540174 (hard 1862542)
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 -  195.7    2408    12721    932264   37889    733 28981   21    60   18  35%   1024    3   23   21  110%
c -  202.8    2408    12721    975425   36250    747 28982   20    54   19  37%   1024  -18   18   24   76%
c -  210.1    2408    12721   1021443   37988    757 28982   24    70   19  34%   1024   -4   27   24  110%
c -  217.7    2408    12721   1066650   38433    763 28990   27    84   16  33%   1024    3   25   25   98%
c -  226.2    2408    12721   1112761   40001    763 28990   20    36   22  55%   1024  -28   19   23   82%
c -  236.0    2408    12721   1158520   40627    765 28990   20    32   23  61%   1024  -18   21   22   96%
c -  246.3    2408    12721   1204025   38751    780 28990   35   134   21  26%   1024   68   38   25  154%
c -  253.6    2408    12721   1252986   41271    784 28991   22    40   17  55%   1024  -27   19   24   78%
c -  262.1    2408    12721   1300620   41818    791 28992   24    48   22  50%   1024  -20   23   25   92%
c -  269.4    2408    12721   1348429   41977    800 28992   21    72   19  30%   1024    5   28   24  118%
c -  278.2    2408    12721   1397290   41007    814 28993   27    88   21  31%   1024    8   18   26   70%
c -  287.6    2408    12721   1448680   43858    817 28994   26    74   22  36%   1024   10   31   24  131%
c -  297.5    2408    12721   1498657   42339    829 28997   33   117   18  28%   1024   48   31   24  128%
c -  305.9    2408    12721   1550964   43486    839 29001   24    43   18  56%   1024  -30   23   25   92%
c 
c [simplification-28] limit 1540174 conflicts (hard 1862542) hit after 1562480 conflicts
c [quatres-15] found 1583 quaternary clauses 17% in total
c [card-7] limit 3311893 penalty 4 = 4 + 0
c [card-7] found 1118 at-most-one constraints of average size 3.4
c [card-7] found 17 at-most-two constraints of average size 4.2
c [card-7] using previous limit 3311893 for elimination
c [card-7] 1135 out of 1135 constraints (100%) meet size limits
c [card-7] no units found
c [card-7] generated 1500 at-most-one constraints, 1266 used 84%
c [card-7] exported 6026 binary clauses, 4.8 per/constraint
c [decomp-85] removed 1 variables
c [simpleprobe-10] all 2407 free variables schedulable
c [simpleprobe-10] limit 100000000 penalty 1 = 1 + 0
c [simpleprobe-10] fully completed simple probing
c [simpleprobe-10] removed 0 variables, found 1853 hbrs, 0 units
c [unhide-22] limit 2500000 with penalty 3 = 3 + 0
c [unhide-22-57] 0 units, 0 failed, 7630 tauts, 0 hbrs, 137293 literals
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 296 transitive binary clauses
c [elim-24] scheduling all variables this time
c [elim-24] scheduled 2407 variables 100%
c [elim-24] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-24] rescheduling of touched variables disabled
c [elim-24-1] eliminated 4 variables 0% in round 1 in 743196 steps
c [elim-24-1] backward subsumption/strengthening limit 743100
c [elim-24-1-1] backward checking 26 touched variables 1%
c [elim-24-1-1] fully completed backward checking in 1 rounds
c [elim-24-1] subsumed 0 and strengthened 0 clauses in 4146 steps
c [elim-24] fully completed in 1 rounds
c [elim-24] transition to [ all 0 rem 0 ] state
c [elim-24] eliminated 4 = 0% variables out of 2407 scheduled
c [elim-24] 4 < 1/100 * 2407 = 24 considered unsuccessful
c [bca-21] limit of 10000000 steps and 25978 added (scaled 2)
c [bca-21] 1295 out of 4808 literals actually usable 27%
c [bca-21] added 1 blocked clauses in 57107 steps
c [sort-queue-28] sorted 2403 enqueued variables after 1562480 conflicts
c [score-dist-28] active 0 (0%), one 0 (0%), zero 2403 (100%)
c [score-dist-28] max exp 0, different 1 (100%)
c [score-dist-28] median active exp 0, avg 0.0
c [simplification-28] removed 5 variables 0.2% (2403 remain 1%)
c [simplification-28] removed 14 irredundant clauses 0.1% (12707 remain 1%)
c [simplification-28] maximum reduction of 0% = max (0%, 0%)
c [simplification-28] full geometric conflict interval increment 644736
c [simplification-28] conflict interval soft limit 1000000 reached
c [simplification-28] new conflict interval 1000000
c [simplification-28] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-28] hard conflict limit 3062480 (soft 2562480 + delta 500000)
c [simplification-28] new conflict limit 2562480 (hard 3062480)
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 -  316.0    2403    12707   1603577   45323    824 28961   24    75   17  33%   1024   14   27   24  112%
c -  324.6    2403    12707   1655249   45271    837 28961   23    56   21  41%   1024  -10   22   24   91%
c -  333.9    2403    12707   1708137   45499    841 28962   28    88   21  32%   1024   17   28   26  108%
c -  343.4    2403    12707   1761707   47384    855 28966   25    57   22  44%   1024  -15   26   26  101%
c -  353.3    2403    12707   1814547   47862    859 28967   29    95   18  31%   1024   24   35   26  135%
c -  362.7    2403    12707   1868240   47383    860 28969   25    72   23  35%   1024    3   13   26   50%
c -  373.5    2403    12707   1923979   47493    866 28970   29   100   22  29%   1024   33   33   24  136%
c -  383.4    2403    12707   1980804   49058    870 28974   26    68   18  38%   1024   -1   26   25  105%
c -  395.5    2403    12707   2037058   50142    871 28975   27    90   24  30%   1024   34   31   22  137%
c -  406.6    2403    12707   2093432   48615    879 28977   22    48   24  45%   1024  -21   21   25   84%
c -  417.2    2403    12707   2152266   49975    888 28978   32   107   24  30%   1024   42   33   24  134%
c -  429.2    2403    12707   2210817   50597    898 28982   31   106   25  29%   1024   32   27   26  105%
c -  439.8    2403    12707   2269760   52015    904 28984   23    51   24  46%   1024  -16   19   25   77%
c -  451.2    2403    12707   2328839   51210    908 28988   28    75   24  37%   1024   -2   29   27  109%
c -  461.6    2403    12707   2389762   52876    921 28988   25    81   19  32%   1024    7   33   25  130%
c -  472.5    2403    12707   2451263   54153    923 28990   19    32   26  60%   1024  -23   21   23   91%
c -  485.1    2403    12707   2511248   52484    930 28995   26    76   24  34%   1024    0   19   26   72%
c -  496.2    2403    12707   2574463   55272    932 28995   22    35   23  62%   1024  -24   20   24   85%
c 
c [simplification-29] limit 2562480 conflicts (hard 3062480) hit after 2595377 conflicts
c [ternres-23] limit 95500271 with penalty 1 = 1 + 0
c [ternres-23] all 2403 free variables schedulable
c [ternres-23] 14 ternary resolvents (0 bin, 14 trn)
c [ternres-23] fully completed ternary resolution
c [transred-25] limit 2000000 with penalty 0 = 0 + 0
c [transred-25] removed 242 transitive binary clauses
c [cce-16] limit of 238750677 steps penalty 2 = 2 + 0
c [cce-16-1] eliminated 1 clauses out of 255 (0%) of length 5
c [cce-16-1] completed large round (ATE)
c [cce-16-1] eliminated 1 large clauses in 1763828 steps
c [cce-16-1] allowing another 881914 steps for small clauses
c [cce-16-1] scheduling 9951 clauses = 7317 binary + 2634 ternary
c [cce-16-1] tried to eliminate 9951 small clauses 100%
c [cce-16-1] eliminated 8 binary clauses 0%
c [cce-16-1] eliminated 3 ternary clauses 0%
c [cce-16-1] eliminated 11 small clauses 0%
c [cce-16-1] eliminated 11 small clauses in 26233635 steps
c [cce-16-1] completed small round (ATE)
c [cce-16-1] eliminated 12 covered clauses in round 1
c [cce-16-2] completed large round (ATE)
c [cce-16-2] allowing another 873873 steps for small clauses
c [cce-16-2] scheduling 9940 clauses = 7309 binary + 2631 ternary
c [cce-16-2] tried to eliminate 9940 small clauses 100%
c [cce-16-2] completed small round (ATE)
c [cce-16-2] eliminated 0 covered clauses in round 2
c [cce-16] eliminated 12 covered clauses in TOTAL during 2 rounds
c [cce-16] 12 < 1/100 * 12706 = 127 considered unsuccessful
c [bca-22] limit of 10000000 steps and 25953 added (scaled 2)
c [bca-22] 1168 out of 4808 literals actually usable 24%
c [bca-22] added 0 blocked clauses in 77916 steps
c [sort-queue-29] sorted 2403 enqueued variables after 2595377 conflicts
c [score-dist-29] active 0 (0%), one 0 (0%), zero 2403 (100%)
c [score-dist-29] max exp 0, different 1 (100%)
c [score-dist-29] median active exp 0, avg 0.0
c [simplification-29] removed 0 variables 0.0% (2403 remain 1%)
c [simplification-29] removed 13 irredundant clauses 0.1% (12694 remain 1%)
c [simplification-29] maximum reduction of 0% = max (0%, 0%)
c [simplification-29] full geometric conflict interval increment 1000000
c [simplification-29] conflict interval soft limit 1000000 reached
c [simplification-29] new conflict interval 1000000
c [simplification-29] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-29] hard conflict limit 4095377 (soft 3595377 + delta 500000)
c [simplification-29] new conflict limit 3595377 (hard 4095377)
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 -  510.9    2403    12694   2635769   54970    951 28764   25    73   24  34%   1024    6   29   25  116%
c -  522.8    2403    12694   2698254   54713    962 28766   27    76   20  35%   1024    3   24   27   91%
c -  534.7    2403    12694   2762474   57053    964 28766   25    64   27  38%   1024   -7   29   25  116%
c -  547.5    2403    12694   2825300   56339    980 28766   25    74   24  34%   1024    0   20   26   77%
c -  561.6    2403    12694   2890011   56428    990 28770   27    88   27  31%   1024   12   24   26   90%
c -  575.7    2403    12694   2956408   57823    999 28773   21    34   24  61%   1024  -33   21   24   87%
c -  590.8    2403    12694   3022797   58742   1004 28773   26    72   25  36%   1024   15   23   23  102%
c -  608.7    2403    12694   3089447   59308   1010 28774   19    30   25  64%   1024  -21   20   22   95%
c -  623.9    2403    12694   3155877   58757   1018 28775   28    80   27  35%   1024   13   35   25  141%
c -  637.2    2403    12694   3224410   60858   1027 28776   23    42   24  55%   1024  -22   22   25   88%
c -  652.8    2403    12694   3291499   62440   1031 28776   25    64   27  39%   1024    2   24   25   95%
c -  666.9    2403    12694   3358663   59927   1039 28776   31   105   26  30%   1024   40   35   25  138%
c -  681.7    2403    12694   3429280   60948   1044 28778   27    73   21  38%   1024   -2   30   27  113%
c -  696.9    2403    12694   3501020   63650   1046 28778   20    36   29  56%   1024  -16   21   24   87%
c -  712.6    2403    12694   3570278   62574   1057 28780   27    83   27  33%   1024   16   29   26  111%
c 
c [simplification-30] limit 3595377 conflicts (hard 4095377) hit after 3601272 conflicts
c [ternres-24] limit 200000000 with penalty 0 = 0 + 0
c [ternres-24] all 2403 free variables schedulable
c [ternres-24] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-24] fully completed ternary resolution
c [transred-26] limit 2000000 with penalty 0 = 0 + 0
c [transred-26] removed 238 transitive binary clauses
c [sort-queue-30] sorted 2403 enqueued variables after 3601272 conflicts
c [score-dist-30] active 0 (0%), one 0 (0%), zero 2403 (100%)
c [score-dist-30] max exp 0, different 1 (100%)
c [score-dist-30] median active exp 0, avg 0.0
c [simplification-30] removed 0 variables 0.0% (2403 remain 1%)
c [simplification-30] removed 0 irredundant clauses 0.0% (12694 remain 1%)
c [simplification-30] maximum reduction of 0% = max (0%, 0%)
c [simplification-30] full geometric conflict interval increment 1000000
c [simplification-30] new conflict interval 2000000
c [simplification-30] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-30] hard conflict limit 6601272 (soft 5601272 + delta 1000000)
c [simplification-30] new conflict limit 5601272 (hard 6601272)
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 -  728.4    2403    12694   3642001   63284   1069 28544   26    71   25  36%   1024    1   21   26   83%
c -  742.8    2403    12694   3713864   64464   1075 28546   25    67   25  37%   1024   -3   24   26   95%
c -  762.7    2403    12694   3785430   65546   1079 28546   19    32   27  59%   1024  -24   18   23   78%
c -  781.8    2403    12694   3856884   64356   1083 28551   26    64   23  40%   1024   -8   29   26  115%
c -  798.4    2403    12694   3930711   65509   1086 28551   27    83   28  32%   1024    8   25   26   97%
c -  814.4    2403    12694   4004707   67190   1090 28553   25    66   27  39%   1024   -6   27   26  104%
c -  830.1    2403    12694   4078388   66267   1096 28554   23    71   26  32%   1024   10   21   23   91%
c -  848.2    2403    12694   4154029   65685   1103 28556   28    85   29  33%   1024   15   20   25   80%
c -  866.5    2403    12694   4231236   67447   1108 28558   27    78   22  34%   1024   -1   24   27   91%
c -  885.1    2403    12694   4307786   68645   1111 28558   24    39   28  60%   1024  -25   30   26  116%
c -  902.5    2403    12694   4384709   69348   1116 28559   25    80   29  32%   1024   17   21   25   84%
c -  921.1    2403    12694   4462182   69120   1120 28559   24    69   23  35%   1024    5   20   25   79%
c -  938.5    2403    12694   4540528   69731   1127 28562   25    49   27  52%   1024  -21   26   26  102%
c -  958.3    2403    12694   4619680   70690   1131 28562   23    45   28  51%   1024  -19   25   25  100%
c -  980.5    2403    12694   4699109   70594   1141 28565   29    86   30  34%   1024   14   24   27   91%
c -  997.7    2403    12694   4779792   72350   1148 28565   27    86   30  32%   1024   12   28   26  107%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 308 basic ate = 292 trn 95% + 16 lrg 5% in 7 updates
c bcas: 22 count, 130 added (55 skipped), 828692 steps
c bkwd: tried 250227 clauses, 499649 lits, 2.00 lits/clause
c bkwd: checked 5912844 occs, 23.63 occs/clause, 11.83 occs/lit
c bkwd: subsumed 55 binary, 302 ternary, 250 large
c bkwd: strengthened 36 binary, 0 ternary (0% self), 677 large (0% self)
c blkd: 6 bces, 916 removed, 1289483 resolutions, 3558236 steps
c blkd: 1785 blocking literals 0%, 12 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 7 count, 0 units, 6026 am1, 21462189 steps
c card: 48 rescheduled, 475 eliminated, 30315 resolved, 66659 subsumed
c card: 19701 at-most-one constraints found, average size 4.22
c card: 19701 at-most-one constraints used 100%, average size 4.22
c card: 17 at-most-two constraints found, average size 4.24
c card: 17 at-most-two constraints used 100%, average size 4.24
c cces: 16 cces, 12268 eliminated, 11306 ate 92%, 962 abce 8%
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: 3541879 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 218 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 88 decompositions, 66210 equivalent 29%
c deco: 2471 decision-only clauses 0%, 48% reduction
c decs: 16633077 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 24 elims, 22694 eliminated 10%, 131 pure 1%
c elms: 72 rounds, 3.0 rounds/bve
c elms: 21799 small 96%, 752 large 3%
c elms: 91558 tried small, 21800 succeeded 24%, 69758 failed 76%
c elms: 7357 subsumed, 10405 strengthened, 587 blocked
c elms: 6638363 copies, 6006068 resolutions, 2985471 ipos
c elms: 1641517 subchks, 936148 strchks
c gaus: 6 extractions, 177 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8260792 steps, 4130396 extr 50%, 3231 elim 0%
c glue: 24.7 orig avg, 24.7 real avg, 4.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 253512 = 47478 simple 19% + 189761 trn 75% + 16273 lrg 6%, 2265 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4785174 clauses, 87.4 length
c lrnd: 418200599 lits = 558615560 orig - 140414961 removed 25%
c lrnd: 2541543 uips 53%, 1516117 flips 32%
c mins: 4777645 mins 100%, 522 bin 0%, 4421 size 0%
c mins: 1090889391 poisoned searches, 200914752 hits, 18% hit rate
c mins: 1442628912 used twice searches, 55098898 hits, 4% hit rate
c move: moved 9447, 6943 bin 73%, 2504 trn 27%
c otfs: 5911 driving 21%, 22134 restarting 79%
c otfs: str 28045, 27993 red 100%, 52 irr 0%
c otfs: str 28045, 0 bin 0%, 51 trn 0%, 27994 lrg 100%
c otfs: sub 3, 3 red 100%, 0 irr 0%
c otfs: sub 3, 0 bin 0%, 0 trn 0%, 3 lrg 100%
c phas: 1 computed, 25352 set, 0 pos (0%), 25352 neg (100%)
c prbs: 9 basic, 33076 probed, 1582 failed, 326 lifted
c prbs: 10 simple, 423844 probed, 2107 failed, 30267 eqs
c prbs: 9 treelook, 356 probed, 40 failed, 0 lifted
c prom: 816079 locked 8% out of 9978914 tried
c prps: 609874057 props, 35 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 15 count, 28 quat, 7 self1, 0 self2, 67 dup
c queu: 30 sorted, 16633078 next (0 steps 0.00)
c queu: 489542 enq (489511 steps 1.00), 0 deq 0%
c redc: 8116 clauses 12%, 65424 tried 1%, 11 sat 0%
c redc: 21597 lits 2%, 924036 tried 0%, 11 sat 0%
c redc: 675 times jump level reduced, 19.8 levels on average
c reds: 85 count, 56349.5 conflicts per reduce
c reds: 0 memlim 0%, 85 arith 100%
c reds: 3910396 collected 86%, 652441 retired 14%
c rmbd: 4568 removed, 1886 red 41%
c rsts: 37954 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: 30 count, 29 confs 97%, 0 vars 0%
c simp: 0 its 0%, 1 bin 3%, 0 trns 0%
c subl: 4785174 count (2995030 tried 0.6), 100979 sub out of 4782864 (2.1%)
c swps: 15 count, 17 rounds, 1705 queries (100.3/round)
c swps: 1447 sat calls, 51 unsat (1.0% success rate)
c swps: 17058 decisions 11.8, 1377 conflicts 1.0
c swps; 223.8 avg class size, 65.9 avg environment size
c swps: 1 failed, 206 impls, 287 equivs
c swp0: 563 type 0 queries, 376 unsat (66.8%), 473 sat (84.0%)
c swp1: 1142 type 1 queries, 811 unsat (71.0%), 945 sat (82.7%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 33266830 calls to obtain time
c tops: 138237 fixed 60%, 57 its, 84029.96 confs/it
c trds: 26 transitive reductions, 11234 removed, 185 failed
c trds: 74325 nodes, 187819 edges, 51794725 steps
c trim: 1488384 words, 5.7 MB
c trnr: 24 count, 3 bin, 1410 trn, 36900885 steps
c unhd: 22 count, 57 rounds, 23626554 steps
c unhd: 3206 non-trivial sccs of average size 2.3
c unhd: 130 units, 128 bin, 2 trn, 0 lrg
c unhd: 4400 failed, 4372 stamp, 0 lits, 12 bin, 6 trn, 0 lrg
c unhd: 108333 tauts, 8959 bin 8%, 1822 trn 2%, 295 lrg 0%
c unhd: 108333 tauts, 97257 stamp 90%, 69335 red 64%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 534790 str, 128 bin 0%, 1389 trn 0%, 533273 lrg 100%, 529241 red 99%
c vars: 2403 remaining 1% and 227141 removed 99% out of 229544
c vars: 138237 fixed 60%, 22694 eliminated 10%, 66210 equivalent 29%
c vsts: 41352274384 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 69.9 search visits per propagation, 8590.6 per conflict
c wchs: 14363819643 pushed, 17959642 enlarged, 462 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        4782892       3910396        652441     150686322      34805334       2478849
c 
c  0 0         21362   0      2412   0         0   0  46231542  31   6254918  18    274809  11     0.7
c  1 5         22802   0      7142   0      9631   1  18927839  13   3810242  11    196588   8     0.3
c  2 6        159190   3     89850   2     47444   7  38838354  26<  9054233  26<   631973  25     1.7
c  3 9        595583  12    467762  12     94837  15  28355779  19   8012283  23    764424  31<    4.7
c  4 14      1228500  26   1059379  27    138475  21  10346341   7   3745520  11    346333  14     9.2
c  5 21      1445219  30<  1237964  32<   159367  24<  4928678   3   2321263   7    162088   7    14.9
c  6 30       871901  18    721406  18    110308  17   2242935   1   1140691   3     73094   3    12.7
c  7 41       281473   6    217826   6     50397   8    577588   0    327286   1     20918   1     4.0
c  8 54        97570   2     69121   2     24386   4    151655   0     89304   0      5399   0     1.5
c  9 69        41172   1     27417   1     12035   2     59739   0     34888   0      2252   0     0.8
c 10 86        14856   0      9529   0      4451   1     21340   0     12411   0       871   0     0.4
c 11 126        3131   0       584   0      1098   0      4372   0      2217   0        98   0     0.1
c 12 230         133   0         4   0        12   0       160   0        78   0         2   0     0.1
c 
c avg                  4.8           4.8           4.8           1.8           2.4           2.7
c std                  1.4           1.3           1.7           1.6           1.7           1.5
c 
c   16.828   2% cce
c   10.829   1% decide
c   10.297   1% probe
c    6.119   1% unhide
c 
c   12.872 < 1% rest (below)
c 
c    5.721   1% elim
c    3.146   0% transred
c    2.009   0% sweep
c    0.601   0% bca
c    0.387   0% block
c    0.339   0% card
c    0.322   0% gauss
c    0.280   0% ternres
c    0.067   0% quatres
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    2.349   0% preprocessing     5%
c   46.572   5% inprocessing     95%
c ==================================
c   48.921   5% simplifying
c  950.524  95% search
c ==================================
c  999.449 100% all
c 
c       4789708 conflicts,        4792.3 confs/sec
c          1299 ternaries,        3687.2 confs/ternary
c           724 binaries,         6615.6 confs/binary
c            57 iterations,      84030.0 confs/iteration
c 
c            85 reductions,          0.1 redus/sec,  56349.5 confs/reduction
c         37954 restarts,           38.0 rests/sec,    126.2 confs/restart
c      16633077 decisions,       16642.2 decis/sec,      3.5 decis/conflict
c     609874057 propagations,   610210.4 props/sec,     36.7 props/decision
c 
c 999.4 seconds, 81.7 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
