c launch: /data/cnf/sc2014/app/ACG-20-5p0.cnf.bz2
c host: atom06
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/ACG-20-5p0.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/ACG-20-5p0.cnf.bz2
c no embedded options
c found 'p cnf 324716 1390931' header
c read 324716 variables, 1390931 clauses, 3269132 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=0
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 313313 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] STATIC (--score=0)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  313313  1378778         0       0      0     0    0     0   66   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 5663 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] 5663 out of 5663 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 51680 variables
c [simpleprobe-1] all 273036 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 559 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 559 variables, found 13627 hbrs, 20 units
c [unhide-1] limit 69539 based on 1112627 irredundant clauses
c [unhide-1-1] 14 units, 2542 failed, 15781 tauts, 0 hbrs, 8850 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 260513 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 101124 not tried 39% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 110343 = 42% variables out of 260513 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 886609 negative 99.4% of 892372 except 5763 0.6%
c [phase-count-1] 738027 positive 82.7% of 892372 except 154345 17.3%
c [phase-count-1] less non-negative clauses 5763 than limit 89200 (10.0%)
c [phase-count-1] non-pos/non-neg = 154345/5763 = 26.78 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 150170 negative 100%
c [sort-queue-1] sorted 150170 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 150170 (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 127703 variables 46.0% (150170 remain 48%)
c [simplification-1] removed 486406 irredundant clauses 35.3% (892372 remain 65%)
c [simplification-1] maximum reduction of 46% = max (46%, 35%)
c [simplification-1] large reduction 46% >= 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    6.7  150169   892372        51      45      2  6182    0    25   63   0%      0   25    2    0 23371%
c i    7.4  150161   892372       212     131     21  6235    0    76   63   0%      0   76    4    0 16837%
c i    7.6  149480   892372       278     148     28  6276    0   121   63   0%      0  121    4    0 15032%
c i    7.7  149359   892372       287     150     29  6281    0   122   63   0%      0  122    4    0 14591%
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [decomp-3] removed 1030 variables
c [simpleprobe-2] all 149140 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 57 variables
c [simpleprobe-2] 143040 variables remain 96% (6043 retained 4%)
c [simpleprobe-2] removed 57 variables, found 2068 hbrs, 7 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 77740 literals 26%
c [treelook-1] scheduling used 386329 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 374943 steps
c [treelook-1] 76424 literals remain 26%
c [treelook-1] 76317 variables remain to probed next time 52%
c [decomp-5] removed 115 variables
c [treelook-1] removed 1445 variables, found 2406 hbrs
c [basicprobe-1] limit 7015408 based on 876926 irredundant clauses
c [basicprobe-1-0] 31439 probes remain 26% after last round
c [basicprobe-1-0] 46 units = 46 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 24840 variables, found 14844 hbrs
c [unhide-2] limit 54807 based on 876926 irredundant clauses
c [unhide-2-2] 15 units, 2027 failed, 1952 tauts, 0 hbrs, 22043 literals
c [elim-2] 81457 variables 69% will be scheduled this time
c [elim-2] scheduled 81457 variables 69%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 18639 not tried 16% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 4496 = 6% variables out of 81457 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 113533 enqueued variables after 290 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 113533 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 35807 variables 24.0% (113533 remain 36%)
c [simplification-2] removed 238564 irredundant clauses 26.7% (653808 remain 47%)
c [simplification-2] maximum reduction of 27% = max (24%, 27%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1001 (hard 11000)
c [simplification-2] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   12.5  113532   653808       303     136     29 13960    0   127   50   0%      0  127    4    0 14327%
c i   12.5  113531   653808       304     136     29 13960    0   127   50   0%      0  127    4    0 14272%
c i   12.5  113530   653808       309     139     30 13960    0   128   50   0%      0  128    4    0 14079%
c i   12.6  113224   653808       327     141     32 13973    0   129   50   0%      0  129    4    0 13251%
c i   12.6  113218   653808       328     141     32 13973    0   129   50   0%      0  129    4    0 13200%
c i   12.7  112522   653808       367     172     35 13976    1   134   50   0%      0  134    4    0 12475%
c i   12.8  111051   653808       390     190     38 13977    1   141   50   0%      0  141    4    0 12013%
c i   12.9  111047   653808       405     203     39 13977    1   153   50   0%      0  152    5    0 13042%
c i   12.9  111039   653808       408     203     39 13979    1   153   50   0%      0  152    5    0 12900%
c i   13.0  111026   653808       466     223     47 14008    1   158   50   0%      0  158    5    0 10808%
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 4949 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] 4949 out of 4949 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 3794 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 61155 literals 28%
c [treelook-2] scheduling used 301882 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 413706 steps
c [treelook-2] 61151 literals remain 28%
c [treelook-2] 40255 variables remain to probed next time 37%
c [decomp-7] removed 3 variables
c [treelook-2] removed 3 variables, found 2331 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 14 units, 733 failed, 11124 tauts, 0 hbrs, 12150 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 107952 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 24875 not tried 23% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 4172 = 4% variables out of 107952 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 103780 enqueued variables after 466 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 103780 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 7243 variables 6.5% (103780 remain 33%)
c [simplification-3] removed 53378 irredundant clauses 8.2% (600430 remain 44%)
c [simplification-3] maximum reduction of 8% = max (7%, 8%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 1026 (hard 11000)
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   16.6  103779   600430       469     206     47 13215    1   159   48   0%      0  158    5    0 10713%
c i   16.6  103778   600430       470     206     47 13215    1   159   48   0%      0  158    5    0 10671%
c i   16.6  103776   600430       472     206     47 13216    1   158   48   0%      0  158    5    0 10594%
c i   16.6  103775   600430       473     206     47 13216    1   158   48   0%      0  158    5    0 10552%
c i   16.6  103774   600430       474     206     47 13216    1   158   48   0%      0  158    5    0 10511%
c i   16.6  103773   600430       476     206     47 13217    1   158   48   0%      0  158    5    0 10435%
c i   16.7  103772   600430       478     206     47 13218    1   158   48   0%      0  158    5    0 10359%
c i   16.7  103771   600430       479     206     47 13218    1   158   48   0%      0  158    5    0 10319%
c i   16.7  103770   600430       480     206     47 13218    1   158   48   0%      0  158    5    0 10279%
c i   16.7  103769   600430       481     206     47 13218    1   158   48   0%      0  158    4    0 10239%
c i   16.7  103767   600430       501     216     53 13221    1   161   48   0%      0  161    4    0 9829%
c i   16.7  103763   600430       502     216     53 13221    1   161   48   0%      0  161    4    0 9791%
c i   16.7  103759   600430       503     216     53 13221    1   161   48   0%      0  161    4    0 9753%
c i   16.7  103755   600430       504     216     53 13221    1   161   48   0%      0  161    4    0 9715%
c i   16.7  103752   600430       505     216     53 13221    1   161   48   0%      0  161    4    0 9677%
c i   16.7  103748   600430       506     216     53 13221    1   161   48   0%      0  161    4    0 9640%
c i   16.7  103744   600430       507     216     53 13221    1   161   48   0%      0  160    4    0 9602%
c i   16.7  103740   600430       508     216     53 13221    1   161   48   0%      0  160    4    0 9565%
c i   16.8  103736   600430       557     248     61 13229    1   170   48   0%      0  169    4    0 8797%
c i   16.9  103621   600430       579     258     62 13239    1   170   48   0%      0  169    4    0 8309%
c i   16.9  103619   600430       580     258     62 13239    1   170   48   0%      0  169    4    0 8277%
c i   16.9  103618   600430       581     258     62 13239    1   170   48   0%      0  169    4    0 8245%
c i   16.9  103617   600430       582     258     62 13239    1   170   48   0%      0  169    4    0 8213%
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.9  103613   600430       602     263     64 13251    1   171   48   0%      0  170    4    0 7857%
c i   16.9  103605   600430       603     263     64 13251    1   171   48   0%      0  170    4    0 7826%
c i   16.9  103603   600430       604     263     64 13251    1   171   48   0%      0  170    4    0 7796%
c i   16.9  103602   600430       607     263     65 13252    1   171   48   0%      0  170    4    0 7716%
c i   16.9  103598   600430       608     263     65 13252    1   171   48   0%      0  170    4    0 7686%
c i   16.9  103595   600430       609     263     65 13252    1   171   48   0%      0  170    4    0 7656%
c i   16.9  103594   600430       610     263     65 13252    1   171   48   0%      0  170    4    0 7626%
c i   16.9  103591   600430       611     263     65 13252    1   171   48   0%      0  170    4    0 7597%
c i   16.9  103589   600430       612     263     65 13252    1   171   48   0%      0  170    4    0 7567%
c i   16.9  103588   600430       613     263     65 13252    1   171   48   0%      0  170    4    0 7538%
c i   16.9  103587   600430       614     263     65 13252    1   171   48   0%      0  170    4    0 7508%
c i   16.9  103583   600430       615     263     65 13252    1   171   48   0%      0  170    4    0 7479%
c i   16.9  103581   600430       616     263     65 13252    1   171   48   0%      0  170    4    0 7450%
c i   16.9  103578   600430       617     263     65 13252    1   171   48   0%      0  170    4    0 7421%
c i   16.9  103577   600430       618     263     65 13252    1   171   48   0%      0  170    4    0 7392%
c i   16.9  103574   600430       619     263     65 13252    1   171   48   0%      0  170    4    0 7363%
c i   16.9  103573   600430       620     263     65 13252    1   171   48   0%      0  170    4    0 7335%
c i   16.9  103570   600430       621     263     65 13252    1   171   48   0%      0  170    4    0 7306%
c i   16.9  103569   600430       622     263     65 13252    1   171   48   0%      0  170    4    0 7278%
c i   16.9  103568   600430       623     263     65 13252    1   170   48   0%      0  169    4    0 7249%
c i   16.9  103561   600430       624     263     65 13252    1   170   48   0%      0  169    4    0 7221%
c i   16.9  103560   600430       625     263     65 13252    1   170   48   0%      0  169    4    0 7193%
c i   16.9  103558   600430       626     263     65 13252    1   170   48   0%      0  169    4    0 7165%
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.9  103557   600430       627     263     65 13252    1   170   48   0%      0  169    3    0 7137%
c i   16.9  103556   600430       628     263     65 13252    1   170   48   0%      0  169    3    0 7109%
c i   16.9  103553   600430       629     263     65 13252    1   170   48   0%      0  169    3    0 7082%
c i   16.9  103552   600430       630     263     65 13252    1   170   48   0%      0  169    3    0 7054%
c i   16.9  103551   600430       631     263     65 13252    1   170   48   0%      0  169    3    0 7027%
c i   17.0  103550   600430       665     276     73 13264    1   174   48   0%      0  173    3    0 6611%
c i   17.0  103549   600430       673     277     75 13268    1   174   48   0%      0  173    3    0 6448%
c i   17.0  103548   600430       677     278     75 13270    1   174   48   0%      0  173    3    0 6377%
c i   17.1  103547   600430       685     282     77 13271    1   175   48   0%      0  174    3    0 6425%
c i   17.3  103531   600430       816     318     91 13348    1   189   48   0%      0  188    3    0 5288%
c i   17.3  103523   600430       847     341     94 13352    1   190   48   0%      0  189    3    0 5705%
c i   17.3  103522   600430       848     341     94 13352    1   190   48   0%      0  189    3    0 5683%
c i   17.3  103521   600430       849     341     94 13352    1   190   48   0%      0  189    3    0 5661%
c i   17.3  103520   600430       850     341     94 13352    1   190   48   0%      0  189    3    0 5639%
c i   17.3  103519   600430       851     341     94 13352    1   190   48   0%      0  189    3    0 5617%
c i   17.3  103518   600430       852     341     94 13352    1   190   48   0%      0  188    3    0 5595%
c i   17.3  103517   600430       853     341     94 13352    1   190   48   0%      0  188    3    0 5573%
c i   17.3  103516   600430       854     341     94 13352    1   190   48   0%      0  188    3    0 5551%
c i   17.3  103515   600430       855     341     94 13352    1   190   48   0%      0  188    3    0 5530%
c i   17.4  103514   600430       868     345    101 13353    1   191   48   0%      0  189    3    0 5467%
c i   17.5  103512   600430       911     372    103 13366    1   194   48   0%      0  192    4    0 6361%
c i   17.5  103511   600430       912     372    103 13366    1   194   48   0%      0  192    4    0 6336%
c i   17.5  103510   600430       913     372    103 13366    1   194   48   0%      0  192    4    0 6312%
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   17.6  103509   600430      1039     393    110 13462    1   212   48   0%      0  209    5    0 6272%
c i   17.6  103508   600430      1040     393    110 13462    1   211   48   0%      0  209    5    0 6248%
c i   17.6  103507   600430      1041     393    110 13462    1   211   48   0%      0  209    5    0 6223%
c i   17.6  103506   600430      1042     393    110 13462    1   211   48   0%      0  209    5    0 6199%
c i   17.6  103505   600430      1043     393    110 13462    1   211   48   0%      0  209    5    0 6175%
c i   17.6  103504   600430      1044     393    110 13462    1   211   48   0%      0  209    5    0 6151%
c i   17.6  103503   600430      1045     393    110 13462    1   211   48   0%      0  209    5    0 6127%
c i   17.7  103502   600430      1086     412    114 13478    1   215   48   0%      0  212    4    0 5820%
c i   17.8  103310   600430      1106     429    116 13478    1   216   48   1%      0  214    4    0 5685%
c i   17.8  103218   600430      1116     432    117 13483    1   216   48   1%      0  214    4    0 5529%
c i   18.1  103201   600430      1267     476    132 13573    1   226   48   1%      0  223    4    0 4281%
c i   18.4  103109   600430      1405     563    152 13603    1   238   48   1%      1  235    4    0 4533%
c i   18.5  103088   600430      1448     578    158 13624    1   254   48   1%      1  250    5    0 4936%
c i   18.5  103078   600430      1449     578    158 13624    1   254   48   1%      1  250    5    0 4917%
c i   18.6  103071   600430      1506     601    165 13650    1   257   48   1%      1  253    4    0 4317%
c i   18.9  102841   600430      1624     669    190 13673    2   265   48   1%      1  261    5    0 4391%
c 
c [simplification-4] limit 1642 conflicts (hard 11000) hit after 1642 conflicts
c [decomp-8] removed 1137 variables
c [basicprobe-2] limit 4757360 based on 594670 irredundant clauses
c [basicprobe-2-0] 28258 probes remain 28% after last round
c [basicprobe-2-0] 29 units = 29 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2339 variables, found 9701 hbrs
c [unhide-4] limit 156932 with penalty 0 = 0 + 0
c [unhide-4-4] 11 units, 861 failed, 2765 tauts, 0 hbrs, 6599 literals
c [elim-4] 17247 variables 18% will be scheduled this time
c [elim-4] scheduled 17247 variables 18%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 48 variables 0% in round 1 in 24364422 steps
c [elim-4-1] backward subsumption/strengthening limit 24364400
c [elim-4-1-1] backward checking 9117 touched variables 9%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 243 and strengthened 96 clauses in 1434898 steps
c [elim-4-1] rescheduled 885 variables 1% by backward subsumption
c [elim-4-2] eliminated 108 variables 0% in round 2 in 674475 steps
c [elim-4-2] backward subsumption/strengthening limit 674400
c [elim-4-2-1] backward checking 762 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 82 and strengthened 82 clauses in 341039 steps
c [elim-4-2] rescheduled 351 variables 0% by backward subsumption
c [elim-4-3] eliminated 24 variables 0% in round 3 in 440422 steps
c [elim-4-3] backward subsumption/strengthening limit 440400
c [elim-4-3-1] backward checking 138 touched variables 0%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 12 and strengthened 3 clauses in 157721 steps
c [elim-4] incomplete 31 not tried 0% in round 3
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 194 = 1% variables out of 17247 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 98252 enqueued variables after 1642 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 98252 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 4585 variables 4.5% (98252 remain 31%)
c [simplification-4] removed 43407 irredundant clauses 7.2% (557023 remain 40%)
c [simplification-4] maximum reduction of 7% = max (4%, 7%)
c [simplification-4] large reduction 7% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 13642 (soft 3642 + delta 10000)
c [simplification-4] new conflict limit 3642 (hard 13642)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   20.9   98251   557023      1730     677    175 18168    2   267   45   1%      1  263    4    0 3649%
c i   21.1   97289   557023      1836     743    181 18199    2   275   45   1%      1  270    5    0 3758%
c i   21.1   97288   557023      1837     743    181 18199    2   275   45   1%      1  270    5    0 3744%
c i   21.1   97287   557023      1838     743    181 18199    2   275   45   1%      1  270    5    0 3729%
c i   21.1   97286   557023      1839     743    181 18199    2   275   45   1%      1  270    5    0 3715%
c i   21.1   97280   557023      1840     743    181 18199    2   275   45   1%      1  270    5    0 3700%
c i   21.4   97276   557023      1979     805    201 18253    2   289   45   1%      1  283    4    0 3301%
c i   21.5   97262   557023      1994     817    201 18255    2   290   45   1%      1  284    5    0 3305%
c i   21.5   97232   557023      2011     820    201 18268    2   291   45   1%      1  285    4    0 3166%
c i   21.5   96491   557023      2020     828    201 18268    2   290   45   1%      1  284    5    0 3312%
c i   21.5   96490   557023      2021     828    201 18268    2   290   45   1%      1  284    5    0 3299%
c i   21.5   96489   557023      2027     829    204 18269    2   291   45   1%      1  285    4    0 3245%
c i   21.5   96488   557023      2028     829    204 18269    2   291   45   1%      1  285    4    0 3232%
c i   21.5   96487   557023      2029     829    204 18269    2   291   45   1%      1  285    4    0 3219%
c i   21.5   96486   557023      2030     829    204 18269    2   291   45   1%      1  285    4    0 3207%
c i   21.5   96485   557023      2031     829    204 18269    2   290   45   1%      1  285    4    0 3194%
c i   21.5   96483   557023      2032     829    204 18269    2   290   45   1%      1  284    4    0 3182%
c i   21.5   96480   557023      2033     829    204 18269    2   290   45   1%      1  284    4    0 3170%
c i   21.5   96479   557023      2034     829    204 18269    2   290   45   1%      1  284    4    0 3157%
c i   21.5   96478   557023      2035     829    204 18269    2   290   45   1%      1  284    4    0 3145%
c i   21.5   96477   557023      2036     829    204 18269    2   290   45   1%      1  284    4    0 3133%
c i   21.5   96476   557023      2037     829    204 18269    2   290   45   1%      1  284    4    0 3121%
c i   21.5   96475   557023      2038     829    204 18269    2   290   45   1%      1  284    4    0 3108%
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   21.8   96473   557023      2211     883    217 18371    2   309   45   1%      1  303    9    0 5017%
c i   22.0   96431   557023      2289     926    224 18398    2   311   45   1%      1  304    7    0 4180%
c i   22.0   96430   557023      2290     926    224 18398    2   311   45   1%      1  304    7    0 4163%
c i   22.0   96429   557023      2291     926    224 18398    2   311   45   1%      1  304    7    0 4147%
c i   22.0   96428   557023      2292     926    224 18398    2   311   45   1%      1  304    7    0 4131%
c i   22.0   96427   557023      2293     926    224 18398    2   311   45   1%      1  304    7    0 4115%
c i   22.0   96426   557023      2313     936    225 18406    2   313   45   1%      1  306    7    0 4039%
c i   22.1   96364   557023      2317     939    225 18406    2   315   45   1%      1  308    8    0 4273%
c i   22.1   96309   557023      2348     960    227 18412    2   320   45   1%      1  313    7    0 4066%
c i   22.4   95881   557023      2437    1019    238 18428    2   329   45   1%      1  321    7    0 3705%
c i   22.4   95880   557023      2438    1019    238 18428    2   328   45   1%      1  321    7    0 3691%
c i   22.4   95879   557023      2439    1019    238 18428    2   328   45   1%      1  321    7    0 3676%
c i   22.4   95866   557023      2440    1019    238 18428    2   328   45   1%      1  320    7    0 3662%
c i   22.4   95865   557023      2441    1019    238 18428    2   328   45   1%      1  320    7    0 3648%
c i   22.5   95859   557023      2530    1064    247 18461    3   373   45   1%      1  365   12    0 5345%
c i   23.0   95855   557023      2770    1214    283 18513    3   412   45   1%      1  402   11    0 4397%
c i   23.1   95696   557023      2792    1228    286 18516    3   412   45   1%      1  402   11    0 4179%
c i   23.1   95581   557023      2803    1235    287 18518    3   412   45   1%      1  402   11    0 4047%
c i   23.1   95580   557023      2804    1235    287 18518    3   412   45   1%      1  402   11    0 4032%
c i   23.2   95579   557023      2846    1265    294 18521    3   415   45   1%      1  405   10    0 3706%
c i   23.2   95577   557023      2847    1265    294 18521    3   415   45   1%      1  405   10    0 3692%
c i   23.2   95576   557023      2849    1265    294 18522    3   415   45   1%      1  405   10    0 3664%
c i   23.2   95575   557023      2866    1279    294 18524    3   416   45   1%      1  406   10    0 3632%
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   23.2   95564   557023      2867    1279    294 18524    3   416   45   1%      1  405   10    0 3618%
c i   23.2   95558   557023      2868    1279    294 18524    3   416   45   1%      1  405   10    0 3604%
c i   23.2   95552   557023      2869    1279    294 18524    3   416   45   1%      1  405   10    0 3590%
c i   23.2   95544   557023      2870    1279    294 18524    3   415   45   1%      1  405   10    0 3576%
c i   23.2   95535   557023      2871    1279    294 18524    3   415   45   1%      1  405   10    0 3562%
c i   23.2   95523   557023      2872    1279    294 18524    3   415   45   1%      1  405   10    0 3548%
c i   23.2   95517   557023      2873    1279    294 18524    3   415   45   1%      1  405    9    0 3534%
c i   23.2   95507   557023      2874    1279    294 18524    3   415   45   1%      1  405    9    0 3520%
c i   23.2   95492   557023      2875    1279    294 18524    3   415   45   1%      1  405    9    0 3507%
c i   23.2   95486   557023      2876    1279    294 18524    3   415   45   1%      1  404    9    0 3493%
c i   23.2   95471   557023      2877    1279    294 18524    3   415   45   1%      1  404    9    0 3479%
c i   23.2   95465   557023      2878    1279    294 18524    3   415   45   1%      1  404    9    0 3466%
c i   23.2   95447   557023      2879    1279    294 18524    3   415   45   1%      1  404    9    0 3452%
c i   23.2   95443   557023      2880    1279    294 18524    3   414   45   1%      1  404    9    0 3439%
c i   23.8   95423   557023      3193    1438    321 18636    4   445   45   1%      1  433    8    0 2637%
c i   24.1   94940   557023      3354    1535    338 18679    4   469   46   1%      1  456   10    0 3076%
c i   24.1   94754   557023      3364    1540    340 18681    4   469   46   1%      1  456   10    0 2983%
c i   24.1   94750   557023      3365    1540    340 18681    4   469   46   1%      1  455   10    0 2971%
c i   24.2   94746   557023      3377    1548    342 18682    4   469   46   1%      1  456   10    0 2902%
c i   24.2   94742   557023      3410    1554    343 18707    4   469   46   1%      1  455    9    0 2601%
c i   24.2   94738   557023      3411    1554    343 18707    4   469   46   1%      1  455    9    0 2591%
c i   24.8   94734   557023      3721    1757    367 18785    4   494   46   1%      2  478    7    0 1947%
c i   25.3   94729   557023      3939    1875    402 18842    4   525   46   1%      2  507   11    0 2847%
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   25.3   94726   557023      3940    1875    402 18842    4   524   46   1%      2  507   11    0 2836%
c i   25.3   94724   557023      3944    1876    402 18844    4   524   46   1%      2  506   11    0 2796%
c i   25.3   94722   557023      3945    1876    402 18844    4   524   46   1%      2  506   11    0 2786%
c i   25.3   94719   557023      3946    1876    402 18844    4   524   46   1%      2  506   11    0 2775%
c i   25.3   94716   557023      3947    1876    402 18844    4   524   46   1%      2  506   11    0 2764%
c i   25.3   94713   557023      3948    1876    402 18844    4   523   46   1%      2  506   11    0 2753%
c i   25.3   94710   557023      3949    1876    402 18844    4   523   46   1%      2  506   11    0 2742%
c i   25.3   94707   557023      3950    1876    402 18844    4   523   46   1%      2  506   11    0 2732%
c i   25.4   94705   557023      3960    1882    403 18846    4   527   46   1%      2  509   11    0 2662%
c 
c [simplification-5] limit 4145 conflicts (hard 13642) hit after 4145 conflicts
c [quatres-1] found 36009 quaternary clauses 47% in total
c [quatres-1-2] added 16 single-self-subsuming ternary resolvents
c [quatres-1-2] added 5 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 94703 free variables schedulable
c [ternres-1] 1660 ternary resolvents (5 bin, 1655 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 1547 xors of average arity 2.0
c [gauss-1] connected 3139 occurrences of 2154 variables (average 1.5)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 1678 variables
c [gauss-1] exported 0 unary, 131 binary and 0 ternary equations
c [decomp-10] removed 2 variables
c [simpleprobe-3] 89227 schedulable variables 96%
c [simpleprobe-3] limit 7192101 penalty 0 = 0 + 0
c [decomp-11] removed 1771 variables
c [simpleprobe-3] 36812 variables remain 40% (54440 retained 60%)
c [simpleprobe-3] removed 1771 variables, found 21313 hbrs, 200 units
c [unhide-5] limit 359605 with penalty 0 = 0 + 0
c [unhide-5-5] 8 units, 251 failed, 10216 tauts, 0 hbrs, 3959 literals
c [transred-1] limit 1798025 with penalty 0 = 0 + 0
c [transred-1] removed 146 transitive binary clauses
c [transred-1] found 4 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 90448 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 6606 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3 clauses out of 128 (2%) of length 10
c [cce-1-1] eliminated 18 clauses out of 506 (4%) of length 9
c [cce-1-1] eliminated 29 clauses out of 528 (5%) of length 8
c [cce-1-1] eliminated 135 clauses out of 939 (14%) of length 7
c [cce-1-1] eliminated 2997 clauses out of 4469 (67%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 3182 large clauses in 30000004 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 311574 clauses = 256963 binary + 54611 ternary
c [cce-1-1] tried to eliminate 360 small clauses 0%
c [cce-1-1] eliminated 87 binary clauses 0%
c [cce-1-1] eliminated 13 ternary clauses 0%
c [cce-1-1] eliminated 100 small clauses 0%
c [cce-1-1] eliminated 100 small clauses in 30000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3282 covered clauses in round 1
c [cce-1] eliminated 3282 covered clauses in TOTAL during 1 rounds
c [cce-1] 3282 < 1/100 * 496879 = 4968 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 90448 variables 100%
c [elim-5] limit of 35960509 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 1001 not tried 1% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 4017 = 4% variables out of 90448 scheduled
c [bca-1] limit of 10000000 steps and 971458 added (scaled 2)
c [bca-1] 155717 out of 172864 literals actually usable 90%
c [bca-1] added 102 blocked clauses in 407369 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 5233 pos 6.1% + 81198 neg 93.9% = 86431 sched 100.0% ret 0
c [sweep-1-1] 1054316 steps 15 queries 16190.80 avg class size
c [sweep-1-1] 75 decisions 12 SAT calls 73.58 avg env size
c [sweep-1-1] 86393 variables remain 100% (38 retained 0%)
c [decomp-12] removed 68 variables
c [sweep-1-1] removed 68 vars (0 failed, 2 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 68 vars in TOTAL (1 rounds, 14 queries)
c [sort-queue-5] sorted 86363 enqueued variables after 4145 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 86363 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 8340 variables 8.8% (86363 remain 28%)
c [simplification-5] removed 71635 irredundant clauses 12.9% (485388 remain 35%)
c [simplification-5] maximum reduction of 13% = max (9%, 13%)
c [simplification-5] large reduction 13% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 16145 (soft 6145 + delta 10000)
c [simplification-5] new conflict limit 6145 (hard 16145)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   31.7   86362   485388      4164    1696   1362 43331    5   535   43   1%      2  516    8    0 1975%
c i   31.8   86359   485388      4197    1719   1367 43334    5   537   43   1%      2  518    8    0 1828%
c i   31.8   86185   485388      4202    1721   1368 43335    5   537   43   1%      2  518    8    0 1806%
c i   31.9   86171   485388      4224    1728   1369 43348    5   536   43   1%      1  516    7    0 1691%
c i   31.9   86027   485388      4225    1728   1369 43348    5   535   43   1%      1  516    7    0 1684%
c i   31.9   85994   485388      4226    1728   1369 43348    5   535   43   1%      1  516    7    0 1678%
c i   31.9   85968   485388      4239    1738   1370 43349    5   535   43   1%      1  515    7    0 1671%
c i   32.0   85952   485388      4259    1753   1371 43352    5   535   43   1%      1  515    7    0 1641%
c i   32.1   85951   485388      4333    1805   1378 43366    5   571   43   1%      1  550    9    0 1982%
c i   32.1   85947   485388      4334    1805   1378 43366    5   571   43   1%      1  550    9    0 1974%
c i   32.1   85938   485388      4337    1807   1378 43366    5   571   43   1%      1  550    9    0 1956%
c i   32.2   85934   485388      4356    1824   1378 43367    5   571   43   1%      1  550    8    0 1886%
c i   32.2   85793   485388      4366    1825   1378 43375    5   571   43   1%      1  550    8    0 1824%
c i   32.3   85781   485388      4425    1880   1379 43376    5   574   43   1%      1  552    8    0 1806%
c i   32.3   85726   485388      4428    1881   1379 43376    5   574   43   1%      1  552    8    0 1788%
c i   32.3   85725   485388      4430    1881   1380 43376    5   573   43   1%      1  552    8    0 1775%
c i   32.4   85715   485388      4487    1908   1392 43391    5   602   43   1%      1  580    9    0 1950%
c i   32.6   85709   485388      4567    1970   1399 43400    5   603   43   1%      1  580    8    0 1781%
c i   32.7   85582   485388      4653    2005   1404 43445    5   597   43   1%      1  573    7    0 1483%
c i   32.9   85564   485388      4732    2062   1415 43454    5   600   43   1%      1  576    6    0 1358%
c i   33.1   85550   485388      4849    2144   1430 43468    5   613   43   1%      1  588    8    0 1672%
c i   33.2   85544   485388      4910    2164   1434 43503    5   608   43   1%      1  583    7    0 1423%
c i   33.2   85533   485388      4934    2176   1435 43513    5   607   43   1%      1  581    7    0 1357%
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   33.3   85405   485388      4963    2202   1436 43514    5   607   43   1%      1  581    7    0 1335%
c i   33.3   85404   485388      4964    2202   1436 43514    5   607   43   1%      1  581    7    0 1329%
c i   33.5   85403   485388      5057    2274   1443 43523    5   633   43   1%      1  606   10    1 2017%
c i   33.7   85395   485388      5147    2339   1449 43539    5   633   43   1%      1  605    9    1 1661%
c i   33.7   85394   485388      5168    2356   1451 43540    5   633   43   1%      1  605    9    1 1640%
c i   33.7   85392   485388      5169    2356   1451 43540    5   633   43   1%      1  605    9    1 1633%
c i   33.7   85391   485388      5170    2356   1451 43540    5   633   43   1%      1  605    9    1 1627%
c i   33.9   85390   485388      5235    2390   1460 43561    5   645   43   1%      1  616   10    1 1892%
c i   34.0   85358   485388      5332    2460   1467 43577    5   644   43   1%      1  615    9    1 1622%
c i   34.4   85357   485388      5507    2591   1481 43603    6   647   43   1%      1  616    8    1 1416%
c i   34.8   85356   485388      5739    2777   1497 43630    6   677   43   1%      1  644    8    1 1413%
c i   34.8   85355   485388      5740    2777   1497 43630    6   677   43   1%      1  644    8    1 1407%
c i   34.8   85354   485388      5741    2777   1497 43630    6   677   43   1%      1  644    8    1 1402%
c i   34.8   85353   485388      5742    2777   1497 43630    6   677   43   1%      1  643    8    1 1396%
c i   34.8   85352   485388      5743    2777   1497 43630    6   677   43   1%      1  643    8    1 1391%
c i   34.8   85351   485388      5744    2777   1497 43630    6   676   43   1%      1  643    8    1 1386%
c i   34.8   85350   485388      5750    2778   1498 43632    6   676   43   1%      1  642    8    1 1364%
c i   34.9   85347   485388      5787    2808   1501 43635    6   682   43   1%      1  648    8    1 1403%
c i   34.9   85345   485388      5789    2808   1501 43636    6   681   43   1%      1  647    8    1 1393%
c i   35.0   85343   485388      5841    2850   1505 43640    6   680   43   1%      1  645    8    1 1282%
c i   35.0   85336   485388      5842    2850   1505 43640    6   680   43   1%      1  645    8    1 1277%
c i   35.0   85335   485388      5843    2850   1505 43640    6   679   43   1%      1  645    8    1 1272%
c i   35.1   85334   485388      5854    2859   1505 43640    6   678   43   1%      1  644    8    1 1263%
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.1   85304   485388      5864    2865   1506 43641    6   678   43   1%      1  643    8    1 1233%
c i   35.1   85297   485388      5874    2870   1506 43644    6   677   43   1%      1  643    7    1 1202%
c i   35.1   85295   485388      5875    2870   1506 43644    6   677   43   1%      1  642    7    1 1198%
c i   35.1   85294   485388      5876    2870   1506 43644    6   677   43   1%      1  642    7    1 1193%
c i   35.1   85293   485388      5877    2870   1506 43644    6   677   43   1%      1  642    7    1 1188%
c i   35.1   85290   485388      5878    2870   1506 43644    6   677   43   1%      1  642    7    1 1184%
c i   35.1   85289   485388      5879    2870   1506 43644    6   676   43   1%      1  642    7    1 1179%
c i   35.1   85288   485388      5880    2870   1506 43644    6   676   43   1%      1  641    7    1 1174%
c i   35.2   85285   485388      5905    2893   1507 43644    6   677   43   1%      1  642    8    1 1232%
c i   35.2   85284   485388      5906    2893   1507 43644    6   677   43   1%      1  642    8    1 1227%
c i   35.2   85283   485388      5907    2893   1507 43644    6   677   43   1%      1  642    8    1 1223%
c i   35.2   85282   485388      5908    2893   1507 43644    6   677   43   1%      1  642    7    1 1218%
c i   35.2   85281   485388      5909    2893   1507 43644    6   677   43   1%      1  642    7    1 1213%
c i   35.2   85280   485388      5910    2893   1507 43644    6   677   43   1%      1  641    7    1 1208%
c i   35.2   85279   485388      5911    2893   1507 43644    6   676   43   1%      1  641    7    1 1204%
c i   35.7   85278   485388      6189    3094   1535 43687    6   693   43   1%      1  656    9    1 1382%
c i   36.0   84941   485388      6332    3202   1550 43704    6   695   43   1%      1  656    8    1 1252%
c i   36.1   84934   485388      6373    3237   1555 43704    6   694   43   1%      1  654    8    1 1206%
c 
c [simplification-6] limit 6417 conflicts (hard 16145) hit after 6417 conflicts
c [quatres-2] found 36935 quaternary clauses 50% in total
c [quatres-2-2] added 5 single-self-subsuming ternary resolvents
c [quatres-2-2] added 52 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 84933 free variables schedulable
c [ternres-2] 456 ternary resolvents (0 bin, 456 trn)
c [ternres-2] 34140 variables remain 40% (50793 retained 60%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2820 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2820 out of 2820 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 179 xors of average arity 2.3
c [gauss-2] connected 407 occurrences of 282 variables (average 1.4)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [decomp-13] removed 228 variables
c [gauss-2] exported 0 unary, 7 binary and 0 ternary equations
c [decomp-14] removed 1 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 54000 literals 32%
c [treelook-3] scheduling used 309933 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 332777 steps
c [treelook-3] 53993 literals remain 32%
c [treelook-3] 23128 variables remain to probed next time 27%
c [decomp-15] removed 1 variables
c [treelook-3] removed 3 variables, found 2305 hbrs
c [unhide-6] limit 548831 with penalty 0 = 0 + 0
c [unhide-6-6] 15 units, 275 failed, 4499 tauts, 0 hbrs, 5119 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 173 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 83806 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 699 blocked clauses
c [block-2] 699 < 1/100 * 475057 = 4750 considered unsuccessful
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 83803 variables 100%
c [elim-6] limit of 54883173 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 1896 variables 2% in round 1 in 38451429 steps
c [elim-6-1] backward subsumption/strengthening limit 16431744
c [elim-6-1-1] backward checking 8047 touched variables 10%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 70 and strengthened 269 clauses in 13167635 steps
c [elim-6-1] rescheduled 696 variables 1% by backward subsumption
c [elim-6-2] eliminated 28 variables 0% in round 2 in 618183 steps
c [elim-6-2] backward subsumption/strengthening limit 618100
c [elim-6-2-1] backward checking 248 touched variables 0%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 9 and strengthened 22 clauses in 169731 steps
c [elim-6-2] rescheduled 67 variables 0% by backward subsumption
c [elim-6-3] eliminated 6 variables 0% in round 3 in 60417 steps
c [elim-6-3] backward subsumption/strengthening limit 60400
c [elim-6-3-1] backward checking 51 touched variables 0%
c [elim-6-3-1] incomplete backward checking 0 remain 0%
c [elim-6-3] subsumed 9 and strengthened 2 clauses in 60401 steps
c [elim-6] incomplete 13 not tried 0% in round 3
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 1940 = 2% variables out of 83803 scheduled
c [bca-2] limit of 10000000 steps and 924291 added (scaled 2)
c [bca-2] 141822 out of 163728 literals actually usable 87%
c [bca-2] added 52 blocked clauses in 355210 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 5114 pos 6.2% + 76715 neg 93.8% = 81829 sched 100.0% ret 34
c [sweep-2-1] 1056881 steps 19 queries 22207.84 avg class size
c [sweep-2-1] 145 decisions 17 SAT calls 39.47 avg env size
c [sweep-2-1] 81684 variables remain 100% (175 retained 0%)
c [decomp-16] removed 38 variables
c [sweep-2-1] removed 38 vars (0 failed, 1 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 38 vars in TOTAL (1 rounds, 18 queries)
c [sort-queue-6] sorted 81825 enqueued variables after 6417 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 81825 (100%)
c [score-dist-6] max exp 0, different 1 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 3108 variables 3.7% (81825 remain 26%)
c [simplification-6] removed 23619 irredundant clauses 4.9% (461769 remain 33%)
c [simplification-6] maximum reduction of 5% = max (4%, 5%)
c [simplification-6] large reduction 5% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 18417 (soft 8417 + delta 10000)
c [simplification-6] new conflict limit 8417 (hard 18417)
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   41.1   81824   461769      6551    3009   1598 40926    6   691   42   1%      1  649    7    1  991%
c i   41.2   81821   461769      6608    3044   1613 40932    6   702   42   1%      1  660    8    1 1171%
c i   41.2   81820   461769      6610    3045   1613 40932    6   702   42   1%      1  660    8    1 1164%
c i   41.3   81815   461769      6634    3061   1617 40932    6   700   42   1%      1  658    8    1 1115%
c i   41.3   81812   461769      6636    3062   1617 40932    6   700   42   1%      1  658    8    1 1107%
c i   41.3   81811   461769      6641    3066   1617 40932    6   700   42   1%      1  657    8    1 1096%
c i   41.3   81728   461769      6643    3066   1618 40932    6   699   42   1%      1  657    8    1 1088%
c i   41.9   81727   461769      6927    3285   1644 40967    6   709   42   1%      1  663    9    1 1199%
c i   41.9   81716   461769      6932    3286   1646 40968    6   709   42   1%      1  664    9    1 1180%
c i   42.4   81714   461769      7197    3468   1666 41027    6   702   42   1%      2  654    7    1  886%
c i   42.5   81467   461769      7225    3489   1668 41031    6   699   42   1%      1  651    6    1  837%
c i   42.9   81455   461769      7434    3654   1694 41045    6   714   42   1%      1  664    8    1  972%
c i   42.9   81454   461769      7437    3655   1694 41046    6   714   42   1%      1  664    7    1  962%
c i   42.9   81444   461769      7448    3661   1696 41048    6   713   42   1%      1  662    7    1  935%
c i   43.3   81442   461769      7649    3811   1712 41078    6   709   42   1%      1  657    6    1  795%
c i   43.5   81440   461769      7758    3888   1724 41096    6   704   42   1%      1  651    7    1  814%
c i   43.5   81308   461769      7761    3888   1725 41096    6   704   42   1%      1  650    6    1  808%
c i   43.8   81305   461769      7883    3992   1731 41103    6   711   42   1%      1  657    7    1  881%
c i   44.0   81300   461769      7980    4068   1742 41110    6   707   42   1%      1  651    7    1  846%
c i   44.0   81299   461769      7983    4069   1743 41110    6   706   42   1%      1  651    7    1  839%
c i   44.2   81298   461769      8090    4133   1749 41143    6   720   42   1%      1  663    8    1  993%
c i   44.2   81296   461769      8091    4133   1749 41143    6   720   42   1%      1  663    8    1  989%
c i   44.2   81293   461769      8092    4133   1749 41143    6   720   42   1%      1  663    8    1  985%
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.5   81292   461769      8264    4237   1771 41182    6   716   42   1%      1  658    7    1  832%
c i   44.5   81290   461769      8265    4237   1771 41182    6   716   42   1%      1  657    7    1  829%
c i   44.5   81288   461769      8266    4237   1771 41182    6   716   42   1%      1  657    7    1  826%
c i   44.5   81286   461769      8267    4237   1771 41182    6   716   42   1%      1  657    7    1  823%
c i   44.5   81284   461769      8268    4237   1771 41182    6   715   42   1%      1  657    7    1  819%
c i   44.5   81282   461769      8269    4237   1771 41182    6   715   42   1%      1  657    7    1  816%
c i   44.5   81280   461769      8270    4237   1771 41182    6   715   42   1%      1  656    7    1  813%
c i   44.5   81278   461769      8278    4243   1771 41183    6   714   42   1%      1  656    7    1  802%
c i   44.5   81276   461769      8279    4243   1771 41183    6   714   42   1%      1  655    7    1  799%
c i   44.5   81272   461769      8280    4243   1771 41183    6   714   42   1%      1  655    7    1  796%
c i   44.5   81269   461769      8281    4243   1771 41183    6   714   42   1%      1  655    7    1  793%
c i   44.5   81266   461769      8282    4243   1771 41183    6   714   42   1%      1  655    7    1  790%
c i   44.7   81263   461769      8341    4295   1775 41185    6   713   42   1%      1  653    7    1  783%
c i   44.7   81262   461769      8342    4295   1775 41185    6   712   42   1%      1  653    7    1  780%
c i   44.7   81261   461769      8343    4295   1775 41185    6   712   42   1%      1  653    7    1  777%
c i   44.7   81260   461769      8344    4295   1775 41185    6   712   42   1%      1  653    7    1  774%
c i   44.9   81259   461769      8456    4375   1788 41202    6   714   42   1%      1  654    7    1  768%
c 
c [simplification-7] limit 8596 conflicts (hard 18417) hit after 8596 conflicts
c [quatres-3] found 37140 quaternary clauses 52% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [quatres-3-2] added 47 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 32585 schedulable variables 40%
c [ternres-3] 2055 ternary resolvents (4 bin, 2051 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 115 xors of average arity 2.5
c [gauss-3] connected 285 occurrences of 221 variables (average 1.3)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 119 variables
c [basicprobe-3] limit 18344140 penalty 0 = 0 + 0
c [basicprobe-3-0] 22369 probes remain 28% after last round
c [basicprobe-3-0] 128 units = 128 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 851 variables, found 30677 hbrs
c [bate-1] eliminated 51 asymmetric tautologies during probing
c [unhide-7] limit 733765 with penalty 0 = 0 + 0
c [unhide-7-7] 38 units, 127 failed, 5773 tauts, 0 hbrs, 6333 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 149 transitive binary clauses
c [transred-3] found 1 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 396 (0%) of length 8
c [cce-2-1] eliminated 6 clauses out of 618 (1%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 7 large clauses in 15000000 steps
c [cce-2-1] allowing another 7500000 steps for small clauses
c [cce-2-1] scheduling 276465 clauses = 224721 binary + 51744 ternary
c [cce-2-1] tried to eliminate 240 small clauses 0%
c [cce-2-1] eliminated 59 binary clauses 0%
c [cce-2-1] eliminated 15 ternary clauses 0%
c [cce-2-1] eliminated 74 small clauses 0%
c [cce-2-1] eliminated 3145 small clauses in 15000003 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 3152 covered clauses in round 1
c [cce-2] eliminated 3152 covered clauses in TOTAL during 1 rounds
c [cce-2] 3152 < 1/100 * 448545 = 4485 considered unsuccessful
c [elim-7] no untried remaining variables left
c [elim-7] scheduled 79769 variables 100%
c [elim-7] limit of 73376563 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 2261 variables 3% in round 1 in 40294463 steps
c [elim-7-1] backward subsumption/strengthening limit 33082100
c [elim-7-1-1] backward checking 8546 touched variables 11%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 71 and strengthened 159 clauses in 2690224 steps
c [elim-7-1] rescheduled 557 variables 1% by backward subsumption
c [elim-7-2] eliminated 61 variables 0% in round 2 in 4210004 steps
c [elim-7-2] backward subsumption/strengthening limit 4210000
c [elim-7-2-1] backward checking 457 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 44 and strengthened 16 clauses in 549337 steps
c [elim-7-2] rescheduled 166 variables 0% by backward subsumption
c [elim-7-3] eliminated 14 variables 0% in round 3 in 4408636 steps
c [elim-7-3] backward subsumption/strengthening limit 4408600
c [elim-7-3-1] backward checking 138 touched variables 0%
c [elim-7-3-1] fully completed backward checking in 1 rounds
c [elim-7-3] subsumed 16 and strengthened 9 clauses in 244465 steps
c [elim-7] incomplete 43 not tried 0% in round 3
c [gc-46] reconnected 66735 binary clauses (produced 0 empty 2 units)
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 2478 = 3% variables out of 79769 scheduled
c [bca-3] limit of 10000000 steps and 875827 added (scaled 2)
c [bca-3] 130847 out of 154584 literals actually usable 85%
c [bca-3] added 34 blocked clauses in 316499 steps
c [sweep-3] limit 1100648 penalty 0 = 0 + 0
c [sweep-3-1] 4938 pos 6.4% + 72184 neg 93.6% = 77122 sched 99.8% ret 169
c [sweep-3-1] 1177881 steps 10 queries 26278.80 avg class size
c [sweep-3-1] 54 decisions 9 SAT calls 33.11 avg env size
c [sweep-3-1] 77106 variables remain 100% (185 retained 0%)
c [decomp-18] removed 85 variables
c [sweep-3-1] removed 85 vars (0 failed, 1 eqs, 2 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 85 vars in TOTAL (1 rounds, 9 queries)
c [sort-queue-7] sorted 77206 enqueued variables after 8596 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 77206 (100%)
c [score-dist-7] max exp 0, different 1 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 4049 variables 5.0% (77206 remain 25%)
c [simplification-7] removed 24262 irredundant clauses 5.3% (437507 remain 32%)
c [simplification-7] maximum reduction of 5% = max (5%, 5%)
c [simplification-7] large reduction 5% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 20596 (soft 10596 + delta 10000)
c [simplification-7] new conflict limit 10596 (hard 20596)
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   50.3   77205   437507      8759    3947   3000 65272    7   706   42   1%      1  643    8    1  893%
c i   50.8   77197   437507      9012    4140   3023 65300    7   703   42   1%      2  638    8    1  821%
c i   51.0   77177   437507      9117    4232   3028 65305    7   701   42   1%      1  634    8    1  803%
c i   51.1   77174   437507      9125    4236   3028 65308    7   700   42   1%      1  634    7    1  783%
c i   51.1   76778   437507      9147    4252   3029 65312    7   722   42   1%      1  655    9    1  926%
c i   51.1   76775   437507      9152    4252   3030 65315    7   722   42   1%      1  655    9    1  910%
c i   51.4   76770   437507      9272    4340   3036 65335    7   716   42   1%      1  648    8    1  795%
c i   51.5   76767   437507      9327    4378   3040 65346    7   716   42   1%      1  647    8    1  808%
c i   51.6   76762   437507      9408    4442   3049 65353    7   710   42   1%      1  641    7    1  718%
c i   52.0   76674   437507      9593    4582   3067 65369    7   708   42   1%      1  637    7    1  758%
c i   52.0   76666   437507      9611    4596   3068 65370    7   708   42   1%      1  636    7    1  741%
c i   52.2   76665   437507      9722    4688   3075 65377    7   721   42   1%      1  648    9    1  870%
c i   52.3   76639   437507      9774    4723   3078 65390    7   716   42   1%      1  642    8    1  794%
c i   52.4   76496   437507      9793    4735   3080 65393    7   714   42   1%      1  641    8    1  770%
c i   52.5   76494   437507      9889    4812   3089 65402    7   716   42   1%      1  641    8    1  819%
c i   52.9   76484   437507     10070    4954   3103 65424    7   705   42   1%      1  629    7    1  721%
c i   53.5   76477   437507     10350    5177   3127 65453    7   724   42   1%      1  645    9    1  799%
c i   53.6   76470   437507     10384    5203   3132 65454    7   736   42   1%      1  657    9    1  862%
c i   53.9   76449   437507     10579    5366   3151 65466    7   735   42   1%      1  654    9    1  790%
c 
c [simplification-8] limit 10599 conflicts (hard 20596) hit after 10599 conflicts
c [quatres-4] found 32738 quaternary clauses 51% in total
c [quatres-4-2] added 4 single-self-subsuming ternary resolvents
c [quatres-4-2] added 20 quaternary resolvents
c [ternres-4] limit 4533937 with penalty 0 = 0 + 0
c [ternres-4] all 76449 free variables schedulable
c [ternres-4] 424 ternary resolvents (0 bin, 424 trn)
c [ternres-4] 22978 variables remain 30% (53471 retained 70%)
c [decomp-19] removed 915 variables
c [simpleprobe-4] 30895 schedulable variables 40%
c [simpleprobe-4] limit 18135751 penalty 0 = 0 + 0
c [decomp-20] removed 1572 variables
c [simpleprobe-4] 7524 variables remain 10% (67195 retained 90%)
c [simpleprobe-4] removed 1572 variables, found 46604 hbrs, 288 units
c [unhide-8] limit 906787 with penalty 0 = 0 + 0
c [unhide-8-8] 18 units, 498 failed, 14066 tauts, 0 hbrs, 5525 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 204 transitive binary clauses
c [transred-4] found 3 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 74046 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 187 blocked clauses
c [block-3] 187 < 1/100 * 421208 = 4212 considered unsuccessful
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 74044 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1813575180 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 2330 variables 3% in round 1 in 37461620 steps
c [elim-8-1] backward subsumption/strengthening limit 37461600
c [elim-8-1-1] backward checking 9047 touched variables 12%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 132 and strengthened 201 clauses in 2653332 steps
c [elim-8-1] rescheduled 697 variables 1% by backward subsumption
c [elim-8-2] eliminated 77 variables 0% in round 2 in 4372815 steps
c [elim-8-2] backward subsumption/strengthening limit 4372800
c [elim-8-2-1] backward checking 580 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 69 and strengthened 23 clauses in 419297 steps
c [elim-8-2] rescheduled 145 variables 0% by backward subsumption
c [elim-8-3] eliminated 22 variables 0% in round 3 in 3368885 steps
c [elim-8-3] backward subsumption/strengthening limit 3368800
c [elim-8-3-1] backward checking 169 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 40 and strengthened 2 clauses in 286058 steps
c [elim-8] incomplete 48 not tried 0% in round 3
c [gc-53] reconnected 92935 binary clauses (produced 0 empty 8 units)
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 2511 = 3% variables out of 74044 scheduled
c [bca-4] limit of 10000000 steps and 815070 added (scaled 2)
c [bca-4] 117598 out of 143068 literals actually usable 82%
c [bca-4] added 40 blocked clauses in 278289 steps
c [sweep-4] limit 1360181 penalty 0 = 0 + 0
c [sweep-4-1] 4905 pos 6.9% + 66456 neg 93.1% = 71361 sched 99.8% ret 172
c [sweep-4-1] 1429227 steps 17 queries 14297.35 avg class size
c [sweep-4-1] 183 decisions 13 SAT calls 51.08 avg env size
c [sweep-4-1] 71304 variables remain 100% (202 retained 0%)
c [decomp-21] removed 86 variables
c [sweep-4-1] removed 86 vars (0 failed, 3 eqs, 7 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 86 vars in TOTAL (1 rounds, 16 queries)
c [sort-queue-8] sorted 71447 enqueued variables after 10599 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 71447 (100%)
c [score-dist-8] max exp 0, different 1 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 5002 variables 6.5% (71447 remain 23%)
c [simplification-8] removed 30560 irredundant clauses 7.0% (406947 remain 30%)
c [simplification-8] maximum reduction of 7% = max (7%, 7%)
c [simplification-8] large reduction 7% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 22599 (soft 12599 + delta 10000)
c [simplification-8] new conflict limit 12599 (hard 22599)
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   58.6   71446   406947     10758    4936   2502 89071    7   728   41   1%      1  645    8    1  718%
c i   58.6   71445   406947     10759    4936   2502 89071    7   728   41   1%      1  645    8    1  715%
c i   58.7   71443   406947     10765    4940   2503 89071    7   728   41   1%      1  645    8    1  743%
c i   58.7   71442   406947     10767    4940   2504 89071    7   728   41   1%      1  645    8    1  737%
c i   58.7   71435   406947     10768    4940   2504 89071    7   727   41   1%      1  644    8    1  734%
c i   58.7   71434   406947     10769    4940   2504 89071    7   727   41   1%      1  644    8    1  731%
c i   58.7   71433   406947     10771    4940   2505 89071    7   727   41   1%      1  644    8    1  726%
c i   58.7   71432   406947     10772    4940   2505 89071    7   727   41   1%      1  644    8    1  723%
c i   58.7   71431   406947     10773    4940   2505 89071    7   727   41   1%      1  643    8    1  720%
c i   58.7   71427   406947     10780    4945   2506 89071    7   727   41   1%      1  644    8    1  720%
c i   60.0   71426   406947     11528    5549   2590 89117    7   716   41   1%      4  625    8    1  695%
c i   60.0   71425   406947     11529    5549   2590 89117    7   715   41   1%      4  625    8    1  692%
c i   60.0   71424   406947     11532    5550   2590 89118    7   715   41   1%      4  625    8    1  685%
c i   60.0   71423   406947     11533    5550   2590 89118    7   715   41   1%      4  624    8    1  683%
c i   60.1   71422   406947     11536    5552   2590 89118    7   714   41   1%      4  624    8    1  676%
c i   60.1   71421   406947     11537    5552   2590 89118    7   714   41   1%      4  624    8    1  673%
c i   60.2   71420   406947     11579    5584   2595 89122    7   711   41   1%      4  620    8    1  635%
c i   60.6   71406   406947     11844    5797   2620 89146    7   697   41   1%      3  603    8    1  618%
c i   60.9   71404   406947     12034    5953   2635 89158    7   696   41   1%      3  601    8    1  662%
c i   61.6   71398   406947     12393    6236   2664 89199    7   698   41   1%      3  600    7    1  583%
c i   62.1   71372   406947     12648    6427   2694 89227    8   696   41   1%      3  596    9    1  662%
c i   62.1   71369   406947     12649    6427   2694 89227    8   696   41   1%      3  596    9    1  660%
c i   62.1   71367   406947     12669    6438   2698 89231    8   696   41   1%      3  595    8    1  629%
c 
c [simplification-9] limit 12707 conflicts (hard 22599) hit after 12707 conflicts
c [quatres-5] found 30228 quaternary clauses 50% in total
c [quatres-5-2] added 2 single-self-subsuming ternary resolvents
c [quatres-5-2] added 24 quaternary resolvents
c [ternres-5] limit 5394249 with penalty 0 = 0 + 0
c [ternres-5] 21385 schedulable variables 30%
c [ternres-5] 1117 ternary resolvents (9 bin, 1108 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 48 xors of average arity 2.8
c [gauss-4] connected 136 occurrences of 129 variables (average 1.1)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [decomp-22] removed 62 variables
c [gauss-4] exported 1 unary, 0 binary and 0 ternary equations
c [treelook-4] limit 539424 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 78428 literals 55%
c [treelook-4] scheduling used 540581 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 539424 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 663010 steps
c [treelook-4] 78284 literals remain 55%
c [treelook-4] 17774 variables remain to probed next time 25%
c [decomp-24] removed 46 variables
c [treelook-4] removed 108 variables, found 4944 hbrs
c [unhide-9] limit 1078849 with penalty 0 = 0 + 0
c [unhide-9-9] 13 units, 66 failed, 4639 tauts, 0 hbrs, 7403 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 184 transitive binary clauses
c [transred-5] found 5 units
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 70943 variables 100%
c [elim-9] limit of 107884999 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 980 variables 1% in round 1 in 36031374 steps
c [elim-9-1] backward subsumption/strengthening limit 36031300
c [elim-9-1-1] backward checking 4435 touched variables 6%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 49 and strengthened 114 clauses in 1633839 steps
c [elim-9-1] rescheduled 314 variables 0% by backward subsumption
c [elim-9-2] eliminated 30 variables 0% in round 2 in 3311567 steps
c [elim-9-2] backward subsumption/strengthening limit 3311500
c [elim-9-2-1] backward checking 240 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 14 and strengthened 6 clauses in 246597 steps
c [elim-9-2] rescheduled 46 variables 0% by backward subsumption
c [elim-9-3] eliminated 4 variables 0% in round 3 in 432749 steps
c [elim-9-3] backward subsumption/strengthening limit 432700
c [elim-9-3-1] backward checking 35 touched variables 0%
c [elim-9-3-1] fully completed backward checking in 1 rounds
c [elim-9-3] subsumed 8 and strengthened 0 clauses in 98942 steps
c [elim-9] incomplete 11 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1024 = 1% variables out of 70943 scheduled
c [bca-5] limit of 10000000 steps and 794990 added (scaled 2)
c [bca-5] 112125 out of 139840 literals actually usable 80%
c [bca-5] added 21 blocked clauses in 264134 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 16182740 penalty 0 = 0 + 0
c [sweep-5-1] 5069 pos 7.3% + 64652 neg 92.7% = 69721 sched 99.7% ret 198
c [sweep-5-1] 16243289 steps 191 queries 4162.55 avg class size
c [sweep-5-1] 1184 decisions 149 SAT calls 43.64 avg env size
c [sweep-5-1] 65356 variables remain 94% (4166 retained 6%)
c [decomp-25] removed 660 variables
c [sweep-5-1] removed 660 vars (0 failed, 50 eqs, 64 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 660 vars in TOTAL (1 rounds, 190 queries)
c [sort-queue-9] sorted 69259 enqueued variables after 12707 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 69259 (100%)
c [score-dist-9] max exp 0, different 1 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 2026 variables 2.8% (69259 remain 22%)
c [simplification-9] removed 13476 irredundant clauses 3.3% (393471 remain 29%)
c [simplification-9] maximum reduction of 3% = max (3%, 3%)
c [simplification-9] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-9] new conflict interval 5000
c [simplification-9] penalized conflict interval 5000 = 1 * 5000
c [simplification-9] hard conflict limit 27707 (soft 17707 + delta 10000)
c [simplification-9] new conflict limit 17707 (hard 27707)
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   67.3   69258   393471     13029    6442   3125 99243    7   676   41   1%      3  572    7    1  506%
c i   68.0   68974   393471     13422    6785   3148 99265    8   690   41   1%      3  582    8    1  596%
c i   68.5   68973   393471     13694    7007   3174 99278    8   693   41   1%      3  583    9    1  603%
c i   68.8   68971   393471     13857    7137   3182 99298    8   688   41   1%      2  576    9    1  601%
c i   68.8   68970   393471     13882    7156   3185 99300    8   686   41   1%      2  574    8    1  575%
c i   69.4   68969   393471     14150    7371   3220 99315    8   696   41   1%      2  582    9    1  632%
c i   70.1   68968   393471     14562    7719   3251 99335    8   682   41   1%      2  564    8    2  535%
c i   70.7   68878   393471     14896    8004   3272 99357    8   677   41   1%      2  557    9    2  547%
c i   70.9   68873   393471     15033    8113   3287 99367    8   671   41   1%      2  550    9    2  540%
c i   71.3   68872   393471     15229    8282   3305 99372    8   675   41   1%      2  552    9    2  573%
c i   71.6   68868   393471     15419    8435   3317 99390    8   669   41   1%      2  545    8    2  523%
c i   71.8   68864   393471     15535    8525   3321 99408    8   668   41   1%      2  542    9    2  557%
c i   72.4   68863   393471     15889    8798   3345 99446    8   668   41   1%      2  540   10    2  587%
c i   72.4   68859   393471     15901    8807   3347 99446    8   668   41   1%      2  539   10    2  576%
c i   72.7   68856   393471     16031    8915   3355 99456    8   664   41   1%      2  534    9    2  532%
c i   73.3   68855   393471     16411    9234   3380 99484    8   649   41   1%      2  516    9    2  494%
c i   73.7   68809   393471     16656    9447   3393 99497    9   661   42   1%      2  526   10    2  564%
c i   73.8   68807   393471     16707    9472   3396 99519    9   670   42   1%      2  535   11    2  635%
c i   74.1   68806   393471     16894    9629   3409 99530    9   663   42   1%      2  526   10    2  571%
c i   74.3   68796   393471     16987    9704   3418 99535    9   660   42   1%      2  523    9    2  515%
c i   74.3   68786   393471     17002    9716   3420 99535    9   660   42   1%      2  522    9    2  505%
c i   74.9   68784   393471     17367   10022   3443 99563    9   654   42   1%      2  513   11    2  569%
c i   74.9   68776   393471     17368   10022   3443 99563    9   654   42   1%      2  513   11    2  567%
c 
c [simplification-10] limit 17717 conflicts (hard 27707) hit after 17718 conflicts
c [quatres-6] found 28826 quaternary clauses 49% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 7 single-self-subsuming ternary resolvents
c [quatres-6-2] added 24 quaternary resolvents
c [ternres-6] limit 7323156 with penalty 0 = 0 + 0
c [ternres-6] all 68769 free variables schedulable
c [ternres-6] 1323 ternary resolvents (14 bin, 1309 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 457697 penalty 3 = 3 + 0
c [card-4] found 2013 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 457697 for elimination
c [card-4] 2013 out of 2013 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] extracted 109 xors of average arity 2.7
c [gauss-5] connected 295 occurrences of 190 variables (average 1.6)
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-26] removed 190 variables
c [basicprobe-4] limit 36615783 penalty 0 = 0 + 0
c [basicprobe-4-0] 17375 probes remain 26% after last round
c [basicprobe-4-0] 253 units = 253 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 626 variables, found 50628 hbrs
c [bate-2] eliminated 100 asymmetric tautologies during probing
c [unhide-10] limit 1464631 with penalty 0 = 0 + 0
c [unhide-10-10] 23 units, 449 failed, 16082 tauts, 0 hbrs, 14567 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 151 transitive binary clauses
c [transred-6] found 3 units
c [cce-3] limit of 9153945 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 19
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 17
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 16
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 15
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 13
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-3-1] eliminated 2 clauses out of 3 (67%) of length 11
c [cce-3-1] eliminated 5 clauses out of 76 (7%) of length 10
c [cce-3-1] eliminated 1 clauses out of 301 (0%) of length 9
c [cce-3-1] eliminated 3 clauses out of 325 (1%) of length 8
c [cce-3-1] eliminated 19 clauses out of 506 (4%) of length 7
c [cce-3-1] eliminated 2 clauses out of 1392 (0%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 44 large clauses in 9153948 steps
c [cce-3-1] allowing another 4576974 steps for small clauses
c [cce-3-1] scheduling 281024 clauses = 195438 binary + 85586 ternary
c [cce-3-1] tried to eliminate 207 small clauses 0%
c [cce-3-1] eliminated 31 binary clauses 0%
c [cce-3-1] eliminated 32 ternary clauses 0%
c [cce-3-1] eliminated 63 small clauses 0%
c [cce-3-1] eliminated 5649 small clauses in 9153947 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 5693 covered clauses in round 1
c [cce-3] eliminated 5693 covered clauses in TOTAL during 1 rounds
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 67211 variables 100%
c [elim-10] limit of 146463134 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 2191 variables 3% in round 1 in 36614252 steps
c [elim-10-1] backward subsumption/strengthening limit 36614200
c [elim-10-1-1] backward checking 8473 touched variables 13%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 87 and strengthened 156 clauses in 2669949 steps
c [elim-10-1] rescheduled 577 variables 1% by backward subsumption
c [elim-10-2] eliminated 41 variables 0% in round 2 in 4258702 steps
c [elim-10-2] backward subsumption/strengthening limit 4258700
c [elim-10-2-1] backward checking 348 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 30 and strengthened 24 clauses in 414694 steps
c [elim-10-2] rescheduled 79 variables 0% by backward subsumption
c [elim-10-3] eliminated 10 variables 0% in round 3 in 2616003 steps
c [elim-10-3] backward subsumption/strengthening limit 2616000
c [elim-10-3-1] backward checking 94 touched variables 0%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 2 and strengthened 4 clauses in 203743 steps
c [elim-10] incomplete 16 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 2257 = 3% variables out of 67211 scheduled
c [bca-6] limit of 10000000 steps and 744800 added (scaled 2)
c [bca-6] 100092 out of 129910 literals actually usable 77%
c [bca-6] added 35 blocked clauses in 234389 steps
c [sweep-6] limit 2196947 penalty 0 = 0 + 0
c [sweep-6-1] 4553 pos 7.4% + 56788 neg 92.6% = 61341 sched 94.4% ret 3613
c [sweep-6-1] 2197466 steps 33 queries 9615.97 avg class size
c [sweep-6-1] 201 decisions 21 SAT calls 69.29 avg env size
c [sweep-6-1] 61248 variables remain 94% (3706 retained 6%)
c [decomp-27] removed 71 variables
c [sweep-6-1] removed 71 vars (0 failed, 12 eqs, 16 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 71 vars in TOTAL (1 rounds, 32 queries)
c [sort-queue-10] sorted 64883 enqueued variables after 17718 conflicts
c [score-dist-10] active 0 (0%), one 0 (0%), zero 64883 (100%)
c [score-dist-10] max exp 0, different 1 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 3886 variables 5.7% (64883 remain 21%)
c [simplification-10] removed 21493 irredundant clauses 5.5% (371978 remain 27%)
c [simplification-10] maximum reduction of 6% = max (6%, 5%)
c [simplification-10] large reduction 6% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 29718 (soft 19718 + delta 10000)
c [simplification-10] new conflict limit 19718 (hard 29718)
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   80.7   64882   371978     17811    9062   3833 122383    9   643   42   1%      2  499   10    2  544%
c i   81.4   64876   371978     18199    9392   3853 122406    9   633   42   1%      3  486    8    2  422%
c i   81.4   64875   371978     18207    9396   3856 122406    9   633   42   1%      2  487    8    2  413%
c i   82.1   64874   371978     18688    9802   3896 122431    9   629   42   1%      3  479   11    2  526%
c i   83.7   64873   371978     19616   10566   3975 122495    9   612   42   1%      6  455    9    2  422%
c 
c [simplification-11] limit 19719 conflicts (hard 29718) hit after 19719 conflicts
c [quatres-7] found 28222 quaternary clauses 49% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 5 single-self-subsuming ternary resolvents
c [quatres-7-2] added 22 quaternary resolvents
c [ternres-7] limit 8067597 with penalty 0 = 0 + 0
c [ternres-7] all 64873 free variables schedulable
c [ternres-7] 1259 ternary resolvents (5 bin, 1254 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-28] removed 42 variables
c [simpleprobe-5] 6313 schedulable variables 10%
c [simpleprobe-5] limit 32270388 penalty 0 = 0 + 0
c [decomp-29] removed 1050 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1050 variables, found 24933 hbrs, 278 units
c [unhide-11] limit 1613519 with penalty 0 = 0 + 0
c [unhide-11-11] 4 units, 43 failed, 5447 tauts, 0 hbrs, 14150 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 233 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 63679 variables 100%
c [block-4] limit of 20168993 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 335 blocked clauses
c [block-4] 335 < 1/100 * 360823 = 3608 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 63676 variables 100%
c [elim-11] limit of 161351944 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 1272 variables 2% in round 1 in 32558904 steps
c [elim-11-1] backward subsumption/strengthening limit 32558900
c [elim-11-1-1] backward checking 5839 touched variables 9%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 112 and strengthened 79 clauses in 1801782 steps
c [elim-11-1] rescheduled 416 variables 1% by backward subsumption
c [elim-11-2] eliminated 50 variables 0% in round 2 in 746327 steps
c [elim-11-2] backward subsumption/strengthening limit 746300
c [elim-11-2-1] backward checking 433 touched variables 1%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 49 and strengthened 15 clauses in 475845 steps
c [elim-11-2] rescheduled 125 variables 0% by backward subsumption
c [elim-11-3] eliminated 9 variables 0% in round 3 in 1176573 steps
c [elim-11-3] backward subsumption/strengthening limit 1176500
c [elim-11-3-1] backward checking 61 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 4 and strengthened 4 clauses in 157868 steps
c [elim-11] incomplete 20 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 1336 = 2% variables out of 63676 scheduled
c [bca-7] limit of 10000000 steps and 711390 added (scaled 2)
c [bca-7] 93496 out of 124682 literals actually usable 75%
c [bca-7] added 12 blocked clauses in 216699 steps
c [sweep-7] limit 2420279 penalty 0 = 0 + 0
c [sweep-7-1] 4409 pos 7.5% + 54520 neg 92.5% = 58929 sched 94.5% ret 3411
c [sweep-7-1] 2636731 steps 41 queries 5930.63 avg class size
c [sweep-7-1] 368 decisions 32 SAT calls 61.66 avg env size
c [sweep-7-1] 58639 variables remain 94% (3692 retained 6%)
c [decomp-30] removed 38 variables
c [sweep-7-1] removed 38 vars (0 failed, 9 eqs, 16 impls)
c [sweep-7] 38 < 1/1000 * 62340 = 62 considered unsuccessful
c [sweep-7] removed 38 vars in TOTAL (1 rounds, 40 queries)
c [sort-queue-11] sorted 62302 enqueued variables after 19719 conflicts
c [score-dist-11] active 0 (0%), one 0 (0%), zero 62302 (100%)
c [score-dist-11] max exp 0, different 1 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 2571 variables 4.0% (62302 remain 20%)
c [simplification-11] removed 16747 irredundant clauses 4.5% (355231 remain 26%)
c [simplification-11] maximum reduction of 5% = max (4%, 5%)
c [simplification-11] large reduction 5% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 31719 (soft 21719 + delta 10000)
c [simplification-11] new conflict limit 21719 (hard 31719)
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.9   62301   355231     19729   10063   4096 138653    9   608   41   1%      5  450    9    2  443%
c i   88.3   62300   355231     19971   10268   4114 138670    9   619   42   1%      4  459   11    2  508%
c i   88.8   62273   355231     20284   10550   4134 138679    9   616   42   1%      4  454   10    2  478%
c i   89.6   62272   355231     20772   10951   4175 138711    9   612   42   1%      4  447    8    2  368%
c i   89.6   62264   355231     20773   10951   4175 138711    9   612   42   1%      4  447    8    2  367%
c i   89.6   62263   355231     20778   10954   4175 138712    9   612   42   1%      4  447    8    2  366%
c i   89.7   62259   355231     20829   10992   4177 138717    9   625   42   1%      3  460    9    2  413%
c i   90.4   62257   355231     21230   11336   4202 138738    9   634   42   1%      3  466   13    2  548%
c i   90.7   62225   355231     21478   11545   4221 138754    9   619   42   1%      3  449   10    2  416%
c 
c [simplification-12] limit 21731 conflicts (hard 31719) hit after 21731 conflicts
c [quatres-8] found 25350 quaternary clauses 47% in total
c [quatres-8-2] added 6 single-self-subsuming ternary resolvents
c [quatres-8-2] added 18 quaternary resolvents
c [ternres-8] limit 8802319 with penalty 0 = 0 + 0
c [ternres-8] all 62196 free variables schedulable
c [ternres-8] 808 ternary resolvents (1 bin, 807 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-6] limit 1000000 penalty 1 = 1 + 0
c [gauss-6] extracted 32 xors of average arity 2.9
c [gauss-6] connected 94 occurrences of 94 variables (average 1.0)
c [gauss-6] limit 1000000 penalty 1 = 1 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 6 variables
c [treelook-5] limit 880231 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 91213 literals 73%
c [treelook-5] scheduling used 880236 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 880231 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 931832 steps
c [treelook-5] 91194 literals remain 73%
c [treelook-5] 14710 variables remain to probed next time 24%
c [treelook-5] removed 4 variables, found 5540 hbrs
c [unhide-12] limit 1760463 with penalty 0 = 0 + 0
c [unhide-12-12] 9 units, 150 failed, 15766 tauts, 0 hbrs, 11442 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 200 transitive binary clauses
c [transred-8] found 2 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 220057980 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 13
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 12
c [cce-4-1] eliminated 3 clauses out of 4 (75%) of length 11
c [cce-4-1] eliminated 3 clauses out of 72 (4%) of length 10
c [cce-4-1] eliminated 2 clauses out of 290 (1%) of length 9
c [cce-4-1] eliminated 2 clauses out of 303 (1%) of length 8
c [cce-4-1] eliminated 18 clauses out of 484 (4%) of length 7
c [cce-4-1] eliminated 97 clauses out of 1386 (7%) of length 6
c [cce-4-1] eliminated 15029 clauses out of 22839 (66%) of length 5
c [cce-4-1] eliminated 3998 clauses out of 24127 (17%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 19155 large clauses in 220057981 steps
c [cce-4-1] allowing another 110028990 steps for small clauses
c [cce-4-1] scheduling 260435 clauses = 181652 binary + 78783 ternary
c [cce-4-1] tried to eliminate 4326 small clauses 2%
c [cce-4-1] eliminated 692 binary clauses 0%
c [cce-4-1] eliminated 487 ternary clauses 1%
c [cce-4-1] eliminated 1179 small clauses 0%
c [cce-4-1] eliminated 2897 small clauses in 220057984 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 22052 covered clauses in round 1
c [cce-4] eliminated 22052 covered clauses in TOTAL during 1 rounds
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 61994 variables 100%
c [elim-12] limit of 176046384 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 10693 variables 17% in round 1 in 28186751 steps
c [elim-12-1] backward subsumption/strengthening limit 28186700
c [elim-12-1-1] backward checking 26250 touched variables 42%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 54 and strengthened 141 clauses in 3991096 steps
c [elim-12-1] rescheduled 418 variables 1% by backward subsumption
c [elim-12-2] eliminated 25 variables 0% in round 2 in 1370459 steps
c [elim-12-2] backward subsumption/strengthening limit 1370400
c [elim-12-2-1] backward checking 287 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 15 and strengthened 7 clauses in 440494 steps
c [elim-12-2] rescheduled 51 variables 0% by backward subsumption
c [elim-12-3] eliminated 7 variables 0% in round 3 in 619341 steps
c [elim-12-3] backward subsumption/strengthening limit 619300
c [elim-12-3-1] backward checking 80 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 13 and strengthened 3 clauses in 404989 steps
c [elim-12] incomplete 23 not tried 0% in round 3
c [gc-87] reconnected 127788 binary clauses (produced 0 empty 1 units)
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 10731 = 17% variables out of 61994 scheduled
c [bca-8] limit of 10000000 steps and 613304 added (scaled 2)
c [bca-8] 89103 out of 102528 literals actually usable 87%
c [bca-8] added 29 blocked clauses in 200530 steps
c [sort-queue-12] sorted 51263 enqueued variables after 21731 conflicts
c [score-dist-12] active 0 (0%), one 0 (0%), zero 51263 (100%)
c [score-dist-12] max exp 0, different 1 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 10933 variables 17.6% (51263 remain 16%)
c [simplification-12] removed 48903 irredundant clauses 13.8% (306328 remain 22%)
c [simplification-12] maximum reduction of 18% = max (18%, 14%)
c [simplification-12] large reduction 18% >= 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 33731 (soft 23731 + delta 10000)
c [simplification-12] new conflict limit 23731 (hard 33731)
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  101.6   51262   306328     22103    4709   4840 111521    9   605   37   2%      4  431    8    2  338%
c i  102.3   51261   306328     22653    5166   4889 111556    9   588   37   2%      4  410    7    2  293%
c i  102.4   51257   306328     22759    5260   4896 111559    9   585   37   2%      3  407    8    2  317%
c i  102.4   51209   306328     22794    5289   4900 111560    9   584   37   2%      3  405    7    2  305%
c i  102.7   51169   306328     22962    5427   4918 111568    9   578   37   2%      3  398    7    2  295%
c i  102.7   51136   306328     22982    5444   4919 111568    9   578   37   2%      3  398    7    2  292%
c i  103.2   51079   306328     23304    5706   4953 111589    9   568   37   2%      3  387    7    2  265%
c i  103.3   51077   306328     23412    5798   4959 111594    9   569   37   2%      2  387    7    2  301%
c i  103.4   51073   306328     23497    5870   4967 111597    9   566   37   2%      2  383    7    2  284%
c 
c [simplification-13] limit 23731 conflicts (hard 33731) hit after 23731 conflicts
c [quatres-9] found 26588 quaternary clauses 69% in total
c [quatres-9-1] removed 3 duplicate quaternary clauses
c [quatres-9-2] added 13 quaternary resolvents
c [ternres-9] limit 9469207 with penalty 0 = 0 + 0
c [ternres-9] all 51073 free variables schedulable
c [ternres-9] 914 ternary resolvents (5 bin, 909 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-33] removed 215 variables
c [basicprobe-5] limit 47346036 penalty 0 = 0 + 0
c [basicprobe-5-0] 10153 probes remain 20% after last round
c [basicprobe-5-0] 351 units = 346 failed (99%) + 5 lifted (1%)
c [basicprobe-5-0] removed 547 variables, found 72558 hbrs
c [bate-3] eliminated 651 asymmetric tautologies during probing
c [unhide-13] limit 1893841 with penalty 0 = 0 + 0
c [unhide-13-14] 8 units, 260 failed, 21569 tauts, 0 hbrs, 6683 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 170 transitive binary clauses
c [transred-9] found 1 units
c [cce-5] limit of 47346036 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 15 (13%) of length 7
c [cce-5-1] eliminated 47 clauses out of 1195 (4%) of length 6
c [cce-5-1] eliminated 79 clauses out of 7930 (1%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 128 large clauses in 47346040 steps
c [cce-5-1] allowing another 23673020 steps for small clauses
c [cce-5-1] scheduling 186662 clauses = 146608 binary + 40054 ternary
c [cce-5-1] tried to eliminate 1059 small clauses 1%
c [cce-5-1] eliminated 223 binary clauses 0%
c [cce-5-1] eliminated 57 ternary clauses 0%
c [cce-5-1] eliminated 280 small clauses 0%
c [cce-5-1] eliminated 2578 small clauses in 47346041 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2706 covered clauses in round 1
c [cce-5] eliminated 2706 covered clauses in TOTAL during 1 rounds
c [cce-5] 2706 < 1/100 * 295276 = 2952 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 50119 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 1512 variables 3% in round 1 in 24966891 steps
c [elim-13-1] backward subsumption/strengthening limit 24966800
c [elim-13-1-1] backward checking 7420 touched variables 15%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 53 and strengthened 126 clauses in 1767691 steps
c [elim-13-1] rescheduled 404 variables 1% by backward subsumption
c [elim-13-2] eliminated 19 variables 0% in round 2 in 384115 steps
c [elim-13-2] backward subsumption/strengthening limit 384100
c [elim-13-2-1] backward checking 208 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 8 and strengthened 7 clauses in 117174 steps
c [elim-13-2] rescheduled 40 variables 0% by backward subsumption
c [elim-13-3] eliminated 1 variables 0% in round 3 in 115101 steps
c [elim-13-3] backward subsumption/strengthening limit 115100
c [elim-13-3-1] backward checking 16 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 2 and strengthened 0 clauses in 56102 steps
c [elim-13] incomplete 5 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 1533 = 3% variables out of 50119 scheduled
c [bca-9] limit of 10000000 steps and 578136 added (scaled 2)
c [bca-9] 80744 out of 97174 literals actually usable 83%
c [bca-9] added 35 blocked clauses in 180811 steps
c [sweep-8] limit 1420381 penalty 1 = 1 + 0
c [sweep-8-1] 3972 pos 8.6% + 42034 neg 91.4% = 46006 sched 94.7% ret 2580
c [sweep-8-1] 1436039 steps 34 queries 9544.18 avg class size
c [sweep-8-1] 453 decisions 32 SAT calls 64.81 avg env size
c [sweep-8-1] 45768 variables remain 94% (2815 retained 6%)
c [decomp-34] removed 37 variables
c [sweep-8-1] removed 37 vars (0 failed, 1 eqs, 3 impls)
c [sweep-8] 37 < 1/1000 * 48586 = 48 considered unsuccessful
c [sweep-8] removed 37 vars in TOTAL (1 rounds, 33 queries)
c [sort-queue-13] sorted 48549 enqueued variables after 23731 conflicts
c [score-dist-13] active 0 (0%), one 0 (0%), zero 48549 (100%)
c [score-dist-13] max exp 0, different 1 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 2524 variables 4.9% (48549 remain 15%)
c [simplification-13] removed 17664 irredundant clauses 5.8% (288664 remain 21%)
c [simplification-13] maximum reduction of 6% = max (5%, 6%)
c [simplification-13] large reduction 6% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 35731 (soft 25731 + delta 10000)
c [simplification-13] new conflict limit 25731 (hard 35731)
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  109.5   48548   288664     23792    5744   4796 150742    8   563   37   2%      2  379    7    2  294%
c i  109.9   48546   288664     24088    6005   4812 150750    9   560   37   2%      2  374    8    3  331%
c i  110.5   48521   288664     24690    6538   4842 150780    8   539   37   2%      3  350    8    3  292%
c i  111.3   48519   288664     25302    7051   4890 150817    8   526   37   2%      4  333    7    3  286%
c i  111.5   48518   288664     25464    7193   4899 150824    8   524   37   2%      3  330    8    3  292%
c i  111.7   48517   288664     25703    7397   4921 150835    8   516   37   2%      3  321    7    3  281%
c 
c [simplification-14] limit 25731 conflicts (hard 35731) hit after 25731 conflicts
c [quatres-10] found 24831 quaternary clauses 68% in total
c [quatres-10-1] removed 2 duplicate quaternary clauses
c [quatres-10-2] added 23 quaternary resolvents
c [ternres-10] limit 10067172 with penalty 0 = 0 + 0
c [ternres-10] all 48503 free variables schedulable
c [ternres-10] 1609 ternary resolvents (9 bin, 1600 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-35] removed 48 variables
c [simpleprobe-6] all 48501 free variables schedulable
c [simpleprobe-6] limit 40268691 penalty 0 = 0 + 0
c [decomp-36] removed 714 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 714 variables, found 42254 hbrs, 180 units
c [unhide-14] limit 2013434 with penalty 0 = 0 + 0
c [unhide-14-16] 12 units, 81 failed, 25207 tauts, 0 hbrs, 8592 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 295 transitive binary clauses
c [transred-10] found 2 units
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 47535 variables 100%
c [elim-14] limit of 201343458 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 745 variables 2% in round 1 in 23753050 steps
c [elim-14-1] backward subsumption/strengthening limit 23753000
c [elim-14-1-1] backward checking 4066 touched variables 9%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 27 and strengthened 31 clauses in 1003050 steps
c [elim-14-1] rescheduled 152 variables 0% by backward subsumption
c [elim-14-2] eliminated 12 variables 0% in round 2 in 249226 steps
c [elim-14-2] backward subsumption/strengthening limit 249200
c [elim-14-2-1] backward checking 172 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 13 and strengthened 7 clauses in 115498 steps
c [elim-14-2] rescheduled 36 variables 0% by backward subsumption
c [elim-14-3] eliminated 2 variables 0% in round 3 in 69191 steps
c [elim-14-3] backward subsumption/strengthening limit 69100
c [elim-14-3-1] backward checking 22 touched variables 0%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 1 and strengthened 0 clauses in 66411 steps
c [elim-14] incomplete 2 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 763 = 2% variables out of 47535 scheduled
c [bca-10] limit of 10000000 steps and 555600 added (scaled 2)
c [bca-10] 74935 out of 93546 literals actually usable 80%
c [bca-10] added 20 blocked clauses in 168501 steps
c [sort-queue-14] sorted 46772 enqueued variables after 25731 conflicts
c [score-dist-14] active 0 (0%), one 0 (0%), zero 46772 (100%)
c [score-dist-14] max exp 0, different 1 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 1731 variables 3.6% (46772 remain 15%)
c [simplification-14] removed 11204 irredundant clauses 3.9% (277460 remain 20%)
c [simplification-14] maximum reduction of 4% = max (4%, 4%)
c [simplification-14] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-14] new conflict interval 9000
c [simplification-14] penalized conflict interval 9000 = 1 * 9000
c [simplification-14] hard conflict limit 44731 (soft 34731 + delta 10000)
c [simplification-14] new conflict limit 34731 (hard 44731)
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  115.2   46771   277460     26012    7368   5201 162733    8   508   37   2%      3  312    9    3  317%
c i  115.2   46769   277460     26058    7411   5203 162733    8   505   37   2%      2  309    8    3  301%
c i  115.9   46768   277460     26590    7871   5251 162753    8   494   37   2%      3  296    7    3  248%
c i  115.9   46767   277460     26651    7922   5255 162758    8   493   37   2%      3  294    7    3  242%
c i  116.1   46766   277460     26774    8030   5261 162762    8   491   37   2%      2  291    7    3  273%
c i  116.4   46765   277460     27113    8325   5282 162782    8   483   37   2%      2  282    8    3  285%
c i  117.1   46763   277460     27647    8797   5322 162797    8   480   37   2%      3  276    9    3  309%
c i  117.2   46750   277460     27742    8880   5329 162799    8   477   37   2%      3  273    8    3  281%
c i  117.3   46749   277460     27802    8926   5335 162805    8   479   37   2%      2  275    9    3  311%
c i  117.4   46734   277460     27862    8974   5339 162809    8   478   37   2%      2  274    8    3  285%
c i  117.7   46717   277460     28154    9233   5357 162819    8   476   37   2%      2  270    9    3  326%
c i  118.6   46715   277460     28890    9866   5411 162855    8   477   37   2%      4  268    9    3  297%
c i  118.7   46638   277460     28989    9960   5415 162855    8   474   37   2%      3  265    8    3  288%
c i  119.0   46637   277460     29241   10181   5434 162863    8   476   37   2%      3  266   10    3  338%
c i  119.2   46636   277460     29391   10315   5442 162868    8   473   37   2%      3  263    9    3  306%
c i  119.2   46635   277460     29395   10315   5441 162870    8   473   37   2%      3  262    9    3  303%
c i  119.2   46629   277460     29407   10324   5442 162871    8   475   37   2%      3  264   10    3  333%
c i  119.5   46628   277460     29687   10561   5463 162888    8   471   37   2%      2  259    8    3  281%
c i  119.6   46624   277460     29710   10579   5465 162890    8   471   37   2%      2  259    8    3  274%
c i  119.6   46622   277460     29766   10622   5469 162892    8   474   37   2%      2  263    9    3  308%
c i  119.6   46582   277460     29767   10622   5469 162892    8   474   37   2%      2  262    9    3  307%
c i  119.6   46579   277460     29768   10622   5469 162892    8   474   37   2%      2  262    9    3  306%
c i  120.1   46578   277460     30091   10883   5496 162915    8   471   38   2%      2  258    8    3  281%
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  120.6   46577   277460     30530   11268   5523 162930    8   471   38   2%      2  256    9    3  291%
c i  120.6   46533   277460     30544   11278   5525 162931    8   470   38   2%      2  255    9    3  284%
c i  120.7   46532   277460     30649   11363   5534 162937    8   473   38   2%      2  257    9    3  305%
c i  121.2   46531   277460     31034   11704   5553 162954    9   477   38   2%      2  260   11    3  346%
c i  121.7   46520   277460     31443   12071   5576 162966    9   476   38   2%      2  258   10    3  311%
c i  122.6   46489   277460     32120   12657   5622 163001    9   474   38   2%      3  253    9    3  277%
c i  122.6   46488   277460     32128   12664   5622 163001    9   474   38   2%      3  252    9    3  280%
c i  123.4   46487   277460     32728   13186   5661 163020    9   471   38   2%      4  247   10    3  301%
c i  123.7   46486   277460     33043   13464   5676 163038    9   470   38   2%      3  246    9    3  286%
c i  125.0   46485   277460     34050   14356   5737 163071    9   461   38   2%      6  232    9    3  272%
c i  125.1   46482   277460     34169   14461   5743 163077    9   460   38   2%      5  231   11    3  312%
c 
c [simplification-15] limit 34754 conflicts (hard 44731) hit after 34754 conflicts
c [quatres-11] found 23213 quaternary clauses 64% in total
c [quatres-11-2] added 1 single-self-subsuming ternary resolvents
c [quatres-11-2] added 17 quaternary resolvents
c [ternres-11] limit 12792465 with penalty 0 = 0 + 0
c [ternres-11] all 46477 free variables schedulable
c [ternres-11] 805 ternary resolvents (3 bin, 802 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 399764 penalty 4 = 4 + 0
c [card-5] found 1212 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 399764 for elimination
c [card-5] 1212 out of 1212 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-7] limit 639623 penalty 2 = 2 + 0
c [gauss-7] extracted 43 xors of average arity 2.5
c [gauss-7] connected 108 occurrences of 95 variables (average 1.1)
c [gauss-7] limit 639623 penalty 2 = 2 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-37] removed 73 variables
c [treelook-6] limit 1279246 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 63885 literals 69%
c [treelook-6] scheduling used 809263 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1279246 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1311385 steps
c [treelook-6] 63798 literals remain 69%
c [treelook-6] 10152 variables remain to probed next time 22%
c [decomp-38] removed 6 variables
c [treelook-6] removed 16 variables, found 11579 hbrs
c [unhide-15] limit 2558493 with penalty 0 = 0 + 0
c [unhide-15-18] 4 units, 127 failed, 12912 tauts, 0 hbrs, 37359 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 210 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 46280 variables 100%
c [block-5] limit of 15990582 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 384 blocked clauses
c [block-5] 384 < 1/100 * 273149 = 2731 considered unsuccessful
c [cce-6] limit of 31981164 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 44
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 43
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 42
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 41
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 40
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 39
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 38
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 37
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 36
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 35
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 34
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 33
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 32
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 31
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 30
c [cce-6-1] eliminated 5 clauses out of 5 (100%) of length 29
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 28
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 27
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 26
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 25
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 24
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 23
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 22
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 21
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 20
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 19
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 18
c [cce-6-1] eliminated 7 clauses out of 9 (78%) of length 17
c [cce-6-1] eliminated 5 clauses out of 10 (50%) of length 16
c [cce-6-1] eliminated 8 clauses out of 10 (80%) of length 15
c [cce-6-1] eliminated 7 clauses out of 10 (70%) of length 14
c [cce-6-1] eliminated 8 clauses out of 11 (73%) of length 13
c [cce-6-1] eliminated 7 clauses out of 10 (70%) of length 12
c [cce-6-1] eliminated 8 clauses out of 11 (73%) of length 11
c [cce-6-1] eliminated 7 clauses out of 10 (70%) of length 10
c [cce-6-1] eliminated 7 clauses out of 11 (64%) of length 9
c [cce-6-1] eliminated 10 clauses out of 18 (56%) of length 8
c [cce-6-1] eliminated 8 clauses out of 26 (31%) of length 7
c [cce-6-1] eliminated 13 clauses out of 1148 (1%) of length 6
c [cce-6-1] eliminated 3 clauses out of 7711 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 190 large clauses in 31981170 steps
c [cce-6-1] allowing another 15990585 steps for small clauses
c [cce-6-1] scheduling 203282 clauses = 137014 binary + 66268 ternary
c [cce-6-1] tried to eliminate 695 small clauses 0%
c [cce-6-1] eliminated 97 binary clauses 0%
c [cce-6-1] eliminated 71 ternary clauses 0%
c [cce-6-1] eliminated 168 small clauses 0%
c [cce-6-1] eliminated 168 small clauses in 31981168 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 358 covered clauses in round 1
c [cce-6] eliminated 358 covered clauses in TOTAL during 1 rounds
c [cce-6] 358 < 1/100 * 272167 = 2721 considered unsuccessful
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 46278 variables 100%
c [elim-15] limit of 255849317 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 426 variables 1% in round 1 in 22550372 steps
c [elim-15-1] backward subsumption/strengthening limit 22550300
c [elim-15-1-1] backward checking 2794 touched variables 6%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 12 and strengthened 39 clauses in 764434 steps
c [elim-15-1] rescheduled 145 variables 0% by backward subsumption
c [elim-15-2] eliminated 9 variables 0% in round 2 in 230693 steps
c [elim-15-2] backward subsumption/strengthening limit 230600
c [elim-15-2-1] backward checking 87 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 8 and strengthened 6 clauses in 101270 steps
c [elim-15-2] rescheduled 16 variables 0% by backward subsumption
c [elim-15-3] eliminated 1 variables 0% in round 3 in 84305 steps
c [elim-15-3] backward subsumption/strengthening limit 84300
c [elim-15-3-1] backward checking 10 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 0 and strengthened 0 clauses in 44933 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 444 = 1% variables out of 46278 scheduled
c [elim-15] 444 < 1/100 * 46278 = 462 considered unsuccessful
c [bca-11] limit of 10000000 steps and 542094 added (scaled 2)
c [bca-11] 66161 out of 91670 literals actually usable 72%
c [bca-11] added 11 blocked clauses in 154103 steps
c [sort-queue-15] sorted 45834 enqueued variables after 34754 conflicts
c [score-dist-15] active 0 (0%), one 0 (0%), zero 45834 (100%)
c [score-dist-15] max exp 0, different 1 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 643 variables 1.4% (45834 remain 15%)
c [simplification-15] removed 6758 irredundant clauses 2.4% (270702 remain 20%)
c [simplification-15] maximum reduction of 2% = max (1%, 2%)
c [simplification-15] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-15] new conflict interval 15666
c [simplification-15] penalized conflict interval 15666 = 1 * 15666
c [simplification-15] hard conflict limit 60420 (soft 50420 + delta 10000)
c [simplification-15] new conflict limit 50420 (hard 60420)
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  130.3   45833   270702     35035   14548   6007 159820    9   455   39   2%      6  223    9    3  264%
c i  130.3   45804   270702     35051   14562   6007 159821    9   454   39   2%      6  222    9    3  256%
c i  130.9   45798   270702     35574   15040   6028 159835    9   450   39   2%      5  216    9    4  266%
c i  131.0   45796   270702     35606   15063   6029 159840    9   451   39   2%      5  218   10    4  283%
c i  131.2   45792   270702     35799   15232   6039 159847    9   448   39   2%      4  214   10    4  286%
c i  131.7   45777   270702     36225   15602   6073 159857    9   447   39   2%      3  211   11    4  305%
c i  131.9   45776   270702     36355   15720   6082 159859    9   443   39   2%      3  207   10    4  275%
c i  132.0   45775   270702     36413   15768   6085 159861    9   445   39   2%      3  208   10    4  280%
c i  132.2   45771   270702     36555   15886   6098 159868    9   444   39   2%      2  208    9    4  251%
c i  132.6   45768   270702     36949   16229   6121 159885    9   444   39   2%      2  206    9    4  250%
c i  133.7   45767   270702     37841   17025   6154 159929    9   433   39   2%      5  192   10    4  262%
c i  133.7   45739   270702     37842   17025   6154 159929    9   432   39   2%      5  192   10    4  261%
c i  134.2   45731   270702     38202   17334   6181 159946    9   428   39   2%      4  186    9    4  233%
c i  134.3   45727   270702     38265   17392   6184 159946    9   428   39   2%      4  186    9    4  241%
c i  134.5   45723   270702     38450   17555   6189 159959    9   423   39   2%      3  181    9    4  239%
c i  134.7   45721   270702     38667   17761   6191 159962   10   420   39   2%      2  177   12    4  309%
c i  134.7   45585   270702     38668   17761   6191 159962   10   420   39   2%      2  177   12    4  308%
c i  135.0   45583   270702     38899   17965   6203 159973   10   417   39   2%      2  173   11    4  295%
c i  135.0   45582   270702     38920   17982   6205 159974   10   417   39   2%      2  173   11    4  293%
c i  137.2   45577   270702     40672   19538   6296 160046   10   415   40   2%     13  167    9    4  237%
c i  137.8   45576   270702     41176   19985   6321 160068   10   413   40   2%      9  164   10    4  251%
c i  137.8   45570   270702     41177   19985   6321 160068   10   413   40   2%      9  164   10    4  250%
c i  137.9   45568   270702     41182   19989   6321 160068   10   413   40   2%      9  163   10    4  247%
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  138.5   45567   270702     41672   20437   6335 160086   10   416   40   2%      7  165   11    4  256%
c i  139.6   45532   270702     42429   21114   6376 160110   10   414   41   2%      6  161    9    4  225%
c i  139.7   45531   270702     42562   21235   6383 160113   10   415   41   2%      5  162   11    4  264%
c i  140.0   45484   270702     42726   21380   6392 160120   10   416   41   2%      4  162   11    4  261%
c i  140.6   45483   270702     43276   21874   6418 160140   10   412   41   2%      4  157   11    4  256%
c i  140.9   45482   270702     43479   22051   6430 160152   10   413   41   2%      3  157   11    4  249%
c i  141.0   45481   270702     43493   22062   6432 160152   10   413   41   2%      3  158   10    4  241%
c i  147.2   45480   270702     48257   26312   6678 160320   11   414   43   3%     55  148   13    5  272%
c i  147.2   45474   270702     48264   26317   6679 160320   11   414   43   3%     55  148   13    5  269%
c i  147.4   45473   270702     48433   26470   6684 160329   11   414   43   3%     46  147   11    5  232%
c i  148.4   45468   270702     49127   27080   6718 160354   12   415   43   3%     24  146   13    5  272%
c i  150.2   45462   270702     50381   28200   6768 160415   11   413   43   3%     12  142   11    5  219%
c 
c [simplification-16] limit 50453 conflicts (hard 60420) hit after 50453 conflicts
c [quatres-12] found 23030 quaternary clauses 61% in total
c [quatres-12-1] removed 3 duplicate quaternary clauses
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [quatres-12-2] added 25 quaternary resolvents
c [ternres-12] limit 17589736 with penalty 0 = 0 + 0
c [ternres-12] all 45458 free variables schedulable
c [ternres-12] 606 ternary resolvents (2 bin, 604 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-39] removed 515 variables
c [basicprobe-6] limit 87948683 penalty 0 = 0 + 0
c [basicprobe-6-0] 4736 probes remain 11% after last round
c [basicprobe-6-0] 595 units = 576 failed (97%) + 19 lifted (3%)
c [basicprobe-6-0] removed 1104 variables, found 105653 hbrs
c [bate-4] eliminated 664 asymmetric tautologies during probing
c [unhide-16] limit 3517947 with penalty 0 = 0 + 0
c [unhide-16-20] 7 units, 410 failed, 26580 tauts, 0 hbrs, 84895 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 206 transitive binary clauses
c [transred-12] found 2 units
c [bca-12] limit of 10000000 steps and 500143 added (scaled 2)
c [bca-12] 56111 out of 87540 literals actually usable 64%
c [bca-12] added 12 blocked clauses in 144029 steps
c [sweep-9] limit 1319230 penalty 2 = 2 + 0
c [sweep-9-1] 3977 pos 9.6% + 37476 neg 90.4% = 41453 sched 94.7% ret 2316
c [sweep-9-1] 1365442 steps 13 queries 8077.85 avg class size
c [sweep-9-1] 150 decisions 11 SAT calls 64.73 avg env size
c [sweep-9-1] 41423 variables remain 95% (2342 retained 5%)
c [decomp-40] removed 591 variables
c [sweep-9-1] removed 591 vars (0 failed, 1 eqs, 1 impls)
c [sweep-9] removed 591 vars in TOTAL (1 rounds, 12 queries)
c [sort-queue-16] sorted 43178 enqueued variables after 50453 conflicts
c [score-dist-16] active 0 (0%), one 0 (0%), zero 43178 (100%)
c [score-dist-16] max exp 0, different 1 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 2280 variables 5.0% (43178 remain 14%)
c [simplification-16] removed 22143 irredundant clauses 8.2% (248559 remain 18%)
c [simplification-16] maximum reduction of 8% = max (5%, 8%)
c [simplification-16] large reduction 8% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 62453 (soft 52453 + delta 10000)
c [simplification-16] new conflict limit 52453 (hard 62453)
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  155.4   43177   248559     50829   28137   6506 227219   11   409   46   3%      8  137   10    5  202%
c i  155.4   43169   248559     50843   28149   6506 227219   11   409   46   3%      8  137   10    5  198%
c i  155.4   43168   248559     50846   28150   6507 227219   11   409   46   3%      8  137   10    5  197%
c i  155.4   43166   248559     50847   28150   6507 227219   11   409   46   3%      8  137   10    5  196%
c 
c [simplification-17] limit 52466 conflicts (hard 62453) hit after 52466 conflicts
c [quatres-13] found 21480 quaternary clauses 59% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 2 single-self-subsuming ternary resolvents
c [quatres-13-2] added 2 quaternary resolvents
c [ternres-13] limit 18201630 with penalty 0 = 0 + 0
c [ternres-13] all 43155 free variables schedulable
c [ternres-13] 334 ternary resolvents (2 bin, 332 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-41] removed 34 variables
c [simpleprobe-7] all 43144 free variables schedulable
c [simpleprobe-7] limit 72806521 penalty 0 = 0 + 0
c [decomp-42] removed 738 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 738 variables, found 31601 hbrs, 159 units
c [unhide-17] limit 3640326 with penalty 0 = 0 + 0
c [unhide-17-22] 5 units, 79 failed, 24981 tauts, 0 hbrs, 63154 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 275 transitive binary clauses
c [transred-13] found 3 units
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 42252 variables 100%
c [elim-16] limit of 182016303 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 1623 variables 4% in round 1 in 20210459 steps
c [elim-16-1] backward subsumption/strengthening limit 20210400
c [elim-16-1-1] backward checking 8028 touched variables 19%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 109 and strengthened 95 clauses in 1760700 steps
c [elim-16-1] rescheduled 547 variables 1% by backward subsumption
c [elim-16-2] eliminated 38 variables 0% in round 2 in 464499 steps
c [elim-16-2] backward subsumption/strengthening limit 464400
c [elim-16-2-1] backward checking 334 touched variables 1%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 14 and strengthened 22 clauses in 155367 steps
c [elim-16-2] rescheduled 99 variables 0% by backward subsumption
c [elim-16-3] eliminated 4 variables 0% in round 3 in 142035 steps
c [elim-16-3] backward subsumption/strengthening limit 142000
c [elim-16-3-1] backward checking 46 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 11 and strengthened 3 clauses in 98266 steps
c [elim-16] incomplete 18 not tried 0% in round 3
c [gc-126] reconnected 230453 binary clauses (produced 0 empty 1 units)
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 1668 = 4% variables out of 42252 scheduled
c [bca-13] limit of 10000000 steps and 475829 added (scaled 2)
c [bca-13] 51297 out of 81170 literals actually usable 63%
c [bca-13] added 14 blocked clauses in 132056 steps
c [sort-queue-17] sorted 40584 enqueued variables after 52466 conflicts
c [score-dist-17] active 0 (0%), one 0 (0%), zero 40584 (100%)
c [score-dist-17] max exp 0, different 1 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 2571 variables 6.0% (40584 remain 13%)
c [simplification-17] removed 10995 irredundant clauses 4.4% (237564 remain 17%)
c [simplification-17] maximum reduction of 6% = max (6%, 4%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 64466 (soft 54466 + delta 10000)
c [simplification-17] new conflict limit 54466 (hard 64466)
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  161.0   40583   237564     52481   25274   6089 218285   12   415   43   3%     11  140   13    5  254%
c i  161.4   40582   237564     52763   25534   6101 218289   12   411   43   3%      8  135   10    5  198%
c 
c [simplification-18] limit 54466 conflicts (hard 64466) hit after 54466 conflicts
c [quatres-14] found 21480 quaternary clauses 59% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 13 quaternary resolvents
c [ternres-14] limit 18739186 with penalty 0 = 0 + 0
c [ternres-14] all 40580 free variables schedulable
c [ternres-14] 769 ternary resolvents (3 bin, 766 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-43] removed 14 variables
c [treelook-7] limit 1873918 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 53877 literals 66%
c [treelook-7] scheduling used 750400 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 1873918 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 1902377 steps
c [treelook-7] 53704 literals remain 66%
c [treelook-7] 7933 variables remain to probed next time 20%
c [decomp-44] removed 5 variables
c [treelook-7] removed 39 variables, found 4690 hbrs
c [unhide-18] limit 3747837 with penalty 0 = 0 + 0
c [unhide-18-25] 2 units, 161 failed, 15151 tauts, 0 hbrs, 38806 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 220 transitive binary clauses
c [cce-7] limit of 23423983 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 41
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 39
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 38
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 37
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 36
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 35
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 34
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 33
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 32
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 31
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 30
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 29
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 28
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 27
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 26
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 24
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 23
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 22
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 21
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 20
c [cce-7-1] eliminated 6 clauses out of 11 (55%) of length 19
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 18
c [cce-7-1] eliminated 7 clauses out of 11 (64%) of length 17
c [cce-7-1] eliminated 5 clauses out of 10 (50%) of length 16
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 15
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 14
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 13
c [cce-7-1] eliminated 4 clauses out of 9 (44%) of length 12
c [cce-7-1] eliminated 4 clauses out of 9 (44%) of length 11
c [cce-7-1] eliminated 6 clauses out of 13 (46%) of length 10
c [cce-7-1] eliminated 8 clauses out of 15 (53%) of length 9
c [cce-7-1] eliminated 14 clauses out of 25 (56%) of length 8
c [cce-7-1] eliminated 11 clauses out of 34 (32%) of length 7
c [cce-7-1] eliminated 16 clauses out of 1024 (2%) of length 6
c [cce-7-1] eliminated 8 clauses out of 7271 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 149 large clauses in 23423986 steps
c [cce-7-1] allowing another 11711993 steps for small clauses
c [cce-7-1] scheduling 176326 clauses = 123616 binary + 52710 ternary
c [cce-7-1] tried to eliminate 734 small clauses 0%
c [cce-7-1] eliminated 108 binary clauses 0%
c [cce-7-1] eliminated 63 ternary clauses 0%
c [cce-7-1] eliminated 171 small clauses 0%
c [cce-7-1] eliminated 482 small clauses in 23423986 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 631 covered clauses in round 1
c [cce-7] eliminated 631 covered clauses in TOTAL during 1 rounds
c [cce-7] 631 < 1/100 * 235457 = 2354 considered unsuccessful
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 40460 variables 100%
c [elim-17] limit of 374783731 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 365 variables 1% in round 1 in 19314650 steps
c [elim-17-1] backward subsumption/strengthening limit 19314600
c [elim-17-1-1] backward checking 2422 touched variables 6%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 25 and strengthened 5 clauses in 623702 steps
c [elim-17-1] rescheduled 76 variables 0% by backward subsumption
c [elim-17-2] eliminated 7 variables 0% in round 2 in 75529 steps
c [elim-17-2] backward subsumption/strengthening limit 75500
c [elim-17-2-1] backward checking 43 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 8 and strengthened 3 clauses in 69847 steps
c [elim-17-2] rescheduled 20 variables 0% by backward subsumption
c [elim-17-3] eliminated 4 variables 0% in round 3 in 34904 steps
c [elim-17-3] backward subsumption/strengthening limit 34900
c [elim-17-3-1] backward checking 16 touched variables 0%
c [elim-17-3-1] incomplete backward checking 16 remain 100%
c [elim-17-3] subsumed 6 and strengthened 6 clauses in 34921 steps
c [elim-17] incomplete 10 not tried 0% in round 3
c [gc-135] reconnected 207806 binary clauses (produced 0 empty 1 units)
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 380 = 1% variables out of 40460 scheduled
c [elim-17] 380 < 1/100 * 40460 = 404 considered unsuccessful
c [bca-14] limit of 10000000 steps and 468788 added (scaled 2)
c [bca-14] 49964 out of 80162 literals actually usable 62%
c [bca-14] added 14 blocked clauses in 130504 steps
c [sweep-10] limit 2810877 penalty 1 = 1 + 0
c [sweep-10-1] 4179 pos 11.0% + 33742 neg 89.0% = 37921 sched 94.6% ret 2159
c [sweep-10-1] 2816587 steps 44 queries 1510.66 avg class size
c [sweep-10-1] 501 decisions 39 SAT calls 94.33 avg env size
c [sweep-10-1] 37381 variables remain 93% (2662 retained 7%)
c [decomp-45] removed 80 variables
c [sweep-10-1] removed 80 vars (0 failed, 7 eqs, 11 impls)
c [sweep-10] removed 80 vars in TOTAL (1 rounds, 43 queries)
c [sort-queue-18] sorted 40000 enqueued variables after 54466 conflicts
c [score-dist-18] active 0 (0%), one 0 (0%), zero 40000 (100%)
c [score-dist-18] max exp 0, different 1 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 580 variables 1.4% (40000 remain 13%)
c [simplification-18] removed 3928 irredundant clauses 1.7% (233636 remain 17%)
c [simplification-18] maximum reduction of 2% = max (1%, 2%)
c [simplification-18] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-18] new conflict interval 22332
c [simplification-18] penalized conflict interval 22332 = 1 * 22332
c [simplification-18] hard conflict limit 87964 (soft 76798 + delta 11166)
c [simplification-18] new conflict limit 76798 (hard 87964)
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  168.1   39999   233636     54897   26946   6487 207483   12   412   43   3%     16  132   12    5  226%
c i  172.1   39998   233636     58249   29975   6640 207588   12   396   43   3%     32  109   12    6  212%
c i  174.5   39997   233636     60177   31748   6704 207644   12   382   43   3%     16   93   11    6  192%
c i  174.5   39996   233636     60204   31774   6704 207644   12   383   43   3%     16   94   13    6  219%
c i  175.0   39984   233636     60646   32173   6724 207655   12   380   43   3%      9   90   12    6  205%
c i  176.8   39981   233636     62067   33469   6785 207696   12   384   43   3%      8   92   13    6  208%
c i  177.1   39967   233636     62358   33725   6798 207708   12   392   43   3%      5  100   14    6  221%
c i  179.6   39966   233636     64423   35624   6884 207750   12   390   44   3%     13   95   13    6  211%
c i  180.0   39965   233636     64713   35890   6892 207758   12   386   44   3%      9   91   12    6  186%
c i  181.8   39963   233636     66119   37185   6940 207799   12   391   45   3%      7   93   12    7  188%
c i  185.5   39953   233636     69100   39943   7061 207865   13   382   47   3%     25   80   12    7  182%
c i  186.1   39913   233636     69632   40440   7076 207877   13   383   47   3%     14   80   13    7  187%
c i  187.8   39912   233636     70942   41652   7129 207902   13   388   47   3%      7   84   15    7  215%
c i  187.9   39910   233636     70971   41680   7129 207902   13   387   47   3%      7   83   15    7  211%
c i  191.1   39905   233636     73396   43916   7235 207946   14   392   47   4%     17   85   17    7  235%
c i  191.4   39904   233636     73574   44082   7241 207949   14   392   47   3%     13   84   15    7  200%
c i  193.5   39896   233636     75213   45609   7285 207983   14   394   50   4%      9   84   15    7  200%
c 
c [simplification-19] limit 76798 conflicts (hard 87964) hit after 76798 conflicts
c [quatres-15] found 21592 quaternary clauses 56% in total
c [quatres-15-1] removed 1 duplicate quaternary clauses
c [quatres-15-2] added 9 single-self-subsuming ternary resolvents
c [quatres-15-2] added 7 quaternary resolvents
c [ternres-15] limit 24873851 with penalty 0 = 0 + 0
c [ternres-15] all 39807 free variables schedulable
c [ternres-15] 567 ternary resolvents (3 bin, 564 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-8] limit 621846 penalty 3 = 3 + 0
c [gauss-8] extracted 57 xors of average arity 2.9
c [gauss-8] connected 165 occurrences of 154 variables (average 1.1)
c [gauss-8] limit 621846 penalty 3 = 3 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-46] removed 58 variables
c [basicprobe-7] limit 124369255 penalty 0 = 0 + 0
c [basicprobe-7-0] 4869 sched 13%, 708 failed, 31 lifted, 86991 hbrs
c [decomp-47] removed 2112 variables
c [basicprobe-7-1] 8381 probes remain 22% after last round
c [basicprobe-7-1] 814 units = 783 failed (96%) + 31 lifted (4%)
c [basicprobe-7-1] removed 2260 variables, found 101973 hbrs
c [bate-5] eliminated 376 asymmetric tautologies during probing
c [unhide-19] limit 4974770 with penalty 0 = 0 + 0
c [unhide-19-28] 0 units, 35 failed, 34315 tauts, 0 hbrs, 220902 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 274 transitive binary clauses
c [transred-15] found 1 units
c [bca-15] limit of 10000000 steps and 422785 added (scaled 2)
c [bca-15] 40446 out of 74850 literals actually usable 54%
c [bca-15] added 6 blocked clauses in 129679 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 74621550 penalty 0 = 0 + 0
c [sweep-11-1] 4149 pos 11.8% + 30948 neg 88.2% = 35097 sched 93.8% ret 2327
c [sweep-11-1] 74730088 steps 1365 queries 130.67 avg class size
c [sweep-11-1] 27116 decisions 1166 SAT calls 114.56 avg env size
c [sweep-11-1] 11539 variables remain 31% (25695 retained 69%)
c [decomp-48] removed 699 variables
c [sweep-11-1] removed 699 vars (0 failed, 214 eqs, 259 impls)
c [sweep-11] removed 699 vars in TOTAL (1 rounds, 1364 queries)
c [sort-queue-19] sorted 36725 enqueued variables after 76798 conflicts
c [score-dist-19] active 0 (0%), one 0 (0%), zero 36725 (100%)
c [score-dist-19] max exp 0, different 1 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 3082 variables 7.7% (36725 remain 12%)
c [simplification-19] removed 24565 irredundant clauses 10.5% (209071 remain 15%)
c [simplification-19] maximum reduction of 11% = max (8%, 11%)
c [simplification-19] large reduction 11% >= 5% limit
c [simplification-19] next conflict interval 2000 = 2000/1
c [simplification-19] penalized conflict interval 2000 = 1 * 2000
c [simplification-19] hard conflict limit 88798 (soft 78798 + delta 10000)
c [simplification-19] new conflict limit 78798 (hard 88798)
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  206.1   36724   209071     76966   47284   6763 266086   14   390   53   3%      9   79   12    8  153%
c i  206.4   36723   209071     77201   47505   6770 266092   13   387   53   3%      6   75   12    8  159%
c i  206.6   36722   209071     77324   47622   6772 266094   13   385   53   4%      5   73   12    8  163%
c 
c [simplification-20] limit 78798 conflicts (hard 88798) hit after 78798 conflicts
c [quatres-16] found 19762 quaternary clauses 53% in total
c [quatres-16-1] removed 4 duplicate quaternary clauses
c [quatres-16-2] added 2 single-self-subsuming ternary resolvents
c [ternres-16] limit 25398248 with penalty 0 = 0 + 0
c [ternres-16] all 36722 free variables schedulable
c [ternres-16] 350 ternary resolvents (3 bin, 347 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-49] removed 6 variables
c [simpleprobe-8] all 36719 free variables schedulable
c [simpleprobe-8] limit 101592994 penalty 0 = 0 + 0
c [decomp-50] removed 338 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 338 variables, found 55330 hbrs, 58 units
c [unhide-20] limit 5079649 with penalty 0 = 0 + 0
c [unhide-20-31] 0 units, 195 failed, 60032 tauts, 0 hbrs, 99868 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 410 transitive binary clauses
c [transred-16] found 2 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 36243 variables 100%
c [block-6] limit of 15873905 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 67 blocked clauses
c [block-6] 67 < 1/100 * 205254 = 2052 considered unsuccessful
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 36242 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 5079649740 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 1293 variables 4% in round 1 in 17376257 steps
c [elim-18-1] backward subsumption/strengthening limit 17376200
c [elim-18-1-1] backward checking 6295 touched variables 17%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 64 and strengthened 54 clauses in 1243714 steps
c [elim-18-1] rescheduled 379 variables 1% by backward subsumption
c [elim-18-2] eliminated 19 variables 0% in round 2 in 342503 steps
c [elim-18-2] backward subsumption/strengthening limit 342500
c [elim-18-2-1] backward checking 222 touched variables 1%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 18 and strengthened 19 clauses in 125068 steps
c [elim-18-2] rescheduled 74 variables 0% by backward subsumption
c [elim-18-3] no variable eliminated in round 3 in 71217 steps
c [elim-18] fully completed in 3 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 1312 = 4% variables out of 36242 scheduled
c [bca-16] limit of 10000000 steps and 406284 added (scaled 2)
c [bca-16] 36632 out of 69862 literals actually usable 52%
c [bca-16] added 4 blocked clauses in 119942 steps
c [sweep-12] limit 7619474 penalty 0 = 0 + 0
c [sweep-12-1] 1825 pos 16.9% + 8998 neg 83.1% = 10823 sched 31.0% ret 24107
c [sweep-12-1] 7637452 steps 169 queries 313.35 avg class size
c [sweep-12-1] 3520 decisions 147 SAT calls 105.76 avg env size
c [sweep-12-1] 9860 variables remain 28% (25060 retained 72%)
c [decomp-51] removed 48 variables
c [sweep-12-1] removed 48 vars (0 failed, 24 eqs, 30 impls)
c [sweep-12] removed 48 vars in TOTAL (1 rounds, 168 queries)
c [sort-queue-20] sorted 34882 enqueued variables after 78798 conflicts
c [score-dist-20] active 0 (0%), one 0 (0%), zero 34882 (100%)
c [score-dist-20] max exp 0, different 1 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 1840 variables 5.0% (34882 remain 11%)
c [simplification-20] removed 6442 irredundant clauses 3.1% (202629 remain 15%)
c [simplification-20] maximum reduction of 5% = max (5%, 3%)
c [simplification-20] large reduction 5% >= 5% limit
c [simplification-20] next conflict interval 2000 = 2000/1
c [simplification-20] penalized conflict interval 2000 = 1 * 2000
c [simplification-20] hard conflict limit 90798 (soft 80798 + delta 10000)
c [simplification-20] new conflict limit 80798 (hard 90798)
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  214.7   34881   202629     79748   45337   6569 249853   14   378   51   4%     16   64   14    8  172%
c 
c [simplification-21] limit 80798 conflicts (hard 90798) hit after 80798 conflicts
c [quatres-17] found 20372 quaternary clauses 54% in total
c [quatres-17-1] removed 2 duplicate quaternary clauses
c [quatres-17-2] added 1 single-self-subsuming ternary resolvents
c [quatres-17-2] added 11 quaternary resolvents
c [ternres-17] limit 25871919 with penalty 0 = 0 + 0
c [ternres-17] all 34881 free variables schedulable
c [ternres-17] 717 ternary resolvents (2 bin, 715 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 808497 penalty 4 = 4 + 0
c [card-6] found 1317 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 808497 for elimination
c [card-6] 1317 out of 1317 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-52] removed 1 variables
c [treelook-8] limit 2587191 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 42410 literals 61%
c [treelook-8] scheduling used 668387 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 2587191 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 2630798 steps
c [treelook-8] 42373 literals remain 61%
c [treelook-8] 5721 variables remain to probed next time 16%
c [treelook-8] removed 0 variables, found 14094 hbrs
c [unhide-21] limit 5174383 with penalty 0 = 0 + 0
c [unhide-21-34] 1 units, 155 failed, 17233 tauts, 0 hbrs, 72136 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 350 transitive binary clauses
c [transred-17] found 2 units
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 34838 variables 100%
c [elim-19] limit of 517438388 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 231 variables 1% in round 1 in 16882553 steps
c [elim-19-1] backward subsumption/strengthening limit 16882500
c [elim-19-1-1] backward checking 1571 touched variables 5%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 5 and strengthened 17 clauses in 361994 steps
c [elim-19-1] rescheduled 65 variables 0% by backward subsumption
c [elim-19-2] eliminated 1 variables 0% in round 2 in 32835 steps
c [elim-19-2] backward subsumption/strengthening limit 32800
c [elim-19-2-1] backward checking 17 touched variables 0%
c [elim-19-2-1] fully completed backward checking in 1 rounds
c [elim-19-2] subsumed 0 and strengthened 0 clauses in 32298 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 232 = 1% variables out of 34838 scheduled
c [elim-19] 232 < 1/100 * 34838 = 348 considered unsuccessful
c [bca-17] limit of 10000000 steps and 401568 added (scaled 2)
c [bca-17] 35964 out of 69214 literals actually usable 52%
c [bca-17] added 3 blocked clauses in 119336 steps
c [sweep-13] limit 7761575 penalty 0 = 0 + 0
c [sweep-13-1] 1671 pos 17.1% + 8125 neg 82.9% = 9796 sched 28.3% ret 24810
c [sweep-13-1] 7772844 steps 194 queries 337.57 avg class size
c [sweep-13-1] 3722 decisions 170 SAT calls 95.01 avg env size
c [sweep-13-1] 8926 variables remain 26% (25680 retained 74%)
c [decomp-54] removed 31 variables
c [sweep-13-1] removed 31 vars (0 failed, 24 eqs, 39 impls)
c [sweep-13] 31 < 1/1000 * 34606 = 34 considered unsuccessful
c [sweep-13] removed 31 vars in TOTAL (1 rounds, 193 queries)
c [sort-queue-21] sorted 34575 enqueued variables after 80798 conflicts
c [score-dist-21] active 0 (0%), one 0 (0%), zero 34575 (100%)
c [score-dist-21] max exp 0, different 1 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 306 variables 0.9% (34575 remain 11%)
c [simplification-21] removed 2248 irredundant clauses 1.1% (200381 remain 15%)
c [simplification-21] maximum reduction of 1% = max (1%, 1%)
c [simplification-21] geometric conflict interval increment 11166 = 22332 / 2
c [simplification-21] new conflict interval 33498
c [simplification-21] penalized conflict interval 33498 = 1 * 33498
c [simplification-21] hard conflict limit 131045 (soft 114296 + delta 16749)
c [simplification-21] new conflict limit 114296 (hard 131045)
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  224.5   34574   200381     84856   48939   7114 248597   13   346   50   4%     54   28   12    8  145%
c i  226.6   34573   200381     86704   50679   7171 248622   14   345   51   4%     15   27   15    8  174%
c i  227.6   34570   200381     87488   51417   7194 248630   14   350   51   4%      5   31   15    9  175%
c i  229.3   34561   200381     88901   52741   7232 248648   14   352   51   4%      3   33   14    9  157%
c i  229.3   34560   200381     88926   52762   7232 248648   14   352   51   4%      3   33   14    9  162%
c i  234.0   34559   200381     92801   56387   7339 248707   15   353   52   4%     34   32   14    9  159%
c i  234.4   34541   200381     93149   56713   7346 248715   15   349   52   4%     21   28   14    9  158%
c i  235.8   34530   200381     94379   57865   7388 248733   15   341   52   4%      6   19   13    9  143%
c i  236.7   34519   200381     95092   58534   7406 248745   15   345   52   4%      0   23   15    9  163%
c i  241.0   34473   200381     98465   61702   7502 248799   15   347   55   4%     25   24   15   10  161%
c -  244.8   34462   200381    101297   20702   7570 248841   16   342   37   5%     19   17   17   10  169%
c i  250.1   34461   200381    106745   25809   7754 248910   14   347   41   4%     96   21   14   10  136%
c 
c [simplification-22] limit 114296 conflicts (hard 131045) hit after 114297 conflicts
c [quatres-18] found 20972 quaternary clauses 53% in total
c [quatres-18-1] removed 1 duplicate quaternary clauses
c [quatres-18-2] added 12 single-self-subsuming ternary resolvents
c [quatres-18-2] added 6 quaternary resolvents
c [ternres-18] limit 33981358 with penalty 0 = 0 + 0
c [ternres-18] all 34459 free variables schedulable
c [ternres-18] 327 ternary resolvents (0 bin, 327 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-55] removed 141 variables
c [basicprobe-8] limit 169906792 penalty 0 = 0 + 0
c [basicprobe-8-0] 8304 sched 25%, 447 failed, 54 lifted, 63480 hbrs
c [decomp-56] removed 1277 variables
c [basicprobe-8-1] 7487 probes remain 23% after last round
c [basicprobe-8-1] 566 units = 509 failed (90%) + 57 lifted (10%)
c [basicprobe-8-1] removed 1405 variables, found 70715 hbrs
c [bate-6] eliminated 147 asymmetric tautologies during probing
c [unhide-22] limit 6796271 with penalty 0 = 0 + 0
c [unhide-22-38] 2 units, 37 failed, 43842 tauts, 0 hbrs, 197506 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 405 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 212383490 steps penalty 3 = 3 + 0
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 41
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 39
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 38
c [cce-8-1] eliminated 1 clauses out of 5 (20%) of length 37
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 36
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 28
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 27
c [cce-8-1] eliminated 2 clauses out of 7 (29%) of length 26
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 25
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 24
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 23
c [cce-8-1] eliminated 4 clauses out of 10 (40%) of length 22
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 21
c [cce-8-1] eliminated 6 clauses out of 9 (67%) of length 20
c [cce-8-1] eliminated 2 clauses out of 7 (29%) of length 19
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 18
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 17
c [cce-8-1] eliminated 3 clauses out of 10 (30%) of length 16
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 15
c [cce-8-1] eliminated 3 clauses out of 10 (30%) of length 14
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 13
c [cce-8-1] eliminated 4 clauses out of 10 (40%) of length 12
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 11
c [cce-8-1] eliminated 3 clauses out of 11 (27%) of length 10
c [cce-8-1] eliminated 2 clauses out of 8 (25%) of length 9
c [cce-8-1] eliminated 8 clauses out of 30 (27%) of length 8
c [cce-8-1] eliminated 6 clauses out of 36 (17%) of length 7
c [cce-8-1] eliminated 9 clauses out of 916 (1%) of length 6
c [cce-8-1] eliminated 316 clauses out of 6665 (5%) of length 5
c [cce-8-1] eliminated 5155 clauses out of 16636 (31%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 5567 large clauses in 165862989 steps
c [cce-8-1] allowing another 82931494 steps for small clauses
c [cce-8-1] scheduling 141192 clauses = 106260 binary + 34932 ternary
c [cce-8-1] tried to eliminate 13971 small clauses 10%
c [cce-8-1] eliminated 1971 binary clauses 2%
c [cce-8-1] eliminated 958 ternary clauses 3%
c [cce-8-1] eliminated 2929 small clauses 2%
c [cce-8-1] eliminated 2942 small clauses in 212383493 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 8509 covered clauses in round 1
c [cce-8] eliminated 8509 covered clauses in TOTAL during 1 rounds
c [bca-18] limit of 10000000 steps and 356682 added (scaled 2)
c [bca-18] 35691 out of 65936 literals actually usable 54%
c [bca-18] added 13 blocked clauses in 105888 steps
c [sort-queue-22] sorted 32967 enqueued variables after 114297 conflicts
c [score-dist-22] active 0 (0%), one 0 (0%), zero 32967 (100%)
c [score-dist-22] max exp 0, different 1 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 1492 variables 4.3% (32967 remain 11%)
c [simplification-22] removed 22401 irredundant clauses 11.2% (177980 remain 13%)
c [simplification-22] maximum reduction of 11% = max (4%, 11%)
c [simplification-22] large reduction 11% >= 5% limit
c [simplification-22] next conflict interval 2000 = 2000/1
c [simplification-22] penalized conflict interval 2000 = 1 * 2000
c [simplification-22] hard conflict limit 126297 (soft 116297 + delta 10000)
c [simplification-22] new conflict limit 116297 (hard 126297)
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  271.5   32966   177980    114855   32921   8407 264412   15   341   43   4%     88   13   15   11  139%
c 
c [simplification-23] limit 116297 conflicts (hard 126297) hit after 116297 conflicts
c [quatres-19] found 14669 quaternary clauses 45% in total
c [quatres-19-1] removed 3 duplicate quaternary clauses
c [quatres-19-2] added 2 single-self-subsuming ternary resolvents
c [quatres-19-2] added 3 quaternary resolvents
c [ternres-19] limit 34422055 with penalty 0 = 0 + 0
c [ternres-19] all 32964 free variables schedulable
c [ternres-19] 155 ternary resolvents (3 bin, 152 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-57] removed 115 variables
c [simpleprobe-9] all 32852 free variables schedulable
c [simpleprobe-9] limit 137688221 penalty 0 = 0 + 0
c [decomp-58] removed 98 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 98 variables, found 38083 hbrs, 20 units
c [unhide-23] limit 6884411 with penalty 0 = 0 + 0
c [unhide-23-42] 0 units, 15 failed, 47476 tauts, 0 hbrs, 78513 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 400 transitive binary clauses
c [transred-19] found 1 units
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 32734 variables 100%
c [elim-20] limit of 344220554 steps penalty 1 = 1 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 1300 variables 4% in round 1 in 13142033 steps
c [elim-20-1] backward subsumption/strengthening limit 13142000
c [elim-20-1-1] backward checking 6829 touched variables 21%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 33 and strengthened 110 clauses in 1271214 steps
c [elim-20-1] rescheduled 376 variables 1% by backward subsumption
c [elim-20-2] eliminated 25 variables 0% in round 2 in 783085 steps
c [elim-20-2] backward subsumption/strengthening limit 783000
c [elim-20-2-1] backward checking 285 touched variables 1%
c [elim-20-2-1] fully completed backward checking in 1 rounds
c [elim-20-2] subsumed 13 and strengthened 15 clauses in 129939 steps
c [elim-20-2] rescheduled 64 variables 0% by backward subsumption
c [elim-20-3] eliminated 4 variables 0% in round 3 in 63443 steps
c [elim-20-3] backward subsumption/strengthening limit 63400
c [elim-20-3-1] backward checking 41 touched variables 0%
c [elim-20-3-1] fully completed backward checking in 1 rounds
c [elim-20-3] subsumed 5 and strengthened 0 clauses in 54280 steps
c [elim-20] incomplete 11 not tried 0% in round 3
c [elim-20] transition to [ all 1 rem 1 ] state
c [elim-20] eliminated 1329 = 4% variables out of 32734 scheduled
c [bca-19] limit of 10000000 steps and 350142 added (scaled 2)
c [bca-19] 34032 out of 62812 literals actually usable 54%
c [bca-19] added 12 blocked clauses in 99846 steps
c [sweep-14] limit 5163308 penalty 1 = 1 + 0
c [sweep-14-1] 1430 pos 17.3% + 6818 neg 82.7% = 8248 sched 26.3% ret 23157
c [sweep-14-1] 5163910 steps 157 queries 541.28 avg class size
c [sweep-14-1] 2857 decisions 140 SAT calls 93.66 avg env size
c [sweep-14-1] 7536 variables remain 24% (23869 retained 76%)
c [decomp-59] removed 17 variables
c [sweep-14-1] removed 17 vars (0 failed, 16 eqs, 30 impls)
c [sweep-14] 17 < 1/1000 * 31405 = 31 considered unsuccessful
c [sweep-14] removed 17 vars in TOTAL (1 rounds, 156 queries)
c [sort-queue-23] sorted 31388 enqueued variables after 116297 conflicts
c [score-dist-23] active 0 (0%), one 0 (0%), zero 31388 (100%)
c [score-dist-23] max exp 0, different 1 (100%)
c [score-dist-23] median active exp 0, avg 0.0
c [simplification-23] removed 1576 variables 4.8% (31388 remain 10%)
c [simplification-23] removed 3293 irredundant clauses 1.9% (174687 remain 13%)
c [simplification-23] maximum reduction of 5% = max (5%, 2%)
c [simplification-23] large reduction 5% >= 5% limit
c [simplification-23] next conflict interval 2000 = 2000/1
c [simplification-23] penalized conflict interval 2000 = 1 * 2000
c [simplification-23] hard conflict limit 128297 (soft 118297 + delta 10000)
c [simplification-23] new conflict limit 118297 (hard 128297)
c 
c [simplification-24] limit 118297 conflicts (hard 128297) hit after 118297 conflicts
c [quatres-20] found 15193 quaternary clauses 46% in total
c [quatres-20-1] removed 3 duplicate quaternary clauses
c [quatres-20-2] added 1 single-self-subsuming ternary resolvents
c [quatres-20-2] added 23 quaternary resolvents
c [ternres-20] limit 34827463 with penalty 0 = 0 + 0
c [ternres-20] all 31388 free variables schedulable
c [ternres-20] 629 ternary resolvents (3 bin, 626 trn)
c [ternres-20] fully completed ternary resolution
c [gauss-9] limit 435343 penalty 4 = 4 + 0
c [gauss-9] extracted 30 xors of average arity 3.0
c [gauss-9] connected 90 occurrences of 78 variables (average 1.2)
c [gauss-9] limit 435343 penalty 4 = 4 + 0
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-24] limit 6965492 with penalty 0 = 0 + 0
c [unhide-24-47] 1 units, 171 failed, 25154 tauts, 0 hbrs, 57304 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 337 transitive binary clauses
c [cce-9] limit of 43534329 steps penalty 2 = 2 + 0
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 58
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 57
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 56
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 55
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 54
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 53
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 52
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 51
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 50
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 49
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 47
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 46
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 45
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 44
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 43
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 42
c [cce-9-1] eliminated 3 clauses out of 3 (100%) of length 41
c [cce-9-1] eliminated 3 clauses out of 4 (75%) of length 40
c [cce-9-1] eliminated 3 clauses out of 4 (75%) of length 39
c [cce-9-1] eliminated 3 clauses out of 4 (75%) of length 38
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 37
c [cce-9-1] eliminated 3 clauses out of 5 (60%) of length 36
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 35
c [cce-9-1] eliminated 5 clauses out of 9 (56%) of length 34
c [cce-9-1] eliminated 3 clauses out of 5 (60%) of length 33
c [cce-9-1] eliminated 4 clauses out of 7 (57%) of length 32
c [cce-9-1] eliminated 4 clauses out of 7 (57%) of length 31
c [cce-9-1] eliminated 6 clauses out of 9 (67%) of length 30
c [cce-9-1] eliminated 5 clauses out of 9 (56%) of length 29
c [cce-9-1] eliminated 6 clauses out of 8 (75%) of length 28
c [cce-9-1] eliminated 6 clauses out of 6 (100%) of length 27
c [cce-9-1] eliminated 3 clauses out of 10 (30%) of length 26
c [cce-9-1] eliminated 5 clauses out of 8 (62%) of length 25
c [cce-9-1] eliminated 5 clauses out of 11 (45%) of length 24
c [cce-9-1] eliminated 5 clauses out of 7 (71%) of length 23
c [cce-9-1] eliminated 4 clauses out of 10 (40%) of length 22
c [cce-9-1] eliminated 6 clauses out of 13 (46%) of length 21
c [cce-9-1] eliminated 5 clauses out of 9 (56%) of length 20
c [cce-9-1] eliminated 5 clauses out of 9 (56%) of length 19
c [cce-9-1] eliminated 4 clauses out of 8 (50%) of length 18
c [cce-9-1] eliminated 5 clauses out of 10 (50%) of length 17
c [cce-9-1] eliminated 4 clauses out of 11 (36%) of length 16
c [cce-9-1] eliminated 7 clauses out of 14 (50%) of length 15
c [cce-9-1] eliminated 4 clauses out of 16 (25%) of length 14
c [cce-9-1] eliminated 9 clauses out of 13 (69%) of length 13
c [cce-9-1] eliminated 4 clauses out of 10 (40%) of length 12
c [cce-9-1] eliminated 8 clauses out of 12 (67%) of length 11
c [cce-9-1] eliminated 5 clauses out of 15 (33%) of length 10
c [cce-9-1] eliminated 8 clauses out of 16 (50%) of length 9
c [cce-9-1] eliminated 7 clauses out of 39 (18%) of length 8
c [cce-9-1] eliminated 16 clauses out of 57 (28%) of length 7
c [cce-9-1] eliminated 14 clauses out of 980 (1%) of length 6
c [cce-9-1] eliminated 28 clauses out of 6420 (0%) of length 5
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 247 large clauses in 43534330 steps
c [cce-9-1] allowing another 21767165 steps for small clauses
c [cce-9-1] scheduling 133505 clauses = 100759 binary + 32746 ternary
c [cce-9-1] tried to eliminate 2388 small clauses 2%
c [cce-9-1] eliminated 392 binary clauses 0%
c [cce-9-1] eliminated 146 ternary clauses 0%
c [cce-9-1] eliminated 538 small clauses 0%
c [cce-9-1] eliminated 560 small clauses in 43534337 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 807 covered clauses in round 1
c [cce-9] eliminated 807 covered clauses in TOTAL during 1 rounds
c [cce-9] 807 < 1/100 * 173626 = 1736 considered unsuccessful
c [elim-21] no untried remaining variables left
c [elim-21] scheduled 31369 variables 100%
c [elim-21] limit of 696549264 steps penalty 0 = 0 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 209 variables 1% in round 1 in 12334715 steps
c [elim-21-1] backward subsumption/strengthening limit 12334700
c [elim-21-1-1] backward checking 1724 touched variables 5%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 15 and strengthened 10 clauses in 420125 steps
c [elim-21-1] rescheduled 59 variables 0% by backward subsumption
c [elim-21-2] eliminated 4 variables 0% in round 2 in 282705 steps
c [elim-21-2] backward subsumption/strengthening limit 282700
c [elim-21-2-1] backward checking 113 touched variables 0%
c [elim-21-2-1] fully completed backward checking in 1 rounds
c [elim-21-2] subsumed 5 and strengthened 0 clauses in 87475 steps
c [elim-21-2] rescheduled 8 variables 0% by backward subsumption
c [elim-21-3] eliminated 2 variables 0% in round 3 in 15473 steps
c [elim-21-3] backward subsumption/strengthening limit 15400
c [elim-21-3-1] backward checking 19 touched variables 0%
c [elim-21-3-1] incomplete backward checking 0 remain 0%
c [elim-21-3] subsumed 0 and strengthened 1 clauses in 15401 steps
c [elim-21] incomplete 4 not tried 0% in round 3
c [elim-21] transition to [ all 1 rem 1 ] state
c [elim-21] eliminated 215 = 1% variables out of 31369 scheduled
c [elim-21] 215 < 1/100 * 31369 = 313 considered unsuccessful
c [bca-20] limit of 10000000 steps and 345606 added (scaled 2)
c [bca-20] 33230 out of 62310 literals actually usable 53%
c [bca-20] added 23 blocked clauses in 99390 steps
c [sort-queue-24] sorted 31154 enqueued variables after 118297 conflicts
c [score-dist-24] active 0 (0%), one 0 (0%), zero 31154 (100%)
c [score-dist-24] max exp 0, different 1 (100%)
c [score-dist-24] median active exp 0, avg 0.0
c [simplification-24] removed 234 variables 0.7% (31154 remain 10%)
c [simplification-24] removed 2251 irredundant clauses 1.3% (172436 remain 13%)
c [simplification-24] maximum reduction of 1% = max (1%, 1%)
c [simplification-24] geometric conflict interval increment 16749 = 33498 / 2
c [simplification-24] new conflict interval 50247
c [simplification-24] penalized conflict interval 50247 = 1 * 50247
c [simplification-24] hard conflict limit 193667 (soft 168544 + delta 25123)
c [simplification-24] new conflict limit 168544 (hard 193667)
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  287.3   31153   172436    123102   34781   8394 201846   14   326   40   4%     85   -3   14   11  128%
c -  325.1   31148   172436    158248   28112   9084 202191   18   314   36   6%    398  -14   18   14  131%
c 
c [simplification-25] limit of 6880 ternary hit after 6894 ternaries
c [quatres-21] found 15857 quaternary clauses 43% in total
c [quatres-21-1] removed 2 duplicate quaternary clauses
c [quatres-21-2] added 10 single-self-subsuming ternary resolvents
c [quatres-21-2] added 2 quaternary resolvents
c [ternres-21] limit 45345853 with penalty 0 = 0 + 0
c [ternres-21] all 31148 free variables schedulable
c [ternres-21] 250 ternary resolvents (1 bin, 249 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-61] removed 17 variables
c [treelook-9] limit 2267292 penalty 1 = 1 + 0 boost 1
c [treelook-9] scheduled 36142 literals 58%
c [treelook-9] scheduling used 539425 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 2267292 penalty 1 = 1 + 0 boost 1
c [treelook-9] used 2312000 steps
c [treelook-9] 36027 literals remain 58%
c [treelook-9] 4589 variables remain to probed next time 15%
c [decomp-62] removed 3 variables
c [treelook-9] removed 10 variables, found 8895 hbrs
c [unhide-25] limit 9069170 with penalty 0 = 0 + 0
c [unhide-25-53] 1 units, 317 failed, 15131 tauts, 0 hbrs, 250104 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 278 transitive binary clauses
c [bca-21] limit of 10000000 steps and 343494 added (scaled 2)
c [bca-21] 31541 out of 62216 literals actually usable 51%
c [bca-21] added 9 blocked clauses in 102423 steps
c [sort-queue-25] sorted 31107 enqueued variables after 167882 conflicts
c [score-dist-25] active 0 (0%), one 0 (0%), zero 31107 (100%)
c [score-dist-25] max exp 0, different 1 (100%)
c [score-dist-25] median active exp 0, avg 0.0
c [simplification-25] removed 41 variables 0.1% (31107 remain 10%)
c [simplification-25] removed 1062 irredundant clauses 0.6% (171374 remain 12%)
c [simplification-25] maximum reduction of 1% = max (0%, 1%)
c [simplification-25] forced so keeping old conflict interval 50247
c [simplification-25] conflict limit remains at 168544 (hard 193667)
c [simplification-25] new ternary interval 10000
c 
c [simplification-26] limit 168544 conflicts (hard 193667) hit after 168544 conflicts
c [quatres-22] found 15737 quaternary clauses 43% in total
c [quatres-22-1] removed 4 duplicate quaternary clauses
c [quatres-22-2] added 1 single-self-subsuming ternary resolvents
c [quatres-22-2] added 2 quaternary resolvents
c [ternres-22] limit 45485446 with penalty 0 = 0 + 0
c [ternres-22] all 31107 free variables schedulable
c [ternres-22] 44 ternary resolvents (2 bin, 42 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-63] removed 16 variables
c [basicprobe-9] limit 227427233 penalty 0 = 0 + 0
c [basicprobe-9-0] 7688 sched 25%, 378 failed, 26 lifted, 37689 hbrs
c [decomp-64] removed 899 variables
c [basicprobe-9-1] 129 probes remain 0% after last round
c [basicprobe-9-1] 654 units = 596 failed (91%) + 58 lifted (9%)
c [basicprobe-9-1] removed 1266 variables, found 58204 hbrs
c [bate-7] eliminated 132 asymmetric tautologies during probing
c [unhide-26] limit 9097089 with penalty 0 = 0 + 0
c [unhide-26-59] 1 units, 24 failed, 33332 tauts, 0 hbrs, 77536 literals
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 340 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 29795 variables 100%
c [block-7] limit of 28428404 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 52 blocked clauses
c [block-7] 52 < 1/100 * 160027 = 1600 considered unsuccessful
c [elim-22] no untried remaining variables left
c [elim-22] scheduled 29795 variables 100%
c [elim-22] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-22] rescheduling of touched variables disabled
c [elim-22-1] eliminated 841 variables 3% in round 1 in 11301711 steps
c [elim-22-1] backward subsumption/strengthening limit 11301700
c [elim-22-1-1] backward checking 3574 touched variables 12%
c [elim-22-1-1] fully completed backward checking in 1 rounds
c [elim-22-1] subsumed 25 and strengthened 8 clauses in 645840 steps
c [elim-22-1] rescheduled 94 variables 0% by backward subsumption
c [elim-22-2] eliminated 3 variables 0% in round 2 in 96215 steps
c [elim-22-2] backward subsumption/strengthening limit 96200
c [elim-22-2-1] backward checking 36 touched variables 0%
c [elim-22-2-1] fully completed backward checking in 1 rounds
c [elim-22-2] subsumed 2 and strengthened 3 clauses in 32075 steps
c [elim-22-2] rescheduled 12 variables 0% by backward subsumption
c [elim-22-3] eliminated 1 variables 0% in round 3 in 9364 steps
c [elim-22-3] backward subsumption/strengthening limit 9300
c [elim-22-3-1] backward checking 9 touched variables 0%
c [elim-22-3-1] incomplete backward checking 0 remain 0%
c [elim-22-3] subsumed 0 and strengthened 0 clauses in 9301 steps
c [elim-22] fully completed in 3 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 845 = 3% variables out of 29795 scheduled
c [bca-22] limit of 10000000 steps and 318152 added (scaled 2)
c [bca-22] 27658 out of 57902 literals actually usable 48%
c [bca-22] added 10 blocked clauses in 93206 steps
c [sweep-15] limit 3411408 penalty 2 = 2 + 0
c [sweep-15-1] 1478 pos 20.1% + 5867 neg 79.9% = 7345 sched 25.4% ret 21605
c [sweep-15-1] 3413027 steps 119 queries 585.74 avg class size
c [sweep-15-1] 2203 decisions 112 SAT calls 75.59 avg env size
c [sweep-15-1] 6818 variables remain 24% (22132 retained 76%)
c [decomp-65] removed 9 variables
c [sweep-15-1] removed 9 vars (0 failed, 6 eqs, 11 impls)
c [sweep-15] 9 < 1/1000 * 28950 = 28 considered unsuccessful
c [sweep-15] removed 9 vars in TOTAL (1 rounds, 118 queries)
c [sort-queue-26] sorted 28941 enqueued variables after 168544 conflicts
c [score-dist-26] active 0 (0%), one 0 (0%), zero 28941 (100%)
c [score-dist-26] max exp 0, different 1 (100%)
c [score-dist-26] median active exp 0, avg 0.0
c [simplification-26] removed 2166 variables 7.0% (28941 remain 9%)
c [simplification-26] removed 12687 irredundant clauses 7.4% (158687 remain 12%)
c [simplification-26] maximum reduction of 7% = max (7%, 7%)
c [simplification-26] large reduction 7% >= 5% limit
c [simplification-26] next conflict interval 2000 = 2000/1
c [simplification-26] penalized conflict interval 2000 = 1 * 2000
c [simplification-26] hard conflict limit 180544 (soft 170544 + delta 10000)
c [simplification-26] new conflict limit 170544 (hard 180544)
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  357.0   28940   158687    179846   46601   8807 207329   17   291   45   6%    574  -30   19   15  134%
c 
c [simplification-27] limit 170544 conflicts (hard 180544) hit after 180544 conflicts
c [quatres-23] found 15713 quaternary clauses 43% in total
c [quatres-23-1] removed 1 duplicate quaternary clauses
c [quatres-23-2] added 4 single-self-subsuming ternary resolvents
c [quatres-23-2] added 5 quaternary resolvents
c [ternres-23] limit 47508671 with penalty 0 = 0 + 0
c [ternres-23] all 28938 free variables schedulable
c [ternres-23] 506 ternary resolvents (9 bin, 497 trn)
c [ternres-23] fully completed ternary resolution
c [decomp-66] removed 7 variables
c [simpleprobe-10] all 28934 free variables schedulable
c [simpleprobe-10] limit 190034687 penalty 0 = 0 + 0
c [decomp-67] removed 33 variables
c [simpleprobe-10] fully completed simple probing
c [simpleprobe-10] removed 33 variables, found 31110 hbrs, 13 units
c [unhide-27] limit 9501734 with penalty 0 = 0 + 0
c [unhide-27-65] 1 units, 7 failed, 37021 tauts, 0 hbrs, 321488 literals
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 398 transitive binary clauses
c [cce-10] limit of 29692919 steps penalty 3 = 3 + 0
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 43
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 42
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 39
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 38
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 37
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 36
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 25
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 24
c [cce-10-1] eliminated 2 clauses out of 8 (25%) of length 23
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 22
c [cce-10-1] eliminated 1 clauses out of 10 (10%) of length 21
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 20
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 19
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 18
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 17
c [cce-10-1] eliminated 2 clauses out of 976 (0%) of length 6
c [cce-10-1] incomplete large round (ATE)
c [cce-10-1] eliminated 22 large clauses in 29692923 steps
c [cce-10-1] allowing another 14846461 steps for small clauses
c [cce-10-1] scheduling 111672 clauses = 94583 binary + 17089 ternary
c [cce-10-1] tried to eliminate 2393 small clauses 2%
c [cce-10-1] eliminated 319 binary clauses 0%
c [cce-10-1] eliminated 114 ternary clauses 1%
c [cce-10-1] eliminated 433 small clauses 0%
c [cce-10-1] eliminated 443 small clauses in 29692924 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 465 covered clauses in round 1
c [cce-10] eliminated 465 covered clauses in TOTAL during 1 rounds
c [cce-10] 465 < 1/100 * 157575 = 1575 considered unsuccessful
c [elim-23] scheduling all variables this time
c [elim-23] scheduled 28880 variables 100%
c [elim-23] almost no limit of 100000000000 steps
c [elim-23] rescheduling of touched variables disabled
c [elim-23-1] eliminated 160 variables 1% in round 1 in 11005860 steps
c [elim-23-1] backward subsumption/strengthening limit 11005800
c [elim-23-1-1] backward checking 1186 touched variables 4%
c [elim-23-1-1] fully completed backward checking in 1 rounds
c [elim-23-1] subsumed 11 and strengthened 9 clauses in 272490 steps
c [elim-23-1] rescheduled 49 variables 0% by backward subsumption
c [elim-23-2] eliminated 2 variables 0% in round 2 in 26410 steps
c [elim-23-2] backward subsumption/strengthening limit 26400
c [elim-23-2-1] backward checking 23 touched variables 0%
c [elim-23-2-1] incomplete backward checking 0 remain 0%
c [elim-23-2] subsumed 0 and strengthened 1 clauses in 26401 steps
c [elim-23-2] rescheduled 5 variables 0% by backward subsumption
c [elim-23-3] no variable eliminated in round 3 in 3801 steps
c [elim-23] fully completed in 3 rounds
c [elim-23] transition to [ all 0 rem 0 ] state
c [elim-23] eliminated 162 = 1% variables out of 28880 scheduled
c [elim-23] 162 < 1/100 * 28880 = 288 considered unsuccessful
c [bca-23] limit of 10000000 steps and 314565 added (scaled 2)
c [bca-23] 25600 out of 57438 literals actually usable 45%
c [bca-23] added 7 blocked clauses in 99238 steps
c [sort-queue-27] sorted 28718 enqueued variables after 180544 conflicts
c [score-dist-27] active 0 (0%), one 0 (0%), zero 28718 (100%)
c [score-dist-27] max exp 0, different 1 (100%)
c [score-dist-27] median active exp 0, avg 0.0
c [simplification-27] removed 220 variables 0.8% (28718 remain 9%)
c [simplification-27] removed 1782 irredundant clauses 1.1% (156905 remain 11%)
c [simplification-27] maximum reduction of 1% = max (1%, 1%)
c [simplification-27] geometric conflict interval increment 25123 = 50247 / 2
c [simplification-27] new conflict interval 75370
c [simplification-27] penalized conflict interval 75370 = 1 * 75370
c [simplification-27] hard conflict limit 293599 (soft 255914 + delta 37685)
c [simplification-27] new conflict limit 255914 (hard 293599)
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  369.5   28717   156905    186244   51735   9112 200784   18   286   49   6%   -199  -32   15   15   98%
c i  374.8   28716   156905    191619   56908   9193 200825   19   292   51   6%   -198  -23   19   15  126%
c i  381.4   28705   156905    198230   63309   9286 200861   18   266   60   7%   -158  -48   18   16  116%
c -  391.2   28705   156905    207228   31008   9434 200919   19   302   35   6%    -98   -6   19   16  120%
c i  424.1   28704   156905    251084   73439   9957 201162   19   239   78   8%    449  -39   19   17  107%
c -  426.7   28701   156905    253384   35369   9986 201171   20   259   37   8%   -252  -18   20   17  117%
c 
c [simplification-28] limit 255914 conflicts (hard 293599) hit after 293600 conflicts
c [quatres-24] found 16824 quaternary clauses 39% in total
c [quatres-24-1] removed 3 duplicate quaternary clauses
c [quatres-24-2] added 8 single-self-subsuming ternary resolvents
c [quatres-24-2] added 7 quaternary resolvents
c [ternres-24] limit 66541176 with penalty 0 = 0 + 0
c [ternres-24] all 28701 free variables schedulable
c [ternres-24] 236 ternary resolvents (2 bin, 234 trn)
c [ternres-24] fully completed ternary resolution
c [card-7] limit 2079411 penalty 4 = 4 + 0
c [card-7] found 3846 at-most-one constraints of average size 3.9
c [card-7] no at-most-two constraint found
c [card-7] using previous limit 2079411 for elimination
c [card-7] 3846 out of 3846 constraints (100%) meet size limits
c [card-7] no units found
c [card-7] no at-most-one constraints generated
c [decomp-68] removed 25 variables
c [treelook-10] limit 6654117 penalty 0 = 0 + 0 boost 1
c [treelook-10] scheduled 31691 literals 55%
c [treelook-10] scheduling used 547779 steps
c [treelook-10] scheduled completely
c [treelook-10] limit 6654117 penalty 0 = 0 + 0 boost 1
c [treelook-10] used 6655550 steps
c [treelook-10] 31399 literals remain 55%
c [treelook-10] 3701 variables remain to probed next time 13%
c [decomp-69] removed 6 variables
c [treelook-10] removed 22 variables, found 27375 hbrs
c [unhide-28] limit 6654117 with penalty 1 = 0 + 1
c [unhide-28-68] 0 units, 0 failed, 20834 tauts, 0 hbrs, 1259431 literals
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 390 transitive binary clauses
c [bca-24] limit of 10000000 steps and 313477 added (scaled 2)
c [bca-24] 22294 out of 57344 literals actually usable 39%
c [bca-24] added 3 blocked clauses in 119990 steps
c [sort-queue-28] sorted 28671 enqueued variables after 293600 conflicts
c [score-dist-28] active 0 (0%), one 0 (0%), zero 28671 (100%)
c [score-dist-28] max exp 0, different 1 (100%)
c [score-dist-28] median active exp 0, avg 0.0
c [simplification-28] removed 30 variables 0.1% (28671 remain 9%)
c [simplification-28] removed 546 irredundant clauses 0.3% (156359 remain 11%)
c [simplification-28] maximum reduction of 0% = max (0%, 0%)
c [simplification-28] full geometric conflict interval increment 75370
c [simplification-28] new conflict interval 150740
c [simplification-28] penalized conflict interval 150740 = 1 * 150740
c [simplification-28] hard conflict limit 519710 (soft 444340 + delta 75370)
c [simplification-28] new conflict limit 444340 (hard 519710)
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 -  466.2   28671   156359    298038   35324  10545 207326   21   236   36   9%    334  -21   23   19  121%
c -  501.1   28671   156359    346086   38056  10914 207487   22   232   36   9%    692  -17   20   20  101%
c i  516.7   28670   156359    372100   63383  11098 207577   21   203   67  10%    801  -33   24   20  117%
c i  531.1   28669   156359    390879   81788  11196 207638   22   228   86  10%   -586   -3   19   21   91%
c -  533.6   28669   156359    393955   40972  11226 207650   23   218   37  10%   -782  -13   23   21  109%
c -  565.9   28669   156359    441303   43508  11505 207780   22   194   37  11%    140  -28   26   22  121%
c 
c [simplification-29] limit 444340 conflicts (hard 519710) hit after 445513 conflicts
c [quatres-25] found 17801 quaternary clauses 36% in total
c [quatres-25-1] removed 3 duplicate quaternary clauses
c [quatres-25-2] added 2 single-self-subsuming ternary resolvents
c [quatres-25-2] added 8 quaternary resolvents
c [ternres-25] limit 89429356 with penalty 0 = 0 + 0
c [ternres-25] all 28669 free variables schedulable
c [ternres-25] 181 ternary resolvents (0 bin, 181 trn)
c [ternres-25] fully completed ternary resolution
c [decomp-70] removed 12 variables
c [basicprobe-10] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-10-0] 513 sched 2%, 182 failed, 15 lifted, 4117 hbrs
c [decomp-71] removed 399 variables
c [basicprobe-10-1] 9256 sched 33%, 215 failed, 23 lifted, 23697 hbrs
c [decomp-72] removed 554 variables
c [basicprobe-10-2] 9085 sched 33%, 130 failed, 4 lifted, 10559 hbrs
c [decomp-73] removed 288 variables
c [basicprobe-10-3] 9062 sched 33%, 98 failed, 8 lifted, 6145 hbrs
c [decomp-74] removed 216 variables
c [basicprobe-10-4] 4556 probes remain 17% after last round
c [basicprobe-10-4] 716 units = 665 failed (93%) + 51 lifted (7%)
c [basicprobe-10-4] removed 1513 variables, found 46372 hbrs
c [bate-8] eliminated 147 asymmetric tautologies during probing
c [transred-25] limit 2000000 with penalty 0 = 0 + 0
c [transred-25] removed 552 transitive binary clauses
c [elim-24] scheduling all variables this time
c [elim-24] scheduled 27146 variables 100%
c [elim-24] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-24] rescheduling of touched variables disabled
c [elim-24-1] eliminated 493 variables 2% in round 1 in 10116884 steps
c [elim-24-1] backward subsumption/strengthening limit 10116800
c [elim-24-1-1] backward checking 2489 touched variables 9%
c [elim-24-1-1] fully completed backward checking in 1 rounds
c [elim-24-1] subsumed 37 and strengthened 30 clauses in 410630 steps
c [elim-24-1] rescheduled 172 variables 1% by backward subsumption
c [elim-24-2] eliminated 13 variables 0% in round 2 in 78188 steps
c [elim-24-2] backward subsumption/strengthening limit 78100
c [elim-24-2-1] backward checking 87 touched variables 0%
c [elim-24-2-1] fully completed backward checking in 1 rounds
c [elim-24-2] subsumed 4 and strengthened 9 clauses in 35071 steps
c [elim-24-2] rescheduled 27 variables 0% by backward subsumption
c [elim-24-3] eliminated 4 variables 0% in round 3 in 10448 steps
c [elim-24-3] backward subsumption/strengthening limit 10400
c [elim-24-3-1] backward checking 27 touched variables 0%
c [elim-24-3-1] incomplete backward checking 0 remain 0%
c [elim-24-3] subsumed 1 and strengthened 3 clauses in 10401 steps
c [elim-24] incomplete 9 not tried 0% in round 3
c [elim-24] transition to [ all 1 rem 1 ] state
c [elim-24] eliminated 510 = 2% variables out of 27146 scheduled
c [bca-25] limit of 10000000 steps and 290658 added (scaled 2)
c [bca-25] 21028 out of 53274 literals actually usable 39%
c [bca-25] added 5 blocked clauses in 90235 steps
c [sort-queue-29] sorted 26636 enqueued variables after 445513 conflicts
c [score-dist-29] active 0 (0%), one 0 (0%), zero 26636 (100%)
c [score-dist-29] max exp 0, different 1 (100%)
c [score-dist-29] median active exp 0, avg 0.0
c [simplification-29] removed 2033 variables 7.1% (26636 remain 9%)
c [simplification-29] removed 11410 irredundant clauses 7.3% (144949 remain 11%)
c [simplification-29] maximum reduction of 7% = max (7%, 7%)
c [simplification-29] large reduction 7% >= 5% limit
c [simplification-29] next conflict interval 4455 = min (445513/100, 150740)
c [simplification-29] penalized conflict interval 4455 = 1 * 4455
c [simplification-29] hard conflict limit 459968 (soft 449968 + delta 10000)
c [simplification-29] new conflict limit 449968 (hard 459968)
c 
c [simplification-30] limit 449968 conflicts (hard 459968) hit after 459968 conflicts
c [quatres-26] found 17449 quaternary clauses 36% in total
c [quatres-26-1] removed 1 duplicate quaternary clauses
c [quatres-26-2] added 2 single-self-subsuming ternary resolvents
c [quatres-26-2] added 3 quaternary resolvents
c [ternres-26] limit 91358900 with penalty 0 = 0 + 0
c [ternres-26] all 26636 free variables schedulable
c [ternres-26] 330 ternary resolvents (1 bin, 329 trn)
c [ternres-26] fully completed ternary resolution
c [gauss-10] limit 1141986 penalty 4 = 4 + 0
c [gauss-10] extracted 71 xors of average arity 3.0
c [gauss-10] connected 211 occurrences of 115 variables (average 1.8)
c [gauss-10] limit 1141986 penalty 4 = 4 + 0
c [gauss-10] fully completed
c [gauss-10] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-75] removed 2 variables
c [simpleprobe-11] all 26634 free variables schedulable
c [simpleprobe-11] limit 200000000 penalty 0 = 0 + 0
c [decomp-76] removed 22 variables
c [simpleprobe-11] fully completed simple probing
c [simpleprobe-11] removed 22 variables, found 28690 hbrs, 4 units
c [unhide-29] limit 9135890 with penalty 1 = 1 + 0
c [unhide-29-73] 3 units, 0 failed, 47250 tauts, 0 hbrs, 1348493 literals
c [transred-26] limit 2000000 with penalty 0 = 0 + 0
c [transred-26] removed 486 transitive binary clauses
c [elim-25] no untried remaining variables left
c [elim-25] scheduled 26609 variables 100%
c [elim-25] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-25] rescheduling of touched variables disabled
c [elim-25-1] eliminated 105 variables 0% in round 1 in 9923192 steps
c [elim-25-1] backward subsumption/strengthening limit 9923100
c [elim-25-1-1] backward checking 667 touched variables 3%
c [elim-25-1-1] fully completed backward checking in 1 rounds
c [elim-25-1] subsumed 1 and strengthened 0 clauses in 136934 steps
c [elim-25-1] rescheduled 3 variables 0% by backward subsumption
c [elim-25-2] no variable eliminated in round 2 in 1832 steps
c [elim-25] fully completed in 2 rounds
c [elim-25] transition to [ all 0 rem 0 ] state
c [elim-25] eliminated 105 = 0% variables out of 26609 scheduled
c [elim-25] 105 < 1/100 * 26609 = 266 considered unsuccessful
c [bca-26] limit of 10000000 steps and 288439 added (scaled 2)
c [bca-26] 19731 out of 53010 literals actually usable 37%
c [bca-26] added 4 blocked clauses in 100307 steps
c [sweep-16] limit 3425958 penalty 3 = 3 + 0
c [sweep-16-1] 1148 pos 17.4% + 5447 neg 82.6% = 6595 sched 24.9% ret 19909
c [sweep-16-1] 3472101 steps 77 queries 272.30 avg class size
c [sweep-16-1] 1914 decisions 73 SAT calls 168.85 avg env size
c [sweep-16-1] 6281 variables remain 24% (20222 retained 76%)
c [decomp-77] removed 6 variables
c [sweep-16-1] removed 6 vars (0 failed, 3 eqs, 5 impls)
c [sweep-16] 6 < 1/1000 * 26504 = 26 considered unsuccessful
c [sweep-16] removed 6 vars in TOTAL (1 rounds, 76 queries)
c [sort-queue-30] sorted 26498 enqueued variables after 459968 conflicts
c [score-dist-30] active 0 (0%), one 0 (0%), zero 26498 (100%)
c [score-dist-30] max exp 0, different 1 (100%)
c [score-dist-30] median active exp 0, avg 0.0
c [simplification-30] removed 138 variables 0.5% (26498 remain 8%)
c [simplification-30] removed 1124 irredundant clauses 0.8% (143825 remain 10%)
c [simplification-30] maximum reduction of 1% = max (1%, 1%)
c [simplification-30] geometric conflict interval increment 75370 = 150740 / 2
c [simplification-30] new conflict interval 226110
c [simplification-30] penalized conflict interval 226110 = 1 * 226110
c [simplification-30] hard conflict limit 799133 (soft 686078 + delta 113055)
c [simplification-30] new conflict limit 686078 (hard 799133)
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 -  619.5   26498   143825    490042   45018  11182 209092   24   204   37  12%    604    3   27   22  119%
c -  650.9   26498   143825    537482   47283  11408 209193   23   193   37  12%    820   -6   28   23  121%
c i  653.3   26497   143825    542082   51812  11426 209202   20   158   46  13%    834  -39   22   23   99%
c -  683.4   26497   143825    585192   48951  11632 209276   25   190   37  13%   -318   -7   26   23  112%
c -  717.1   26497   143825    633618   51161  11852 209366   22   173   37  13%    383  -19   20   24   85%
c -  751.7   26497   143825    682256   53298  12039 209458   25   203   38  12%    719   20   22   24   94%
c 
c [simplification-31] limit 686078 conflicts (hard 799133) hit after 688231 conflicts
c [quatres-27] found 18524 quaternary clauses 34% in total
c [quatres-27-1] removed 5 duplicate quaternary clauses
c [quatres-27-2] added 7 single-self-subsuming ternary resolvents
c [quatres-27-2] added 6 quaternary resolvents
c [ternres-27] limit 124368823 with penalty 0 = 0 + 0
c [ternres-27] all 26497 free variables schedulable
c [ternres-27] 220 ternary resolvents (2 bin, 218 trn)
c [ternres-27] fully completed ternary resolution
c [decomp-78] removed 7 variables
c [treelook-11] limit 12436882 penalty 0 = 0 + 0 boost 1
c [treelook-11] scheduled 28558 literals 54%
c [treelook-11] scheduling used 492653 steps
c [treelook-11] scheduled completely
c [treelook-11] limit 12436882 penalty 0 = 0 + 0 boost 1
c [treelook-11] used 12465731 steps
c [treelook-11] 27839 literals remain 53%
c [treelook-11] 2941 variables remain to probed next time 11%
c [decomp-79] removed 43 variables
c [treelook-11] removed 68 variables, found 67776 hbrs
c [unhide-30] limit 20000000 with penalty 0 = 0 + 0
c [unhide-30-84] 2 units, 24 failed, 64204 tauts, 0 hbrs, 914463 literals
c [transred-27] limit 2000000 with penalty 0 = 0 + 0
c [transred-27] removed 345 transitive binary clauses
c [transred-27] found 1 units
c [cce-11] limit of 38865257 steps penalty 4 = 4 + 0
c [cce-11-1] eliminated 2 clauses out of 9 (22%) of length 11
c [cce-11-1] eliminated 2 clauses out of 13 (15%) of length 10
c [cce-11-1] eliminated 2 clauses out of 17 (12%) of length 9
c [cce-11-1] eliminated 3 clauses out of 36 (8%) of length 8
c [cce-11-1] eliminated 4 clauses out of 43 (9%) of length 7
c [cce-11-1] eliminated 7 clauses out of 979 (1%) of length 6
c [cce-11-1] eliminated 82 clauses out of 6203 (1%) of length 5
c [cce-11-1] eliminated 2 clauses out of 10885 (0%) of length 4
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 104 large clauses in 38865258 steps
c [cce-11-1] allowing another 19432629 steps for small clauses
c [cce-11-1] scheduling 102622 clauses = 88525 binary + 14097 ternary
c [cce-11-1] tried to eliminate 4184 small clauses 4%
c [cce-11-1] eliminated 739 binary clauses 1%
c [cce-11-1] eliminated 189 ternary clauses 1%
c [cce-11-1] eliminated 928 small clauses 1%
c [cce-11-1] eliminated 992 small clauses in 38865258 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 1096 covered clauses in round 1
c [cce-11] eliminated 1096 covered clauses in TOTAL during 1 rounds
c [cce-11] 1096 < 1/100 * 142746 = 1427 considered unsuccessful
c [bca-27] limit of 10000000 steps and 284065 added (scaled 2)
c [bca-27] 19064 out of 52786 literals actually usable 36%
c [bca-27] added 5 blocked clauses in 97982 steps
c [sort-queue-31] sorted 26392 enqueued variables after 688231 conflicts
c [score-dist-31] active 0 (0%), one 0 (0%), zero 26392 (100%)
c [score-dist-31] max exp 0, different 1 (100%)
c [score-dist-31] median active exp 0, avg 0.0
c [simplification-31] removed 105 variables 0.4% (26392 remain 8%)
c [simplification-31] removed 2175 irredundant clauses 1.5% (141650 remain 10%)
c [simplification-31] maximum reduction of 2% = max (0%, 2%)
c [simplification-31] geometric conflict interval increment 75370 = 226110 / 3
c [simplification-31] new conflict interval 301480
c [simplification-31] penalized conflict interval 301480 = 1 * 301480
c [simplification-31] hard conflict limit 1140451 (soft 989711 + delta 150740)
c [simplification-31] new conflict limit 989711 (hard 1140451)
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 -  794.4   26392   141650    730705   54332  12476 211677   22   165   38  14%    878  -16   20   24   87%
c -  831.3   26392   141650    779551   55599  12647 211754   24   191   39  12%    955   20   24   23  107%
c -  869.4   26392   141650    829133   56520  12795 211831   25   173   39  14%    992   -4   25   23  108%
c i  881.3   26391   141650    846414   73522  12851 211866   24   186   68  13%    999   12   25   23  105%
c -  907.9   26388   141650    879897   58460  12955 211904   20   131   39  15%  -1889  -40   18   23   79%
c -  947.2   26388   141650    930755   59714  13102 211982   24   194   40  12%   -317   31   22   23   95%
c -  987.9   26388   141650    982283   61258  13254 212069   18   120   40  15%    413  -39   17   22   76%
c 
c [simplification-32] limit 989711 conflicts (hard 1140451) hit after 989711 conflicts
c [quatres-28] found 19409 quaternary clauses 32% in total
c [quatres-28-1] removed 27 duplicate quaternary clauses
c [quatres-28-2] added 8 single-self-subsuming ternary resolvents
c [quatres-28-2] added 13 quaternary resolvents
c [ternres-28] limit 171073436 with penalty 0 = 0 + 0
c [ternres-28] all 26388 free variables schedulable
c [ternres-28] 216 ternary resolvents (2 bin, 214 trn)
c [ternres-28] fully completed ternary resolution
c [decomp-80] removed 31 variables
c [basicprobe-11] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-11-0] 4656 sched 18%, 112 failed, 3 lifted, 10662 hbrs
c [decomp-81] removed 294 variables
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2325 basic ate = 2037 trn 88% + 288 lrg 12% in 8 updates
c bcas: 27 count, 535 added (495 skipped), 4560585 steps
c bkwd: tried 1012935 clauses, 2023252 lits, 2.00 lits/clause
c bkwd: checked 35473404 occs, 35.02 occs/clause, 17.53 occs/lit
c bkwd: subsumed 159 binary, 1342 ternary, 269 large
c bkwd: strengthened 34 binary, 4 ternary (100% self), 2038 large (0% self)
c blkd: 7 bces, 8330 removed, 7784907 resolutions, 21517367 steps
c blkd: 9030 blocking literals 1%, 11 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 7 count, 0 units, 0 am1, 73849582 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 79435 subsumed
c card: 21820 at-most-one constraints found, average size 4.61
c card: 21820 at-most-one constraints used 100%, average size 4.61
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: 11 cces, 35658 eliminated, 35453 ate 99%, 205 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: 4660063 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 252 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 81 decompositions, 15794 equivalent 5%
c deco: 350 decision-only clauses 0%, 61% reduction
c decs: 30756326 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 25 elims, 154702 eliminated 48%, 44 pure 0%
c elms: 83 rounds, 3.3 rounds/bve
c elms: 140107 small 91%, 14540 large 9%
c elms: 636069 tried small, 140107 succeeded 22%, 495962 failed 78%
c elms: 57540 subsumed, 77504 strengthened, 325 blocked
c elms: 29979562 copies, 26780850 resolutions, 28032172 ipos
c elms: 4748388 subchks, 3850511 strchks
c gaus: 10 extractions, 2231 extracted, 2.2 size, 3 max
c gaus: exported 1 units, 138 binary and 0 ternary equations
c gaus: 0 gc, 25678856 steps, 12839428 extr 50%, 179824 elim 1%
c glue: 20.6 orig avg, 20.6 real avg, 3.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1110129 = 335613 simple 30% + 706174 trn 64% + 68342 lrg 6%, 6155 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 989721 clauses, 215.5 length
c lrnd: 213324898 lits = 278541228 orig - 65216330 removed 23%
c lrnd: 674775 uips 68%, 91466 flips 9%
c mins: 969131 mins 98%, 6337 bin 1%, 13741 size 1%
c mins: 712021664 poisoned searches, 147652206 hits, 21% hit rate
c mins: 816973076 used twice searches, 6465445 hits, 1% hit rate
c move: moved 25500, 12127 bin 48%, 13373 trn 52%
c otfs: 1361 driving 23%, 4674 restarting 77%
c otfs: str 6035, 5845 red 97%, 190 irr 3%
c otfs: str 6035, 0 bin 0%, 206 trn 3%, 5829 lrg 97%
c otfs: sub 2, 2 red 100%, 0 irr 0%
c otfs: sub 2, 0 bin 0%, 2 trn 100%, 0 lrg 0%
c phas: 1 computed, 150170 set, 0 pos (0%), 150170 neg (100%)
c prbs: 11 basic, 171548 probed, 4124 failed, 229 lifted
c prbs: 11 simple, 1554764 probed, 1227 failed, 3853 eqs
c prbs: 11 treelook, 1329 probed, 40 failed, 0 lifted
c prom: 265011 locked 8% out of 3478299 tried
c prps: 2243894610 props, 69 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 28 count, 401 quat, 119 self1, 0 self2, 926 dup
c queu: 31 sorted, 30756326 next (0 steps 0.00)
c queu: 2018570 enq (2018538 steps 1.00), 0 deq 0%
c redc: 30734 clauses 32%, 95911 tried 10%, 230 sat 0%
c redc: 71484 lits 6%, 1197018 tried 0%, 231 sat 0%
c redc: 2489 times jump level reduced, 74.6 levels on average
c reds: 19 count, 52090.1 conflicts per reduce
c reds: 0 memlim 0%, 19 arith 100%
c reds: 542803 collected 64%, 307793 retired 36%
c rmbd: 62727 removed, 19013 red 30%
c rsts: 26655 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 32 count, 29 confs 91%, 0 vars 0%
c simp: 1 its 3%, 1 bin 3%, 1 trns 3%
c subl: 989721 count (1276220 tried 1.3), 11980 sub out of 969224 (1.2%)
c swps: 16 count, 16 rounds, 2482 queries (155.1/round)
c swps: 2143 sat calls, 51 unsat (0.6% success rate)
c swps: 44646 decisions 20.8, 1371 conflicts 0.6
c swps; 1408.0 avg class size, 101.8 avg environment size
c swps: 0 failed, 500 impls, 374 equivs
c swp0: 823 type 0 queries, 390 unsat (47.4%), 741 sat (90.0%)
c swp1: 1659 type 1 queries, 1136 unsat (68.5%), 1367 sat (82.4%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 61513758 calls to obtain time
c tops: 128319 fixed 40%, 493 its, 2007.53 confs/it
c trds: 27 transitive reductions, 7781 removed, 35 failed
c trds: 50820 nodes, 138001 edges, 53845329 steps
c trim: 521998 words, 2.0 MB
c trnr: 28 count, 95 bin, 18772 trn, 141051515 steps
c unhd: 30 count, 84 rounds, 172543362 steps
c unhd: 8709 non-trivial sccs of average size 2.4
c unhd: 232 units, 228 bin, 3 trn, 1 lrg
c unhd: 10120 failed, 10036 stamp, 0 lits, 40 bin, 23 trn, 1 lrg
c unhd: 680334 tauts, 12022 bin 2%, 24193 trn 4%, 1737 lrg 0%
c unhd: 680334 tauts, 642382 stamp 94%, 608021 red 89%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 5255373 str, 228 bin 0%, 14770 trn 0%, 5240375 lrg 100%, 5189306 red 99%
c vars: 25901 remaining 8% and 298815 removed 92% out of 324716
c vars: 128319 fixed 40%, 154702 eliminated 48%, 15794 equivalent 5%
c vsts: 18197205962 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 8.1 search visits per propagation, 17285.2 per conflict
c wchs: 4152356862 pushed, 101482429 enlarged, 393 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         969625        542803        307793     144444805      12065202        447928
c 
c  0 0         71080   7     17238   3         0   0  95487288  66   5725251  47    131746  29     1.7
c  1 5         32312   3     17859   3      6612   2  17239314  12<  1606269  13<    55467  12     0.7
c  2 6        104262  11     63570  12     24489   8  20766762  14   2525248  21    116313  26<    2.4
c  3 9        168279  17    104883  19     47612  15   8437658   6   1414581  12     88860  20     7.0
c  4 14       191150  20<   119407  22<    62360  20   1476519   1    401684   3     28479   6    14.4
c  5 21       175122  18    103104  19     65122  21<   559041   0    202590   2     13935   3    17.3
c  6 30       126402  13     69467  13     52309  17    314581   0    122763   1      8027   2    14.5
c  7 41        66152   7     32963   6     30743  10    109361   0     47058   0      3564   1    10.7
c  8 54        23982   2     10479   2     12517   4     35236   0     14196   0      1123   0     5.1
c  9 69         6972   1      2698   0      3880   1     13872   0      3891   0       263   0     1.3
c 10 86         2761   0       913   0      1481   0      3676   0      1271   0       115   0     0.4
c 11 126         730   0       191   0       400   0      1035   0       286   0        34   0     0.1
c 12 230         380   0        28   0       242   0       419   0       106   0         2   0     0.1
c 13 534          41   0         3   0        26   0        43   0         8   0         0   0     0.0
c 
c avg                  4.0           4.1           4.7           0.7           1.2           1.8
c std                  2.0           1.8           1.8           1.1           1.5           1.6
c 
c   53.409   5% probe
c   40.958   4% unhide
c   36.069   4% elim
c   22.293   2% cce
c   19.304   2% decide
c    9.006   1% sweep
c    3.286   0% bca
c 
c   11.012 < 1% rest (below)
c 
c    3.158   0% transred
c    2.763   0% gauss
c    2.268   0% block
c    1.200   0% ternres
c    1.196   0% quatres
c    0.427   0% card
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    6.462   1% preprocessing     3%
c  180.856  18% inprocessing     97%
c ==================================
c  187.318  19% simplifying
c  811.903  81% search
c ==================================
c  999.226 100% all
c 
c        989711 conflicts,         990.5 confs/sec
c         11546 ternaries,          85.7 confs/ternary
c          8152 binaries,          121.4 confs/binary
c           493 iterations,       2007.5 confs/iteration
c 
c            19 reductions,          0.0 redus/sec,  52090.1 confs/reduction
c         26655 restarts,           26.7 rests/sec,     37.1 confs/restart
c      30756326 decisions,       30780.2 decis/sec,     31.1 decis/conflict
c    2243894610 propagations,  2245633.0 props/sec,     73.0 props/decision
c 
c 999.2 seconds, 132.9 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
