c launch: /data/cnf/sc2014/app/UTI-20-10p0.cnf.bz2
c host: atom01
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/UTI-20-10p0.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UTI-20-10p0.cnf.bz2
c no embedded options
c found 'p cnf 259616 1374599' header
c read 259616 variables, 1374599 clauses, 3310772 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=1
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 246467 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] INC (--score=1)
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  246467  1360580         0       0      0     0    0     0   58   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 5955 at-most-one constraints of average size 5.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 5955 out of 5955 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 62762 variables
c [simpleprobe-1] all 196854 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 1628 variables
c [simpleprobe-1] 21067 variables remain 11% (174159 retained 89%)
c [simpleprobe-1] removed 1628 variables, found 23803 hbrs, 363 units
c [unhide-1] limit 64496 based on 1031945 irredundant clauses
c [unhide-1-1] 0 units, 4425 failed, 12056 tauts, 0 hbrs, 11144 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 193813 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 60087 not tried 31% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 74911 = 39% variables out of 193813 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 850066 negative 99.2% of 856586 except 6520 0.8%
c [phase-count-1] 685394 positive 80.0% of 856586 except 171192 20.0%
c [phase-count-1] less non-negative clauses 6520 than limit 85600 (10.0%)
c [phase-count-1] non-pos/non-neg = 171192/6520 = 26.26 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 118902 negative 100%
c [sort-queue-1] sorted 118902 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 118902 (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 84137 variables 41.4% (118902 remain 48%)
c [simplification-1] removed 503994 irredundant clauses 37.0% (856586 remain 63%)
c [simplification-1] maximum reduction of 41% = max (41%, 37%)
c [simplification-1] large reduction 41% >= 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    5.1  118901   856586         8       1      0 16098    0     2   56   0%      0    2    0    0 25278%
c i    5.2  118891   856586       128      95      6 16103    2    12   57  12%      0   12   19    0 19667%
c i    5.2  118311   856586       169     111     19 16105    2    12   57  13%      0   12   17    0 17055%
c i    5.2  118294   856586       173     110     19 16106    2    12   57  13%      0   12   17    0 16798%
c 
c [simplification-2] limit 1003 conflicts (hard 11000) hit after 1006 conflicts
c [decomp-3] removed 666 variables
c [simpleprobe-2] 19725 schedulable variables 17%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 23082 variables remain 20% (95154 retained 80%)
c [simpleprobe-2] removed 0 variables, found 4220 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 80845 literals 34%
c [treelook-1] scheduling used 606800 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 333978 steps
c [treelook-1] 80840 literals remain 34%
c [treelook-1] 79586 variables remain to probed next time 67%
c [treelook-1] removed 0 variables, found 2256 hbrs
c [basicprobe-1] limit 6817736 based on 852217 irredundant clauses
c [basicprobe-1-0] 43595 probes remain 39% after last round
c [basicprobe-1-0] 39 units = 39 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 5466 variables, found 20670 hbrs
c [unhide-2] limit 53263 based on 852217 irredundant clauses
c [unhide-2-2] 2 units, 3137 failed, 5676 tauts, 0 hbrs, 3093 literals
c [elim-2] 57985 variables 52% will be scheduled this time
c [elim-2] scheduled 57985 variables 52%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 23358 not tried 21% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 32 = 0% variables out of 57985 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 783281 negative 99.2% of 789791 except 6510 0.8%
c [phase-count-2] 629978 positive 79.8% of 789791 except 159813 20.2%
c [phase-count-2] less non-negative clauses 6510 than limit 78900 (10.0%)
c [phase-count-2] non-pos/non-neg = 159813/6510 = 24.55 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 9459 negative 100%
c [sort-queue-2] sorted 104368 enqueued variables after 1006 conflicts
c [score-dist-2] active 6847 (6%), one 0 (0%), zero 104368 (94%)
c [score-dist-2] max exp 510, different 10 (2%)
c [score-dist-2] median active exp 504, avg 504.2
c [simplification-2] removed 7073 variables 6.0% (111215 remain 45%)
c [simplification-2] removed 66795 irredundant clauses 7.8% (789791 remain 58%)
c [simplification-2] maximum reduction of 8% = max (6%, 8%)
c [simplification-2] large reduction 8% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13006 (soft 3006 + delta 10000)
c [simplification-2] new conflict limit 3006 (hard 13006)
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    9.7  111214   789791      2282    1782     67 34278   18    58   56  31%     19   57   24    1 1647%
c i    9.9  110990   789791      2366    1834     87 34289   17    63   56  28%     17   61   18    1 1253%
c i    9.9  110662   789791      2398    1860     88 34293   17    65   56  27%     17   63   17    1 1155%
c i    9.9  110652   789791      2405    1860     89 34297   17    65   56  27%     17   64   17    1 1130%
c i    9.9  110644   789791      2406    1860     89 34297   17    65   56  27%     17   64   16    1 1126%
c i   10.0  110633   789791      2407    1860     89 34297   17    65   56  27%     17   64   16    1 1122%
c i   10.0  110623   789791      2408    1860     89 34297   17    65   56  27%     17   64   16    1 1117%
c i   10.0  110613   789791      2409    1860     89 34297   17    65   56  27%     17   64   16    1 1113%
c i   10.0  110600   789791      2410    1860     89 34297   17    65   56  27%     17   64   16    1 1108%
c i   10.6  110591   789791      2704    2092    117 34323   17    93   56  18%     13   91   11    1  750%
c 
c [simplification-3] limit of 14 iterations hit after 14 iterations
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4117 at-most-one constraints of average size 4.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4117 out of 4117 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 912 variables
c [unhide-3] limit 66535 with penalty 1 = 0 + 1
c [unhide-3-3] 0 units, 1459 failed, 15707 tauts, 0 hbrs, 3355 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 109063 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 31234 not tried 29% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1265 = 1% variables out of 109063 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 751666 negative 99.2% of 758080 except 6414 0.8%
c [phase-count-3] 604720 positive 79.8% of 758080 except 153360 20.2%
c [phase-count-3] less non-negative clauses 6414 than limit 75800 (10.0%)
c [phase-count-3] non-pos/non-neg = 153360/6414 = 23.91 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 3505 negative 100%
c [sort-queue-3] sorted 89184 enqueued variables after 2704 conflicts
c [score-dist-3] active 18614 (17%), one 0 (0%), zero 89184 (83%)
c [score-dist-3] max exp 512, different 12 (2%)
c [score-dist-3] median active exp 504, avg 504.3
c [simplification-3] removed 2646 variables 2.4% (107798 remain 44%)
c [simplification-3] removed 31711 irredundant clauses 4.0% (758080 remain 56%)
c [simplification-3] maximum reduction of 4% = max (2%, 4%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3057 (hard 13006)
c [simplification-3] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   13.4  107797   758080      2844    2208    116 30657   17   111   55  16%     11  109   20    2 1258%
c 
c [simplification-4] limit 3057 conflicts (hard 13006) hit after 3058 conflicts
c [decomp-7] removed 270 variables
c [treelook-2] limit 188017 based on 752069 irredundant clauses
c [treelook-2] scheduled 50322 literals 23%
c [treelook-2] scheduling used 263898 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 188017 based on 752069 irredundant clauses
c [treelook-2] used 274437 steps
c [treelook-2] 50315 literals remain 23%
c [treelook-2] 42282 variables remain to probed next time 39%
c [treelook-2] removed 0 variables, found 1825 hbrs
c [unhide-4] limit 98418 with penalty 1 = 0 + 1
c [unhide-4-4] 1 units, 718 failed, 3077 tauts, 0 hbrs, 4982 literals
c [elim-4] 22762 variables 21% will be scheduled this time
c [elim-4] scheduled 22762 variables 21%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 45062136 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 22762 scheduled
c [phase-count-4] 737405 negative 99.1% of 743819 except 6414 0.9%
c [phase-count-4] 587520 positive 79.0% of 743819 except 156299 21.0%
c [phase-count-4] less non-negative clauses 6414 than limit 74300 (10.0%)
c [phase-count-4] non-pos/non-neg = 156299/6414 = 24.37 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1755 negative 100%
c [sort-queue-4] sorted 76128 enqueued variables after 3058 conflicts
c [score-dist-4] active 30864 (29%), one 0 (0%), zero 76128 (71%)
c [score-dist-4] max exp 512, different 12 (2%)
c [score-dist-4] median active exp 504, avg 504.3
c [simplification-4] removed 538 variables 0.5% (106992 remain 43%)
c [simplification-4] removed 14261 irredundant clauses 1.9% (743819 remain 55%)
c [simplification-4] maximum reduction of 2% = max (1%, 2%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 6666
c [simplification-4] penalized conflict interval 6666 = 1 * 6666
c [simplification-4] hard conflict limit 19724 (soft 9724 + delta 10000)
c [simplification-4] new conflict limit 9724 (hard 19724)
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   16.8  106991   743819      3196    2478    137 28715   19   148   54  13%      9  145   34    2 1957%
c i   18.7  106750   743819      3941    3106    146 28736   34   220   55  15%      7  215  139    3 4777%
c i   19.4  106742   743819      4220    3318    149 28737   48   243   55  20%      6  237  233    4 5878%
c i   20.7  106733   743819      4660    3598    159 28762   63   289   56  22%      5  281  153    5 2892%
c i   20.9  106732   743819      4702    3630    160 28769   63   297   56  21%      5  289  139    5 2618%
c i   20.9  106731   743819      4708    3634    160 28770   63   298   56  21%      5  290  138    5 2584%
c i   21.1  106730   743819      4784    3691    162 28772   63   312   57  20%      4  304  114    5 2123%
c i   22.2  106676   743819      5256    4109    174 28781   69   370   57  19%      4  360  112    6 1812%
c i   22.8  106642   743819      5474    4309    178 28784   70   404   58  17%      3  392  108    6 1676%
c i   23.1  106451   743819      5583    4382    182 28785   75   415   58  18%      3  402  160    7 2328%
c i   23.7  106440   743819      5785    4557    186 28786   81   435   59  19%      3  421  176    7 2358%
c i   23.7  106431   743819      5786    4557    186 28786   81   435   59  19%      3  421  175    7 2348%
c i   24.0  106424   743819      5885    4648    186 28789   81   446   59  18%      2  431  142    8 1883%
c i   24.0  106423   743819      5891    4652    186 28789   81   446   59  18%      2  432  140    8 1850%
c i   25.2  106422   743819      6271    4970    193 28789   94   484   60  19%      2  467  217    9 2458%
c i   26.6  106370   743819      6762    5382    197 28796  114   539   62  21%      3  518  261   11 2420%
c i   27.6  106369   743819      7084    5636    204 28802  123   570   62  22%      3  547  241   12 2034%
c i   29.0  106368   743819      7549    6077    204 28805  119   612   63  19%      3  585  103   12  829%
c 
c [simplification-5] limit of 212 binary hit after 212 binaries
c [quatres-1] found 37417 quaternary clauses 32% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 21000045 with penalty 0 = 0 + 0
c [ternres-1] all 106368 free variables schedulable
c [ternres-1] 41 ternary resolvents (0 bin, 41 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 26 xors of average arity 2.8
c [gauss-1] connected 74 occurrences of 51 variables (average 1.5)
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 10 variables
c [basicprobe-2] limit 21000047 penalty 0 = 0 + 0
c [basicprobe-2-0] 36956 probes remain 37% after last round
c [basicprobe-2-0] 117 units = 117 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 6080 variables, found 52553 hbrs
c [bate-1] eliminated 66 asymmetric tautologies during probing
c [unhide-5] limit 420000 with penalty 1 = 0 + 1
c [unhide-5-5] 3 units, 771 failed, 17190 tauts, 0 hbrs, 66838 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 201 transitive binary clauses
c [transred-1] found 3 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 99765 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 11088 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 19 clauses out of 340 (6%) of length 10
c [cce-1-1] eliminated 115 clauses out of 2184 (5%) of length 9
c [cce-1-1] eliminated 9 clauses out of 517 (2%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 143 large clauses in 30000002 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 345962 clauses = 327437 binary + 18525 ternary
c [cce-1-1] tried to eliminate 477 small clauses 0%
c [cce-1-1] eliminated 169 binary clauses 0%
c [cce-1-1] eliminated 7 ternary clauses 0%
c [cce-1-1] eliminated 176 small clauses 0%
c [cce-1-1] eliminated 176 small clauses in 30000003 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 319 covered clauses in round 1
c [cce-1] eliminated 319 covered clauses in TOTAL during 1 rounds
c [cce-1] 319 < 1/100 * 672022 = 6720 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1343906 added (scaled 2)
c [bca-1] 177641 out of 199532 literals actually usable 89%
c [bca-1] added 245 blocked clauses in 534725 steps
c [sweep-1] limit 1343406 based on 671703 irredundant clauses
c [sweep-1-1] 8600 pos 8.6% + 91165 neg 91.4% = 99765 sched 100.0% ret 0
c [sweep-1-1] 1686966 steps 6 queries 32534.83 avg class size
c [sweep-1-1] 64 decisions 3 SAT calls 38.67 avg env size
c [sweep-1-1] 99763 variables remain 100% (2 retained 0%)
c [decomp-10] removed 212 variables
c [sweep-1-1] removed 212 vars (0 failed, 2 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 212 vars in TOTAL (1 rounds, 5 queries)
c [phase-count-5] 664895 negative 99.0% of 671289 except 6394 1.0%
c [phase-count-5] 545890 positive 81.3% of 671289 except 125399 18.7%
c [phase-count-5] less non-negative clauses 6394 than limit 67100 (10.0%)
c [phase-count-5] non-pos/non-neg = 125399/6394 = 19.61 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 670 negative 100%
c [sort-queue-5] sorted 50796 enqueued variables after 7635 conflicts
c [score-dist-5] active 48757 (49%), one 0 (0%), zero 50796 (51%)
c [score-dist-5] max exp 512, different 12 (2%)
c [score-dist-5] median active exp 505, avg 505.7
c [simplification-5] removed 6815 variables 6.4% (99553 remain 40%)
c [simplification-5] removed 72530 irredundant clauses 9.8% (671289 remain 49%)
c [simplification-5] maximum reduction of 10% = max (6%, 10%)
c [simplification-5] forced so keeping old conflict interval 6666
c [simplification-5] conflict limit remains at 9736 (hard 19724)
c [simplification-5] 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   35.4   99552   671289      7947    6390    276 85927  132   648   63  20%      3  617  227   14 1635%
c i   39.4   99542   671289      9695    6988    294 85956  296   687   66  43%     14  640  597   29 2040%
c 
c [simplification-6] limit 9736 conflicts (hard 19724) hit after 9738 conflicts
c [ternres-2] limit 5255690 with penalty 0 = 0 + 0
c [ternres-2] all 99535 free variables schedulable
c [ternres-2] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-2] 62480 variables remain 63% (37055 retained 37%)
c [card-3] limit 656961 penalty 2 = 2 + 0
c [card-3] found 2554 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 656961 for elimination
c [card-3] 2554 out of 2554 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 19 variables
c [unhide-6] limit 525569 with penalty 1 = 0 + 1
c [unhide-6-6] 0 units, 766 failed, 5475 tauts, 0 hbrs, 53177 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 194 transitive binary clauses
c [transred-2] found 2 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 99052 variables 100%
c [block-2] limit of 52556902 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 932 blocked clauses
c [block-2] 932 < 1/100 * 671047 = 6710 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 99052 variables 100%
c [elim-5] limit of 52556902 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 3730 not tried 4% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2194 = 2% variables out of 99052 scheduled
c [bca-2] limit of 10000000 steps and 1320732 added (scaled 2)
c [bca-2] 175022 out of 193718 literals actually usable 90%
c [bca-2] added 168 blocked clauses in 535622 steps
c [sweep-2] limit 1576707 penalty 0 = 0 + 0
c [sweep-2-1] 9090 pos 9.4% + 87767 neg 90.6% = 96857 sched 100.0% ret 1
c [sweep-2-1] 1606988 steps 27 queries 22202.15 avg class size
c [sweep-2-1] 275 decisions 25 SAT calls 57.16 avg env size
c [sweep-2-1] 96570 variables remain 100% (272 retained 0%)
c [decomp-12] removed 17 variables
c [sweep-2-1] removed 17 vars (0 failed, 1 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 17 vars in TOTAL (1 rounds, 26 queries)
c [phase-count-6] 653585 negative 99.1% of 659851 except 6266 0.9%
c [phase-count-6] 534910 positive 81.1% of 659851 except 124941 18.9%
c [phase-count-6] less non-negative clauses 6266 than limit 65900 (10.0%)
c [phase-count-6] non-pos/non-neg = 124941/6266 = 19.94 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 494 negative 100%
c [sort-queue-6] sorted 46435 enqueued variables after 9738 conflicts
c [score-dist-6] active 50406 (52%), one 0 (0%), zero 46435 (48%)
c [score-dist-6] max exp 513, different 13 (3%)
c [score-dist-6] median active exp 505, avg 505.8
c [simplification-6] removed 2694 variables 2.7% (96841 remain 39%)
c [simplification-6] removed 11438 irredundant clauses 1.7% (659851 remain 48%)
c [simplification-6] maximum reduction of 3% = max (3%, 2%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 11666
c [simplification-6] penalized conflict interval 11666 = 1 * 11666
c [simplification-6] hard conflict limit 31404 (soft 21404 + delta 10000)
c [simplification-6] new conflict limit 21404 (hard 31404)
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   44.8   96840   659851     10202    4382    291 81602  309   688   55  45%     10  636  486   32 1513%
c i   45.0   96839   659851     10368    4495    292 81606  313   687   55  46%      8  634  444   33 1341%
c i   45.1   96838   659851     10443    4552    294 81613  312   687   55  45%      8  632  401   33 1203%
c i   46.1   96835   659851     11052    4975    313 81641  302   699   57  43%      6  638  170   35  482%
c i   48.0   96834   659851     11974    5801    329 81660  267   806   58  33%      7  735  145   36  399%
c i   48.0   96826   659851     11977    5803    329 81660  267   805   58  33%      7  735  145   36  396%
c i   48.0   96818   659851     11981    5805    330 81660  267   805   58  33%      7  735  142   36  390%
c i   49.0   96812   659851     12346    6115    341 81681  254   840   58  30%      5  765  139   37  377%
c i   49.0   96811   659851     12348    6116    341 81681  253   839   58  30%      5  765  139   37  375%
c i   49.3   96810   659851     12484    6237    342 81684  251   850   58  29%      5  774  145   37  391%
c i   50.4   96806   659851     12899    6591    352 81697  245   876   59  28%      4  796  202   38  531%
c i   50.4   96805   659851     12900    6591    352 81697  245   876   59  28%      4  795  201   38  529%
c i   50.4   96804   659851     12901    6591    352 81697  245   876   59  28%      4  795  201   38  527%
c i   64.4   96803   659851     17546    8606    383 81727  623  1049   79  59%     54  908  664   88  753%
c 
c [simplification-7] limit 21434 conflicts (hard 31404) hit after 21436 conflicts
c [quatres-2] found 44033 quaternary clauses 40% in total
c [quatres-2-2] added 4 quaternary resolvents
c [ternres-3] limit 12449380 with penalty 0 = 0 + 0
c [ternres-3] 60776 schedulable variables 63%
c [ternres-3] 28 ternary resolvents (0 bin, 28 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1244938 penalty 1 = 1 + 0
c [gauss-2] extracted 13 xors of average arity 2.9
c [gauss-2] connected 38 occurrences of 38 variables (average 1.0)
c [gauss-2] limit 1244938 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 27 variables
c [simpleprobe-3] 19519 schedulable variables 20%
c [simpleprobe-3] limit 24898760 penalty 1 = 1 + 0
c [decomp-14] removed 738 variables
c [simpleprobe-3] 25148 variables remain 26% (70883 retained 74%)
c [simpleprobe-3] removed 738 variables, found 62143 hbrs, 345 units
c [unhide-7] limit 1244938 with penalty 1 = 0 + 1
c [unhide-7-7] 0 units, 55 failed, 5724 tauts, 0 hbrs, 390065 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 257 transitive binary clauses
c [transred-3] found 2 units
c [cce-2] limit of 31123450 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 26 clauses out of 514 (5%) of length 8
c [cce-2-1] eliminated 35 clauses out of 926 (4%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 61 large clauses in 31123458 steps
c [cce-2-1] allowing another 15561729 steps for small clauses
c [cce-2-1] scheduling 521124 clauses = 315066 binary + 206058 ternary
c [cce-2-1] tried to eliminate 363 small clauses 0%
c [cce-2-1] eliminated 72 binary clauses 0%
c [cce-2-1] eliminated 25 ternary clauses 0%
c [cce-2-1] eliminated 97 small clauses 0%
c [cce-2-1] eliminated 1063 small clauses in 31123463 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1124 covered clauses in round 1
c [cce-2] eliminated 1124 covered clauses in TOTAL during 1 rounds
c [cce-2] 1124 < 1/100 * 647060 = 6470 considered unsuccessful
c [elim-6] 3723 variables 4% will be scheduled this time
c [elim-6] scheduled 3723 variables 4%
c [elim-6] limit of 248987603 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 9925323 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 3723 scheduled
c [bca-3] limit of 10000000 steps and 1291416 added (scaled 2)
c [bca-3] 167009 out of 191878 literals actually usable 87%
c [bca-3] added 59 blocked clauses in 506088 steps
c [sweep-3] limit 3734814 penalty 0 = 0 + 0
c [sweep-3-1] 8714 pos 9.1% + 86974 neg 90.9% = 95688 sched 99.7% ret 250
c [sweep-3-1] 3908729 steps 33 queries 23031.42 avg class size
c [sweep-3-1] 314 decisions 28 SAT calls 85.71 avg env size
c [sweep-3-1] 95132 variables remain 100% (465 retained 0%)
c [decomp-15] removed 345 variables
c [sweep-3-1] removed 345 vars (0 failed, 4 eqs, 10 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 345 vars in TOTAL (1 rounds, 32 queries)
c [phase-count-7] 632135 negative 99.0% of 638403 except 6268 1.0%
c [phase-count-7] 515516 positive 80.8% of 638403 except 122887 19.2%
c [phase-count-7] less non-negative clauses 6268 than limit 63800 (10.0%)
c [phase-count-7] non-pos/non-neg = 122887/6268 = 19.61 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 350 negative 100%
c [sort-queue-7] sorted 39768 enqueued variables after 21436 conflicts
c [score-dist-7] active 55825 (58%), one 0 (0%), zero 39768 (42%)
c [score-dist-7] max exp 515, different 15 (3%)
c [score-dist-7] median active exp 507, avg 507.1
c [simplification-7] removed 1203 variables 1.2% (95593 remain 39%)
c [simplification-7] removed 21448 irredundant clauses 3.3% (638403 remain 47%)
c [simplification-7] maximum reduction of 3% = max (1%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 16666
c [simplification-7] penalized conflict interval 16666 = 1 * 16666
c [simplification-7] hard conflict limit 48102 (soft 38102 + delta 10000)
c [simplification-7] new conflict limit 38102 (hard 48102)
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   87.7   95592   638403     23120   10711    441 146695  851  1197   88  71%     65  974  816  155  527%
c i   91.1   95217   638403     24358   11487    459 146729  774  1191   88  65%     23  950  570  162  352%
c i   95.7   95208   638403     26025   11790    459 146731  866  1174  106  74%     12  909 1122  184  609%
c i   95.7   95207   638403     26027   11791    459 146731  865  1174  106  74%     12  909 1114  184  605%
c i   96.0   95206   638403     26117   11871    460 146731  853  1175  106  73%     10  909  877  184  476%
c i   98.2   95202   638403     26841   12126    465 146747  847  1163  106  73%      5  887  805  191  421%
c i  100.6   95201   638403     27549   12212    471 146756  856  1132  106  76%      2  846  899  199  452%
c i  102.1   95028   638403     27963   12242    473 146764  861  1115  106  77%      0  825  907  203  446%
c i  102.3   95027   638403     28044   12253    473 146764  863  1112  106  78%     -0  820  914  204  448%
c i  102.6   95026   638403     28144   12258    473 146764  864  1108  106  78%     -1  815  920  205  448%
c i  103.6   95025   638403     28495   12307    474 146767  868  1094  106  79%     -2  797  919  209  440%
c i  103.9   95024   638403     28642   12307    475 146768  870  1089  106  80%     -2  790  920  211  437%
c i  103.9   95023   638403     28643   12307    475 146768  870  1088  106  80%     -2  790  917  211  435%
c i  103.9   95022   638403     28668   12307    475 146768  870  1087  106  80%     -3  788  914  211  434%
c i  105.8   95021   638403     29595   12384    479 146778  867  1050  106  83%     -0  740  817  220  371%
c i  105.9   95020   638403     29612   12389    479 146778  867  1049  106  83%     -0  739  814  220  370%
c i  106.0   95019   638403     29655   12402    482 146778  865  1047  106  83%     -1  736  804  220  365%
c i  106.0   95018   638403     29656   12402    482 146778  865  1047  106  83%     -1  736  801  220  363%
c i  106.3   95017   638403     29839   12415    485 146788  859  1036  106  83%     -1  724  768  222  346%
c i  106.4   95016   638403     29840   12415    485 146788  859  1036  106  83%     -1  723  765  222  345%
c i  106.4   95015   638403     29841   12415    485 146788  859  1036  106  83%     -1  723  762  222  343%
c i  106.4   95014   638403     29842   12415    485 146788  859  1035  106  83%     -1  723  759  222  342%
c i  106.5   95013   638403     29906   12421    485 146788  857  1032  106  83%     -2  718  756  222  340%
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  107.3   95012   638403     30323   12449    490 146816  845  1009  106  84%     -2  691  740  226  328%
c i  107.3   95011   638403     30324   12449    490 146816  845  1009  106  84%     -2  691  738  226  327%
c i  107.3   95010   638403     30343   12449    490 146816  844  1008  106  84%     -2  690  738  226  327%
c i  107.3   95009   638403     30358   12450    490 146817  844  1007  106  84%     -3  689  735  226  325%
c i  107.4   95008   638403     30364   12452    490 146818  843  1006  106  84%     -3  688  730  226  323%
c i  107.9   95007   638403     30646   12489    494 146824  836   992  106  84%     -3  670  731  228  321%
c i  109.0   95006   638403     31701   12523    494 146847  821   946  141  87%      1  615  764  237  323%
c i  109.2   95005   638403     31881   12530    495 146847  818   939  141  87%     -0  606  758  238  319%
c i  111.1   94973   638403     33115   12585    495 146849  802   894  141  90%      3  551  755  248  305%
c i  112.3   94972   638403     34034   12635    496 146850  794   870  141  91%      2  519  758  255  298%
c i  112.4   94971   638403     34035   12635    496 146850  794   870  141  91%      2  519  755  255  297%
c i  114.6   94970   638403     36203   13261    500 146868  709   797  141  89%     14  430  614  265  232%
c i  114.6   94969   638403     36204   13261    500 146868  709   797  141  89%     14  430  612  265  231%
c i  114.6   94968   638403     36205   13261    500 146868  708   796  141  89%     14  429  609  265  230%
c i  114.6   94967   638403     36206   13261    500 146868  708   796  141  89%     14  429  607  265  229%
c i  114.6   94966   638403     36207   13261    500 146868  708   796  141  89%     14  429  605  265  228%
c i  114.6   94965   638403     36208   13261    500 146868  708   796  141  89%     14  429  602  265  227%
c i  114.6   94964   638403     36209   13261    500 146868  708   796  141  89%     14  429  600  265  226%
c 
c [simplification-8] limit 38238 conflicts (hard 48102) hit after 38239 conflicts
c [quatres-3] found 40389 quaternary clauses 39% in total
c [ternres-4] limit 19236217 with penalty 0 = 0 + 0
c [ternres-4] all 94964 free variables schedulable
c [ternres-4] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-16] removed 645 variables
c [unhide-8] limit 961810 with penalty 2 = 0 + 2
c [unhide-8-8] 2 units, 1072 failed, 9683 tauts, 0 hbrs, 295163 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 268 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 94166 variables 100%
c [block-3] limit of 96181088 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 425 blocked clauses
c [block-3] 425 < 1/100 * 635537 = 6355 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1256932 added (scaled 2)
c [bca-4] 162220 out of 188334 literals actually usable 86%
c [bca-4] added 117 blocked clauses in 491565 steps
c [sweep-4] limit 5770865 penalty 0 = 0 + 0
c [sweep-4-1] 8707 pos 9.3% + 85033 neg 90.7% = 93740 sched 99.5% ret 426
c [sweep-4-1] 5771411 steps 81 queries 9515.43 avg class size
c [sweep-4-1] 1038 decisions 61 SAT calls 138.67 avg env size
c [sweep-4-1] 92482 variables remain 98% (1597 retained 2%)
c [decomp-17] removed 109 variables
c [sweep-4-1] removed 109 vars (0 failed, 20 eqs, 37 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 109 vars in TOTAL (1 rounds, 80 queries)
c [phase-count-8] 620420 negative 99.0% of 626687 except 6267 1.0%
c [phase-count-8] 505206 positive 80.6% of 626687 except 121481 19.4%
c [phase-count-8] less non-negative clauses 6267 than limit 62600 (10.0%)
c [phase-count-8] non-pos/non-neg = 121481/6267 = 19.38 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 303 negative 100%
c [sort-queue-8] sorted 37347 enqueued variables after 38239 conflicts
c [score-dist-8] active 56710 (60%), one 0 (0%), zero 37347 (40%)
c [score-dist-8] max exp 516, different 16 (3%)
c [score-dist-8] median active exp 507, avg 507.4
c [simplification-8] removed 907 variables 1.0% (94057 remain 38%)
c [simplification-8] removed 11716 irredundant clauses 1.8% (626687 remain 46%)
c [simplification-8] maximum reduction of 2% = max (1%, 2%)
c [simplification-8] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-8] new conflict interval 23332
c [simplification-8] penalized conflict interval 23332 = 1 * 23332
c [simplification-8] hard conflict limit 73237 (soft 61571 + delta 11666)
c [simplification-8] new conflict limit 61571 (hard 73237)
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  128.5   94056   626687     46170   15587    493 139995  553   675  107  82%    124  260  362  308  118%
c i  129.3   94055   626687     46772   16040    494 140000  530   693  107  76%     63  275  426  308  138%
c i  137.5   94054   626687     53548   19319    500 140013  486   638  140  76%     70  195  474  325  146%
c i  137.5   94053   626687     53550   19320    500 140013  486   638  140  76%     70  194  470  325  145%
c i  137.9   94052   626687     53857   19376    500 140013  484   629  140  77%     47  185  473  325  145%
c i  137.9   94051   626687     53892   19402    501 140014  482   628  140  77%     45  184  438  325  135%
c i  138.0   94050   626687     53946   19440    501 140014  479   627  140  76%     41  182  402  325  123%
c i  138.0   94049   626687     53960   19446    501 140014  478   626  140  76%     41  181  401  325  123%
c 
c [simplification-9] limit 61576 conflicts (hard 73237) hit after 61576 conflicts
c [ternres-5] limit 23974048 with penalty 0 = 0 + 0
c [ternres-5] all 94049 free variables schedulable
c [ternres-5] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-18] removed 8 variables
c [unhide-9] limit 1198702 with penalty 2 = 0 + 2
c [unhide-9-9] 0 units, 77 failed, 9147 tauts, 0 hbrs, 620019 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 195 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 93937 variables 100%
c [elim-7] limit of 239740480 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 1565 variables 2% in round 1 in 56990673 steps
c [elim-7-1] backward subsumption/strengthening limit 56990600
c [elim-7-1-1] backward checking 5700 touched variables 6%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 14 clauses in 2353231 steps
c [elim-7-1] rescheduled 30 variables 0% by backward subsumption
c [elim-7-2] eliminated 4 variables 0% in round 2 in 37470 steps
c [elim-7-2] backward subsumption/strengthening limit 37400
c [elim-7-2-1] backward checking 31 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 37401 steps
c [elim-7-2] fully rescheduled 92364 variables 98%
c [elim-7-3] eliminated 2 variables 0% in round 3 in 56686231 steps
c [elim-7-3] backward subsumption/strengthening limit 56686200
c [elim-7-3-1] backward checking 17 touched variables 0%
c [elim-7-3-1] fully completed backward checking in 1 rounds
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 122858 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1575 = 2% variables out of 93937 scheduled
c [bca-5] limit of 10000000 steps and 1228898 added (scaled 2)
c [bca-5] 160487 out of 184726 literals actually usable 87%
c [bca-5] added 63 blocked clauses in 499005 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 71922140 penalty 0 = 0 + 0
c [sweep-5-1] 8514 pos 9.4% + 82419 neg 90.6% = 90933 sched 98.5% ret 1429
c [sweep-5-1] 71933409 steps 896 queries 1116.64 avg class size
c [sweep-5-1] 8796 decisions 785 SAT calls 86.30 avg env size
c [sweep-5-1] 60661 variables remain 67% (30437 retained 33%)
c [decomp-19] removed 1672 variables
c [sweep-5-1] removed 1672 vars (0 failed, 116 eqs, 215 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1672 vars in TOTAL (1 rounds, 895 queries)
c [phase-count-9] 593201 negative 99.0% of 599409 except 6208 1.0%
c [phase-count-9] 480260 positive 80.1% of 599409 except 119149 19.9%
c [phase-count-9] less non-negative clauses 6208 than limit 59900 (10.0%)
c [phase-count-9] non-pos/non-neg = 119149/6208 = 19.19 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 260 negative 100%
c [sort-queue-9] sorted 33540 enqueued variables after 61576 conflicts
c [score-dist-9] active 57150 (63%), one 0 (0%), zero 33540 (37%)
c [score-dist-9] max exp 517, different 17 (3%)
c [score-dist-9] median active exp 507, avg 507.4
c [simplification-9] removed 3359 variables 3.6% (90690 remain 37%)
c [simplification-9] removed 27278 irredundant clauses 4.4% (599409 remain 44%)
c [simplification-9] maximum reduction of 4% = max (4%, 4%)
c [simplification-9] geometric conflict interval increment 4666 = 23332 / 5
c [simplification-9] new conflict interval 27998
c [simplification-9] penalized conflict interval 27998 = 1 * 27998
c [simplification-9] hard conflict limit 103573 (soft 89574 + delta 13999)
c [simplification-9] new conflict limit 89574 (hard 103573)
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  157.8   90689   599409     62070   17755    494 212853  473   554   91  85%     86   94  497  339  147%
c i  158.5   90686   599409     62894   18118    494 212855  457   547   92  84%     28   86  338  340   99%
c i  160.3   90682   599409     64934   19446    500 212876  418   548   92  76%     -0   84  373  341  110%
c i  160.7   90681   599409     65416   19876    510 212881  380   613   92  62%     -8  148  106  339   31%
c i  163.2   90567   599409     68297   22471    551 212922  309  1132  110  27%      6  650  310  334   93%
c i  164.1   90566   599409     69089   23126    558 212925  322  1222  111  26%     -7  732  361  334  108%
c i  169.0   90565   599409     73102   26633    584 212957  345  1457  124  24%     22  917  294  336   88%
c i  169.0   90556   599409     73105   26635    584 212957  345  1457  124  24%     22  917  293  336   87%
c i  170.0   90546   599409     74341   27725    592 212968  317  1467  124  22%     -3  911  190  334   57%
c i  170.2   90544   599409     74502   27842    595 212972  324  1467  124  22%     -6  909  345  334  103%
c i  173.4   90543   599409     77456   30379    610 213004  281  1494  165  19%      7  897   73  331   22%
c i  174.1   90528   599409     78121   30966    615 213008  277  1497  165  19%     -5  891  272  331   82%
c i  174.1   90519   599409     78124   30966    616 213008  277  1496  165  19%     -5  890  270  331   82%
c i  174.2   90518   599409     78140   30981    616 213008  277  1496  165  19%     -6  890  271  331   82%
c i  174.2   90499   599409     78141   30981    616 213008  277  1496  165  19%     -6  889  270  331   82%
c i  174.9   90498   599409     78929   31681    619 213013  276  1494  165  18%    -12  877  278  330   84%
c i  174.9   90497   599409     78931   31682    619 213013  276  1494  165  18%    -12  877  277  330   84%
c i  174.9   90496   599409     78971   31715    619 213013  277  1494  165  19%    -13  877  284  330   86%
c i  175.5   90495   599409     79639   32312    622 213014  283  1500  171  19%    -15  875  342  330  104%
c i  176.7   90494   599409     80807   33360    624 213018  296  1513  171  20%    -14  873  272  330   82%
c i  179.5   90415   599409     82514   34474    626 213044  401  1495  171  27%     -8  833  873  336  260%
c i  185.1   90376   599409     85390   36350    632 213062  505  1435  191  35%      7  739  331  349   95%
c i  186.3   90281   599409     86547   37407    638 213074  450  1427  191  32%     -6  718  162  348   47%
c 
c [simplification-10] limit 89595 conflicts (hard 103573) hit after 89597 conflicts
c [quatres-4] found 35504 quaternary clauses 36% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 3 quaternary resolvents
c [ternres-6] limit 30914374 with penalty 0 = 0 + 0
c [ternres-6] all 90281 free variables schedulable
c [ternres-6] 30 ternary resolvents (0 bin, 30 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1932148 penalty 3 = 3 + 0
c [card-4] found 5441 at-most-one constraints of average size 4.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1932148 for elimination
c [card-4] 5441 out of 5441 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1545718 penalty 2 = 2 + 0
c [gauss-3] extracted 319 xors of average arity 2.2
c [gauss-3] connected 690 occurrences of 350 variables (average 2.0)
c [gauss-3] limit 1545718 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 315 variables
c [treelook-3] limit 772859 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 100039 literals 56%
c [treelook-3] scheduling used 826158 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 772859 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 875948 steps
c [treelook-3] 100020 literals remain 56%
c [treelook-3] 30634 variables remain to probed next time 34%
c [decomp-21] removed 1 variables
c [treelook-3] removed 2 variables, found 4587 hbrs
c [unhide-10] limit 772859 with penalty 3 = 0 + 3
c [unhide-10-10] 7 units, 474 failed, 11513 tauts, 0 hbrs, 2648943 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 286 transitive binary clauses
c [cce-3] limit of 38642968 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1880 (0%) of length 9
c [cce-3-1] eliminated 55 clauses out of 801 (7%) of length 7
c [cce-3-1] eliminated 3672 clauses out of 5872 (63%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 3728 large clauses in 38642972 steps
c [cce-3-1] allowing another 19321486 steps for small clauses
c [cce-3-1] scheduling 321459 clauses = 299007 binary + 22452 ternary
c [cce-3-1] tried to eliminate 720 small clauses 0%
c [cce-3-1] eliminated 197 binary clauses 0%
c [cce-3-1] eliminated 35 ternary clauses 0%
c [cce-3-1] eliminated 232 small clauses 0%
c [cce-3-1] eliminated 4613 small clauses in 38642976 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 8341 covered clauses in round 1
c [cce-3] eliminated 8341 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 89347 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 12365749760 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 2700 variables 3% in round 1 in 53687092 steps
c [elim-8-1] backward subsumption/strengthening limit 53687000
c [elim-8-1-1] backward checking 8609 touched variables 10%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 3 and strengthened 164 clauses in 3676750 steps
c [elim-8-1] rescheduled 390 variables 0% by backward subsumption
c [elim-8-2] eliminated 54 variables 0% in round 2 in 1176990 steps
c [elim-8-2] backward subsumption/strengthening limit 1176900
c [elim-8-2-1] backward checking 411 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 341189 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 2754 = 3% variables out of 89347 scheduled
c [bca-6] limit of 10000000 steps and 1156034 added (scaled 2)
c [bca-6] 149006 out of 173188 literals actually usable 86%
c [bca-6] added 373 blocked clauses in 471218 steps
c [sweep-6] limit 9274312 penalty 0 = 0 + 0
c [sweep-6-1] 6967 pos 12.0% + 51073 neg 88.0% = 58040 sched 67.0% ret 28553
c [sweep-6-1] 9428766 steps 142 queries 3755.81 avg class size
c [sweep-6-1] 1414 decisions 126 SAT calls 111.21 avg env size
c [sweep-6-1] 56301 variables remain 65% (30170 retained 35%)
c [decomp-22] removed 158 variables
c [sweep-6-1] removed 158 vars (0 failed, 16 eqs, 33 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 158 vars in TOTAL (1 rounds, 141 queries)
c [phase-count-10] 574565 negative 99.6% of 576640 except 2075 0.4%
c [phase-count-10] 460444 positive 79.8% of 576640 except 116196 20.2%
c [phase-count-10] less non-negative clauses 2075 than limit 57600 (10.0%)
c [phase-count-10] non-pos/non-neg = 116196/2075 = 56.00 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 160 negative 100%
c [sort-queue-10] sorted 27519 enqueued variables after 89597 conflicts
c [score-dist-10] active 58916 (68%), one 0 (0%), zero 27519 (32%)
c [score-dist-10] max exp 517, different 17 (3%)
c [score-dist-10] median active exp 508, avg 508.1
c [simplification-10] removed 3846 variables 4.3% (86435 remain 35%)
c [simplification-10] removed 22769 irredundant clauses 3.8% (576640 remain 42%)
c [simplification-10] maximum reduction of 4% = max (4%, 4%)
c [simplification-10] geometric conflict interval increment 5599 = 27998 / 5
c [simplification-10] new conflict interval 33597
c [simplification-10] penalized conflict interval 33597 = 1 * 33597
c [simplification-10] hard conflict limit 139992 (soft 123194 + delta 16798)
c [simplification-10] new conflict limit 123194 (hard 139992)
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  225.3   86434   576640     96381   30166    720 206611  725  1388  180  52%    108  585  360  423   85%
c i  225.3   86425   576640     96384   30168    720 206611  724  1388  180  52%    108  585  357  423   84%
c i  233.3   86424   576640    100836   33327    732 206615  613  1411  194  43%     25  568  679  430  158%
c i  237.5   86423   576640    103657   35584    735 206631  504  1445  195  35%      2  579  499  429  116%
c i  237.8   86418   576640    103814   35718    735 206634  497  1451  195  34%     -3  583  414  428   97%
c i  237.8   86417   576640    103816   35719    735 206634  497  1451  195  34%     -3  583  412  428   96%
c i  250.9   86416   576640    108978   38458    759 206652  813  1491  249  55%     34  577  824  464  178%
c i  251.7   86415   576640    109316   38721    759 206652  786  1492  251  53%     16  576  617  464  133%
c i  251.8   86403   576640    109324   38724    759 206652  786  1492  251  53%     16  575  627  464  135%
c i  253.9   86401   576640    110072   39067    759 206655  812  1484  251  55%     -5  561  913  469  195%
c i  266.5   86386   576640    115800   42480    777 206705  737  1470  271  50%     42  502  807  489  165%
c 
c [simplification-11] limit 123203 conflicts (hard 139992) hit after 123203 conflicts
c [quatres-5] found 34309 quaternary clauses 38% in total
c [ternres-7] limit 43952968 with penalty 0 = 0 + 0
c [ternres-7] all 86386 free variables schedulable
c [ternres-7] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-23] removed 49 variables
c [basicprobe-3] limit 219764844 penalty 0 = 0 + 0
c [basicprobe-3-0] 25782 probes remain 31% after last round
c [basicprobe-3-0] 964 units = 954 failed (99%) + 10 lifted (1%)
c [basicprobe-3-0] removed 3172 variables, found 711726 hbrs
c [bate-2] eliminated 582 asymmetric tautologies during probing
c [unhide-11] limit 549412 with penalty 4 = 0 + 4
c [unhide-11-11] 3 units, 158 failed, 9323 tauts, 0 hbrs, 2469985 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 127 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 82994 variables 100%
c [block-4] limit of 109882422 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 83 blocked clauses
c [block-4] 83 < 1/100 * 550466 = 5504 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 82991 variables 100%
c [elim-9] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 2274 variables 3% in round 1 in 49379107 steps
c [elim-9-1] backward subsumption/strengthening limit 49379100
c [elim-9-1-1] backward checking 7761 touched variables 9%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 3 and strengthened 511 clauses in 2470222 steps
c [elim-9-1] rescheduled 1187 variables 1% by backward subsumption
c [elim-9-2] eliminated 159 variables 0% in round 2 in 1236070 steps
c [elim-9-2] backward subsumption/strengthening limit 1236000
c [elim-9-2-1] backward checking 1198 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 3 and strengthened 4 clauses in 568731 steps
c [elim-9-2] rescheduled 10 variables 0% by backward subsumption
c [elim-9-3] eliminated 1 variables 0% in round 3 in 7873 steps
c [elim-9-3] backward subsumption/strengthening limit 7800
c [elim-9-3-1] backward checking 10 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 0 and strengthened 0 clauses in 7801 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 2445 = 3% variables out of 82991 scheduled
c [bca-7] limit of 10000000 steps and 1082450 added (scaled 2)
c [bca-7] 139329 out of 161094 literals actually usable 86%
c [bca-7] added 73 blocked clauses in 414298 steps
c [sweep-7] limit 13185890 penalty 0 = 0 + 0
c [sweep-7-1] 7051 pos 13.3% + 46161 neg 86.7% = 53212 sched 66.1% ret 27334
c [sweep-7-1] 13292126 steps 185 queries 3364.68 avg class size
c [sweep-7-1] 2206 decisions 155 SAT calls 110.33 avg env size
c [sweep-7-1] 51083 variables remain 63% (29454 retained 37%)
c [decomp-24] removed 131 variables
c [sweep-7-1] removed 131 vars (0 failed, 29 eqs, 59 impls)
c [sweep-7] removed 131 vars in TOTAL (1 rounds, 184 queries)
c [phase-count-11] 538436 negative 99.6% of 540459 except 2023 0.4%
c [phase-count-11] 432359 positive 80.0% of 540459 except 108100 20.0%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 37 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 22110 enqueued variables after 123203 conflicts
c [score-dist-11] active 58305 (73%), one 0 (0%), zero 22110 (27%)
c [score-dist-11] max exp 517, different 17 (3%)
c [score-dist-11] median active exp 509, avg 508.9
c [simplification-11] removed 5971 variables 6.9% (80415 remain 33%)
c [simplification-11] removed 36181 irredundant clauses 6.3% (540459 remain 40%)
c [simplification-11] maximum reduction of 7% = max (7%, 6%)
c [simplification-11] large reduction 7% >= 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 135203 (soft 125203 + delta 10000)
c [simplification-11] new conflict limit 125203 (hard 135203)
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  309.8   80414   540459    123498   13173   1023 839431 1163  1584   77  73%     70  555  756  569  133%
c i  310.6   80411   540459    124073   13567   1039 839454 1084  1602   79  68%     27  567  616  569  108%
c 
c [simplification-12] limit 125203 conflicts (hard 135203) hit after 127062 conflicts
c [ternres-8] limit 45215885 with penalty 0 = 0 + 0
c [ternres-8] all 80411 free variables schedulable
c [ternres-8] 116 ternary resolvents (0 bin, 116 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-25] removed 4 variables
c [simpleprobe-4] 22752 schedulable variables 28%
c [simpleprobe-4] limit 180863541 penalty 0 = 0 + 0
c [decomp-26] removed 2901 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 2901 variables, found 114650 hbrs, 1850 units
c [unhide-12] limit 4521588 with penalty 1 = 0 + 1
c [unhide-12-12] 5 units, 77 failed, 68895 tauts, 0 hbrs, 187694 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 188 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 1130397130 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 9 clauses out of 742 (1%) of length 7
c [cce-4-1] eliminated 72 clauses out of 2224 (3%) of length 6
c [cce-4-1] eliminated 27119 clauses out of 39356 (69%) of length 5
c [cce-4-1] eliminated 17660 clauses out of 32517 (54%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 44860 large clauses in 610332674 steps
c [cce-4-1] allowing another 305166337 steps for small clauses
c [cce-4-1] scheduling 409675 clauses = 264112 binary + 145563 ternary
c [cce-4-1] tried to eliminate 34227 small clauses 8%
c [cce-4-1] eliminated 6013 binary clauses 2%
c [cce-4-1] eliminated 1542 ternary clauses 1%
c [cce-4-1] eliminated 7555 small clauses 2%
c [cce-4-1] eliminated 8885 small clauses in 1130397133 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 53745 covered clauses in round 1
c [cce-4] eliminated 53745 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 77246 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 19858 variables 26% in round 1 in 38344804 steps
c [elim-10-1] backward subsumption/strengthening limit 38344800
c [elim-10-1-1] backward checking 42030 touched variables 54%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 26 and strengthened 74 clauses in 5880664 steps
c [elim-10-1] rescheduled 199 variables 0% by backward subsumption
c [elim-10-2] eliminated 8 variables 0% in round 2 in 107607 steps
c [elim-10-2] backward subsumption/strengthening limit 107600
c [elim-10-2-1] backward checking 95 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 0 and strengthened 6 clauses in 107601 steps
c [elim-10-2] rescheduled 15 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 14366 steps
c [elim-10-3] backward subsumption/strengthening limit 14300
c [elim-10-3-1] backward checking 10 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 0 and strengthened 2 clauses in 14301 steps
c [elim-10] incomplete 8 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 19867 = 26% variables out of 77246 scheduled
c [bca-8] limit of 10000000 steps and 823799 added (scaled 2)
c [bca-8] 107830 out of 114760 literals actually usable 94%
c [bca-8] added 459 blocked clauses in 255290 steps
c [sweep-8] limit 13564765 penalty 0 = 0 + 0
c [sweep-8-1] 7063 pos 16.9% + 34655 neg 83.1% = 41718 sched 72.7% ret 15661
c [sweep-8-1] 13601348 steps 263 queries 1703.84 avg class size
c [sweep-8-1] 2972 decisions 234 SAT calls 79.39 avg env size
c [sweep-8-1] 38586 variables remain 67% (18584 retained 33%)
c [decomp-27] removed 346 variables
c [sweep-8-1] removed 346 vars (0 failed, 29 eqs, 57 impls)
c [sweep-8] removed 346 vars in TOTAL (1 rounds, 262 queries)
c [phase-count-12] 408745 negative 99.8% of 409486 except 741 0.2%
c [phase-count-12] 308254 positive 75.3% of 409486 except 101232 24.7%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 21 negative 100%
c [sort-queue-12] sorted 13318 enqueued variables after 127062 conflicts
c [score-dist-12] active 43715 (77%), one 0 (0%), zero 13318 (23%)
c [score-dist-12] max exp 517, different 17 (3%)
c [score-dist-12] median active exp 509, avg 508.7
c [simplification-12] removed 23378 variables 29.1% (57033 remain 23%)
c [simplification-12] removed 130973 irredundant clauses 24.2% (409486 remain 30%)
c [simplification-12] maximum reduction of 29% = max (29%, 24%)
c [simplification-12] large reduction 29% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 139062 (soft 129062 + delta 10000)
c [simplification-12] new conflict limit 129062 (hard 139062)
c 
c [simplification-13] limit 129062 conflicts (hard 139062) hit after 129067 conflicts
c [quatres-6] found 26733 quaternary clauses 57% in total
c [quatres-6-2] added 17 quaternary resolvents
c [ternres-9] limit 45388613 with penalty 0 = 0 + 0
c [ternres-9] all 57033 free variables schedulable
c [ternres-9] 393 ternary resolvents (0 bin, 393 trn)
c [ternres-9] fully completed ternary resolution
c [unhide-13] limit 9077722 with penalty 0 = 0 + 0
c [unhide-13-16] 8 units, 104 failed, 42350 tauts, 0 hbrs, 127365 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 111 transitive binary clauses
c [cce-5] limit of 226943065 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 7 clauses out of 58 (12%) of length 7
c [cce-5-1] eliminated 275 clauses out of 3618 (8%) of length 6
c [cce-5-1] eliminated 2722 clauses out of 15578 (17%) of length 5
c [cce-5-1] eliminated 1 clauses out of 26127 (0%) of length 4
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 3005 large clauses in 226943072 steps
c [cce-5-1] allowing another 113471536 steps for small clauses
c [cce-5-1] scheduling 333726 clauses = 192850 binary + 140876 ternary
c [cce-5-1] tried to eliminate 4671 small clauses 1%
c [cce-5-1] eliminated 856 binary clauses 0%
c [cce-5-1] eliminated 290 ternary clauses 0%
c [cce-5-1] eliminated 1146 small clauses 0%
c [cce-5-1] eliminated 1390 small clauses in 226943070 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 4395 covered clauses in round 1
c [cce-5] eliminated 4395 covered clauses in TOTAL during 1 rounds
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 56910 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 397 variables 1% in round 1 in 33291058 steps
c [elim-11-1] backward subsumption/strengthening limit 33291000
c [elim-11-1-1] backward checking 2680 touched variables 5%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 14 clauses in 677307 steps
c [elim-11-1] rescheduled 41 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 21285 steps
c [elim-11-2] backward subsumption/strengthening limit 21200
c [elim-11-2-1] backward checking 21 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 21201 steps
c [elim-11-2] rescheduled 2 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 437 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 398 = 1% variables out of 56910 scheduled
c [elim-11] 398 < 1/100 * 56910 = 569 considered unsuccessful
c [bca-9] limit of 10000000 steps and 794586 added (scaled 2)
c [bca-9] 103615 out of 113026 literals actually usable 92%
c [bca-9] added 507 blocked clauses in 245053 steps
c [sweep-9] limit 13616583 penalty 0 = 0 + 0
c [sweep-9-1] 6525 pos 17.1% + 31566 neg 82.9% = 38091 sched 67.4% ret 18421
c [sweep-9-1] 13715942 steps 265 queries 2131.63 avg class size
c [sweep-9-1] 3138 decisions 248 SAT calls 86.47 avg env size
c [sweep-9-1] 35487 variables remain 63% (20964 retained 37%)
c [decomp-29] removed 143 variables
c [sweep-9-1] removed 143 vars (0 failed, 18 eqs, 36 impls)
c [sweep-9] removed 143 vars in TOTAL (1 rounds, 264 queries)
c [phase-count-13] 395384 negative 99.8% of 396099 except 715 0.2%
c [phase-count-13] 297896 positive 75.2% of 396099 except 98203 24.8%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 12709 enqueued variables after 129067 conflicts
c [score-dist-13] active 43660 (77%), one 0 (0%), zero 12709 (23%)
c [score-dist-13] max exp 517, different 17 (3%)
c [score-dist-13] median active exp 509, avg 508.7
c [simplification-13] removed 664 variables 1.2% (56369 remain 23%)
c [simplification-13] removed 13387 irredundant clauses 3.3% (396099 remain 29%)
c [simplification-13] maximum reduction of 3% = max (1%, 3%)
c [simplification-13] geometric conflict interval increment 8399 = 33597 / 4
c [simplification-13] new conflict interval 41996
c [simplification-13] penalized conflict interval 41996 = 1 * 41996
c [simplification-13] hard conflict limit 192061 (soft 171063 + delta 20998)
c [simplification-13] new conflict limit 171063 (hard 192061)
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  383.0   56368   396099    145157   13885   2740 593357  601   936  121  64%    244 -151  794  555  143%
c i  409.4   56349   396099    163583   20350   2851 593513  617   783  166  79%    182 -248  557  563   99%
c i  430.8   56348   396099    177460   23333   2897 593543  734   840  231  87%    106 -149  798  588  136%
c 
c [simplification-14] limit 171063 conflicts (hard 192061) hit after 192061 conflicts
c [quatres-7] found 26385 quaternary clauses 61% in total
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 15 quaternary resolvents
c [ternres-10] limit 60343117 with penalty 0 = 0 + 0
c [ternres-10] all 56348 free variables schedulable
c [ternres-10] 668 ternary resolvents (0 bin, 668 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1508577 penalty 3 = 3 + 0
c [gauss-4] extracted 8 xors of average arity 2.5
c [gauss-4] connected 20 occurrences of 18 variables (average 1.1)
c [gauss-4] limit 1508577 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-30] removed 2 variables
c [treelook-4] limit 3017155 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 74523 literals 66%
c [treelook-4] scheduling used 1607054 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 3017155 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 3022122 steps
c [treelook-4] 74404 literals remain 66%
c [treelook-4] 13237 variables remain to probed next time 23%
c [treelook-4] removed 1 variables, found 18472 hbrs
c [unhide-14] limit 3017155 with penalty 2 = 0 + 2
c [unhide-14-17] 1 units, 44 failed, 13840 tauts, 0 hbrs, 1001103 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 110 transitive binary clauses
c [cce-6] limit of 301715585 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 47 (2%) of length 7
c [cce-6-1] eliminated 1 clauses out of 3316 (0%) of length 6
c [cce-6-1] eliminated 27 clauses out of 12596 (0%) of length 5
c [cce-6-1] eliminated 5 clauses out of 26046 (0%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 34 large clauses in 301715588 steps
c [cce-6-1] allowing another 150857794 steps for small clauses
c [cce-6-1] scheduling 213367 clauses = 190664 binary + 22703 ternary
c [cce-6-1] tried to eliminate 12284 small clauses 6%
c [cce-6-1] eliminated 3250 binary clauses 2%
c [cce-6-1] eliminated 558 ternary clauses 2%
c [cce-6-1] eliminated 3808 small clauses 2%
c [cce-6-1] eliminated 4157 small clauses in 301715593 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 4191 covered clauses in round 1
c [cce-6] eliminated 4191 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 784646 added (scaled 2)
c [bca-10] 97315 out of 112624 literals actually usable 86%
c [bca-10] added 142 blocked clauses in 248399 steps
c [sweep-10] limit 18102935 penalty 0 = 0 + 0
c [sweep-10-1] 6267 pos 17.7% + 29132 neg 82.3% = 35399 sched 62.9% ret 20912
c [sweep-10-1] 18178546 steps 357 queries 1469.15 avg class size
c [sweep-10-1] 5705 decisions 331 SAT calls 130.25 avg env size
c [sweep-10-1] 32534 variables remain 58% (23688 retained 42%)
c [decomp-32] removed 152 variables
c [sweep-10-1] removed 152 vars (0 failed, 27 eqs, 61 impls)
c [sweep-10] removed 152 vars in TOTAL (1 rounds, 356 queries)
c [phase-count-14] 390104 negative 99.8% of 390813 except 709 0.2%
c [phase-count-14] 295045 positive 75.5% of 390813 except 95768 24.5%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 11840 enqueued variables after 192061 conflicts
c [score-dist-14] active 44319 (79%), one 0 (0%), zero 11840 (21%)
c [score-dist-14] max exp 518, different 18 (3%)
c [score-dist-14] median active exp 510, avg 509.5
c [simplification-14] removed 189 variables 0.3% (56159 remain 23%)
c [simplification-14] removed 5286 irredundant clauses 1.3% (390813 remain 29%)
c [simplification-14] maximum reduction of 1% = max (0%, 1%)
c [simplification-14] geometric conflict interval increment 20998 = 41996 / 2
c [simplification-14] new conflict interval 62994
c [simplification-14] penalized conflict interval 62994 = 1 * 62994
c [simplification-14] hard conflict limit 286552 (soft 255055 + delta 31497)
c [simplification-14] new conflict limit 255055 (hard 286552)
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  477.2   56158   390813    201918   25487   4063 622487  851   911  183  93%    241  -46  858  669  128%
c i  487.8   56157   390813    210496   26128   4093 622511  875   951  239  92%     -4   -3  592  698   85%
c i  496.2   56156   390813    217465   30654   4120 622524  581  1014  239  57%    -23   57  384  677   57%
c i  498.1   56154   390813    219781   32789   4126 622525  424  1108  241  38%    -82  147  374  661   57%
c i  499.8   56153   390813    220638   33101   4129 622525  506  1115  241  45%    -94  151  865  663  130%
c i  510.4   56152   390813    225428   34921   4136 622537  671  1109  241  61%    -47  136  225  672   34%
c i  512.0   56059   390813    227084   36256   4144 622542  567  1128  263  50%    -80  151  612  664   92%
c i  527.0   56058   390813    235849   39718   4169 622564  662   967  377  68%     22  -15  465  668   70%
c i  549.2   56006   390813    250165   44936   4201 622591  677   881  377  77%    107  -88  488  676   72%
c i  553.3   55858   390813    254161   48336   4221 622607  439   871  377  50%    -48  -92   80  655   12%
c -  558.1   55858   390813    259039   23909   4253 622624  313   931   76  34%    -34  -29  424  625   68%
c 
c [simplification-15] limit 255055 conflicts (hard 286552) hit after 286552 conflicts
c [quatres-8] found 25981 quaternary clauses 60% in total
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 4 quaternary resolvents
c [ternres-11] limit 83445249 with penalty 0 = 0 + 0
c [ternres-11] all 55858 free variables schedulable
c [ternres-11] 473 ternary resolvents (1 bin, 472 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 2607664 penalty 4 = 4 + 0
c [card-5] found 3070 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2607664 for elimination
c [card-5] 3070 out of 3070 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-33] removed 306 variables
c [basicprobe-4] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 18192 sched 35%, 1896 failed, 146 lifted, 1173647 hbrs
c [decomp-34] removed 3672 variables
c [basicprobe-4-1] 12804 probes remain 25% after last round
c [basicprobe-4-1] 2225 units = 2065 failed (93%) + 160 lifted (7%)
c [basicprobe-4-1] removed 3963 variables, found 1318119 hbrs
c [bate-3] eliminated 1838 asymmetric tautologies during probing
c [unhide-15] limit 4172262 with penalty 2 = 0 + 2
c [unhide-15-19] 1 units, 48 failed, 142136 tauts, 0 hbrs, 487624 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 156 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 51843 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 500 blocked clauses
c [block-5] 500 < 1/100 * 346696 = 3466 considered unsuccessful
c [cce-7] limit of 417226245 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 2 clauses out of 2848 (0%) of length 6
c [cce-7-1] eliminated 34 clauses out of 10428 (0%) of length 5
c [cce-7-1] eliminated 2152 clauses out of 20702 (10%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 2188 large clauses in 381842522 steps
c [cce-7-1] allowing another 190921261 steps for small clauses
c [cce-7-1] scheduling 292534 clauses = 176790 binary + 115744 ternary
c [cce-7-1] tried to eliminate 12232 small clauses 4%
c [cce-7-1] eliminated 2145 binary clauses 1%
c [cce-7-1] eliminated 442 ternary clauses 0%
c [cce-7-1] eliminated 2587 small clauses 1%
c [cce-7-1] eliminated 2587 small clauses in 417226249 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 4775 covered clauses in round 1
c [cce-7] eliminated 4775 covered clauses in TOTAL during 1 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 51811 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 1974 variables 4% in round 1 in 29522856 steps
c [elim-12-1] backward subsumption/strengthening limit 29522800
c [elim-12-1-1] backward checking 10465 touched variables 20%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 20 and strengthened 91 clauses in 2399524 steps
c [elim-12-1] rescheduled 266 variables 1% by backward subsumption
c [elim-12-2] eliminated 24 variables 0% in round 2 in 247115 steps
c [elim-12-2] backward subsumption/strengthening limit 247100
c [elim-12-2-1] backward checking 232 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 3 and strengthened 20 clauses in 196109 steps
c [elim-12-2] rescheduled 68 variables 0% by backward subsumption
c [elim-12-3] eliminated 9 variables 0% in round 3 in 150660 steps
c [elim-12-3] backward subsumption/strengthening limit 150600
c [elim-12-3-1] backward checking 87 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 9 and strengthened 10 clauses in 150601 steps
c [elim-12] incomplete 47 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 2007 = 4% variables out of 51811 scheduled
c [bca-11] limit of 10000000 steps and 677581 added (scaled 2)
c [bca-11] 83055 out of 99610 literals actually usable 83%
c [bca-11] added 186 blocked clauses in 205816 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 250335740 penalty 0 = 0 + 0
c [sweep-11-1] 6079 pos 21.0% + 22862 neg 79.0% = 28941 sched 58.1% ret 20863
c [sweep-11-1] 244456351 steps 8354 queries 64.40 avg class size
c [sweep-11-1] 48579 decisions 6643 SAT calls 69.03 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-35] removed 2445 variables
c [sweep-11-1] removed 2445 vars (0 failed, 1732 eqs, 1765 impls)
c [sweep-11-2] 7788 pos 16.4% + 39571 neg 83.6% = 47359 sched 100.0% ret 0
c [sweep-11-2] 5891306 steps 92 queries 4196.39 avg class size
c [sweep-11-2] 2527 decisions 90 SAT calls 209.80 avg env size
c [sweep-11-2] 45438 variables remain 96% (1891 retained 4%)
c [decomp-36] removed 36 variables
c [sweep-11-2] removed 36 vars (0 failed, 1 eqs, 2 impls)
c [sweep-11] removed 2481 vars in TOTAL (2 rounds, 8444 queries)
c [phase-count-15] 330319 negative 99.8% of 331029 except 710 0.2%
c [phase-count-15] 248624 positive 75.1% of 331029 except 82405 24.9%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 7413 enqueued variables after 286552 conflicts
c [score-dist-15] active 39910 (84%), one 0 (0%), zero 7413 (16%)
c [score-dist-15] max exp 519, different 19 (4%)
c [score-dist-15] median active exp 511, avg 510.3
c [simplification-15] removed 8535 variables 15.3% (47323 remain 19%)
c [simplification-15] removed 59784 irredundant clauses 15.3% (331029 remain 24%)
c [simplification-15] maximum reduction of 15% = max (15%, 15%)
c [simplification-15] large reduction 15% >= 5% limit
c [simplification-15] next conflict interval 2865 = min (286552/100, 62994)
c [simplification-15] penalized conflict interval 2865 = 1 * 2865
c [simplification-15] hard conflict limit 299417 (soft 289417 + delta 10000)
c [simplification-15] new conflict limit 289417 (hard 299417)
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  644.2   47322   331029    286599   20134   3482 1303789  737   748   94  98%    329 -155  670  664  101%
c i  656.9   47296   331029    294264   21624   3485 1303796  640   659  124  97%    -52 -222  601  660   91%
c 
c [simplification-16] limit 289417 conflicts (hard 299417) hit after 299417 conflicts
c [quatres-9] found 20955 quaternary clauses 57% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-2] added 4 single-self-subsuming ternary resolvents
c [quatres-9-2] added 15 quaternary resolvents
c [ternres-12] limit 88584818 with penalty 0 = 0 + 0
c [ternres-12] all 47296 free variables schedulable
c [ternres-12] 2765 ternary resolvents (0 bin, 2765 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-37] removed 27 variables
c [simpleprobe-5] all 47296 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-38] removed 139 variables
c [simpleprobe-5] 3412 variables remain 7% (43745 retained 93%)
c [simpleprobe-5] removed 139 variables, found 164535 hbrs, 109 units
c [unhide-16] limit 4429240 with penalty 2 = 0 + 2
c [unhide-16-20] 0 units, 12 failed, 167217 tauts, 0 hbrs, 33815 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 291 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 4429240920 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 118
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 114
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 110
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 106
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 102
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 98
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 94
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 90
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 86
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 85
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 83
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 82
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 81
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 79
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 78
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 77
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 76
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 75
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 74
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 73
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 72
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 71
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 70
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 69
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 68
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 67
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 66
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 65
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 64
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 63
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 62
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 61
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 60
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 59
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 58
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 57
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 56
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 55
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 54
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 53
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 52
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 51
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 50
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 49
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 48
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 47
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 46
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 45
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 44
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 43
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 42
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 41
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 40
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 39
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 38
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 37
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 36
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 35
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 34
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 33
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 32
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 31
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 30
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 29
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 28
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 27
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 26
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 25
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 24
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 23
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 22
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 21
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 20
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 19
c [cce-8-1] eliminated 6 clauses out of 11 (55%) of length 18
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 17
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 16
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 15
c [cce-8-1] eliminated 8 clauses out of 15 (53%) of length 14
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 13
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 12
c [cce-8-1] eliminated 5 clauses out of 9 (56%) of length 11
c [cce-8-1] eliminated 20 clauses out of 28 (71%) of length 10
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 9
c [cce-8-1] eliminated 5 clauses out of 11 (45%) of length 8
c [cce-8-1] eliminated 10 clauses out of 69 (14%) of length 7
c [cce-8-1] eliminated 18 clauses out of 2772 (1%) of length 6
c [cce-8-1] eliminated 80 clauses out of 9964 (1%) of length 5
c [cce-8-1] eliminated 1169 clauses out of 20147 (6%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 1549 large clauses in 434012376 steps
c [cce-8-1] allowing another 217006188 steps for small clauses
c [cce-8-1] scheduling 277837 clauses = 170873 binary + 106964 ternary
c [cce-8-1] tried to eliminate 238810 small clauses 86%
c [cce-8-1] eliminated 34998 binary clauses 20%
c [cce-8-1] eliminated 5686 ternary clauses 5%
c [cce-8-1] eliminated 40684 small clauses 15%
c [cce-8-1] eliminated 40750 small clauses in 4429240925 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 42299 covered clauses in round 1
c [cce-8] eliminated 42299 covered clauses in TOTAL during 1 rounds
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 47152 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 2102 variables 4% in round 1 in 28694263 steps
c [elim-13-1] backward subsumption/strengthening limit 28694200
c [elim-13-1-1] backward checking 11557 touched variables 25%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 2 and strengthened 75 clauses in 2146769 steps
c [elim-13-1] rescheduled 178 variables 0% by backward subsumption
c [elim-13-2] eliminated 8 variables 0% in round 2 in 261430 steps
c [elim-13-2] backward subsumption/strengthening limit 261400
c [elim-13-2-1] backward checking 77 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 1 and strengthened 0 clauses in 113388 steps
c [elim-13-2] rescheduled 4 variables 0% by backward subsumption
c [elim-13-3] no variable eliminated in round 3 in 21071 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 2110 = 4% variables out of 47152 scheduled
c [bca-12] limit of 10000000 steps and 565832 added (scaled 2)
c [bca-12] 70912 out of 90086 literals actually usable 79%
c [bca-12] added 166 blocked clauses in 168616 steps
c [sweep-12] limit 26575445 penalty 0 = 0 + 0
c [sweep-12-1] 7497 pos 17.3% + 35765 neg 82.7% = 43262 sched 96.0% ret 1780
c [sweep-12-1] 26585688 steps 526 queries 651.87 avg class size
c [sweep-12-1] 8367 decisions 510 SAT calls 130.81 avg env size
c [sweep-12-1] 30909 variables remain 69% (14107 retained 31%)
c [decomp-39] removed 45 variables
c [sweep-12-1] removed 45 vars (0 failed, 19 eqs, 53 impls)
c [sweep-12] removed 45 vars in TOTAL (1 rounds, 525 queries)
c [phase-count-16] 281268 negative 99.8% of 281843 except 575 0.2%
c [phase-count-16] 218519 positive 77.5% of 281843 except 63324 22.5%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-16] sorted 7119 enqueued variables after 299417 conflicts
c [score-dist-16] active 37878 (84%), one 0 (0%), zero 7119 (16%)
c [score-dist-16] max exp 519, different 19 (4%)
c [score-dist-16] median active exp 511, avg 510.4
c [simplification-16] removed 2299 variables 4.9% (44997 remain 18%)
c [simplification-16] removed 49186 irredundant clauses 14.9% (281843 remain 21%)
c [simplification-16] maximum reduction of 15% = max (5%, 15%)
c [simplification-16] large reduction 15% >= 5% limit
c [simplification-16] next conflict interval 2994 = min (299417/100, 62994)
c [simplification-16] penalized conflict interval 2994 = 1 * 2994
c [simplification-16] hard conflict limit 312411 (soft 302411 + delta 10000)
c [simplification-16] new conflict limit 302411 (hard 312411)
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  761.2   44996   281843    305867   18288   8368 1122709  327   692   83  47%     20 -150  166  622   27%
c 
c [simplification-17] limit 302411 conflicts (hard 312411) hit after 312414 conflicts
c [quatres-10] found 20509 quaternary clauses 54% in total
c [quatres-10-2] added 2 single-self-subsuming ternary resolvents
c [quatres-10-2] added 5 quaternary resolvents
c [ternres-13] limit 90569609 with penalty 0 = 0 + 0
c [ternres-13] all 44995 free variables schedulable
c [ternres-13] 631 ternary resolvents (0 bin, 631 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-40] removed 2 variables
c [treelook-5] limit 9056960 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 62690 literals 70%
c [treelook-5] scheduling used 1844996 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 9056960 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 9206372 steps
c [treelook-5] 62525 literals remain 69%
c [treelook-5] 10050 variables remain to probed next time 22%
c [treelook-5] removed 6 variables, found 27617 hbrs
c [unhide-17] limit 9056960 with penalty 1 = 0 + 1
c [unhide-17-24] 1 units, 18 failed, 85425 tauts, 0 hbrs, 254336 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 83 transitive binary clauses
c [cce-9] limit of 452848047 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 118
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 117
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 116
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 115
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 114
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 113
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 112
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 111
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 110
c [cce-9-1] eliminated 3 clauses out of 4 (75%) of length 108
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 107
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 106
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 105
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 104
c [cce-9-1] eliminated 3 clauses out of 4 (75%) of length 103
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 102
c [cce-9-1] eliminated 3 clauses out of 4 (75%) of length 101
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 100
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 99
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 98
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 97
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 96
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 95
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 94
c [cce-9-1] eliminated 3 clauses out of 5 (60%) of length 93
c [cce-9-1] eliminated 3 clauses out of 5 (60%) of length 92
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 91
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 90
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 89
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 88
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 87
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 86
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 85
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 84
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 83
c [cce-9-1] eliminated 4 clauses out of 7 (57%) of length 82
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 81
c [cce-9-1] eliminated 2 clauses out of 6 (33%) of length 80
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 79
c [cce-9-1] eliminated 4 clauses out of 8 (50%) of length 78
c [cce-9-1] eliminated 5 clauses out of 9 (56%) of length 77
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 76
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 75
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 74
c [cce-9-1] eliminated 3 clauses out of 8 (38%) of length 73
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 72
c [cce-9-1] eliminated 3 clauses out of 5 (60%) of length 71
c [cce-9-1] eliminated 2 clauses out of 6 (33%) of length 70
c [cce-9-1] eliminated 3 clauses out of 8 (38%) of length 69
c [cce-9-1] eliminated 2 clauses out of 6 (33%) of length 68
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 67
c [cce-9-1] eliminated 3 clauses out of 9 (33%) of length 66
c [cce-9-1] eliminated 3 clauses out of 8 (38%) of length 65
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 64
c [cce-9-1] eliminated 2 clauses out of 8 (25%) of length 63
c [cce-9-1] eliminated 4 clauses out of 7 (57%) of length 62
c [cce-9-1] eliminated 5 clauses out of 10 (50%) of length 61
c [cce-9-1] eliminated 4 clauses out of 8 (50%) of length 60
c [cce-9-1] eliminated 4 clauses out of 10 (40%) of length 59
c [cce-9-1] eliminated 5 clauses out of 10 (50%) of length 58
c [cce-9-1] eliminated 4 clauses out of 10 (40%) of length 57
c [cce-9-1] eliminated 5 clauses out of 11 (45%) of length 56
c [cce-9-1] eliminated 4 clauses out of 11 (36%) of length 55
c [cce-9-1] eliminated 6 clauses out of 15 (40%) of length 54
c [cce-9-1] eliminated 5 clauses out of 12 (42%) of length 53
c [cce-9-1] eliminated 5 clauses out of 12 (42%) of length 52
c [cce-9-1] eliminated 4 clauses out of 11 (36%) of length 51
c [cce-9-1] eliminated 5 clauses out of 11 (45%) of length 50
c [cce-9-1] eliminated 6 clauses out of 12 (50%) of length 49
c [cce-9-1] eliminated 6 clauses out of 13 (46%) of length 48
c [cce-9-1] eliminated 5 clauses out of 14 (36%) of length 47
c [cce-9-1] eliminated 5 clauses out of 11 (45%) of length 46
c [cce-9-1] eliminated 5 clauses out of 11 (45%) of length 45
c [cce-9-1] eliminated 5 clauses out of 10 (50%) of length 44
c [cce-9-1] eliminated 6 clauses out of 12 (50%) of length 43
c [cce-9-1] eliminated 6 clauses out of 11 (55%) of length 42
c [cce-9-1] eliminated 5 clauses out of 12 (42%) of length 41
c [cce-9-1] eliminated 5 clauses out of 12 (42%) of length 40
c [cce-9-1] eliminated 5 clauses out of 11 (45%) of length 39
c [cce-9-1] eliminated 7 clauses out of 13 (54%) of length 38
c [cce-9-1] eliminated 6 clauses out of 13 (46%) of length 37
c [cce-9-1] eliminated 5 clauses out of 13 (38%) of length 36
c [cce-9-1] eliminated 6 clauses out of 13 (46%) of length 35
c [cce-9-1] eliminated 9 clauses out of 16 (56%) of length 34
c [cce-9-1] eliminated 7 clauses out of 14 (50%) of length 33
c [cce-9-1] eliminated 5 clauses out of 13 (38%) of length 32
c [cce-9-1] eliminated 6 clauses out of 16 (38%) of length 31
c [cce-9-1] eliminated 10 clauses out of 20 (50%) of length 30
c [cce-9-1] eliminated 8 clauses out of 18 (44%) of length 29
c [cce-9-1] eliminated 11 clauses out of 19 (58%) of length 28
c [cce-9-1] eliminated 9 clauses out of 20 (45%) of length 27
c [cce-9-1] eliminated 11 clauses out of 21 (52%) of length 26
c [cce-9-1] eliminated 9 clauses out of 21 (43%) of length 25
c [cce-9-1] eliminated 9 clauses out of 19 (47%) of length 24
c [cce-9-1] eliminated 8 clauses out of 19 (42%) of length 23
c [cce-9-1] eliminated 10 clauses out of 19 (53%) of length 22
c [cce-9-1] eliminated 9 clauses out of 24 (38%) of length 21
c [cce-9-1] eliminated 12 clauses out of 24 (50%) of length 20
c [cce-9-1] eliminated 10 clauses out of 24 (42%) of length 19
c [cce-9-1] eliminated 12 clauses out of 24 (50%) of length 18
c [cce-9-1] eliminated 9 clauses out of 25 (36%) of length 17
c [cce-9-1] eliminated 11 clauses out of 24 (46%) of length 16
c [cce-9-1] eliminated 11 clauses out of 23 (48%) of length 15
c [cce-9-1] eliminated 12 clauses out of 30 (40%) of length 14
c [cce-9-1] eliminated 16 clauses out of 32 (50%) of length 13
c [cce-9-1] eliminated 16 clauses out of 32 (50%) of length 12
c [cce-9-1] eliminated 17 clauses out of 39 (44%) of length 11
c [cce-9-1] eliminated 23 clauses out of 77 (30%) of length 10
c [cce-9-1] eliminated 31 clauses out of 65 (48%) of length 9
c [cce-9-1] eliminated 41 clauses out of 99 (41%) of length 8
c [cce-9-1] eliminated 60 clauses out of 167 (36%) of length 7
c [cce-9-1] eliminated 100 clauses out of 2945 (3%) of length 6
c [cce-9-1] eliminated 141 clauses out of 10214 (1%) of length 5
c [cce-9-1] eliminated 7 clauses out of 19846 (0%) of length 4
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 929 large clauses in 452848048 steps
c [cce-9-1] allowing another 226424024 steps for small clauses
c [cce-9-1] scheduling 149626 clauses = 133516 binary + 16110 ternary
c [cce-9-1] tried to eliminate 15065 small clauses 10%
c [cce-9-1] eliminated 981 binary clauses 1%
c [cce-9-1] eliminated 322 ternary clauses 2%
c [cce-9-1] eliminated 1303 small clauses 1%
c [cce-9-1] eliminated 1322 small clauses in 452848050 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 2251 covered clauses in round 1
c [cce-9] eliminated 2251 covered clauses in TOTAL during 1 rounds
c [cce-9] 2251 < 1/100 * 281090 = 2810 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 44977 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 170 variables 0% in round 1 in 25554799 steps
c [elim-14-1] backward subsumption/strengthening limit 25554700
c [elim-14-1-1] backward checking 1634 touched variables 4%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 1 and strengthened 7 clauses in 393569 steps
c [elim-14-1] rescheduled 22 variables 0% by backward subsumption
c [elim-14-2] eliminated 1 variables 0% in round 2 in 10323 steps
c [elim-14-2] backward subsumption/strengthening limit 10300
c [elim-14-2-1] backward checking 11 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 0 and strengthened 0 clauses in 10301 steps
c [elim-14-2] fully rescheduled 44806 variables 100%
c [elim-14-3] eliminated 9 variables 0% in round 3 in 25529943 steps
c [elim-14-3] backward subsumption/strengthening limit 25529900
c [elim-14-3-1] backward checking 100 touched variables 0%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 0 and strengthened 0 clauses in 76167 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 180 = 0% variables out of 44977 scheduled
c [elim-14] 180 < 1/100 * 44977 = 449 considered unsuccessful
c [bca-13] limit of 10000000 steps and 558839 added (scaled 2)
c [bca-13] 69216 out of 89596 literals actually usable 77%
c [bca-13] added 38 blocked clauses in 171816 steps
c [sweep-13] limit 27170882 penalty 0 = 0 + 0
c [sweep-13-1] 6865 pos 22.3% + 23900 neg 77.7% = 30765 sched 68.7% ret 14032
c [sweep-13-1] 27214341 steps 618 queries 509.50 avg class size
c [sweep-13-1] 8320 decisions 594 SAT calls 110.34 avg env size
c [sweep-13-1] 23421 variables remain 52% (21359 retained 48%)
c [decomp-42] removed 42 variables
c [sweep-13-1] removed 42 vars (0 failed, 25 eqs, 67 impls)
c [sweep-13] 42 < 1/1000 * 44797 = 44 considered unsuccessful
c [sweep-13] removed 42 vars in TOTAL (1 rounds, 617 queries)
c [phase-count-17] 277778 negative 99.8% of 278343 except 565 0.2%
c [phase-count-17] 215906 positive 77.6% of 278343 except 62437 22.4%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-17] sorted 6862 enqueued variables after 312414 conflicts
c [score-dist-17] active 37893 (85%), one 0 (0%), zero 6862 (15%)
c [score-dist-17] max exp 519, different 19 (4%)
c [score-dist-17] median active exp 511, avg 510.5
c [simplification-17] removed 240 variables 0.5% (44755 remain 18%)
c [simplification-17] removed 3500 irredundant clauses 1.2% (278343 remain 20%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 31497 = 62994 / 2
c [simplification-17] new conflict interval 94491
c [simplification-17] penalized conflict interval 94491 = 1 * 94491
c [simplification-17] hard conflict limit 454150 (soft 406905 + delta 47245)
c [simplification-17] new conflict limit 406905 (hard 454150)
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  808.3   44754   278343    330665   25896   8540 1070437  538   663  159  81%    210 -132  529  600   88%
c i  812.3   44753   278343    333769   27327   8547 1070440  506   657  159  77%   -108 -132  528  594   89%
c i  869.0   44752   278343    378651   32477   8595 1070448  556   624  379  89%    419  -89  332  599   55%
c i  886.5   44749   278343    393211   35331   8636 1070461  753   786  388  96%    -31   72  736  612  120%
c 
c [simplification-18] limit 406905 conflicts (hard 454150) hit after 408157 conflicts
c [quatres-11] found 20629 quaternary clauses 55% in total
c [quatres-11-2] added 3 single-self-subsuming ternary resolvents
c [quatres-11-2] added 8 quaternary resolvents
c [ternres-14] limit 114555667 with penalty 0 = 0 + 0
c [ternres-14] all 44748 free variables schedulable
c [ternres-14] 193 ternary resolvents (0 bin, 193 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-43] removed 7 variables
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 12177 sched 28%, 538 failed, 13 lifted, 444607 hbrs
c [decomp-44] removed 789 variables
c [basicprobe-5-1] 2822 probes remain 6% after last round
c [basicprobe-5-1] 730 units = 713 failed (98%) + 17 lifted (2%)
c [basicprobe-5-1] removed 1243 variables, found 581994 hbrs
c [bate-4] eliminated 240 asymmetric tautologies during probing
c [unhide-18] limit 5000000 with penalty 2 = 0 + 2
c [unhide-18-25] 0 units, 1 failed, 112835 tauts, 0 hbrs, 369523 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 93 transitive binary clauses
c [bca-14] limit of 10000000 steps and 536430 added (scaled 2)
c [bca-14] 65692 out of 87010 literals actually usable 75%
c [bca-14] added 68 blocked clauses in 176683 steps
c [phase-count-18] 266720 negative 99.8% of 267316 except 596 0.2%
c [phase-count-18] 205058 positive 76.7% of 267316 except 62258 23.3%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 6141 enqueued variables after 408157 conflicts
c [score-dist-18] active 37363 (86%), one 0 (0%), zero 6141 (14%)
c [score-dist-18] max exp 520, different 20 (4%)
c [score-dist-18] median active exp 512, avg 510.9
c [simplification-18] removed 1244 variables 2.8% (43504 remain 18%)
c [simplification-18] removed 11027 irredundant clauses 4.0% (267316 remain 20%)
c [simplification-18] maximum reduction of 4% = max (3%, 4%)
c [simplification-18] geometric conflict interval increment 18898 = 94491 / 5
c [simplification-18] new conflict interval 113389
c [simplification-18] penalized conflict interval 113389 = 1 * 113389
c [simplification-18] hard conflict limit 578240 (soft 521546 + delta 56694)
c [simplification-18] new conflict limit 521546 (hard 578240)
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2726 basic ate = 2663 trn 98% + 63 lrg 2% in 4 updates
c bcas: 14 count, 2664 added (282 skipped), 4924194 steps
c bkwd: tried 489822 clauses, 979399 lits, 2.00 lits/clause
c bkwd: checked 14201035 occs, 28.99 occs/clause, 14.50 occs/lit
c bkwd: subsumed 4 binary, 56 ternary, 14 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 991 large (0% self)
c blkd: 5 bces, 13028 removed, 9540502 resolutions, 26567750 steps
c blkd: 16542 blocking literals 3%, 35 pure
c bump: 485565 bumped seen, 850592867 lits 1751.8 on average
c card: 5 count, 0 units, 0 am1, 215588358 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 87037 subsumed
c card: 21137 at-most-one constraints found, average size 4.68
c card: 21137 at-most-one constraints used 100%, average size 4.68
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 9 cces, 114085 eliminated, 112983 ate 99%, 1102 abce 1%
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: 4685371 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 135 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 44 decompositions, 10133 equivalent 4%
c deco: 338426 decision-only clauses 70%, 52% reduction
c decs: 10289162 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 14 elims, 109754 eliminated 42%, 154 pure 0%
c elms: 35 rounds, 2.5 rounds/bve
c elms: 85559 small 78%, 24006 large 22%
c elms: 226085 tried small, 85559 succeeded 38%, 140526 failed 62%
c elms: 47804 subsumed, 72885 strengthened, 1527 blocked
c elms: 23851555 copies, 23716897 resolutions, 6013763 ipos
c elms: 6408723 subchks, 4267736 strchks
c gaus: 4 extractions, 366 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12599554 steps, 6299777 extr 50%, 4207 elim 0%
c glue: 631.9 orig avg, 631.9 real avg, 11.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 3470690 = 369351 simple 11% + 3076840 trn 89% + 24499 lrg 1%, 6192 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 485564 clauses, 747.0 length
c lrnd: 362708296 lits = 665189838 orig - 302481542 removed 45%
c lrnd: 156694 uips 32%, 252805 flips 52%
c mins: 81490 mins 19%, 1350 bin 0%, 2454 size 1%
c mins: 37510267 poisoned searches, 8521325 hits, 23% hit rate
c mins: 46647010 used twice searches, 5451094 hits, 12% hit rate
c move: moved 79102, 61027 bin 77%, 18075 trn 23%
c otfs: 4534 driving 23%, 14768 restarting 77%
c otfs: str 19302, 19249 red 100%, 53 irr 0%
c otfs: str 19302, 0 bin 0%, 58 trn 0%, 19244 lrg 100%
c otfs: sub 13, 13 red 100%, 0 irr 0%
c otfs: sub 13, 0 bin 0%, 0 trn 0%, 13 lrg 100%
c phas: 18 computed, 135916 set, 37 pos (0%), 135879 neg (100%)
c prbs: 5 basic, 101838 probed, 3888 failed, 187 lifted
c prbs: 5 simple, 760695 probed, 2667 failed, 701 eqs
c prbs: 5 treelook, 307 probed, 6 failed, 0 lifted
c prom: 867 locked 0% out of 574739 tried
c prps: 1798867482 props, 165 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 11 count, 71 quat, 11 self1, 0 self2, 471 dup
c queu: 18 sorted, 10289162 next (40953 steps 0.00)
c queu: 851565133 enq (2266190488 steps 2.66), 850594805 deq 100%
c redc: 1751 clauses 24%, 7401 tried 2%, 51 sat 1%
c redc: 3678 lits 6%, 65366 tried 0%, 51 sat 0%
c redc: 177 times jump level reduced, 155.4 levels on average
c reds: 1 count, 486411.0 conflicts per reduce
c reds: 0 memlim 0%, 1 arith 100%
c reds: 25014 collected 87%, 3675 retired 13%
c rmbd: 59964 removed, 18408 red 31%
c rsts: 7663 restarts 61%, 4821 skipped 39%
c rsts: 4821 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 18 count, 16 confs 89%, 0 vars 0%
c simp: 1 its 6%, 1 bin 6%, 0 trns 0%
c subl: 485564 count (782979 tried 1.6), 332222 sub out of 481437 (69.0%)
c swps: 13 count, 14 rounds, 11831 queries (845.1/round)
c swps: 9833 sat calls, 95 unsat (0.4% success rate)
c swps: 93715 decisions 9.5, 3688 conflicts 0.4
c swps; 642.5 avg class size, 81.8 avg environment size
c swps: 0 failed, 2401 impls, 2039 equivs
c swp0: 3938 type 0 queries, 2718 unsat (69.0%), 3117 sat (79.2%)
c swp1: 7893 type 1 queries, 5050 unsat (64.0%), 6675 sat (84.6%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 21549940 calls to obtain time
c tops: 96225 fixed 37%, 154 its, 3158.51 confs/it
c trds: 14 transitive reductions, 2560 removed, 8 failed
c trds: 12814 nodes, 40128 edges, 28015704 steps
c trim: 1634943 words, 6.2 MB
c trnr: 14 count, 1 bin, 5369 trn, 191631794 steps
c unhd: 18 count, 25 rounds, 92996228 steps
c unhd: 982 non-trivial sccs of average size 2.0
c unhd: 34 units, 34 bin, 0 trn, 0 lrg
c unhd: 13416 failed, 13235 stamp, 0 lits, 167 bin, 10 trn, 0 lrg
c unhd: 737269 tauts, 20805 bin 3%, 14459 trn 2%, 467 lrg 0%
c unhd: 737269 tauts, 701538 stamp 95%, 668575 red 91%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 9028224 str, 34 bin 0%, 2840 trn 0%, 9025350 lrg 100%, 9009567 red 100%
c vars: 43504 remaining 17% and 216112 removed 83% out of 259616
c vars: 96225 fixed 37%, 109754 eliminated 42%, 10133 equivalent 4%
c vsts: 13879701653 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 7.6 search visits per propagation, 26539.8 per conflict
c wchs: 861809300 pushed, 50147236 enlarged, 197 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         481508         25014          3675      29885131      11488985        240669
c 
c  0 0          6613   1        19   0         0   0   7477624  25   1441216  13     11208   5     0.2
c  1 5          1289   0         0   0        74   2   1296116   4    361770   3      2384   1     0.1
c  2 6          2833   1         4   0        86   2   2229646   7    596856   5      5912   2     0.2
c  3 9          3605   1         7   0        78   2   2201203   7    725303   6      5548   2     0.4
c  4 14         4099   1        18   0        84   2   2265876   8    974974   8     10442   4     0.5
c  5 21         4617   1        34   0       114   3   1561518   5<   602450   5     12677   5     0.7
c  6 30         5219   1        97   0        60   2   1416327   5    592144   5      6025   3     1.1
c  7 41         5317   1       201   1       138   4   1414052   5    579849   5<     4674   2     1.2
c  8 54         5905   1       347   1       104   3   1397681   5    572855   5      6068   3     1.9
c  9 69         6708   1       563   2       103   3   1503198   5    785918   7      6292   3     3.0
c 10 86        14388   3      1809   7       246   7   2192551   7   1000438   9     17281   7<    8.1
c 11 126       27423   6      6806  27       434  12<  2103922   7   1190119  10     29253  12    26.8
c 12 230       42700   9<     9389  38<      465  13   2199456   7   1634709  14    100959  42    59.9
c 13 534      341896  71      5720  23      1689  46    612081   2    422547   4     21775   9   226.6
c 14 1526       8896   2         0   0         0   0     13880   0      7837   0       171   0    37.5
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                 12.0          11.6          10.7           5.1           6.8           9.6
c std                  2.5           1.3           3.3           4.3           4.3           3.8
c 
c  189.231  19% bump
c  152.308  15% cce
c   64.962   7% probe
c   41.396   4% unhide
c   28.190   3% sweep
c   21.336   2% elim
c    6.483   1% decide
c 
c   13.897 < 1% rest (below)
c 
c    3.984   0% bca
c    3.595   0% block
c    2.041   0% gauss
c    1.772   0% transred
c    1.435   0% ternres
c    0.611   0% quatres
c    0.459   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.072   1% preprocessing     2%
c  332.302  33% inprocessing     98%
c ==================================
c  337.374  34% simplifying
c  661.834  66% search
c ==================================
c  999.212 100% all
c 
c        486411 conflicts,         486.8 confs/sec
c          1414 ternaries,         344.0 confs/ternary
c          1497 binaries,          324.9 confs/binary
c           154 iterations,       3158.5 confs/iteration
c 
c             1 reductions,          0.0 redus/sec, 486411.0 confs/reduction
c          7663 restarts,            7.7 rests/sec,     63.5 confs/restart
c      10289162 decisions,       10297.3 decis/sec,     21.2 decis/conflict
c    1798867482 propagations,  1800285.5 props/sec,    174.8 props/decision
c 
c 999.2 seconds, 407.6 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
