c launch: /data/cnf/sc2014/app/UR-20-5p0.cnf.bz2
c host: atom08
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/UR-20-5p0.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UR-20-5p0.cnf.bz2
c no embedded options
c found 'p cnf 224569 1190619' header
c read 224569 variables, 1190619 clauses, 2868508 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 --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 213166 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 
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  213166  1178466         0       0      0     0    0     0   53   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 5764 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] 5764 out of 5764 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 51698 variables
c [simpleprobe-1] all 172871 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 126 variables
c [simpleprobe-1] 9560 variables remain 6% (163185 retained 94%)
c [simpleprobe-1] removed 126 variables, found 14869 hbrs, 1 units
c [unhide-1] limit 57112 based on 913796 irredundant clauses
c [unhide-1-1] 0 units, 811 failed, 6035 tauts, 0 hbrs, 9748 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 172047 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 47852 not tried 28% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 66092 = 38% variables out of 172047 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 763627 negative 99.2% of 769527 except 5900 0.8%
c [phase-count-1] 618351 positive 80.4% of 769527 except 151176 19.6%
c [phase-count-1] less non-negative clauses 5900 than limit 76900 (10.0%)
c [phase-count-1] non-pos/non-neg = 151176/5900 = 25.62 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 105955 negative 100%
c [sort-queue-1] sorted 105955 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 105955 (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 71771 variables 40.4% (105955 remain 50%)
c [simplification-1] removed 408939 irredundant clauses 34.7% (769527 remain 65%)
c [simplification-1] maximum reduction of 40% = max (40%, 35%)
c [simplification-1] large reduction 40% >= 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    4.6  105954   769527        77      68      2 11960    0    12   51   1%      0   12    2    0 21468%
c i    4.7  105222   769527        85      74      3 11960    0    12   51   1%      0   12    2    0 21182%
c i    4.7  104292   769527        89      75      4 11961    0    12   51   1%      0   12    2    0 20894%
c i    4.7  104280   769527        99      81      4 11964    0    15   51   1%      0   15    2    0 20283%
c i    4.7  102685   769527       100      81      4 11964    0    15   51   1%      0   15    2    0 20204%
c i    4.7  102674   769527       102      81      5 11964    0    15   51   1%      0   15    2    0 20063%
c i    4.7  102660   769527       104      82      5 11964    0    15   51   1%      0   15    2    0 19946%
c i    4.7  102571   769527       105      82      5 11964    0    15   51   1%      0   15    2    0 19868%
c i    4.7  101751   769527       107      82      5 11965    0    15   51   1%      0   15    2    0 19722%
c i    4.8  101552   769527       140     106     11 11967    0    16   51   1%      0   16    3    0 18886%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 6022 variables
c [simpleprobe-2] 8965 schedulable variables 9%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 9627 variables remain 10% (90306 retained 90%)
c [simpleprobe-2] removed 0 variables, found 1601 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 73779 literals 37%
c [treelook-1] scheduling used 559969 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 333162 steps
c [treelook-1] 73768 literals remain 37%
c [treelook-1] 73131 variables remain to probed next time 73%
c [treelook-1] removed 4 variables, found 1891 hbrs
c [basicprobe-1] limit 5775728 based on 721966 irredundant clauses
c [basicprobe-1-0] 32312 probes remain 36% after last round
c [basicprobe-1-0] 40 units = 40 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 10217 variables, found 21924 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 11 units, 1640 failed, 7870 tauts, 0 hbrs, 1026 literals
c [elim-2] 42560 variables 49% will be scheduled this time
c [elim-2] scheduled 42560 variables 49%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 13158 not tried 15% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 309 = 1% variables out of 42560 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 598695 negative 99.0% of 604625 except 5930 1.0%
c [phase-count-2] 483276 positive 79.9% of 604625 except 121349 20.1%
c [phase-count-2] less non-negative clauses 5930 than limit 60400 (10.0%)
c [phase-count-2] non-pos/non-neg = 121349/5930 = 20.46 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 13401 negative 100%
c [sort-queue-2] sorted 86317 enqueued variables after 140 conflicts
c [score-dist-2] active 0 (0%), one 5533 (6%), zero 80784 (94%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 13884 variables 13.9% (86317 remain 40%)
c [simplification-2] removed 164902 irredundant clauses 21.4% (604625 remain 51%)
c [simplification-2] maximum reduction of 21% = max (14%, 21%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1039 (hard 11000)
c [simplification-2] 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    7.5   86316   604625       150     109     13 21434    0    17   41   2%      0   16    3    0 19678%
c i    7.5   86147   604625       162     117     15 21435    0    17   41   2%      0   17    4    0 19316%
c i    7.5   85795   604625       176     123     15 21442    0    17   41   2%      0   17    4    0 18572%
c i    7.5   85788   604625       188     131     16 21444    0    17   41   2%      0   17    4    0 17939%
c i    7.7   85777   604625       470     359     33 21474    1    21   41   4%      1   21    6    0 11428%
c i    7.8   85770   604625       737     543     58 21525    1    23   41   5%      1   23    5    0 7454%
c i    7.8   85765   604625       744     547     58 21527    1    24   41   5%      1   23    5    0 7363%
c 
c [simplification-3] limit of 113 binary hit after 113 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3823 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] 3823 out of 3823 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1036 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 52530 literals 31%
c [treelook-2] scheduling used 301551 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 314015 steps
c [treelook-2] 52520 literals remain 31%
c [treelook-2] 41453 variables remain to probed next time 49%
c [treelook-2] removed 3 variables, found 1542 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 659 failed, 13907 tauts, 0 hbrs, 300 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 84589 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 17954 not tried 21% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2223 = 3% variables out of 84589 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 570589 negative 99.0% of 576426 except 5837 1.0%
c [phase-count-3] 459920 positive 79.8% of 576426 except 116506 20.2%
c [phase-count-3] less non-negative clauses 5837 than limit 57600 (10.0%)
c [phase-count-3] non-pos/non-neg = 116506/5837 = 19.96 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 11397 negative 100%
c [sort-queue-3] sorted 82366 enqueued variables after 791 conflicts
c [score-dist-3] active 0 (0%), one 11962 (15%), zero 70404 (85%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 3397 variables 4.0% (82366 remain 39%)
c [simplification-3] removed 28199 irredundant clauses 4.7% (576426 remain 49%)
c [simplification-3] maximum reduction of 5% = max (4%, 5%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 1041 (hard 11000)
c [simplification-3] 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   10.1   82365   576426       816     586     65 19951    1    24   40   5%      1   24    5    0 6608%
c i   10.1   82355   576426       894     642     69 19965    1    26   40   5%      1   26    6    0 6504%
c i   10.2   82346   576426       981     698     80 19982    1    27   40   5%      1   26    6    0 6071%
c i   10.2   82295   576426      1012     724     83 19983    1    27   40   5%      1   27    6    0 6078%
c 
c [simplification-4] limit 1041 conflicts (hard 11000) hit after 1042 conflicts
c [decomp-8] removed 81 variables
c [basicprobe-2] limit 4607656 based on 575957 irredundant clauses
c [basicprobe-2-0] 28028 probes remain 36% after last round
c [basicprobe-2-0] 51 units = 51 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 4676 variables, found 16717 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 3 units, 936 failed, 5864 tauts, 0 hbrs, 970 literals
c [elim-4] 12620 variables 16% will be scheduled this time
c [elim-4] scheduled 12620 variables 16%
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 4 variables 0% in round 1 in 26435416 steps
c [elim-4-1] backward subsumption/strengthening limit 26435400
c [elim-4-1-1] backward checking 100 touched variables 0%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 103295 steps
c [elim-4-1] fully rescheduled 76719 variables 100%
c [elim-4-2] eliminated 1254 variables 2% in round 2 in 49319980 steps
c [elim-4-2] backward subsumption/strengthening limit 49319900
c [elim-4-2-1] backward checking 4444 touched variables 6%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 1 and strengthened 21 clauses in 1299075 steps
c [elim-4-2] rescheduled 61 variables 0% by backward subsumption
c [elim-4-3] eliminated 2 variables 0% in round 3 in 41769 steps
c [elim-4-3] backward subsumption/strengthening limit 41700
c [elim-4-3-1] backward checking 33 touched variables 0%
c [elim-4-3-1] incomplete backward checking 0 remain 0%
c [elim-4-3] subsumed 0 and strengthened 0 clauses in 41701 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 1266 = 10% variables out of 12620 scheduled
c [phase-count-4] 520770 negative 98.9% of 526472 except 5702 1.1%
c [phase-count-4] 419199 positive 79.6% of 526472 except 107273 20.4%
c [phase-count-4] less non-negative clauses 5702 than limit 52600 (10.0%)
c [phase-count-4] non-pos/non-neg = 107273/5702 = 18.81 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 10980 negative 100%
c [sort-queue-4] sorted 75457 enqueued variables after 1042 conflicts
c [score-dist-4] active 0 (0%), one 12949 (17%), zero 62508 (83%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 6831 variables 8.3% (75457 remain 35%)
c [simplification-4] removed 49954 irredundant clauses 8.7% (526472 remain 45%)
c [simplification-4] maximum reduction of 9% = max (8%, 9%)
c [simplification-4] large reduction 9% >= 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 13042 (soft 3042 + delta 10000)
c [simplification-4] new conflict limit 3042 (hard 13042)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   13.0   75456   526472      1096     722     88 25722    2    29   37   6%      1   29    8    0 6979%
c i   13.0   75453   526472      1110     725     90 25725    2    29   37   6%      1   29    8    0 6699%
c i   13.0   75449   526472      1112     725     90 25726    2    29   37   6%      1   29    8    0 6649%
c i   13.0   75363   526472      1113     725     90 25726    2    29   37   6%      1   29    8    0 6623%
c i   13.0   75362   526472      1155     754     98 25730    2    30   37   6%      1   29    7    0 6229%
c i   13.0   75361   526472      1213     802    101 25734    2    31   37   6%      1   31    7    0 5893%
c i   13.1   75336   526472      1238     819    103 25739    2    31   37   6%      1   31    7    0 5586%
c i   13.1   75335   526472      1246     824    105 25739    2    31   37   6%      1   31    7    0 5460%
c i   13.1   75321   526472      1260     833    105 25743    2    31   37   6%      1   31    7    0 5310%
c i   13.1   75319   526472      1284     849    112 25743    2    32   37   6%      1   31    7    0 5054%
c i   13.2   75315   526472      1544    1070    130 25758    2    36   37   6%      1   36    9    0 5408%
c i   13.2   75314   526472      1609    1132    131 25759    3    37   37   7%      1   36   11    0 5918%
c i   13.3   75238   526472      1684    1190    137 25768    3    38   37   8%      1   37   15    0 6911%
c i   13.3   75232   526472      1757    1250    141 25774    3    39   37   8%      1   39   13    0 5945%
c i   13.4   75228   526472      2008    1445    158 25807    4    46   38   8%      1   45   11    0 4019%
c i   13.5   75224   526472      2034    1462    161 25812    4    46   38   8%      1   45   10    0 3831%
c i   13.5   75216   526472      2117    1520    169 25827    4    49   38   7%      1   48    9    0 3358%
c i   13.6   75197   526472      2251    1627    176 25844    4    51   38   8%      1   50   10    0 3382%
c i   13.6   75188   526472      2267    1642    176 25844    4    51   38   8%      1   50   11    0 3763%
c i   13.6   75187   526472      2272    1644    177 25845    4    51   38   8%      1   50   12    0 3760%
c i   13.7   75177   526472      2367    1718    185 25855    4    52   38   8%      1   51   12    0 3565%
c i   13.8   75175   526472      2655    1957    202 25880    5    56   38   8%      1   54   11    0 2850%
c i   13.8   75174   526472      2740    2020    209 25890    5    56   38   8%      1   54    9    0 2517%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   13.9   75173   526472      2841    2106    214 25896    5    57   38   9%      1   55   11    0 2769%
c i   13.9   75172   526472      2867    2122    217 25900    5    57   38   9%      1   56   11    0 2668%
c i   13.9   75063   526472      2930    2173    222 25904    5    57   38   9%      1   56   10    0 2486%
c i   13.9   75057   526472      2992    2221    226 25911    5    58   38   9%      1   57   10    0 2443%
c 
c [simplification-5] limit 3060 conflicts (hard 13042) hit after 3060 conflicts
c [quatres-1] found 36906 quaternary clauses 45% in total
c [quatres-1-2] added 2 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 75009 free variables schedulable
c [ternres-1] 50 ternary resolvents (0 bin, 50 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 102 xors of average arity 2.4
c [gauss-1] connected 244 occurrences of 207 variables (average 1.2)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 76 variables
c [gauss-1] exported 2 unary, 0 binary and 0 ternary equations
c [unhide-5] limit 112402 with penalty 0 = 0 + 0
c [unhide-5-5] 14 units, 290 failed, 13388 tauts, 0 hbrs, 2256 literals
c [transred-1] limit 562014 with penalty 0 = 0 + 0
c [transred-1] removed 90 transitive binary clauses
c [transred-1] found 5 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 74556 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 7211 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 5 clauses out of 148 (3%) of length 10
c [cce-1-1] eliminated 38 clauses out of 742 (5%) of length 9
c [cce-1-1] eliminated 51 clauses out of 528 (10%) of length 8
c [cce-1-1] eliminated 73 clauses out of 837 (9%) of length 7
c [cce-1-1] eliminated 3260 clauses out of 4547 (72%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 3427 large clauses in 30000007 steps
c [cce-1-1] allowing another 15000003 steps for small clauses
c [cce-1-1] scheduling 401022 clauses = 236957 binary + 164065 ternary
c [cce-1-1] tried to eliminate 353 small clauses 0%
c [cce-1-1] eliminated 86 binary clauses 0%
c [cce-1-1] eliminated 27 ternary clauses 0%
c [cce-1-1] eliminated 113 small clauses 0%
c [cce-1-1] eliminated 113 small clauses in 30000009 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3540 covered clauses in round 1
c [cce-1] eliminated 3540 covered clauses in TOTAL during 1 rounds
c [cce-1] 3540 < 1/100 * 499493 = 4994 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 74556 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 12299 not tried 16% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 568 = 1% variables out of 74556 scheduled
c [elim-5] 568 < 1/100 * 74556 = 745 considered unsuccessful
c [bca-1] limit of 10000000 steps and 986812 added (scaled 2)
c [bca-1] 139496 out of 147978 literals actually usable 94%
c [bca-1] added 1686 blocked clauses in 438197 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 4403 pos 6.0% + 69585 neg 94.0% = 73988 sched 100.0% ret 0
c [sweep-1-1] 1118365 steps 14 queries 22504.86 avg class size
c [sweep-1-1] 144 decisions 13 SAT calls 58.15 avg env size
c [sweep-1-1] 73844 variables remain 100% (37 retained 0%)
c [decomp-11] removed 112 variables
c [sweep-1-1] removed 112 vars (0 failed, 0 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 112 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-5] 490218 negative 99.5% of 492749 except 2531 0.5%
c [phase-count-5] 397030 positive 80.6% of 492749 except 95719 19.4%
c [phase-count-5] less non-negative clauses 2531 than limit 49200 (10.0%)
c [phase-count-5] non-pos/non-neg = 95719/2531 = 37.82 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 10652 negative 100%
c [sort-queue-5] sorted 73876 enqueued variables after 3060 conflicts
c [score-dist-5] active 0 (0%), one 15344 (21%), zero 58532 (79%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 1133 variables 1.5% (73876 remain 35%)
c [simplification-5] removed 33723 irredundant clauses 6.4% (492749 remain 42%)
c [simplification-5] maximum reduction of 6% = max (2%, 6%)
c [simplification-5] large reduction 6% >= 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 15060 (soft 5060 + delta 10000)
c [simplification-5] new conflict limit 5060 (hard 15060)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   18.1   73875   492749      3149    1959    302 35501    5    60   37   9%      1   58   11    0 2411%
c i   18.1   73874   492749      3167    1975    303 35501    5    60   37   9%      1   58   12    0 2635%
c i   18.2   73872   492749      3276    2069    307 35509    6    62   37   9%      1   60   13    0 2715%
c i   18.4   73867   492749      3595    2326    337 35536    6    67   37   9%      1   64    9    1 1754%
c i   18.4   73813   492749      3650    2364    342 35545    6    67   37   9%      1   65    9    1 1731%
c i   18.4   73666   492749      3656    2369    342 35545    6    67   37   9%      1   65    9    1 1704%
c i   18.4   73662   492749      3667    2377    344 35545    6    67   37   9%      1   65    9    1 1654%
c i   18.5   73611   492749      3801    2483    351 35557    6    68   37   9%      1   65   13    1 2313%
c i   18.5   73607   492749      3899    2560    357 35570    6    67   37   9%      1   65   11    1 1899%
c i   18.5   73598   492749      3905    2563    357 35572    6    67   37   9%      1   65   11    1 1864%
c i   18.6   73589   492749      3927    2580    358 35574    6    68   37   9%      1   66   10    1 1766%
c i   18.6   73585   492749      4001    2644    362 35578    6    69   37   9%      1   66   10    1 1679%
c i   18.7   73571   492749      4043    2674    366 35584    6    69   37   9%      1   66    9    1 1583%
c i   18.7   73563   492749      4047    2674    368 35585    6    69   37   9%      1   66    9    1 1562%
c i   19.0   73554   492749      4522    3065    409 35615    7    75   37   9%      2   72   10    1 1483%
c i   19.1   73549   492749      4739    3246    424 35626    7    76   37  10%      2   72   15    1 2068%
c i   19.3   73540   492749      4960    3431    441 35644    8    78   37  10%      2   75   14    1 1877%
c i   19.3   73496   492749      4977    3438    446 35648    8    78   37  10%      2   75   13    1 1778%
c i   19.3   73488   492749      4995    3449    448 35652    8    78   37  10%      2   75   13    1 1695%
c 
c [simplification-6] limit 5064 conflicts (hard 15060) hit after 5065 conflicts
c [quatres-2] found 37322 quaternary clauses 48% in total
c [quatres-2-2] added 3 single-self-subsuming ternary resolvents
c [quatres-2-2] added 5 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 73488 free variables schedulable
c [ternres-2] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-2] 45196 variables remain 62% (28292 retained 38%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2109 at-most-one constraints of average size 4.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2109 out of 2109 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 55 xors of average arity 2.8
c [gauss-2] connected 153 occurrences of 80 variables (average 1.9)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 14 variables
c [simpleprobe-3] 7237 schedulable variables 10%
c [simpleprobe-3] limit 1946368 penalty 1 = 1 + 0
c [decomp-13] removed 10 variables
c [simpleprobe-3] 8272 variables remain 11% (65192 retained 89%)
c [simpleprobe-3] removed 10 variables, found 2424 hbrs, 2 units
c [unhide-6] limit 194636 with penalty 0 = 0 + 0
c [unhide-6-6] 1 units, 503 failed, 3354 tauts, 0 hbrs, 3570 literals
c [transred-2] limit 973184 with penalty 0 = 0 + 0
c [transred-2] removed 134 transitive binary clauses
c [transred-2] found 2 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 72837 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 61 blocked clauses
c [block-2] 61 < 1/100 * 490475 = 4904 considered unsuccessful
c [bca-2] limit of 10000000 steps and 970301 added (scaled 2)
c [bca-2] 133084 out of 145676 literals actually usable 91%
c [bca-2] added 97 blocked clauses in 409576 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4789 pos 6.6% + 68011 neg 93.4% = 72800 sched 99.9% ret 37
c [sweep-2-1] 1021648 steps 18 queries 18540.72 avg class size
c [sweep-2-1] 134 decisions 13 SAT calls 73.62 avg env size
c [sweep-2-1] 72760 variables remain 100% (77 retained 0%)
c [decomp-14] removed 11 variables
c [sweep-2-1] removed 11 vars (0 failed, 4 eqs, 8 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 11 vars in TOTAL (1 rounds, 17 queries)
c [phase-count-6] 481922 negative 99.5% of 484458 except 2536 0.5%
c [phase-count-6] 389843 positive 80.5% of 484458 except 94615 19.5%
c [phase-count-6] less non-negative clauses 2536 than limit 48400 (10.0%)
c [phase-count-6] non-pos/non-neg = 94615/2536 = 37.31 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 3022 negative 100%
c [sort-queue-6] sorted 72826 enqueued variables after 5065 conflicts
c [score-dist-6] active 0 (0%), one 24938 (34%), zero 47888 (66%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 662 variables 0.9% (72826 remain 34%)
c [simplification-6] removed 8291 irredundant clauses 1.7% (484458 remain 41%)
c [simplification-6] maximum reduction of 2% = max (1%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 6666
c [simplification-6] penalized conflict interval 6666 = 1 * 6666
c [simplification-6] hard conflict limit 21731 (soft 11731 + delta 10000)
c [simplification-6] new conflict limit 11731 (hard 21731)
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.5   72825   484458      5069    3476    493 35557    8    79   37  10%      2   76   11    1 1441%
c i   21.5   72820   484458      5079    3485    493 35557    8    79   37  10%      2   76   11    1 1450%
c i   21.5   72815   484458      5154    3552    493 35558    8    80   37  10%      2   76   17    1 2084%
c i   21.7   72801   484458      5348    3706    507 35575    8    83   37  10%      2   79   13    1 1608%
c i   21.7   72795   484458      5400    3747    511 35578    8    82   37  10%      2   78   12    1 1484%
c i   21.9   72790   484458      5801    4087    534 35607    9    84   37  11%      2   79   13    1 1462%
c i   21.9   72783   484458      5923    4187    543 35615    9    85   37  10%      2   80   13    1 1403%
c i   22.0   72774   484458      6031    4282    547 35620    9    85   37  11%      2   80   16    1 1615%
c i   22.2   72769   484458      6502    4666    578 35658   11    88   37  12%      3   82   21    1 1847%
c i   22.2   72762   484458      6535    4681    584 35668   11    87   37  12%      2   82   19    1 1666%
c i   22.2   72756   484458      6572    4710    586 35673   11    88   37  12%      2   82   17    1 1516%
c i   22.3   72556   484458      6678    4787    598 35686   10    88   37  12%      2   82   14    1 1258%
c i   22.4   72284   484458      6729    4824    602 35692   10    88   37  12%      2   83   13    1 1160%
c i   22.4   71919   484458      6751    4836    605 35698   10    89   37  12%      2   83   13    1 1094%
c i   22.4   71905   484458      6797    4867    610 35705   10    88   37  12%      2   82   12    1 1040%
c i   22.4   71904   484458      6813    4878    612 35707   10    88   37  12%      2   82   11    1  989%
c i   22.4   71903   484458      6814    4878    612 35707   10    88   37  12%      2   82   11    1  986%
c i   22.4   71902   484458      6815    4878    612 35707   10    88   37  12%      2   82   11    1  982%
c i   22.5   71901   484458      6867    4917    618 35712   10    88   37  12%      2   82   10    1  859%
c i   22.5   71877   484458      6917    4957    621 35718   10    88   37  12%      2   82    9    1  768%
c i   22.5   71864   484458      6932    4967    623 35720   10    88   37  12%      2   82    8    1  735%
c i   22.5   71857   484458      6944    4974    624 35723   10    88   37  12%      2   82    8    1  715%
c i   22.5   71856   484458      6945    4974    624 35723   10    88   37  12%      2   82    8    1  713%
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   22.5   71855   484458      6951    4975    625 35726   10    88   37  12%      2   82    8    1  700%
c i   22.5   71846   484458      6963    4977    628 35731   10    88   37  12%      2   82    8    1  675%
c i   22.6   71837   484458      6996    5002    632 35734   10    87   37  12%      2   81    7    1  628%
c i   22.6   71598   484458      7028    5022    634 35741   10    87   37  11%      2   81    7    1  595%
c i   22.7   71409   484458      7110    5079    645 35753   10    88   37  11%      2   81    6    1  545%
c i   22.7   71408   484458      7113    5081    645 35753   10    88   37  11%      2   81    6    1  544%
c i   22.7   71405   484458      7135    5097    645 35754   10    88   37  11%      1   81    6    1  555%
c i   22.7   71293   484458      7236    5171    652 35771   10    88   37  11%      1   82    7    1  608%
c i   22.8   71292   484458      7297    5219    660 35774   10    88   37  11%      1   82    7    1  609%
c i   22.8   71281   484458      7317    5237    660 35775   10    88   37  11%      1   82    7    1  599%
c i   22.8   71274   484458      7320    5237    660 35777   10    88   37  11%      1   82    7    1  593%
c i   22.9   71244   484458      7390    5279    668 35795   10    88   37  11%      1   81    6    1  529%
c i   22.9   71236   484458      7417    5298    672 35798   10    88   37  11%      1   81    6    1  521%
c i   22.9   71230   484458      7489    5353    678 35808   10    88   37  11%      1   81    6    1  472%
c i   23.0   71219   484458      7602    5436    694 35816   10    89   37  11%      1   82    7    1  564%
c i   23.0   71211   484458      7631    5454    699 35821   10    89   37  11%      1   82    7    1  540%
c i   23.2   71207   484458      7788    5566    717 35843   10    91   37  10%      1   84    8    1  637%
c i   23.2   71199   484458      7791    5567    717 35844   10    91   37  10%      1   84    8    1  632%
c i   23.2   71179   484458      7831    5590    726 35851    9    92   37  10%      1   85    7    1  590%
c i   23.3   71175   484458      7895    5633    732 35865    9    91   37  10%      1   84    6    1  526%
c i   23.3   71150   484458      7923    5654    734 35868    9    91   37  10%      1   84    6    1  513%
c i   23.3   71148   484458      7937    5664    735 35870    9    91   37  10%      1   84    6    1  494%
c i   23.4   71146   484458      7993    5709    741 35872    9    91   37  10%      1   84    6    1  467%
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.4   71144   484458      8008    5721    743 35872    9    91   37  10%      1   84    6    1  462%
c i   23.4   71091   484458      8057    5753    750 35881    9    91   37  10%      1   84    6    1  454%
c i   23.5   70060   484458      8102    5790    752 35885    9    91   37  10%      1   84    6    1  457%
c i   23.5   70057   484458      8199    5871    759 35891    9    92   37  10%      1   84    8    1  670%
c i   23.6   69823   484458      8275    5940    763 35893    9    92   37  10%      1   85   12    1  902%
c i   23.6   69817   484458      8324    5984    763 35896   10    93   37  10%      1   85   12    1  953%
c i   23.7   69816   484458      8437    6081    768 35905   10    94   37  10%      1   86   12    1  916%
c i   23.7   69809   484458      8469    6105    771 35907   10    94   38  10%      1   86   12    1  940%
c i   23.8   69806   484458      8706    6313    781 35920   10    96   38  11%      1   88   17    1 1245%
c i   23.9   69774   484458      8802    6386    789 35932   10    96   38  11%      1   88   16    1 1149%
c i   24.0   69766   484458      8911    6481    793 35938   10    97   38  11%      1   88   15    1 1050%
c i   24.1   69761   484458      9122    6657    808 35949   11    96   38  11%      1   87   18    1 1183%
c i   24.2   69760   484458      9399    6894    827 35964   11    99   38  11%      1   90   19    2 1208%
c i   24.3   69757   484458      9507    6981    835 35976   11   102   38  11%      1   92   15    2  974%
c i   24.3   69746   484458      9510    6983    835 35976   11   102   38  11%      1   92   15    2  964%
c i   24.4   69743   484458      9559    7021    837 35982   11   101   38  11%      1   92   17    2 1096%
c i   24.4   69651   484458      9587    7038    841 35988   11   101   38  11%      1   92   16    2 1006%
c i   24.5   69640   484458      9643    7080    847 35994   11   102   38  11%      1   92   14    2  880%
c i   24.5   69633   484458      9653    7087    848 35995   11   102   38  11%      1   93   14    2  866%
c i   24.6   69538   484458      9706    7128    856 35998   11   102   38  11%      1   93   13    2  819%
c i   24.6   69537   484458      9724    7138    860 35999   11   103   38  11%      1   93   14    2  853%
c i   24.7   69483   484458      9885    7274    867 36012   12   106   38  11%      1   96   17    2 1014%
c i   24.7   69476   484458      9896    7284    867 36012   12   106   38  11%      1   96   17    2 1049%
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   24.8   69475   484458      9997    7369    870 36021   12   108   38  11%      1   98   20    2 1170%
c i   24.8   69474   484458     10099    7463    873 36021   13   108   38  12%      1   98   25    2 1442%
c i   24.9   69469   484458     10163    7519    876 36025   12   108   38  12%      1   98   21    2 1226%
c i   24.9   69466   484458     10200    7547    880 36028   12   108   39  12%      1   98   20    2 1139%
c i   25.0   69463   484458     10298    7630    889 36031   12   109   39  11%      1   99   17    2  949%
c i   25.0   69452   484458     10392    7700    895 36040   12   109   39  11%      1   99   15    2  834%
c i   25.1   69451   484458     10405    7707    894 36045   12   109   39  11%      1   98   14    2  811%
c i   25.1   69450   484458     10424    7724    895 36045   12   109   39  11%      1   98   14    2  792%
c i   25.1   69448   484458     10466    7756    898 36049   12   108   39  11%      1   98   14    2  801%
c i   25.1   69320   484458     10503    7782    902 36055   12   108   39  11%      1   97   14    2  757%
c i   25.1   69318   484458     10539    7814    902 36057   12   109   39  11%      1   98   13    2  750%
c i   25.1   69317   484458     10579    7843    905 36063   12   109   39  11%      1   98   14    2  756%
c i   25.2   69310   484458     10634    7894    907 36064   12   110   39  11%      1   99   14    2  748%
c i   25.2   69305   484458     10662    7915    908 36069   12   110   39  11%      1   99   13    2  722%
c i   25.3   69302   484458     10665    7917    908 36069   12   110   39  11%      1   99   13    2  714%
c i   25.3   69293   484458     10703    7945    912 36074   12   111   39  11%      1  100   12    2  649%
c i   25.3   69284   484458     10734    7966    915 36080   12   112   39  11%      1  100   11    2  596%
c i   25.3   69265   484458     10752    7981    915 36082   12   112   39  11%      1  101   11    2  583%
c i   25.3   69264   484458     10757    7983    916 36083   12   112   39  11%      1  100   10    2  573%
c i   25.4   69251   484458     10805    8017    924 36088   12   113   39  11%      1  101   11    2  620%
c i   25.4   69143   484458     10838    8041    929 36090   12   114   39  11%      1  102   10    2  571%
c i   25.4   69142   484458     10848    8047    930 36092   12   114   39  11%      1  102   10    2  560%
c i   25.5   68982   484458     10890    8080    936 36094   12   113   39  11%      1  102   10    2  563%
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.5   68978   484458     10899    8087    936 36094   12   113   39  11%      1  102   10    2  566%
c i   26.0   68968   484458     11345    8437    963 36152   13   118   39  11%      2  106   16    2  848%
c i   26.1   68967   484458     11494    8563    976 36159   13   118   39  11%      1  106   17    2  858%
c i   26.2   68952   484458     11726    8772    985 36163   14   119   39  12%      2  106   28    2 1345%
c i   26.2   68943   484458     11727    8772    985 36163   14   119   39  12%      2  106   28    2 1340%
c i   26.3   68940   484458     11767    8806    986 36166   14   121   39  12%      1  108   26    2 1233%
c i   26.3   68916   484458     11776    8813    987 36166   14   121   39  12%      1  108   26    2 1209%
c i   26.3   68915   484458     11785    8821    987 36166   14   121   39  12%      1  108   25    2 1177%
c 
c [simplification-7] limit of 167 iterations hit after 167 iterations
c [quatres-3] found 32864 quaternary clauses 50% in total
c [quatres-3-2] added 2 single-self-subsuming ternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 42474 schedulable variables 58%
c [ternres-3] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-3] 14337 variables remain 21% (54576 retained 79%)
c [decomp-15] removed 4168 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 50621 literals 37%
c [treelook-3] scheduling used 369863 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 348682 steps
c [treelook-3] 50614 literals remain 37%
c [treelook-3] 27576 variables remain to probed next time 40%
c [treelook-3] removed 0 variables, found 1430 hbrs
c [unhide-7] limit 482878 with penalty 0 = 0 + 0
c [unhide-7-7] 13 units, 213 failed, 9879 tauts, 0 hbrs, 14082 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 243 transitive binary clauses
c [transred-3] found 6 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 394 (0%) of length 8
c [cce-2-1] eliminated 2 clauses out of 651 (0%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 3 large clauses in 15000004 steps
c [cce-2-1] allowing another 7500002 steps for small clauses
c [cce-2-1] scheduling 360307 clauses = 211792 binary + 148515 ternary
c [cce-2-1] tried to eliminate 164 small clauses 0%
c [cce-2-1] eliminated 30 binary clauses 0%
c [cce-2-1] eliminated 5 ternary clauses 0%
c [cce-2-1] eliminated 35 small clauses 0%
c [cce-2-1] eliminated 2628 small clauses in 15000006 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2631 covered clauses in round 1
c [cce-2] eliminated 2631 covered clauses in TOTAL during 1 rounds
c [cce-2] 2631 < 1/100 * 450190 = 4501 considered unsuccessful
c [elim-6] 11880 variables 17% will be scheduled this time
c [elim-6] scheduled 11880 variables 17%
c [elim-6] limit of 24143916 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 1 variables 0% in round 1 in 23206073 steps
c [elim-6-1] backward subsumption/strengthening limit 937843
c [elim-6-1-1] backward checking 64 touched variables 0%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 91950 steps
c [elim-6-1] fully rescheduled 68355 variables 100%
c [elim-6] incomplete 61141 not tried 89% in round 2
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 1286 = 11% variables out of 11880 scheduled
c [bca-3] limit of 10000000 steps and 890107 added (scaled 2)
c [bca-3] 114950 out of 134142 literals actually usable 86%
c [bca-3] added 56 blocked clauses in 329841 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 4580 pos 6.8% + 62420 neg 93.2% = 67000 sched 99.9% ret 70
c [sweep-3-1] 1006515 steps 20 queries 17811.35 avg class size
c [sweep-3-1] 143 decisions 16 SAT calls 53.62 avg env size
c [sweep-3-1] 66926 variables remain 100% (140 retained 0%)
c [decomp-17] removed 29 variables
c [sweep-3-1] removed 29 vars (0 failed, 3 eqs, 10 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 29 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-7] 441887 negative 99.5% of 444253 except 2366 0.5%
c [phase-count-7] 358604 positive 80.7% of 444253 except 85649 19.3%
c [phase-count-7] less non-negative clauses 2366 than limit 44400 (10.0%)
c [phase-count-7] non-pos/non-neg = 85649/2366 = 36.20 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 545 negative 100%
c [sort-queue-7] sorted 67041 enqueued variables after 11785 conflicts
c [score-dist-7] active 0 (0%), one 35895 (54%), zero 31146 (46%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 1872 variables 2.7% (67041 remain 31%)
c [simplification-7] removed 40205 irredundant clauses 8.3% (444253 remain 38%)
c [simplification-7] maximum reduction of 8% = max (3%, 8%)
c [simplification-7] forced so keeping old conflict interval 6666
c [simplification-7] conflict limit remains at 11795 (hard 21731)
c [simplification-7] new iteration interval 1000
c 
c [simplification-8] limit 11795 conflicts (hard 21731) hit after 11797 conflicts
c [quatres-4] found 38130 quaternary clauses 53% in total
c [quatres-4-2] added 2 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 13935 schedulable variables 21%
c [ternres-4] 39 ternary resolvents (2 bin, 37 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 27 xors of average arity 3.0
c [gauss-3] connected 81 occurrences of 48 variables (average 1.7)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 12104471 penalty 0 = 0 + 0
c [basicprobe-3-0] 22358 probes remain 34% after last round
c [basicprobe-3-0] 127 units = 127 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1247 variables, found 37539 hbrs
c [bate-1] eliminated 53 asymmetric tautologies during probing
c [unhide-8] limit 484178 with penalty 0 = 0 + 0
c [unhide-8-8] 13 units, 578 failed, 6185 tauts, 0 hbrs, 4669 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 331 transitive binary clauses
c [transred-4] found 10 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 65231 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 68 blocked clauses
c [block-3] 68 < 1/100 * 434661 = 4346 considered unsuccessful
c [elim-7] 59655 variables 91% will be scheduled this time
c [elim-7] scheduled 59655 variables 91%
c [elim-7] limit of 48417886 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 837 variables 1% in round 1 in 37818082 steps
c [elim-7-1] backward subsumption/strengthening limit 10599804
c [elim-7-1-1] backward checking 4578 touched variables 7%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 22 and strengthened 136 clauses in 1398401 steps
c [elim-7-1] rescheduled 505 variables 1% by backward subsumption
c [elim-7-2] eliminated 45 variables 0% in round 2 in 349005 steps
c [elim-7-2] backward subsumption/strengthening limit 349000
c [elim-7-2-1] backward checking 407 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 21 and strengthened 17 clauses in 217125 steps
c [elim-7-2] rescheduled 66 variables 0% by backward subsumption
c [elim-7-3] eliminated 8 variables 0% in round 3 in 51335 steps
c [elim-7-3] backward subsumption/strengthening limit 51300
c [elim-7-3-1] backward checking 55 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 4 and strengthened 3 clauses in 51301 steps
c [elim-7] incomplete 25 not tried 0% in round 3
c [gc-52] reconnected 61106 binary clauses (produced 0 empty 1 units)
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 901 = 2% variables out of 59655 scheduled
c [bca-4] limit of 10000000 steps and 853209 added (scaled 2)
c [bca-4] 110227 out of 128662 literals actually usable 86%
c [bca-4] added 101 blocked clauses in 313142 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 4471 pos 7.0% + 59737 neg 93.0% = 64208 sched 99.8% ret 122
c [sweep-4-1] 1002236 steps 38 queries 16281.34 avg class size
c [sweep-4-1] 420 decisions 33 SAT calls 54.21 avg env size
c [sweep-4-1] 63900 variables remain 99% (430 retained 1%)
c [decomp-19] removed 124 variables
c [sweep-4-1] removed 124 vars (0 failed, 4 eqs, 8 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 124 vars in TOTAL (1 rounds, 37 queries)
c [phase-count-8] 423382 negative 99.4% of 425759 except 2377 0.6%
c [phase-count-8] 340648 positive 80.0% of 425759 except 85111 20.0%
c [phase-count-8] less non-negative clauses 2377 than limit 42500 (10.0%)
c [phase-count-8] non-pos/non-neg = 85111/2377 = 35.81 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 500 negative 100%
c [sort-queue-8] sorted 64206 enqueued variables after 11797 conflicts
c [score-dist-8] active 0 (0%), one 35509 (55%), zero 28697 (45%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 2835 variables 4.2% (64206 remain 30%)
c [simplification-8] removed 18494 irredundant clauses 4.2% (425759 remain 36%)
c [simplification-8] maximum reduction of 4% = max (4%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 10666
c [simplification-8] penalized conflict interval 10666 = 1 * 10666
c [simplification-8] hard conflict limit 32463 (soft 22463 + delta 10000)
c [simplification-8] new conflict limit 22463 (hard 32463)
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   32.6   64205   425759     11834    6420    895 61980   14   122   36  12%      1  109   22    2 1041%
c i   32.7   64200   425759     11902    6467    903 61989   14   122   36  12%      1  109   18    2  839%
c i   32.7   64195   425759     11915    6473    907 61991   14   122   36  12%      1  109   17    2  806%
c i   32.7   64189   425759     11934    6486    909 61994   14   122   36  12%      1  109   16    2  757%
c i   32.7   64162   425759     11950    6497    912 61994   14   121   36  12%      1  108   16    2  742%
c i   32.7   64159   425759     11957    6503    912 61994   14   121   36  12%      1  108   16    2  727%
c i   32.7   64120   425759     12000    6540    915 61995   14   122   36  12%      1  108   16    2  731%
c i   32.8   64119   425759     12013    6551    915 61996   14   122   36  12%      1  109   15    2  709%
c i   32.8   64114   425759     12062    6595    917 61998   14   122   36  11%      1  109   15    2  688%
c i   32.8   64113   425759     12118    6643    919 62003   14   122   36  12%      1  109   17    2  797%
c i   32.9   64112   425759     12251    6764    922 62009   14   121   36  12%      1  108   15    2  679%
c i   33.0   64111   425759     12400    6899    927 62015   14   123   36  12%      1  109   17    2  763%
c i   33.1   64109   425759     12453    6945    929 62018   14   125   36  11%      1  111   15    2  687%
c i   33.2   64105   425759     12537    7017    932 62023   14   126   36  11%      1  112   13    2  598%
c i   33.2   64098   425759     12629    7097    935 62030   14   125   36  11%      1  111   12    2  531%
c i   33.3   64096   425759     12673    7133    936 62032   14   124   36  11%      1  110   12    2  521%
c i   33.4   64090   425759     12843    7269    950 62045   14   125   36  11%      1  111   13    2  551%
c i   33.4   64085   425759     12851    7274    950 62047   14   125   36  11%      1  111   12    2  538%
c i   33.4   64079   425759     12870    7287    953 62049   14   125   36  11%      1  110   12    2  509%
c i   33.6   64077   425759     13013    7403    960 62068   14   128   36  11%      1  113   13    2  563%
c i   33.6   64073   425759     13043    7427    961 62071   14   127   36  11%      1  113   13    2  550%
c i   33.6   64069   425759     13048    7428    962 62073   14   127   36  11%      1  112   13    2  545%
c i   33.7   64066   425759     13095    7459    968 62080   14   127   36  11%      1  112   11    2  494%
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.7   64063   425759     13132    7485    971 62085   14   126   36  11%      1  111   11    2  469%
c i   33.7   64056   425759     13135    7486    972 62085   14   126   36  11%      1  111   11    2  464%
c i   33.7   64054   425759     13198    7528    977 62098   14   127   36  11%      1  111   10    2  423%
c i   33.9   63961   425759     13297    7600    992 62107   13   127   36  11%      1  112    9    2  368%
c i   34.0   63957   425759     13383    7680    993 62111   13   127   36  11%      1  112   10    2  428%
c i   34.0   63950   425759     13408    7700    994 62113   13   128   36  11%      1  112   10    2  434%
c i   34.0   63888   425759     13438    7713    998 62125   13   128   36  10%      1  112    9    2  394%
c i   34.0   63883   425759     13445    7715    999 62128   13   127   36  10%      1  112    9    2  386%
c i   34.1   63875   425759     13480    7745    999 62132   13   128   36  10%      1  112    9    2  362%
c i   34.1   63871   425759     13519    7775   1003 62136   13   128   36  10%      1  113    9    2  365%
c i   34.2   63869   425759     13561    7810   1004 62140   13   130   36  10%      1  114    9    2  363%
c i   34.2   63858   425759     13569    7815   1004 62142   13   130   36  10%      1  114    8    2  358%
c i   34.3   63850   425759     13678    7907   1011 62151   13   133   36  10%      1  117    9    2  388%
c i   34.3   63846   425759     13728    7949   1015 62152   13   133   36  10%      1  117   11    2  463%
c i   34.4   63842   425759     13801    8003   1024 62161   13   134   36  10%      1  118   11    2  474%
c i   34.4   63839   425759     13813    8009   1028 62162   13   135   36  10%      1  119   11    2  464%
c i   34.6   63835   425759     13942    8110   1034 62180   13   136   36  10%      1  120   14    2  564%
c i   34.6   63822   425759     13956    8121   1034 62182   13   137   36  10%      1  121   13    2  548%
c i   34.7   63816   425759     14021    8173   1039 62186   13   138   36  10%      1  122   13    2  529%
c i   34.8   63814   425759     14076    8218   1041 62190   13   141   36   9%      1  124   12    2  491%
c i   34.9   63803   425759     14274    8389   1053 62199   13   141   36   9%      1  124   14    2  576%
c i   34.9   63800   425759     14275    8389   1053 62199   13   141   36   9%      1  124   14    2  574%
c i   35.0   63799   425759     14315    8424   1055 62201   13   142   36   9%      1  124   14    2  573%
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.0   63789   425759     14316    8424   1055 62201   13   142   36   9%      1  124   14    2  570%
c i   35.0   63782   425759     14319    8425   1056 62201   13   141   36   9%      1  124   14    2  565%
c i   35.0   63778   425759     14341    8439   1056 62206   13   142   36   9%      1  124   16    3  644%
c i   35.0   63777   425759     14383    8473   1057 62208   14   141   36  10%      1  124   17    3  669%
c i   35.0   63773   425759     14431    8509   1059 62216   13   140   36  10%      1  123   16    3  617%
c i   35.0   63769   425759     14435    8512   1059 62216   13   140   36  10%      1  123   15    3  609%
c i   35.0   63758   425759     14436    8512   1059 62216   13   140   36  10%      1  123   15    3  606%
c i   35.1   63749   425759     14536    8601   1064 62220   13   140   36  10%      1  122   14    3  567%
c i   35.1   63745   425759     14543    8607   1064 62220   13   140   36  10%      1  122   14    3  563%
c i   35.2   63738   425759     14632    8689   1066 62224   13   140   36  10%      1  123   14    3  567%
c i   35.2   63733   425759     14646    8699   1066 62227   13   140   36  10%      1  123   14    3  554%
c i   35.3   63727   425759     14814    8838   1080 62238   13   140   36  10%      1  122   14    3  552%
c i   35.5   63726   425759     14948    8955   1089 62244   14   141   36  10%      1  123   14    3  541%
c i   35.6   63721   425759     15141    9121   1098 62254   15   144   36  10%      1  125   27    3  982%
c i   35.7   63707   425759     15267    9224   1100 62263   15   145   36  10%      1  126   26    3  934%
c i   35.8   63701   425759     15299    9237   1108 62269   15   144   36  10%      1  125   23    3  837%
c i   35.8   63700   425759     15322    9254   1111 62270   15   144   36  10%      1  125   22    3  793%
c i   36.1   63695   425759     15640    9516   1140 62292   14   143   36  10%      1  123   15    3  522%
c i   36.1   63694   425759     15662    9533   1143 62293   14   143   36  10%      1  123   14    3  510%
c i   36.1   63692   425759     15683    9544   1147 62297   14   143   36  10%      1  123   13    3  481%
c i   36.1   63691   425759     15689    9546   1149 62298   14   142   36  10%      1  123   13    3  472%
c i   36.1   63684   425759     15696    9547   1151 62301   14   142   36  10%      1  123   13    3  461%
c i   36.1   63682   425759     15699    9549   1151 62301   14   142   36  10%      1  122   13    3  457%
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   36.2   63681   425759     15727    9573   1152 62302   14   142   36  10%      1  122   12    3  428%
c i   36.2   63672   425759     15810    9641   1159 62308   14   141   36  10%      1  121   12    3  443%
c i   36.2   63671   425759     15811    9641   1159 62308   14   141   36  10%      1  121   12    3  442%
c i   36.4   63668   425759     15948    9764   1165 62312   14   143   36  10%      1  123   16    3  557%
c i   36.5   63665   425759     16191    9984   1168 62325   15   143   36  11%      1  122   24    3  800%
c i   36.6   63661   425759     16225   10014   1169 62326   15   143   36  11%      1  122   23    3  776%
c i   36.6   63660   425759     16285   10067   1172 62329   15   143   36  11%      1  123   22    3  731%
c i   36.6   63652   425759     16291   10070   1173 62330   15   143   36  11%      1  122   21    3  717%
c i   36.8   63649   425759     16484   10245   1179 62338   15   144   37  10%      1  123   16    3  532%
c i   36.8   63648   425759     16491   10250   1179 62339   15   144   37  10%      1  122   16    3  525%
c i   36.9   63641   425759     16546   10299   1181 62340   15   144   37  11%      1  123   17    3  579%
c i   36.9   63640   425759     16557   10306   1181 62342   15   144   37  11%      1  123   18    3  582%
c i   37.1   63639   425759     16738   10465   1193 62350   15   147   37  10%      1  125   18    3  580%
c i   37.1   63638   425759     16765   10488   1194 62352   15   147   37  10%      1  125   17    3  562%
c i   37.1   63631   425759     16767   10489   1194 62352   15   147   37  10%      1  125   17    3  563%
c i   37.2   63622   425759     16848   10550   1201 62364   15   147   37  10%      1  125   15    3  478%
c i   37.2   63614   425759     16863   10563   1201 62365   15   147   37  10%      1  125   14    3  463%
c i   37.2   63613   425759     16886   10578   1203 62370   15   146   37  10%      1  124   13    3  434%
c i   37.2   63604   425759     16887   10578   1203 62370   15   146   37  10%      1  124   13    3  433%
c i   37.3   63594   425759     16890   10580   1203 62370   15   146   37  10%      1  124   13    3  428%
c i   37.3   63589   425759     16934   10614   1205 62377   15   145   37  10%      1  123   12    3  390%
c i   37.4   63584   425759     16984   10659   1206 62378   15   147   37  10%      1  125   13    3  408%
c i   37.5   63583   425759     17135   10787   1212 62388   15   147   37  10%      1  125   15    3  486%
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   37.5   63578   425759     17145   10793   1212 62391   15   147   37  10%      1  124   15    3  472%
c i   37.5   63568   425759     17168   10814   1213 62391   15   147   37  10%      1  124   15    3  485%
c i   37.5   63565   425759     17169   10814   1213 62391   15   147   37  10%      1  124   15    3  483%
c i   37.5   63564   425759     17170   10814   1213 62391   15   147   37  10%      1  124   15    3  481%
c i   37.6   63557   425759     17288   10916   1217 62401   15   147   37  10%      1  124   14    3  463%
c i   37.6   63548   425759     17298   10923   1217 62403   15   147   37  10%      1  124   14    3  461%
c i   37.8   63543   425759     17541   11134   1223 62418   15   147   37  10%      1  124   13    3  402%
c i   37.8   63514   425759     17552   11144   1223 62418   15   147   37  10%      1  124   13    3  419%
c i   37.9   63493   425759     17590   11171   1223 62418   15   148   37  10%      1  125   14    3  445%
c i   38.1   63492   425759     17888   11436   1234 62431   15   147   38  10%      1  123   18    3  546%
c i   38.1   63479   425759     17904   11447   1234 62435   15   147   38  10%      1  123   17    3  522%
c i   38.2   63477   425759     17986   11507   1239 62445   15   147   38  10%      1  123   17    3  521%
c i   38.2   63457   425759     18011   11525   1240 62448   15   147   38  10%      1  123   16    3  493%
c i   38.4   63445   425759     18119   11621   1243 62453   16   148   38  11%      1  124   21    3  622%
c i   38.4   63439   425759     18130   11631   1243 62453   16   148   38  11%      1  124   20    3  609%
c i   38.4   63422   425759     18149   11643   1244 62458   16   148   38  11%      1  123   19    3  578%
c i   38.4   63418   425759     18251   11734   1246 62463   16   146   38  11%      1  122   17    3  522%
c i   38.5   63417   425759     18376   11845   1249 62469   16   146   38  11%      1  121   22    3  663%
c i   38.6   63413   425759     18491   11951   1252 62470   16   145   38  11%      1  120   26    3  760%
c i   38.6   63405   425759     18502   11960   1253 62470   16   145   38  11%      1  120   25    3  736%
c i   38.6   63404   425759     18589   12040   1255 62472   16   144   38  11%      1  119   23    3  654%
c i   38.8   63397   425759     18691   12129   1259 62480   16   148   38  11%      1  123   21    3  607%
c i   38.8   63394   425759     18712   12149   1259 62480   17   149   38  11%      1  124   21    3  610%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   39.0   63387   425759     18861   12277   1266 62492   16   150   38  11%      1  124   17    4  478%
c i   39.2   63386   425759     19088   12487   1272 62497   17   150   38  11%      1  124   21    4  593%
c i   39.2   63384   425759     19109   12507   1272 62497   17   150   38  11%      1  124   21    4  595%
c i   39.2   63383   425759     19128   12523   1273 62498   17   149   38  11%      1  123   21    4  583%
c i   39.3   63379   425759     19207   12598   1273 62500   17   149   38  11%      1  123   19    4  539%
c i   39.4   63375   425759     19262   12642   1273 62508   17   149   38  11%      1  123   22    4  609%
c i   39.5   63371   425759     19428   12784   1280 62522   17   152   38  11%      1  126   20    4  558%
c i   39.6   63367   425759     19511   12857   1281 62528   17   152   38  11%      1  125   20    4  537%
c i   39.7   63366   425759     19589   12925   1286 62531   17   152   38  11%      1  125   20    4  529%
c i   39.7   63365   425759     19646   12970   1288 62538   17   153   38  11%      1  126   18    4  490%
c i   39.7   63357   425759     19666   12981   1290 62543   17   153   38  11%      1  126   17    4  458%
c i   39.8   63266   425759     19675   12986   1290 62546   17   153   38  11%      1  126   16    4  444%
c i   39.8   63265   425759     19708   13014   1291 62548   17   154   38  11%      1  127   16    4  426%
c i   39.8   63260   425759     19709   13014   1291 62548   17   154   38  11%      1  127   16    4  424%
c i   39.8   63236   425759     19764   13062   1294 62549   17   155   38  11%      1  127   16    4  439%
c i   40.0   63231   425759     19891   13167   1301 62558   17   157   39  11%      1  130   19    4  514%
c i   40.2   63226   425759     20177   13413   1315 62574   17   160   39  11%      1  132   18    4  474%
c i   40.4   63200   425759     20419   13622   1325 62588   17   158   39  11%      1  129   21    4  539%
c i   40.4   63198   425759     20442   13635   1329 62593   17   158   39  11%      1  129   20    4  507%
c i   40.5   63192   425759     20477   13666   1330 62595   17   158   39  11%      1  130   19    4  498%
c i   40.6   63187   425759     20601   13759   1342 62603   17   159   39  11%      1  130   17    4  439%
c i   40.7   63138   425759     20619   13775   1343 62603   17   159   39  11%      1  130   17    4  444%
c i   40.7   63135   425759     20628   13782   1343 62604   17   159   39  11%      1  130   17    4  438%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   40.7   63125   425759     20645   13794   1343 62608   17   159   39  11%      1  130   16    4  417%
c i   40.7   63124   425759     20646   13794   1343 62608   17   159   39  11%      1  130   16    4  416%
c i   40.7   63119   425759     20664   13811   1343 62608   17   159   39  11%      1  130   16    4  398%
c i   40.8   63109   425759     20693   13833   1343 62611   17   159   39  11%      1  130   15    4  387%
c i   40.8   62774   425759     20727   13856   1346 62616   17   159   39  11%      1  130   15    4  378%
c i   40.8   62770   425759     20740   13867   1346 62617   17   160   39  11%      1  130   15    4  370%
c i   41.0   62769   425759     20865   13977   1353 62621   17   160   39  11%      1  131   16    4  405%
c i   41.1   62765   425759     21012   14101   1360 62635   17   160   39  11%      1  130   14    4  345%
c i   41.1   62764   425759     21016   14104   1360 62635   17   160   39  11%      1  130   14    4  341%
c i   41.2   62758   425759     21024   14110   1360 62635   17   160   39  11%      1  130   14    4  342%
c i   41.2   62753   425759     21025   14110   1360 62635   17   160   39  11%      1  130   14    4  340%
c i   41.2   62743   425759     21026   14110   1360 62635   17   160   39  11%      1  130   13    4  339%
c i   41.2   62739   425759     21069   14139   1362 62646   17   161   39  10%      1  131   13    4  327%
c i   41.4   62728   425759     21247   14290   1365 62654   17   163   39  11%      1  133   18    4  455%
c i   41.4   62719   425759     21253   14295   1365 62654   17   163   39  10%      1  133   18    4  447%
c i   41.4   62713   425759     21283   14312   1369 62662   17   163   39  10%      1  133   17    4  431%
c i   41.5   62701   425759     21295   14320   1369 62663   17   164   39  10%      1  133   17    4  428%
c i   41.5   62696   425759     21296   14320   1369 62663   17   164   39  10%      1  133   17    4  426%
c i   41.5   62690   425759     21315   14337   1370 62663   17   164   39  10%      1  133   17    4  423%
c i   41.5   62686   425759     21346   14364   1371 62663   17   165   39  10%      1  135   18    4  443%
c i   41.5   62650   425759     21348   14365   1371 62663   17   165   39  10%      1  135   18    4  440%
c i   41.7   62641   425759     21556   14530   1385 62686   17   165   39  10%      1  134   15    4  380%
c i   41.7   62640   425759     21563   14536   1385 62686   17   165   39  10%      1  134   15    4  379%
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.8   62638   425759     21575   14547   1385 62686   17   165   39  10%      1  134   16    4  390%
c i   41.8   62632   425759     21604   14574   1386 62686   17   165   39  10%      1  134   15    4  374%
c i   41.8   62624   425759     21620   14589   1386 62686   17   165   39  10%      1  134   15    4  365%
c i   41.9   62623   425759     21706   14667   1388 62691   17   164   39  10%      1  133   15    4  365%
c i   41.9   62622   425759     21762   14711   1392 62698   17   163   39  10%      1  132   13    4  327%
c i   42.2   62617   425759     21967   14897   1400 62704   17   163   39  10%      1  131   15    4  369%
c i   42.2   62614   425759     21969   14898   1400 62704   17   163   39  10%      1  131   15    4  367%
c i   42.2   62611   425759     22021   14942   1403 62707   17   163   39  10%      1  131   15    4  361%
c i   42.2   62604   425759     22022   14942   1403 62707   17   163   39  10%      1  131   15    4  359%
c i   42.2   62603   425759     22046   14963   1403 62709   17   163   39  10%      1  131   15    4  352%
c i   42.5   62598   425759     22320   15215   1408 62720   17   164   39  10%      1  132   20    4  467%
c i   42.5   62590   425759     22368   15256   1412 62722   17   165   39  10%      1  132   18    4  424%
c i   42.7   62587   425759     22513   15376   1423 62727   17   167   39  10%      1  134   19    4  456%
c 
c [simplification-9] limit 22642 conflicts (hard 32463) hit after 22642 conflicts
c [quatres-5] found 33286 quaternary clauses 53% in total
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 3 single-self-subsuming ternary resolvents
c [quatres-5-2] added 4 quaternary resolvents
c [ternres-5] limit 5595590 with penalty 0 = 0 + 0
c [ternres-5] all 62575 free variables schedulable
c [ternres-5] 109 ternary resolvents (0 bin, 109 trn)
c [ternres-5] 23284 variables remain 37% (39291 retained 63%)
c [decomp-20] removed 1832 variables
c [simpleprobe-4] 7088 schedulable variables 11%
c [simpleprobe-4] limit 22382361 penalty 0 = 0 + 0
c [decomp-21] removed 1298 variables
c [simpleprobe-4] 1045 variables remain 2% (60031 retained 98%)
c [simpleprobe-4] removed 1298 variables, found 29376 hbrs, 343 units
c [unhide-9] limit 1119118 with penalty 0 = 0 + 0
c [unhide-9-9] 11 units, 178 failed, 10998 tauts, 0 hbrs, 26290 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 394 transitive binary clauses
c [transred-5] found 5 units
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 60667 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2238236120 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 3355 variables 6% in round 1 in 35411320 steps
c [elim-8-1] backward subsumption/strengthening limit 35411300
c [elim-8-1-1] backward checking 9813 touched variables 16%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 71 and strengthened 216 clauses in 2599543 steps
c [elim-8-1] rescheduled 538 variables 1% by backward subsumption
c [elim-8-2] eliminated 67 variables 0% in round 2 in 838498 steps
c [elim-8-2] backward subsumption/strengthening limit 838400
c [elim-8-2-1] backward checking 516 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 22 and strengthened 14 clauses in 306470 steps
c [elim-8-2] rescheduled 65 variables 0% by backward subsumption
c [elim-8-3] eliminated 4 variables 0% in round 3 in 416517 steps
c [elim-8-3] backward subsumption/strengthening limit 416500
c [elim-8-3-1] backward checking 115 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 6 and strengthened 2 clauses in 184133 steps
c [elim-8] incomplete 13 not tried 0% in round 3
c [gc-58] reconnected 81057 binary clauses (produced 0 empty 3 units)
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 3452 = 6% variables out of 60667 scheduled
c [bca-5] limit of 10000000 steps and 766300 added (scaled 2)
c [bca-5] 91862 out of 114432 literals actually usable 80%
c [bca-5] added 80 blocked clauses in 251208 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 16786770 penalty 0 = 0 + 0
c [sweep-5-1] 4279 pos 7.5% + 52550 neg 92.5% = 56829 sched 99.3% ret 386
c [sweep-5-1] 16786783 steps 289 queries 1172.75 avg class size
c [sweep-5-1] 2880 decisions 247 SAT calls 77.21 avg env size
c [sweep-5-1] 47513 variables remain 83% (9401 retained 17%)
c [decomp-22] removed 451 variables
c [sweep-5-1] removed 451 vars (0 failed, 47 eqs, 80 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 451 vars in TOTAL (1 rounds, 288 queries)
c [phase-count-9] 377548 negative 99.4% of 379648 except 2100 0.6%
c [phase-count-9] 304902 positive 80.3% of 379648 except 74746 19.7%
c [phase-count-9] less non-negative clauses 2100 than limit 37900 (10.0%)
c [phase-count-9] non-pos/non-neg = 74746/2100 = 35.59 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 16 negative 100%
c [sort-queue-9] sorted 56764 enqueued variables after 22642 conflicts
c [score-dist-9] active 0 (0%), one 37446 (66%), zero 19318 (34%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 5811 variables 9.3% (56764 remain 27%)
c [simplification-9] removed 46111 irredundant clauses 10.8% (379648 remain 32%)
c [simplification-9] maximum reduction of 11% = max (9%, 11%)
c [simplification-9] large reduction 11% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 34642 (soft 24642 + delta 10000)
c [simplification-9] new conflict limit 24642 (hard 34642)
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   47.1   56763   379648     22711   11540   1264 93657   17   167   36  10%      1  134   16    4  367%
c i   47.1   56761   379648     22731   11558   1265 93657   17   166   37  10%      1  133   16    4  369%
c i   47.3   56758   379648     22897   11696   1271 93667   16   164   37  10%      1  131   13    4  300%
c i   47.4   56756   379648     23003   11791   1276 93669   17   166   37  10%      1  133   17    4  390%
c i   47.5   56751   379648     23226   11979   1291 93682   17   165   37  10%      1  130   21    4  478%
c i   47.7   56749   379648     23392   12127   1296 93691   17   165   37  10%      1  131   17    4  381%
c i   48.0   56745   379648     23693   12399   1303 93705   17   166   37  10%      1  131   16    4  356%
c i   48.1   56730   379648     23898   12579   1312 93707   17   167   37  10%      1  131   15    5  342%
c i   48.2   56728   379648     23968   12632   1319 93711   17   168   37  10%      1  132   16    5  358%
c i   48.2   56723   379648     23975   12637   1319 93712   17   168   37  10%      1  132   16    5  351%
c i   48.3   56720   379648     24060   12714   1321 93717   17   168   37  10%      1  132   15    5  321%
c i   48.3   56719   379648     24064   12717   1321 93717   17   168   37  10%      1  132   14    5  318%
c i   48.4   56713   379648     24140   12788   1323 93719   17   166   37  10%      1  130   16    5  345%
c i   48.4   56711   379648     24154   12799   1324 93720   17   166   37  10%      1  130   16    5  342%
c i   48.5   56709   379648     24221   12859   1327 93723   16   165   37  10%      1  128   14    5  300%
c i   48.6   56702   379648     24387   13009   1331 93729   17   163   37  10%      1  127   16    5  339%
c i   48.6   56701   379648     24389   13009   1331 93730   17   163   37  10%      1  127   15    5  337%
c i   48.6   56685   379648     24427   13038   1336 93731   16   164   37  10%      1  127   15    5  316%
c i   48.7   56684   379648     24533   13137   1338 93733   17   163   37  10%      1  126   17    5  370%
c i   48.8   56672   379648     24611   13201   1345 93736   17   163   37  10%      1  126   16    5  335%
c 
c [simplification-10] limit 24650 conflicts (hard 34642) hit after 24650 conflicts
c [quatres-6] found 29193 quaternary clauses 51% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 5 single-self-subsuming ternary resolvents
c [quatres-6-2] added 14 quaternary resolvents
c [ternres-6] limit 6181798 with penalty 0 = 0 + 0
c [ternres-6] 21104 schedulable variables 37%
c [ternres-6] 652 ternary resolvents (0 bin, 652 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 386362 penalty 3 = 3 + 0
c [card-4] found 1517 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 386362 for elimination
c [card-4] 1517 out of 1517 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-23] removed 127 variables
c [unhide-10] limit 1236359 with penalty 0 = 0 + 0
c [unhide-10-10] 23 units, 487 failed, 11851 tauts, 0 hbrs, 16262 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 344 transitive binary clauses
c [transred-6] found 9 units
c [cce-3] limit of 7727247 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 38
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 37
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 36
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 35
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 34
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 33
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 32
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 31
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 30
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 29
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 28
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 27
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 26
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 25
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 24
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 23
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 22
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 21
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 20
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 19
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 18
c [cce-3-1] eliminated 2 clauses out of 3 (67%) of length 17
c [cce-3-1] eliminated 3 clauses out of 5 (60%) of length 16
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 15
c [cce-3-1] eliminated 4 clauses out of 7 (57%) of length 14
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 13
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 12
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 11
c [cce-3-1] eliminated 8 clauses out of 75 (11%) of length 10
c [cce-3-1] eliminated 8 clauses out of 217 (4%) of length 9
c [cce-3-1] eliminated 7 clauses out of 318 (2%) of length 8
c [cce-3-1] eliminated 14 clauses out of 488 (3%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 102 large clauses in 7727250 steps
c [cce-3-1] allowing another 3863625 steps for small clauses
c [cce-3-1] scheduling 195211 clauses = 177676 binary + 17535 ternary
c [cce-3-1] tried to eliminate 265 small clauses 0%
c [cce-3-1] eliminated 59 binary clauses 0%
c [cce-3-1] eliminated 9 ternary clauses 0%
c [cce-3-1] eliminated 68 small clauses 0%
c [cce-3-1] eliminated 4948 small clauses in 7727249 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 5050 covered clauses in round 1
c [cce-3] eliminated 5050 covered clauses in TOTAL during 1 rounds
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 56156 variables 100%
c [elim-9] limit of 123635963 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 805 variables 1% in round 1 in 33919986 steps
c [elim-9-1] backward subsumption/strengthening limit 33919900
c [elim-9-1-1] backward checking 3459 touched variables 6%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 36 and strengthened 162 clauses in 1092053 steps
c [elim-9-1] rescheduled 460 variables 1% by backward subsumption
c [elim-9-2] eliminated 40 variables 0% in round 2 in 675046 steps
c [elim-9-2] backward subsumption/strengthening limit 675000
c [elim-9-2-1] backward checking 400 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 24 and strengthened 23 clauses in 282994 steps
c [elim-9-2] rescheduled 124 variables 0% by backward subsumption
c [elim-9-3] eliminated 13 variables 0% in round 3 in 480010 steps
c [elim-9-3] backward subsumption/strengthening limit 480000
c [elim-9-3-1] backward checking 92 touched variables 0%
c [elim-9-3-1] fully completed backward checking in 1 rounds
c [elim-9-3] subsumed 3 and strengthened 10 clauses in 121003 steps
c [elim-9] incomplete 32 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 888 = 2% variables out of 56156 scheduled
c [bca-6] limit of 10000000 steps and 741960 added (scaled 2)
c [bca-6] 87010 out of 110538 literals actually usable 79%
c [bca-6] added 73 blocked clauses in 236154 steps
c [sweep-6] limit 1854539 penalty 0 = 0 + 0
c [sweep-6-1] 3817 pos 8.2% + 42589 neg 91.8% = 46406 sched 84.0% ret 8862
c [sweep-6-1] 1967037 steps 54 queries 9467.87 avg class size
c [sweep-6-1] 476 decisions 47 SAT calls 59.02 avg env size
c [sweep-6-1] 46021 variables remain 83% (9241 retained 17%)
c [decomp-24] removed 126 variables
c [sweep-6-1] removed 126 vars (0 failed, 7 eqs, 16 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 126 vars in TOTAL (1 rounds, 53 queries)
c [phase-count-10] 367999 negative 99.4% of 370035 except 2036 0.6%
c [phase-count-10] 296185 positive 80.0% of 370035 except 73850 20.0%
c [phase-count-10] less non-negative clauses 2036 than limit 37000 (10.0%)
c [phase-count-10] non-pos/non-neg = 73850/2036 = 36.27 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 13 negative 100%
c [sort-queue-10] sorted 55142 enqueued variables after 24650 conflicts
c [score-dist-10] active 0 (0%), one 37045 (67%), zero 18097 (33%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 1513 variables 2.7% (55142 remain 26%)
c [simplification-10] removed 9613 irredundant clauses 2.5% (370035 remain 31%)
c [simplification-10] maximum reduction of 3% = max (3%, 3%)
c [simplification-10] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-10] new conflict interval 15666
c [simplification-10] penalized conflict interval 15666 = 1 * 15666
c [simplification-10] hard conflict limit 50316 (soft 40316 + delta 10000)
c [simplification-10] new conflict limit 40316 (hard 50316)
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   51.8   55141   370035     24729   12603   1745 81964   16   162   36  10%      1  125   13    5  271%
c i   51.9   55125   370035     24845   12693   1758 81974   16   162   36  10%      1  124   10    5  213%
c i   52.5   55124   370035     25454   13234   1788 82005   16   160   37  10%      3  122   14    5  289%
c i   52.5   55119   370035     25459   13237   1788 82006   16   160   37  10%      3  122   13    5  285%
c i   52.6   55112   370035     25518   13290   1790 82007   16   161   37  10%      2  122   16    5  329%
c i   52.7   55022   370035     25745   13477   1808 82026   15   159   37  10%      2  120   11    5  232%
c i   53.0   55016   370035     26023   13717   1822 82045   16   164   37  10%      2  124   16    5  341%
c i   53.1   55011   370035     26155   13832   1825 82054   16   163   37  10%      2  123   15    5  312%
c i   53.1   55010   370035     26177   13853   1825 82054   16   163   37  10%      2  123   15    5  303%
c i   53.2   55008   370035     26282   13943   1829 82061   16   163   37  10%      2  123   15    5  314%
c i   53.3   55005   370035     26328   13984   1829 82062   16   162   37  10%      2  122   15    5  299%
c i   53.3   54993   370035     26342   13996   1829 82063   15   162   37  10%      2  122   14    5  298%
c i   53.3   54992   370035     26379   14029   1830 82065   15   163   37   9%      2  123   13    5  275%
c i   53.5   54942   370035     26504   14137   1838 82071   15   162   37   9%      1  122   13    5  270%
c i   53.5   54936   370035     26543   14174   1838 82071   15   162   37  10%      1  122   15    5  312%
c i   53.5   54932   370035     26565   14190   1841 82073   15   162   37  10%      1  122   15    5  302%
c i   53.5   54927   370035     26577   14197   1842 82075   15   162   37  10%      1  121   15    5  299%
c i   53.6   54926   370035     26689   14285   1852 82088   15   163   37   9%      1  123   13    5  272%
c i   53.7   54919   370035     26704   14295   1852 82092   15   163   37   9%      1  122   13    5  266%
c i   53.8   54917   370035     26856   14419   1863 82103   15   163   37   9%      1  122   11    5  217%
c i   53.8   54913   370035     26858   14420   1863 82103   15   163   37   9%      1  122   11    5  216%
c i   54.0   54910   370035     27036   14581   1871 82108   16   166   37   9%      1  125   21    5  418%
c i   54.0   54883   370035     27038   14581   1871 82109   16   166   37   9%      1  125   21    5  415%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   54.0   54878   370035     27082   14620   1873 82110   15   166   37   9%      1  125   18    5  372%
c i   54.1   54866   370035     27144   14668   1877 82118   15   166   37   9%      1  124   17    5  336%
c i   54.2   54865   370035     27219   14736   1879 82119   16   165   37   9%      1  124   18    5  363%
c i   54.3   54864   370035     27363   14863   1885 82122   16   165   37  10%      1  123   20    5  394%
c i   54.5   54863   370035     27657   15123   1892 82138   16   163   37  10%      1  121   19    5  366%
c i   54.5   54862   370035     27659   15123   1892 82139   16   163   37  10%      1  121   18    5  363%
c i   54.6   54857   370035     27742   15198   1893 82142   16   164   37  10%      1  121   17    5  334%
c i   55.0   54843   370035     28109   15521   1910 82163   16   165   37  10%      2  121   20    5  382%
c i   55.0   54842   370035     28137   15542   1910 82165   16   164   37  10%      1  121   24    5  455%
c i   55.0   54841   370035     28156   15559   1911 82165   16   165   37  10%      1  122   23    5  436%
c i   55.1   54837   370035     28189   15588   1911 82166   16   166   37  10%      1  122   21    5  410%
c i   55.3   54834   370035     28356   15734   1919 82176   17   170   37  10%      1  126   21    5  393%
c i   55.4   54833   370035     28518   15883   1924 82182   16   168   37  10%      1  124   17    5  332%
c i   55.6   54831   370035     28652   16002   1927 82189   16   169   37  10%      1  125   17    5  320%
c i   55.7   54830   370035     28757   16089   1931 82193   17   171   37  10%      1  126   21    5  386%
c i   55.7   54821   370035     28793   16122   1931 82195   17   170   37  10%      1  126   19    5  353%
c i   55.8   54820   370035     28862   16180   1937 82197   17   172   37  10%      1  127   17    5  320%
c i   55.8   54818   370035     28888   16200   1938 82201   16   172   37  10%      1  127   16    5  307%
c i   55.8   54808   370035     28924   16227   1941 82206   16   171   37  10%      1  126   15    5  282%
c i   55.9   54807   370035     28960   16251   1947 82210   16   170   37  10%      1  125   14    5  256%
c i   56.0   54805   370035     29159   16410   1958 82233   16   168   37  10%      1  122   12    5  218%
c i   56.0   54800   370035     29212   16453   1961 82238   16   167   37   9%      1  122   11    5  211%
c i   56.1   54797   370035     29268   16494   1968 82244   16   167   37   9%      1  121   10    5  190%
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   56.1   54793   370035     29287   16508   1970 82246   16   167   37   9%      1  121   10    5  182%
c i   56.2   54777   370035     29412   16594   1985 82267   15   166   37   9%      1  120    8    5  155%
c i   56.3   54776   370035     29501   16662   1988 82276   15   166   37   9%      1  120    8    5  158%
c i   56.4   54772   370035     29601   16754   1990 82281   15   166   37   9%      1  120    9    5  171%
c i   56.5   54766   370035     29706   16849   1994 82286   15   167   37   9%      1  121   11    5  199%
c i   56.6   54765   370035     29836   16955   1998 82297   15   166   37   9%      1  119   12    5  215%
c i   56.7   54759   370035     29866   16984   1998 82297   15   166   37   9%      1  120   16    5  289%
c i   56.7   54752   370035     29896   17008   2001 82299   15   166   37   9%      1  119   15    5  281%
c i   56.8   54745   370035     29973   17070   2006 82308   15   166   37   9%      1  119   15    5  279%
c i   56.8   54737   370035     29999   17095   2006 82308   15   166   37   9%      1  119   15    5  284%
c i   56.9   54734   370035     30038   17123   2008 82315   15   166   37   9%      0  119   14    5  259%
c i   56.9   54704   370035     30068   17149   2011 82315   15   167   37   9%      0  120   15    5  270%
c i   57.0   54703   370035     30107   17183   2014 82316   15   167   37   9%      0  120   15    5  277%
c i   57.0   54702   370035     30167   17237   2017 82317   15   167   37   9%      0  120   16    5  294%
c i   57.2   54701   370035     30381   17429   2027 82324   15   166   37   9%      1  119   16    5  295%
c i   57.2   54698   370035     30385   17431   2027 82324   15   166   37   9%      1  119   16    5  295%
c i   57.4   54694   370035     30533   17558   2033 82334   15   168   37   9%      1  120   18    6  318%
c i   57.4   54680   370035     30598   17620   2033 82334   16   169   37   9%      1  121   18    6  326%
c i   57.7   54662   370035     30780   17778   2044 82345   16   171   37   9%      1  123   18    6  323%
c i   57.8   54660   370035     30948   17936   2049 82349   16   173   37   9%      1  124   22    6  394%
c i   57.9   54654   370035     30960   17946   2049 82350   16   173   37   9%      1  124   21    6  381%
c i   57.9   54653   370035     30961   17946   2049 82350   16   173   37   9%      1  124   21    6  379%
c i   57.9   54646   370035     30989   17968   2050 82354   16   172   37   9%      1  123   21    6  377%
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   57.9   54644   370035     31016   17988   2054 82355   16   171   37   9%      1  122   19    6  346%
c i   57.9   54639   370035     31046   18014   2056 82356   16   171   37   9%      1  122   18    6  322%
c i   58.1   54635   370035     31165   18120   2059 82358   16   173   37   9%      1  124   21    6  377%
c i   58.3   54634   370035     31447   18370   2065 82376   17   176   37  10%      1  127   26    6  442%
c i   58.5   54633   370035     31584   18471   2076 82395   17   174   37  10%      1  124   20    6  339%
c i   58.5   54627   370035     31588   18472   2077 82396   17   174   37  10%      1  124   19    6  334%
c i   58.6   54619   370035     31775   18632   2087 82400   17   173   37  10%      1  123   18    6  303%
c i   58.7   54614   370035     31801   18656   2088 82400   17   174   37  10%      1  124   18    6  313%
c i   58.7   54613   370035     31820   18672   2089 82400   17   174   37  10%      1  124   18    6  306%
c i   58.8   54611   370035     31948   18785   2095 82406   18   177   37  10%      1  126   27    6  463%
c i   58.9   54608   370035     31998   18827   2098 82408   18   178   37  10%      1  127   30    6  511%
c i   59.0   54479   370035     32062   18886   2098 82411   18   180   38  10%      1  129   29    6  487%
c i   59.0   54478   370035     32068   18891   2098 82411   18   180   38  10%      1  129   28    6  478%
c i   59.1   54477   370035     32153   18960   2105 82414   18   179   38  10%      1  128   25    6  418%
c i   59.2   54474   370035     32253   19047   2110 82419   18   178   38  10%      1  127   24    6  402%
c i   59.2   54473   370035     32287   19076   2110 82423   18   178   38  10%      1  127   22    6  374%
c i   59.5   54469   370035     32546   19310   2121 82431   18   178   38  10%      1  127   18    6  298%
c i   59.5   54464   370035     32626   19382   2124 82433   18   178   38  10%      1  126   16    6  272%
c i   59.9   54462   370035     32953   19681   2137 82445   19   181   38  10%      1  128   24    6  386%
c i   60.0   54459   370035     33058   19764   2147 82454   19   182   38  10%      1  129   22    6  353%
c i   60.1   54456   370035     33198   19879   2155 82461   19   179   38  11%      1  126   22    6  356%
c i   60.1   54455   370035     33240   19913   2156 82467   19   179   38  11%      1  126   21    6  337%
c i   60.2   54446   370035     33355   20012   2157 82479   19   178   39  10%      1  125   18    6  294%
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   60.2   54445   370035     33387   20042   2158 82479   19   178   39  11%      1  124   18    6  293%
c i   60.3   54442   370035     33405   20059   2158 82479   19   178   39  11%      1  125   19    6  311%
c i   60.4   54441   370035     33513   20150   2163 82490   19   178   39  10%      1  125   19    6  302%
c i   60.4   54434   370035     33561   20193   2165 82492   19   179   39  11%      1  126   21    6  333%
c i   60.5   54428   370035     33564   20195   2165 82492   19   179   39  11%      1  125   21    6  330%
c i   60.5   54367   370035     33580   20206   2169 82492   19   179   39  10%      1  125   20    6  317%
c i   60.5   54360   370035     33654   20266   2172 82502   19   179   39  10%      1  125   18    6  282%
c i   60.7   54328   370035     33828   20417   2180 82514   19   181   39  10%      1  127   23    6  357%
c i   60.8   54327   370035     33961   20537   2184 82519   19   181   40  11%      1  126   23    6  360%
c i   61.0   54323   370035     34163   20721   2193 82525   20   184   41  11%      1  129   25    6  382%
c i   61.1   54317   370035     34186   20736   2196 82529   19   183   41  11%      1  128   23    6  356%
c i   61.1   54316   370035     34231   20776   2197 82532   19   183   41  11%      1  128   21    6  328%
c i   61.3   54315   370035     34412   20935   2205 82537   20   184   41  11%      1  129   32    7  485%
c i   61.5   54311   370035     34584   21093   2214 82540   20   185   41  11%      1  129   25    7  382%
c i   61.6   54309   370035     34610   21115   2215 82541   20   185   41  11%      1  129   24    7  364%
c i   61.7   54232   370035     34775   21266   2218 82545   21   187   41  11%      1  131   29    7  442%
c i   61.8   54225   370035     34848   21329   2220 82551   21   187   41  11%      1  131   31    7  461%
c i   62.3   54222   370035     35354   21774   2244 82570   21   185   41  12%      2  128   25    7  367%
c i   62.3   54221   370035     35377   21795   2244 82571   21   185   41  12%      2  128   25    7  365%
c i   62.6   54220   370035     35656   22044   2247 82585   23   188   41  12%      2  130   33    7  480%
c i   62.6   54213   370035     35674   22059   2247 82587   23   187   41  12%      2  129   32    7  453%
c i   62.8   54212   370035     35856   22228   2250 82590   23   190   41  12%      2  132   29    7  418%
c i   62.8   54210   370035     35857   22228   2250 82590   23   190   41  12%      2  132   29    7  417%
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   62.8   54201   370035     35894   22262   2251 82591   23   189   41  12%      2  131   30    7  423%
c i   62.8   54200   370035     35897   22263   2252 82591   23   189   41  12%      2  131   30    7  423%
c i   62.9   54199   370035     36007   22358   2257 82595   23   189   41  12%      1  131   26    7  367%
c i   63.0   54196   370035     36017   22365   2257 82597   23   189   41  12%      1  130   26    7  361%
c i   63.2   54193   370035     36258   22588   2261 82602   23   188   41  12%      1  129   26    7  360%
c i   63.2   54192   370035     36259   22588   2261 82602   23   188   41  12%      1  129   26    7  359%
c i   63.2   54191   370035     36280   22606   2261 82604   23   187   41  12%      1  128   24    7  338%
c i   63.2   54190   370035     36337   22656   2262 82605   23   187   41  12%      1  128   23    7  325%
c i   63.2   54189   370035     36343   22660   2263 82605   23   187   41  12%      1  128   23    7  321%
c i   63.3   54185   370035     36360   22672   2267 82605   23   188   41  12%      1  128   22    7  305%
c i   63.5   54183   370035     36557   22848   2274 82612   24   188   41  13%      1  129   38    7  529%
c i   63.6   54175   370035     36710   22974   2282 82618   24   189   41  13%      1  129   33    7  457%
c i   63.9   54174   370035     36999   23230   2288 82627   25   189   41  13%      1  129   35    7  470%
c i   64.0   54173   370035     37093   23308   2296 82632   25   189   41  13%      1  129   30    7  401%
c i   64.2   54172   370035     37237   23439   2301 82636   25   189   41  13%      1  128   26    7  350%
c i   64.2   54167   370035     37249   23448   2302 82637   25   189   41  13%      1  128   25    7  337%
c i   64.2   54166   370035     37250   23448   2302 82637   24   189   41  13%      1  128   25    7  336%
c i   64.4   54165   370035     37454   23635   2306 82641   24   188   41  13%      1  127   24    8  316%
c i   64.4   54160   370035     37507   23681   2307 82642   24   188   42  13%      1  126   23    8  309%
c i   64.8   54159   370035     37813   23956   2320 82651   25   186   42  13%      1  124   26    8  343%
c i   64.9   54158   370035     37962   24089   2322 82656   26   186   42  14%      1  124   39    8  507%
c i   65.0   54151   370035     37994   24117   2323 82658   26   185   42  14%      1  123   36    8  461%
c i   65.1   54146   370035     38139   24240   2327 82664   26   184   42  14%      1  122   29    8  374%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   65.1   54145   370035     38142   24242   2327 82664   26   184   42  14%      1  121   29    8  370%
c i   65.3   54143   370035     38302   24385   2332 82672   26   186   42  14%      1  123   35    8  441%
c i   65.8   54142   370035     38845   24873   2353 82695   26   189   42  14%      2  125   29    8  363%
c i   65.9   54005   370035     38908   24925   2356 82701   26   188   42  14%      2  124   28    8  343%
c i   65.9   53999   370035     38909   24925   2356 82701   26   188   42  14%      2  124   27    8  342%
c i   65.9   53996   370035     38930   24945   2356 82701   26   188   42  14%      2  124   27    8  330%
c i   66.0   53995   370035     39010   25017   2361 82703   26   189   42  14%      2  125   25    8  305%
c i   66.1   53994   370035     39058   25061   2363 82704   26   188   42  14%      2  124   26    8  319%
c i   66.7   53991   370035     39598   25549   2377 82719   29   193   43  15%      3  127   44    8  521%
c i   66.7   53984   370035     39616   25564   2378 82719   29   193   43  15%      3  127   43    8  509%
c i   66.7   53981   370035     39617   25564   2378 82719   29   193   43  15%      3  127   43    8  507%
c i   67.0   53977   370035     39813   25746   2387 82722   29   199   43  14%      2  133   33    8  392%
c i   67.3   53974   370035     40068   25976   2395 82734   28   200   43  14%      2  134   27    8  316%
c i   67.3   53973   370035     40131   26029   2397 82739   28   200   43  14%      2  133   24    9  280%
c i   67.3   53970   370035     40139   26035   2397 82740   28   200   43  14%      2  133   24    9  278%
c i   67.5   53968   370035     40300   26187   2400 82744   28   199   43  14%      2  133   25    9  297%
c i   67.6   53965   370035     40374   26248   2406 82748   28   198   43  14%      2  131   22    9  261%
c 
c [simplification-11] limit 40410 conflicts (hard 50316) hit after 40411 conflicts
c [quatres-7] found 26800 quaternary clauses 49% in total
c [quatres-7-2] added 3 single-self-subsuming ternary resolvents
c [quatres-7-2] added 18 quaternary resolvents
c [ternres-7] limit 10948974 with penalty 0 = 0 + 0
c [ternres-7] all 53952 free variables schedulable
c [ternres-7] 297 ternary resolvents (3 bin, 294 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 547448 penalty 2 = 2 + 0
c [gauss-4] extracted 42 xors of average arity 2.6
c [gauss-4] connected 108 occurrences of 85 variables (average 1.3)
c [gauss-4] limit 547448 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 141 variables
c [treelook-4] limit 547448 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 62196 literals 58%
c [treelook-4] scheduling used 547518 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 547448 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 554003 steps
c [treelook-4] 62182 literals remain 58%
c [treelook-4] 18863 variables remain to probed next time 35%
c [treelook-4] removed 3 variables, found 2579 hbrs
c [unhide-11] limit 2189794 with penalty 0 = 0 + 0
c [unhide-11-11] 10 units, 131 failed, 5596 tauts, 0 hbrs, 61456 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 324 transitive binary clauses
c [transred-7] found 4 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 53608 variables 100%
c [block-4] limit of 27372435 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 177 blocked clauses
c [block-4] 177 < 1/100 * 355106 = 3551 considered unsuccessful
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 53601 variables 100%
c [elim-10] limit of 218979484 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 1581 variables 3% in round 1 in 34074542 steps
c [elim-10-1] backward subsumption/strengthening limit 34074500
c [elim-10-1-1] backward checking 5547 touched variables 10%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 45 and strengthened 237 clauses in 1826369 steps
c [elim-10-1] rescheduled 631 variables 1% by backward subsumption
c [elim-10-2] eliminated 95 variables 0% in round 2 in 2068829 steps
c [elim-10-2] backward subsumption/strengthening limit 2068800
c [elim-10-2-1] backward checking 632 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 36 and strengthened 24 clauses in 284924 steps
c [elim-10-2] rescheduled 130 variables 0% by backward subsumption
c [elim-10-3] eliminated 11 variables 0% in round 3 in 366047 steps
c [elim-10-3] backward subsumption/strengthening limit 366000
c [elim-10-3-1] backward checking 76 touched variables 0%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 4 and strengthened 4 clauses in 111758 steps
c [elim-10] incomplete 19 not tried 0% in round 3
c [gc-74] reconnected 81086 binary clauses (produced 0 empty 4 units)
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 1734 = 3% variables out of 53601 scheduled
c [bca-7] limit of 10000000 steps and 698522 added (scaled 2)
c [bca-7] 74490 out of 103736 literals actually usable 72%
c [bca-7] added 41 blocked clauses in 203307 steps
c [sweep-7] limit 3284692 penalty 0 = 0 + 0
c [sweep-7-1] 3391 pos 7.8% + 39825 neg 92.2% = 43216 sched 83.3% ret 8651
c [sweep-7-1] 3450276 steps 62 queries 4582.05 avg class size
c [sweep-7-1] 741 decisions 53 SAT calls 92.98 avg env size
c [sweep-7-1] 42654 variables remain 82% (9201 retained 18%)
c [decomp-27] removed 37 variables
c [sweep-7-1] removed 37 vars (0 failed, 9 eqs, 17 impls)
c [sweep-7] 37 < 1/1000 * 51867 = 51 considered unsuccessful
c [sweep-7] removed 37 vars in TOTAL (1 rounds, 61 queries)
c [sort-queue-11] sorted 51830 enqueued variables after 40411 conflicts
c [score-dist-11] active 0 (0%), one 37764 (73%), zero 14066 (27%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 2122 variables 3.9% (51830 remain 24%)
c [simplification-11] removed 21770 irredundant clauses 5.9% (348265 remain 30%)
c [simplification-11] maximum reduction of 6% = max (4%, 6%)
c [simplification-11] large reduction 6% >= 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 52411 (soft 42411 + delta 10000)
c [simplification-11] new conflict limit 42411 (hard 52411)
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   71.3   51829   348265     40516   21985   2405 82559   28   195   41  14%      1  128   23    9  268%
c i   71.5   51828   348265     40698   22153   2409 82567   28   197   42  14%      1  129   22    9  255%
c i   71.5   51826   348265     40715   22165   2411 82568   27   197   42  14%      1  129   21    9  243%
c i   71.7   51825   348265     40860   22288   2420 82577   27   196   42  14%      1  129   19    9  217%
c i   71.9   51818   348265     41022   22432   2426 82584   27   196   42  14%      1  128   23    9  262%
c i   72.0   51815   348265     41102   22509   2428 82584   27   195   42  14%      1  127   22    9  253%
c i   72.1   51811   348265     41263   22654   2435 82590   26   194   42  14%      1  126   19    9  220%
c i   72.6   51807   348265     41744   23092   2450 82611   26   194   42  14%      2  125   27    9  306%
c i   72.6   51804   348265     41751   23097   2450 82612   26   194   42  14%      2  125   27    9  301%
c i   73.1   51799   348265     42301   23590   2467 82634   27   196   42  14%      3  126   29    9  319%
c 
c [simplification-12] limit 42412 conflicts (hard 52411) hit after 42413 conflicts
c [quatres-8] found 27676 quaternary clauses 50% in total
c [quatres-8-1] removed 2 duplicate quaternary clauses
c [quatres-8-2] added 3 single-self-subsuming ternary resolvents
c [quatres-8-2] added 13 quaternary resolvents
c [ternres-8] limit 11554821 with penalty 0 = 0 + 0
c [ternres-8] all 51799 free variables schedulable
c [ternres-8] 446 ternary resolvents (1 bin, 445 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 35 variables
c [basicprobe-4] limit 57774105 penalty 0 = 0 + 0
c [basicprobe-4-0] 14063 probes remain 28% after last round
c [basicprobe-4-0] 665 units = 660 failed (99%) + 5 lifted (1%)
c [basicprobe-4-0] removed 1152 variables, found 101748 hbrs
c [bate-2] eliminated 251 asymmetric tautologies during probing
c [unhide-12] limit 2310964 with penalty 0 = 0 + 0
c [unhide-12-12] 37 units, 623 failed, 19007 tauts, 0 hbrs, 31392 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 347 transitive binary clauses
c [transred-8] found 2 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 288870525 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 74
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 73
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 71
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 70
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 69
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 65
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 64
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 63
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 62
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 61
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 60
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 59
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 58
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 57
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 56
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 55
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 54
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 53
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 52
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 50
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 49
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 47
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 46
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 45
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 44
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 43
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 42
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 41
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 39
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 38
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 37
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 36
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 35
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 34
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 33
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 32
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 31
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 30
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 29
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 28
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 27
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 26
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 24
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 23
c [cce-4-1] eliminated 2 clauses out of 5 (40%) of length 22
c [cce-4-1] eliminated 4 clauses out of 5 (80%) of length 21
c [cce-4-1] eliminated 2 clauses out of 5 (40%) of length 20
c [cce-4-1] eliminated 4 clauses out of 5 (80%) of length 19
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 18
c [cce-4-1] eliminated 5 clauses out of 5 (100%) of length 17
c [cce-4-1] eliminated 6 clauses out of 12 (50%) of length 16
c [cce-4-1] eliminated 6 clauses out of 9 (67%) of length 15
c [cce-4-1] eliminated 6 clauses out of 10 (60%) of length 14
c [cce-4-1] eliminated 6 clauses out of 10 (60%) of length 13
c [cce-4-1] eliminated 6 clauses out of 10 (60%) of length 12
c [cce-4-1] eliminated 7 clauses out of 11 (64%) of length 11
c [cce-4-1] eliminated 7 clauses out of 53 (13%) of length 10
c [cce-4-1] eliminated 7 clauses out of 140 (5%) of length 9
c [cce-4-1] eliminated 6 clauses out of 273 (2%) of length 8
c [cce-4-1] eliminated 7 clauses out of 386 (2%) of length 7
c [cce-4-1] eliminated 64 clauses out of 1216 (5%) of length 6
c [cce-4-1] eliminated 11670 clauses out of 17494 (67%) of length 5
c [cce-4-1] eliminated 15271 clauses out of 25112 (61%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 27168 large clauses in 257448968 steps
c [cce-4-1] allowing another 128724484 steps for small clauses
c [cce-4-1] scheduling 271590 clauses = 161666 binary + 109924 ternary
c [cce-4-1] tried to eliminate 6861 small clauses 3%
c [cce-4-1] eliminated 1150 binary clauses 1%
c [cce-4-1] eliminated 307 ternary clauses 0%
c [cce-4-1] eliminated 1457 small clauses 1%
c [cce-4-1] eliminated 6042 small clauses in 288870533 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 33210 covered clauses in round 1
c [cce-4] eliminated 33210 covered clauses in TOTAL during 1 rounds
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 50110 variables 100%
c [elim-11] limit of 231096420 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 10923 variables 22% in round 1 in 25901980 steps
c [elim-11-1] backward subsumption/strengthening limit 25901900
c [elim-11-1-1] backward checking 25257 touched variables 50%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 108 and strengthened 411 clauses in 3413488 steps
c [elim-11-1] rescheduled 1134 variables 2% by backward subsumption
c [elim-11-2] eliminated 73 variables 0% in round 2 in 609825 steps
c [elim-11-2] backward subsumption/strengthening limit 609800
c [elim-11-2-1] backward checking 728 touched variables 1%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 23 and strengthened 44 clauses in 609801 steps
c [elim-11-2] rescheduled 169 variables 0% by backward subsumption
c [elim-11-3] eliminated 13 variables 0% in round 3 in 392155 steps
c [elim-11-3] backward subsumption/strengthening limit 392100
c [elim-11-3-1] backward checking 261 touched variables 1%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 9 and strengthened 3 clauses in 392101 steps
c [elim-11] incomplete 30 not tried 0% in round 3
c [gc-82] reconnected 155127 binary clauses (produced 0 empty 1 units)
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 11026 = 22% variables out of 50110 scheduled
c [bca-8] limit of 10000000 steps and 564853 added (scaled 2)
c [bca-8] 64091 out of 78170 literals actually usable 82%
c [bca-8] added 242 blocked clauses in 150413 steps
c [sort-queue-12] sorted 39084 enqueued variables after 42413 conflicts
c [score-dist-12] active 0 (0%), one 28320 (72%), zero 10764 (28%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 12715 variables 24.5% (39084 remain 18%)
c [simplification-12] removed 66622 irredundant clauses 19.1% (281643 remain 24%)
c [simplification-12] maximum reduction of 25% = max (25%, 19%)
c [simplification-12] large reduction 25% >= 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 54413 (soft 44413 + delta 10000)
c [simplification-12] new conflict limit 44413 (hard 54413)
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   85.7   39083   281643     42531    6788   2741 126248   27   193   29  14%      2  122   25    9  274%
c i   86.1   39081   281643     43328    7464   2787 126289   24   190   29  12%      4  118   10    9  114%
c i   86.1   39080   281643     43365    7491   2793 126290   23   189   29  12%      4  117   10    9  107%
c i   86.4   39039   281643     44018    8046   2848 126318   21   183   29  12%      5  110   11    9  116%
c 
c [simplification-13] limit 44413 conflicts (hard 54413) hit after 44414 conflicts
c [quatres-9] found 17384 quaternary clauses 59% in total
c [quatres-9-1] removed 5 duplicate quaternary clauses
c [quatres-9-2] added 35 quaternary resolvents
c [ternres-9] limit 11867437 with penalty 0 = 0 + 0
c [ternres-9] all 39039 free variables schedulable
c [ternres-9] 746 ternary resolvents (1 bin, 745 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-29] removed 122 variables
c [simpleprobe-5] 832 schedulable variables 2%
c [simpleprobe-5] limit 47469750 penalty 0 = 0 + 0
c [decomp-30] removed 460 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 460 variables, found 46570 hbrs, 291 units
c [unhide-13] limit 2373487 with penalty 0 = 0 + 0
c [unhide-13-14] 4 units, 354 failed, 22671 tauts, 0 hbrs, 7494 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 486 transitive binary clauses
c [transred-9] found 5 units
c [cce-5] limit of 59337187 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 31
c [cce-5-1] eliminated 1 clauses out of 4 (25%) of length 30
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 29
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 28
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 27
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 26
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 25
c [cce-5-1] eliminated 2 clauses out of 5 (40%) of length 24
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 23
c [cce-5-1] eliminated 1 clauses out of 5 (20%) of length 22
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 21
c [cce-5-1] eliminated 1 clauses out of 5 (20%) of length 20
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 19
c [cce-5-1] eliminated 1 clauses out of 6 (17%) of length 18
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 17
c [cce-5-1] eliminated 1 clauses out of 8 (12%) of length 16
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 15
c [cce-5-1] eliminated 2 clauses out of 5 (40%) of length 14
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 13
c [cce-5-1] eliminated 1 clauses out of 6 (17%) of length 12
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 11
c [cce-5-1] eliminated 2 clauses out of 9 (22%) of length 10
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 9
c [cce-5-1] eliminated 1 clauses out of 20 (5%) of length 8
c [cce-5-1] eliminated 5 clauses out of 22 (23%) of length 7
c [cce-5-1] eliminated 72 clauses out of 1003 (7%) of length 6
c [cce-5-1] eliminated 1119 clauses out of 7493 (15%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1235 large clauses in 59337187 steps
c [cce-5-1] allowing another 29668593 steps for small clauses
c [cce-5-1] scheduling 226690 clauses = 124237 binary + 102453 ternary
c [cce-5-1] tried to eliminate 1432 small clauses 1%
c [cce-5-1] eliminated 255 binary clauses 0%
c [cce-5-1] eliminated 66 ternary clauses 0%
c [cce-5-1] eliminated 321 small clauses 0%
c [cce-5-1] eliminated 1616 small clauses in 59337190 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2851 covered clauses in round 1
c [cce-5] eliminated 2851 covered clauses in TOTAL during 1 rounds
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 38276 variables 100%
c [elim-12] limit of 237348750 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 523 variables 1% in round 1 in 22784741 steps
c [elim-12-1] backward subsumption/strengthening limit 22784700
c [elim-12-1-1] backward checking 3443 touched variables 9%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 22 and strengthened 127 clauses in 874321 steps
c [elim-12-1] rescheduled 345 variables 1% by backward subsumption
c [elim-12-2] eliminated 20 variables 0% in round 2 in 194032 steps
c [elim-12-2] backward subsumption/strengthening limit 194000
c [elim-12-2-1] backward checking 179 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 12 and strengthened 6 clauses in 111284 steps
c [elim-12-2] rescheduled 29 variables 0% by backward subsumption
c [elim-12-3] eliminated 6 variables 0% in round 3 in 69426 steps
c [elim-12-3] backward subsumption/strengthening limit 69400
c [elim-12-3-1] backward checking 40 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 2 and strengthened 3 clauses in 53369 steps
c [elim-12] incomplete 11 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 551 = 1% variables out of 38276 scheduled
c [bca-9] limit of 10000000 steps and 534450 added (scaled 2)
c [bca-9] 59643 out of 75452 literals actually usable 79%
c [bca-9] added 112 blocked clauses in 141067 steps
c [sweep-8] limit 1780115 penalty 1 = 1 + 0
c [sweep-8-1] 3716 pos 11.6% + 28268 neg 88.4% = 31984 sched 84.8% ret 5741
c [sweep-8-1] 1844835 steps 37 queries 5614.11 avg class size
c [sweep-8-1] 620 decisions 34 SAT calls 99.35 avg env size
c [sweep-8-1] 31685 variables remain 84% (6035 retained 16%)
c [decomp-31] removed 24 variables
c [sweep-8-1] removed 24 vars (0 failed, 2 eqs, 4 impls)
c [sweep-8] 24 < 1/1000 * 37725 = 37 considered unsuccessful
c [sweep-8] removed 24 vars in TOTAL (1 rounds, 36 queries)
c [sort-queue-13] sorted 37701 enqueued variables after 44414 conflicts
c [score-dist-13] active 0 (0%), one 27873 (74%), zero 9828 (26%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 1338 variables 3.4% (37701 remain 18%)
c [simplification-13] removed 15338 irredundant clauses 5.4% (266305 remain 23%)
c [simplification-13] maximum reduction of 5% = max (3%, 5%)
c [simplification-13] large reduction 5% >= 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 56414 (soft 46414 + delta 10000)
c [simplification-13] new conflict limit 46414 (hard 56414)
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   91.5   37700   266305     45722    9283   3285 147629   18   162   30  11%     14   86   12    9  129%
c i   91.6   37699   266305     45894    9443   3290 147629   18   164   30  11%     12   87   13    9  139%
c i   91.6   37696   266305     45895    9443   3290 147629   18   164   30  11%     12   87   13    9  138%
c i   91.9   37695   266305     46261    9758   3314 147642   17   163   30  11%      9   86   14    9  155%
c 
c [simplification-14] limit 46424 conflicts (hard 56414) hit after 46424 conflicts
c [quatres-10] found 17389 quaternary clauses 61% in total
c [quatres-10-1] removed 3 duplicate quaternary clauses
c [quatres-10-2] added 6 single-self-subsuming ternary resolvents
c [quatres-10-2] added 9 quaternary resolvents
c [ternres-10] limit 12278753 with penalty 0 = 0 + 0
c [ternres-10] all 37692 free variables schedulable
c [ternres-10] 390 ternary resolvents (0 bin, 390 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-32] removed 11 variables
c [treelook-5] limit 1227875 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 57577 literals 76%
c [treelook-5] scheduling used 943713 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1227875 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1239825 steps
c [treelook-5] 57538 literals remain 76%
c [treelook-5] 9156 variables remain to probed next time 24%
c [treelook-5] removed 5 variables, found 6678 hbrs
c [unhide-14] limit 2455750 with penalty 0 = 0 + 0
c [unhide-14-16] 3 units, 170 failed, 9879 tauts, 0 hbrs, 13874 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 383 transitive binary clauses
c [cce-6] limit of 61393767 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 29
c [cce-6-1] eliminated 2 clauses out of 20 (10%) of length 8
c [cce-6-1] eliminated 1 clauses out of 19 (5%) of length 7
c [cce-6-1] eliminated 1 clauses out of 940 (0%) of length 6
c [cce-6-1] eliminated 139 clauses out of 6365 (2%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 144 large clauses in 61393771 steps
c [cce-6-1] allowing another 30696885 steps for small clauses
c [cce-6-1] scheduling 138358 clauses = 120974 binary + 17384 ternary
c [cce-6-1] tried to eliminate 3195 small clauses 2%
c [cce-6-1] eliminated 715 binary clauses 1%
c [cce-6-1] eliminated 170 ternary clauses 1%
c [cce-6-1] eliminated 885 small clauses 1%
c [cce-6-1] eliminated 1037 small clauses in 61393772 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1181 covered clauses in round 1
c [cce-6] eliminated 1181 covered clauses in TOTAL during 1 rounds
c [cce-6] 1181 < 1/100 * 262798 = 2627 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 37571 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 309 variables 1% in round 1 in 22199530 steps
c [elim-13-1] backward subsumption/strengthening limit 22199500
c [elim-13-1-1] backward checking 2255 touched variables 6%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 7 and strengthened 71 clauses in 545739 steps
c [elim-13-1] rescheduled 165 variables 0% by backward subsumption
c [elim-13-2] eliminated 9 variables 0% in round 2 in 97495 steps
c [elim-13-2] backward subsumption/strengthening limit 97400
c [elim-13-2-1] backward checking 94 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 5 and strengthened 4 clauses in 88349 steps
c [elim-13-2] rescheduled 21 variables 0% by backward subsumption
c [elim-13-3] eliminated 2 variables 0% in round 3 in 164290 steps
c [elim-13-3] backward subsumption/strengthening limit 164200
c [elim-13-3-1] backward checking 8 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 2 and strengthened 3 clauses in 35845 steps
c [elim-13] incomplete 6 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 325 = 1% variables out of 37571 scheduled
c [elim-13] 325 < 1/100 * 37571 = 375 considered unsuccessful
c [bca-10] limit of 10000000 steps and 523400 added (scaled 2)
c [bca-10] 57539 out of 74494 literals actually usable 77%
c [bca-10] added 46 blocked clauses in 137582 steps
c [sort-queue-14] sorted 37246 enqueued variables after 46424 conflicts
c [score-dist-14] active 0 (0%), one 27675 (74%), zero 9571 (26%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 446 variables 1.2% (37246 remain 17%)
c [simplification-14] removed 5477 irredundant clauses 2.1% (260828 remain 22%)
c [simplification-14] maximum reduction of 2% = max (1%, 2%)
c [simplification-14] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-14] new conflict interval 22332
c [simplification-14] penalized conflict interval 22332 = 1 * 22332
c [simplification-14] hard conflict limit 79922 (soft 68756 + delta 11166)
c [simplification-14] new conflict limit 68756 (hard 79922)
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   95.8   37245   260828     46603    9843   3592 144536   17   164   30  10%      7   87   14    9  153%
c i   96.4   37242   260828     47579   10726   3627 144568   17   159   30  11%      7   81   18    9  197%
c i   96.4   37240   260828     47590   10734   3628 144569   17   159   30  11%      7   81   18    9  190%
c i   96.5   37239   260828     47655   10793   3632 144570   17   159   30  11%      7   80   16    9  169%
c i   97.0   37238   260828     48605   11655   3666 144592   16   152   30  11%      7   72   16    9  173%
c i   97.2   37237   260828     48969   11981   3683 144606   16   149   30  11%      5   69   14    9  144%
c i   97.3   37233   260828     49029   12037   3683 144607   16   149   30  11%      5   69   14    9  149%
c i   97.4   37231   260828     49183   12179   3686 144609   17   149   30  11%      4   69   19    9  200%
c i   97.5   37230   260828     49373   12346   3697 144611   17   147   30  11%      4   67   18    9  185%
c i   97.5   37226   260828     49435   12399   3701 144613   16   147   31  11%      3   67   16    9  173%
c i   97.6   37225   260828     49535   12484   3705 144619   16   147   31  11%      3   66   14    9  149%
c i   97.8   37223   260828     49972   12868   3725 144640   16   148   31  11%      3   67   16    9  167%
c i   97.8   37222   260828     50034   12924   3727 144642   16   147   31  11%      3   66   16    9  168%
c i   98.2   37194   260828     50621   13460   3749 144658   16   149   31  11%      3   67   16   10  164%
c i   98.6   37193   260828     51287   14067   3775 144675   16   153   31  11%      4   70   19   10  196%
c i   98.8   37192   260828     51484   14241   3783 144682   16   155   31  11%      3   73   19   10  195%
c i   99.6   37191   260828     52757   15396   3830 144715   17   151   32  11%      8   67   16   10  167%
c i   99.8   37190   260828     52991   15605   3836 144719   17   150   32  11%      7   66   18   10  178%
c i   99.9   37189   260828     53127   15737   3836 144719   17   150   32  11%      6   66   20   10  198%
c i  100.1   37188   260828     53489   16064   3853 144729   17   151   32  11%      4   66   20   10  200%
c i  100.1   37187   260828     53494   16065   3854 144731   17   151   32  11%      4   66   19   10  196%
c i  100.1   37180   260828     53495   16065   3854 144731   17   151   32  11%      4   66   19   10  195%
c i  100.7   37179   260828     54374   16836   3887 144767   17   146   33  12%      5   61   17   10  173%
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.0   37164   260828     54713   17151   3899 144772   18   147   33  12%      4   61   22   10  219%
c i  101.9   37160   260828     56048   18360   3942 144804   19   149   33  13%      9   62   29   10  277%
c i  102.8   37157   260828     57270   19482   3971 144831   20   149   33  14%      9   60   21   11  201%
c i  102.9   37156   260828     57420   19623   3977 144833   20   147   34  14%      8   59   21   11  196%
c i  104.6   37155   260828     60354   22280   4064 144891   24   159   36  15%     29   68   35   11  307%
c i  104.8   37154   260828     60671   22577   4070 144894   24   160   36  15%     21   68   30   11  266%
c i  104.9   37153   260828     60852   22746   4073 144895   25   160   36  15%     17   69   33   11  288%
c i  105.0   37152   260828     60938   22829   4073 144896   25   162   36  15%     16   70   33   12  286%
c i  105.5   37151   260828     61662   23491   4092 144908   27   167   36  16%     10   74   43   12  363%
c i  105.5   37150   260828     61663   23491   4092 144908   27   167   36  16%      9   74   43   12  361%
c i  105.5   37149   260828     61696   23519   4093 144910   27   167   36  16%      9   74   40   12  339%
c i  107.7   37084   260828     65495   26969   4188 144999   28   165   38  17%     40   68   31   13  240%
c i  107.8   37083   260828     65560   27028   4190 145000   28   167   38  17%     37   70   33   13  258%
c i  109.3   37078   260828     67892   29186   4228 145033   31   166   41  19%     22   67   40   14  292%
c 
c [simplification-15] limit 68778 conflicts (hard 79922) hit after 68778 conflicts
c [quatres-11] found 17641 quaternary clauses 55% in total
c [quatres-11-2] added 9 single-self-subsuming ternary resolvents
c [quatres-11-2] added 14 quaternary resolvents
c [ternres-11] limit 17047564 with penalty 0 = 0 + 0
c [ternres-11] all 37078 free variables schedulable
c [ternres-11] 285 ternary resolvents (2 bin, 283 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 532736 penalty 4 = 4 + 0
c [card-5] found 1333 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 532736 for elimination
c [card-5] 1333 out of 1333 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-5] limit 426189 penalty 3 = 3 + 0
c [gauss-5] extracted 16 xors of average arity 2.7
c [gauss-5] connected 43 occurrences of 38 variables (average 1.1)
c [gauss-5] limit 426189 penalty 3 = 3 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-34] removed 71 variables
c [basicprobe-5] limit 85237824 penalty 0 = 0 + 0
c [basicprobe-5-0] 5571 probes remain 15% after last round
c [basicprobe-5-0] 557 units = 536 failed (96%) + 21 lifted (4%)
c [basicprobe-5-0] removed 788 variables, found 141304 hbrs
c [bate-3] eliminated 1125 asymmetric tautologies during probing
c [unhide-15] limit 3409512 with penalty 0 = 0 + 0
c [unhide-15-18] 4 units, 204 failed, 26463 tauts, 0 hbrs, 142032 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 306 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 36053 variables 100%
c [block-5] limit of 21309456 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 139 blocked clauses
c [block-5] 139 < 1/100 * 245539 = 2455 considered unsuccessful
c [bca-11] limit of 10000000 steps and 490439 added (scaled 2)
c [bca-11] 47548 out of 72102 literals actually usable 66%
c [bca-11] added 46 blocked clauses in 133059 steps
c [sort-queue-15] sorted 36050 enqueued variables after 68778 conflicts
c [score-dist-15] active 0 (0%), one 27879 (77%), zero 8171 (23%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 1028 variables 2.8% (36050 remain 17%)
c [simplification-15] removed 16492 irredundant clauses 6.3% (244336 remain 21%)
c [simplification-15] maximum reduction of 6% = max (3%, 6%)
c [simplification-15] large reduction 6% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 80778 (soft 70778 + delta 10000)
c [simplification-15] new conflict limit 70778 (hard 80778)
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.8   36049   244336     69935   30756   5119 246893   33   169   46  19%     17   67   28   14  196%
c 
c [simplification-16] limit 70778 conflicts (hard 80778) hit after 70778 conflicts
c [quatres-12] found 16886 quaternary clauses 54% in total
c [quatres-12-1] removed 2 duplicate quaternary clauses
c [quatres-12-2] added 4 single-self-subsuming ternary resolvents
c [quatres-12-2] added 2 quaternary resolvents
c [ternres-12] limit 17434927 with penalty 0 = 0 + 0
c [ternres-12] all 36049 free variables schedulable
c [ternres-12] 404 ternary resolvents (0 bin, 404 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-35] removed 131 variables
c [simpleprobe-6] all 35919 free variables schedulable
c [simpleprobe-6] limit 69739709 penalty 0 = 0 + 0
c [decomp-36] removed 246 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 246 variables, found 40478 hbrs, 151 units
c [unhide-16] limit 3486985 with penalty 0 = 0 + 0
c [unhide-16-20] 4 units, 41 failed, 24046 tauts, 0 hbrs, 95910 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 388 transitive binary clauses
c [cce-7] limit of 43587318 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 75
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 74
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 73
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 68
c [cce-7-1] eliminated 1 clauses out of 19 (5%) of length 8
c [cce-7-1] eliminated 1 clauses out of 20 (5%) of length 7
c [cce-7-1] eliminated 9 clauses out of 889 (1%) of length 6
c [cce-7-1] eliminated 49 clauses out of 5969 (1%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 65 large clauses in 43587323 steps
c [cce-7-1] allowing another 21793661 steps for small clauses
c [cce-7-1] scheduling 201116 clauses = 114278 binary + 86838 ternary
c [cce-7-1] tried to eliminate 1167 small clauses 1%
c [cce-7-1] eliminated 157 binary clauses 0%
c [cce-7-1] eliminated 66 ternary clauses 0%
c [cce-7-1] eliminated 223 small clauses 0%
c [cce-7-1] eliminated 274 small clauses in 43587330 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 339 covered clauses in round 1
c [cce-7] eliminated 339 covered clauses in TOTAL during 1 rounds
c [cce-7] 339 < 1/100 * 239260 = 2392 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 35616 variables 100%
c [elim-14] limit of 174349273 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 678 variables 2% in round 1 in 19951016 steps
c [elim-14-1] backward subsumption/strengthening limit 19951000
c [elim-14-1-1] backward checking 4077 touched variables 11%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 24 and strengthened 110 clauses in 966139 steps
c [elim-14-1] rescheduled 311 variables 1% by backward subsumption
c [elim-14-2] eliminated 17 variables 0% in round 2 in 203890 steps
c [elim-14-2] backward subsumption/strengthening limit 203800
c [elim-14-2-1] backward checking 206 touched variables 1%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 19 and strengthened 10 clauses in 172505 steps
c [elim-14-2] rescheduled 55 variables 0% by backward subsumption
c [elim-14-3] eliminated 7 variables 0% in round 3 in 495603 steps
c [elim-14-3] backward subsumption/strengthening limit 495600
c [elim-14-3-1] backward checking 84 touched variables 0%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 5 and strengthened 0 clauses in 67460 steps
c [elim-14] incomplete 9 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 702 = 2% variables out of 35616 scheduled
c [bca-12] limit of 10000000 steps and 477032 added (scaled 2)
c [bca-12] 45852 out of 69830 literals actually usable 66%
c [bca-12] added 51 blocked clauses in 128777 steps
c [sweep-9] limit 1307619 penalty 2 = 2 + 0
c [sweep-9-1] 3460 pos 11.6% + 26252 neg 88.4% = 29712 sched 85.1% ret 5202
c [sweep-9-1] 1385643 steps 33 queries 4743.94 avg class size
c [sweep-9-1] 1052 decisions 30 SAT calls 161.93 avg env size
c [sweep-9-1] 29370 variables remain 84% (5542 retained 16%)
c [decomp-37] removed 8 variables
c [sweep-9-1] removed 8 vars (0 failed, 2 eqs, 5 impls)
c [sweep-9] 8 < 1/1000 * 34914 = 34 considered unsuccessful
c [sweep-9] removed 8 vars in TOTAL (1 rounds, 32 queries)
c [sort-queue-16] sorted 34906 enqueued variables after 70778 conflicts
c [score-dist-16] active 0 (0%), one 27111 (78%), zero 7795 (22%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 1143 variables 3.2% (34906 remain 16%)
c [simplification-16] removed 6767 irredundant clauses 2.8% (237569 remain 20%)
c [simplification-16] maximum reduction of 3% = max (3%, 3%)
c [simplification-16] geometric conflict interval increment 5583 = 22332 / 4
c [simplification-16] new conflict interval 27915
c [simplification-16] penalized conflict interval 27915 = 1 * 27915
c [simplification-16] hard conflict limit 112650 (soft 98693 + delta 13957)
c [simplification-16] new conflict limit 98693 (hard 112650)
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  122.2   34905   237569     71935   29852   5115 253248   33   170   44  19%     15   66   31   15  211%
c i  122.7   34903   237569     72774   30621   5135 253263   32   165   44  19%      8   61   23   15  151%
c i  123.3   34874   237569     73860   31589   5179 253289   33   162   44  20%      5   57   30   15  195%
c i  123.8   34873   237569     74614   32280   5198 253297   33   161   44  21%      3   54   36   16  231%
c i  125.2   34871   237569     76642   34169   5233 253323   36   169   45  22%     13   61   31   16  189%
c i  126.9   34868   237569     79282   36576   5290 253354   36   163   46  22%     22   52   32   17  190%
c i  127.1   34866   237569     79707   36968   5296 253362   36   161   46  22%     13   51   35   17  205%
c i  127.8   34865   237569     80702   37896   5314 253376   35   156   46  22%      7   45   28   17  159%
c i  127.9   34822   237569     80966   38134   5321 253377   35   158   46  22%      4   47   32   17  185%
c i  128.9   34821   237569     82516   39532   5347 253392   38   164   47  23%      7   52   40   18  218%
c i  131.7   34820   237569     86483   43206   5410 253442   39   159   52  24%     39   44   32   19  165%
c i  133.6   34790   237569     89197   45692   5451 253476   39   159   54  24%     23   42   39   20  192%
c i  136.0   34757   237569     92290   48518   5511 253516   41   167   54  25%     26   47   48   21  228%
c i  137.0   34752   237569     93699   49778   5540 253532   42   169   57  25%     10   48   36   22  168%
c i  139.1   34739   237569     96373   52232   5570 253559   47   177   59  26%     19   54   51   23  223%
c i  139.6   34738   237569     96935   52762   5572 253568   46   175   60  26%      9   52   47   23  206%
c 
c [simplification-17] limit 98693 conflicts (hard 112650) hit after 98694 conflicts
c [quatres-13] found 17170 quaternary clauses 51% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 4 single-self-subsuming ternary resolvents
c [quatres-13-2] added 13 quaternary resolvents
c [ternres-13] limit 23116880 with penalty 0 = 0 + 0
c [ternres-13] all 34738 free variables schedulable
c [ternres-13] 473 ternary resolvents (0 bin, 473 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-38] removed 169 variables
c [treelook-6] limit 2311688 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 53670 literals 77%
c [treelook-6] scheduling used 1078709 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 2311688 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 2326351 steps
c [treelook-6] 53265 literals remain 77%
c [treelook-6] 8070 variables remain to probed next time 23%
c [decomp-39] removed 2 variables
c [treelook-6] removed 150 variables, found 12875 hbrs
c [unhide-17] limit 2311688 with penalty 1 = 0 + 1
c [unhide-17-22] 0 units, 52 failed, 13656 tauts, 0 hbrs, 370924 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 340 transitive binary clauses
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 34531 variables 100%
c [elim-15] limit of 462337601 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 252 variables 1% in round 1 in 19109013 steps
c [elim-15-1] backward subsumption/strengthening limit 19109000
c [elim-15-1-1] backward checking 1459 touched variables 4%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 9 and strengthened 26 clauses in 392698 steps
c [elim-15-1] rescheduled 86 variables 0% by backward subsumption
c [elim-15-2] eliminated 8 variables 0% in round 2 in 83238 steps
c [elim-15-2] backward subsumption/strengthening limit 83200
c [elim-15-2-1] backward checking 86 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 3 and strengthened 7 clauses in 83178 steps
c [elim-15-2] rescheduled 19 variables 0% by backward subsumption
c [elim-15-3] eliminated 2 variables 0% in round 3 in 15839 steps
c [elim-15-3] backward subsumption/strengthening limit 15800
c [elim-15-3-1] backward checking 18 touched variables 0%
c [elim-15-3-1] incomplete backward checking 0 remain 0%
c [elim-15-3] subsumed 5 and strengthened 4 clauses in 15801 steps
c [elim-15] incomplete 11 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 262 = 1% variables out of 34531 scheduled
c [elim-15] 262 < 1/100 * 34531 = 345 considered unsuccessful
c [bca-13] limit of 10000000 steps and 462695 added (scaled 2)
c [bca-13] 40935 out of 68540 literals actually usable 60%
c [bca-13] added 39 blocked clauses in 141258 steps
c [sort-queue-17] sorted 34269 enqueued variables after 98694 conflicts
c [score-dist-17] active 0 (0%), one 26942 (79%), zero 7327 (21%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 469 variables 1.4% (34269 remain 16%)
c [simplification-17] removed 7129 irredundant clauses 3.0% (230440 remain 20%)
c [simplification-17] maximum reduction of 3% = max (1%, 3%)
c [simplification-17] geometric conflict interval increment 6978 = 27915 / 4
c [simplification-17] new conflict interval 34893
c [simplification-17] penalized conflict interval 34893 = 1 * 34893
c [simplification-17] hard conflict limit 151033 (soft 133587 + delta 17446)
c [simplification-17] new conflict limit 133587 (hard 151033)
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  147.3   34268   230440    101069   54436   5897 242877   51   172   66  30%     39   46   42   25  167%
c i  150.3   34266   230440    104623   57712   5950 242905   51   173   66  30%     30   45   50   26  190%
c i  150.6   34265   230440    105083   58123   5955 242918   49   170   66  29%     16   41   36   26  135%
c i  151.9   34264   230440    106625   59519   5977 242931   51   170   66  30%      6   40   49   27  181%
c i  151.9   33834   230440    106636   59528   5977 242932   50   170   66  30%      6   40   48   27  176%
c i  152.1   33833   230440    106910   59780   5981 242937   50   166   66  30%      2   36   43   27  158%
c -  154.6   33833   230440    109984   22961   6018 242965   54   172   34  32%     21   40   56   29  195%
c i  155.6   33832   230440    111387   24258   6034 242974   53   172   38  31%     41   39   59   29  203%
c i  156.4   33831   230440    112600   25381   6050 242983   51   173   39  29%     11   39   39   29  134%
c i  156.4   33823   230440    112681   25454   6051 242984   52   172   39  30%      9   39   53   29  181%
c i  157.0   33822   230440    113516   26214   6061 243001   50   170   39  29%      1   36   38   29  128%
c i  158.2   33821   230440    115325   27869   6087 243025   47   161   40  29%      4   26   30   30  102%
c i  159.4   33820   230440    117323   29692   6116 243047   46   157   42  29%      7   22   58   30  192%
c i  160.8   33816   230440    119452   31669   6134 243059   45   158   44  29%      8   21   46   31  152%
c i  161.4   33812   230440    120442   32556   6142 243070   47   165   45  29%      0   29   57   31  185%
c i  161.4   33810   230440    120443   32556   6142 243070   47   165   45  29%      0   29   57   31  184%
c i  164.8   33809   230440    125141   36842   6181 243108   49   160   49  30%     43   22   45   32  140%
c i  165.2   33808   230440    125689   37352   6188 243109   49   161   49  30%     21   22   52   32  159%
c i  169.0   33807   230440    130611   41804   6240 243152   54   167   54  33%     45   26   54   34  158%
c 
c [simplification-18] limit 133597 conflicts (hard 151033) hit after 133598 conflicts
c [quatres-14] found 17409 quaternary clauses 51% in total
c [quatres-14-1] removed 4 duplicate quaternary clauses
c [quatres-14-2] added 1 single-self-subsuming ternary resolvents
c [quatres-14-2] added 6 quaternary resolvents
c [ternres-14] limit 30334493 with penalty 0 = 0 + 0
c [ternres-14] all 33806 free variables schedulable
c [ternres-14] 164 ternary resolvents (0 bin, 164 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-40] removed 476 variables
c [basicprobe-6] limit 151672467 penalty 0 = 0 + 0
c [basicprobe-6-0] 5841 sched 18%, 641 failed, 20 lifted, 109379 hbrs
c [decomp-41] removed 996 variables
c [basicprobe-6-1] 7088 probes remain 22% after last round
c [basicprobe-6-1] 821 units = 797 failed (97%) + 24 lifted (3%)
c [basicprobe-6-1] removed 1218 variables, found 137177 hbrs
c [bate-4] eliminated 490 asymmetric tautologies during probing
c [unhide-18] limit 6066898 with penalty 0 = 0 + 0
c [unhide-18-25] 0 units, 89 failed, 37429 tauts, 0 hbrs, 512879 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 258 transitive binary clauses
c [bca-14] limit of 10000000 steps and 406973 added (scaled 2)
c [bca-14] 39440 out of 64892 literals actually usable 61%
c [bca-14] added 23 blocked clauses in 129119 steps
c [sort-queue-18] sorted 32445 enqueued variables after 133598 conflicts
c [score-dist-18] active 0 (0%), one 26763 (82%), zero 5682 (18%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 1361 variables 4.0% (32445 remain 15%)
c [simplification-18] removed 27871 irredundant clauses 12.1% (202569 remain 17%)
c [simplification-18] maximum reduction of 12% = max (4%, 12%)
c [simplification-18] large reduction 12% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 145598 (soft 135598 + delta 10000)
c [simplification-18] new conflict limit 135598 (hard 145598)
c 
c [simplification-19] limit 135598 conflicts (hard 145598) hit after 135600 conflicts
c [quatres-15] found 16427 quaternary clauses 50% in total
c [quatres-15-1] removed 3 duplicate quaternary clauses
c [quatres-15-2] added 2 single-self-subsuming ternary resolvents
c [quatres-15-2] added 1 quaternary resolvents
c [ternres-15] limit 30697949 with penalty 0 = 0 + 0
c [ternres-15] all 32445 free variables schedulable
c [ternres-15] 388 ternary resolvents (0 bin, 388 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-42] removed 12 variables
c [simpleprobe-7] all 32433 free variables schedulable
c [simpleprobe-7] limit 122791796 penalty 0 = 0 + 0
c [decomp-43] removed 89 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 89 variables, found 44041 hbrs, 34 units
c [unhide-19] limit 6139589 with penalty 0 = 0 + 0
c [unhide-19-29] 4 units, 11 failed, 38336 tauts, 0 hbrs, 291440 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 277 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 383724362 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 37
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 36
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 35
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 34
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 33
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 32
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 31
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 30
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 29
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 28
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 27
c [cce-8-1] eliminated 4 clauses out of 5 (80%) of length 26
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 25
c [cce-8-1] eliminated 4 clauses out of 5 (80%) of length 24
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 23
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 22
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 21
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 20
c [cce-8-1] eliminated 5 clauses out of 9 (56%) of length 19
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 18
c [cce-8-1] eliminated 5 clauses out of 10 (50%) of length 17
c [cce-8-1] eliminated 5 clauses out of 10 (50%) of length 16
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 15
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 14
c [cce-8-1] eliminated 5 clauses out of 11 (45%) of length 13
c [cce-8-1] eliminated 4 clauses out of 9 (44%) of length 12
c [cce-8-1] eliminated 9 clauses out of 15 (60%) of length 11
c [cce-8-1] eliminated 4 clauses out of 13 (31%) of length 10
c [cce-8-1] eliminated 7 clauses out of 22 (32%) of length 9
c [cce-8-1] eliminated 14 clauses out of 34 (41%) of length 8
c [cce-8-1] eliminated 9 clauses out of 38 (24%) of length 7
c [cce-8-1] eliminated 15 clauses out of 832 (2%) of length 6
c [cce-8-1] eliminated 63 clauses out of 5718 (1%) of length 5
c [cce-8-1] eliminated 1898 clauses out of 14230 (13%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 2106 large clauses in 134969650 steps
c [cce-8-1] allowing another 67484825 steps for small clauses
c [cce-8-1] scheduling 118903 clauses = 104852 binary + 14051 ternary
c [cce-8-1] tried to eliminate 52761 small clauses 44%
c [cce-8-1] eliminated 9698 binary clauses 9%
c [cce-8-1] eliminated 1911 ternary clauses 14%
c [cce-8-1] eliminated 11609 small clauses 10%
c [cce-8-1] eliminated 11638 small clauses in 383724362 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 13744 covered clauses in round 1
c [cce-8] eliminated 13744 covered clauses in TOTAL during 1 rounds
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 32326 variables 100%
c [elim-16] limit of 306979490 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 1451 variables 4% in round 1 in 13954772 steps
c [elim-16-1] backward subsumption/strengthening limit 13954700
c [elim-16-1-1] backward checking 8047 touched variables 25%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 24 and strengthened 145 clauses in 1347807 steps
c [elim-16-1] rescheduled 387 variables 1% by backward subsumption
c [elim-16-2] eliminated 38 variables 0% in round 2 in 479683 steps
c [elim-16-2] backward subsumption/strengthening limit 479600
c [elim-16-2-1] backward checking 311 touched variables 1%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 24 and strengthened 19 clauses in 159987 steps
c [elim-16-2] rescheduled 78 variables 0% by backward subsumption
c [elim-16-3] eliminated 7 variables 0% in round 3 in 58074 steps
c [elim-16-3] backward subsumption/strengthening limit 58000
c [elim-16-3-1] backward checking 61 touched variables 0%
c [elim-16-3-1] incomplete backward checking 0 remain 0%
c [elim-16-3] subsumed 8 and strengthened 0 clauses in 58001 steps
c [elim-16] incomplete 17 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 1496 = 5% variables out of 32326 scheduled
c [bca-15] limit of 10000000 steps and 368872 added (scaled 2)
c [bca-15] 38725 out of 61662 literals actually usable 63%
c [bca-15] added 30 blocked clauses in 118153 steps
c [sort-queue-19] sorted 30830 enqueued variables after 135600 conflicts
c [score-dist-19] active 0 (0%), one 25397 (82%), zero 5433 (18%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 1615 variables 5.0% (30830 remain 14%)
c [simplification-19] removed 19056 irredundant clauses 9.4% (183513 remain 16%)
c [simplification-19] maximum reduction of 9% = max (5%, 9%)
c [simplification-19] large reduction 9% >= 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 147600 (soft 137600 + delta 10000)
c [simplification-19] new conflict limit 137600 (hard 147600)
c 
c [simplification-20] limit 137600 conflicts (hard 147600) hit after 137600 conflicts
c [quatres-16] found 14994 quaternary clauses 50% in total
c [quatres-16-1] removed 4 duplicate quaternary clauses
c [quatres-16-2] added 7 quaternary resolvents
c [ternres-16] limit 31025588 with penalty 0 = 0 + 0
c [ternres-16] all 30830 free variables schedulable
c [ternres-16] 600 ternary resolvents (0 bin, 600 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-6] limit 387819 penalty 4 = 4 + 0
c [gauss-6] extracted 1 xors of average arity 3.0
c [gauss-6] connected 3 occurrences of 3 variables (average 1.0)
c [gauss-6] limit 387819 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-44] removed 1 variables
c [treelook-7] limit 3102558 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 46547 literals 75%
c [treelook-7] scheduling used 926017 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 3102558 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 3114394 steps
c [treelook-7] 46388 literals remain 75%
c [treelook-7] 6487 variables remain to probed next time 21%
c [treelook-7] removed 25 variables, found 10460 hbrs
c [unhide-20] limit 6205117 with penalty 0 = 0 + 0
c [unhide-20-33] 1 units, 4 failed, 16444 tauts, 0 hbrs, 79918 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 250 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 30786 variables 100%
c [block-6] limit of 19390992 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 15 blocked clauses
c [block-6] 15 < 1/100 * 182743 = 1827 considered unsuccessful
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 30786 variables 100%
c [elim-17] limit of 620511772 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 93 variables 0% in round 1 in 13613054 steps
c [elim-17-1] backward subsumption/strengthening limit 13613000
c [elim-17-1-1] backward checking 779 touched variables 3%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 2 and strengthened 8 clauses in 212089 steps
c [elim-17-1] rescheduled 33 variables 0% by backward subsumption
c [elim-17-2] no variable eliminated in round 2 in 15041 steps
c [elim-17] fully completed in 2 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 93 = 0% variables out of 30786 scheduled
c [elim-17] 93 < 1/100 * 30786 = 307 considered unsuccessful
c [bca-16] limit of 10000000 steps and 366537 added (scaled 2)
c [bca-16] 38315 out of 61388 literals actually usable 62%
c [bca-16] added 18 blocked clauses in 118530 steps
c [sweep-10] limit 1163459 penalty 3 = 3 + 0
c [sweep-10-1] 2712 pos 10.2% + 23777 neg 89.8% = 26489 sched 86.3% ret 4204
c [sweep-10-1] 1317242 steps 24 queries 4072.62 avg class size
c [sweep-10-1] 1156 decisions 23 SAT calls 181.65 avg env size
c [sweep-10-1] 26220 variables remain 85% (4473 retained 15%)
c [decomp-46] removed 2 variables
c [sweep-10-1] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-10] 2 < 1/1000 * 30693 = 30 considered unsuccessful
c [sweep-10] removed 2 vars in TOTAL (1 rounds, 23 queries)
c [sort-queue-20] sorted 30691 enqueued variables after 137600 conflicts
c [score-dist-20] active 0 (0%), one 25302 (82%), zero 5389 (18%)
c [score-dist-20] max exp 1, different 2 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 139 variables 0.5% (30691 remain 14%)
c [simplification-20] removed 1178 irredundant clauses 0.6% (182335 remain 15%)
c [simplification-20] maximum reduction of 1% = max (0%, 1%)
c [simplification-20] geometric conflict interval increment 17446 = 34893 / 2
c [simplification-20] new conflict interval 52339
c [simplification-20] penalized conflict interval 52339 = 1 * 52339
c [simplification-20] hard conflict limit 216108 (soft 189939 + delta 26169)
c [simplification-20] new conflict limit 189939 (hard 216108)
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  202.3   30690   182335    138025   35625   7672 292505   48   149   46  32%     80    7   50   36  139%
c i  202.7   30687   182335    138689   36249   7676 292508   44   144   46  31%     34    2   27   36   75%
c i  203.1   30686   182335    139479   36973   7685 292515   44   145   46  31%      8    3   41   36  115%
c i  205.1   30607   182335    143312   40490   7747 292543   38   119   46  32%     24  -23   32   36   90%
c i  206.2   30606   182335    145034   42038   7771 292564   42   130   47  33%      1  -12   47   36  130%
c i  210.8   30580   182335    151766   48164   7836 292610   51   144   58  35%     66    3   43   38  113%
c i  212.0   30572   182335    153842   50098   7851 292622   38   105   60  37%      6  -36   14   37   38%
c i  212.0   30571   182335    153895   50147   7851 292625   38   103   60  37%      5  -37   12   37   33%
c i  212.2   30570   182335    154200   50400   7854 292627   41   110   62  37%     -2  -30   59   37  159%
c i  212.5   30568   182335    154599   50768   7857 292629   41   111   62  37%     -8  -28   46   37  124%
c i  218.0   30565   182335    162690   58170   7925 292666   48   131   67  37%     83   -5   60   38  158%
c i  218.6   30563   182335    163376   58805   7930 292672   48   136   70  36%     32   -0   49   38  129%
c -  222.6   30563   182335    168900   28743   7984 292709   54   136   34  40%     42    1   68   39  173%
c i  225.8   30562   182335    173803   33172   8022 292734   54   142   42  38%    112    7   52   40  130%
c i  228.4   30561   182335    178490   37477   8046 292755   41   104   46  39%     23  -30   49   40  123%
c i  228.5   30558   182335    178565   37551   8046 292755   41   104   46  39%     19  -30   48   40  120%
c i  232.8   30545   182335    184503   42867   8095 292791   60   151   54  40%     40   18   57   42  137%
c i  233.7   30544   182335    185663   43873   8109 292797   63   155   54  41%     -5   21   82   42  194%
c i  234.9   30543   182335    187129   45185   8123 292798   62   151   54  41%    -18   17   59   43  138%
c i  234.9   30542   182335    187137   45188   8124 292800   62   151   54  41%    -18   17   57   43  134%
c i  235.2   30394   182335    187476   45456   8129 292802   64   153   54  42%    -23   19   76   43  176%
c 
c [simplification-21] limit 189940 conflicts (hard 216108) hit after 190700 conflicts
c [quatres-17] found 15009 quaternary clauses 49% in total
c [quatres-17-1] removed 2 duplicate quaternary clauses
c [quatres-17-2] added 2 quaternary resolvents
c [ternres-17] limit 39937211 with penalty 0 = 0 + 0
c [ternres-17] all 30394 free variables schedulable
c [ternres-17] 139 ternary resolvents (1 bin, 138 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 1248037 penalty 4 = 4 + 0
c [card-6] found 1971 at-most-one constraints of average size 3.9
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1248037 for elimination
c [card-6] 1971 out of 1971 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-47] removed 306 variables
c [basicprobe-7] limit 199686057 penalty 0 = 0 + 0
c [basicprobe-7-0] 7309 sched 25%, 435 failed, 40 lifted, 42580 hbrs
c [decomp-48] removed 773 variables
c [basicprobe-7-1] 1661 probes remain 6% after last round
c [basicprobe-7-1] 687 units = 637 failed (93%) + 50 lifted (7%)
c [basicprobe-7-1] removed 1057 variables, found 64107 hbrs
c [bate-5] eliminated 192 asymmetric tautologies during probing
c [unhide-21] limit 7987442 with penalty 0 = 0 + 0
c [unhide-21-38] 3 units, 73 failed, 29078 tauts, 0 hbrs, 775687 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 246 transitive binary clauses
c [cce-9] limit of 99843028 steps penalty 1 = 1 + 0
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 2 clauses out of 3 (67%) 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 2 (50%) of length 39
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 38
c [cce-9-1] eliminated 1 clauses out of 7 (14%) of length 11
c [cce-9-1] eliminated 5 clauses out of 19 (26%) of length 10
c [cce-9-1] eliminated 3 clauses out of 16 (19%) of length 9
c [cce-9-1] eliminated 2 clauses out of 27 (7%) of length 8
c [cce-9-1] eliminated 7 clauses out of 51 (14%) of length 7
c [cce-9-1] eliminated 14 clauses out of 773 (2%) of length 6
c [cce-9-1] eliminated 62 clauses out of 5189 (1%) of length 5
c [cce-9-1] eliminated 175 clauses out of 12443 (1%) of length 4
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 278 large clauses in 99843028 steps
c [cce-9-1] allowing another 49921514 steps for small clauses
c [cce-9-1] scheduling 134749 clauses = 88554 binary + 46195 ternary
c [cce-9-1] tried to eliminate 7628 small clauses 6%
c [cce-9-1] eliminated 992 binary clauses 1%
c [cce-9-1] eliminated 292 ternary clauses 1%
c [cce-9-1] eliminated 1284 small clauses 1%
c [cce-9-1] eliminated 1297 small clauses in 99843038 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 1575 covered clauses in round 1
c [cce-9] eliminated 1575 covered clauses in TOTAL during 1 rounds
c [cce-9] 1575 < 1/100 * 164841 = 1648 considered unsuccessful
c [bca-17] limit of 10000000 steps and 328402 added (scaled 2)
c [bca-17] 34917 out of 58514 literals actually usable 60%
c [bca-17] added 29 blocked clauses in 121870 steps
c [sort-queue-21] sorted 29256 enqueued variables after 190700 conflicts
c [score-dist-21] active 0 (0%), one 24853 (85%), zero 4403 (15%)
c [score-dist-21] max exp 1, different 2 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 1138 variables 3.7% (29256 remain 14%)
c [simplification-21] removed 19069 irredundant clauses 10.5% (163266 remain 14%)
c [simplification-21] maximum reduction of 10% = max (4%, 10%)
c [simplification-21] large reduction 10% >= 5% limit
c [simplification-21] next conflict interval 2000 = 2000/1
c [simplification-21] penalized conflict interval 2000 = 1 * 2000
c [simplification-21] hard conflict limit 202700 (soft 192700 + delta 10000)
c [simplification-21] new conflict limit 192700 (hard 202700)
c 
c [simplification-22] limit 192700 conflicts (hard 202700) hit after 192700 conflicts
c [quatres-18] found 14471 quaternary clauses 48% in total
c [quatres-18-1] removed 6 duplicate quaternary clauses
c [quatres-18-2] added 2 single-self-subsuming ternary resolvents
c [quatres-18-2] added 6 quaternary resolvents
c [ternres-18] limit 40261372 with penalty 0 = 0 + 0
c [ternres-18] all 29256 free variables schedulable
c [ternres-18] 156 ternary resolvents (0 bin, 156 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-49] removed 33 variables
c [simpleprobe-8] all 29223 free variables schedulable
c [simpleprobe-8] limit 161045490 penalty 0 = 0 + 0
c [decomp-50] removed 63 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 63 variables, found 26298 hbrs, 27 units
c [unhide-22] limit 8052274 with penalty 0 = 0 + 0
c [unhide-22-43] 0 units, 21 failed, 32218 tauts, 0 hbrs, 243770 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 216 transitive binary clauses
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 29149 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 738 variables 3% in round 1 in 11565415 steps
c [elim-18-1] backward subsumption/strengthening limit 11565400
c [elim-18-1-1] backward checking 4314 touched variables 15%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 9 and strengthened 66 clauses in 721991 steps
c [elim-18-1] rescheduled 181 variables 1% by backward subsumption
c [elim-18-2] eliminated 8 variables 0% in round 2 in 99046 steps
c [elim-18-2] backward subsumption/strengthening limit 99000
c [elim-18-2-1] backward checking 115 touched variables 0%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 3 and strengthened 5 clauses in 54225 steps
c [elim-18-2] rescheduled 18 variables 0% by backward subsumption
c [elim-18-3] eliminated 3 variables 0% in round 3 in 22475 steps
c [elim-18-3] backward subsumption/strengthening limit 22400
c [elim-18-3-1] backward checking 24 touched variables 0%
c [elim-18-3-1] incomplete backward checking 0 remain 0%
c [elim-18-3] subsumed 0 and strengthened 0 clauses in 22401 steps
c [elim-18] fully completed in 3 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 749 = 3% variables out of 29149 scheduled
c [bca-18] limit of 10000000 steps and 324963 added (scaled 2)
c [bca-18] 34265 out of 56802 literals actually usable 60%
c [bca-18] added 31 blocked clauses in 114489 steps
c [sort-queue-22] sorted 28400 enqueued variables after 192700 conflicts
c [score-dist-22] active 0 (0%), one 24201 (85%), zero 4199 (15%)
c [score-dist-22] max exp 1, different 2 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 856 variables 2.9% (28400 remain 13%)
c [simplification-22] removed 1727 irredundant clauses 1.1% (161539 remain 14%)
c [simplification-22] maximum reduction of 3% = max (3%, 1%)
c [simplification-22] geometric conflict interval increment 13084 = 52339 / 4
c [simplification-22] new conflict interval 65423
c [simplification-22] penalized conflict interval 65423 = 1 * 65423
c [simplification-22] hard conflict limit 290834 (soft 258123 + delta 32711)
c [simplification-22] new conflict limit 258123 (hard 290834)
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  269.7   28399   161539    206269   52004   7617 275404   43   107   59  40%    216  -25   57   44  129%
c i  269.9   28397   161539    206539   52243   7619 275407   44   108   60  40%    151  -24   52   44  117%
c i  273.3   28390   161539    212234   57462   7663 275434   33    77   63  42%     10  -52   20   43   47%
c i  273.8   28384   161539    213002   58178   7668 275441   31    73   66  42%    -25  -56   22   43   51%
c i  278.4   28382   161539    219591   63976   7686 275455   36    66   72  55%     26  -57   64   42  151%
c i  278.4   28381   161539    219592   63976   7686 275455   36    66   72  55%     25  -57   64   42  151%
c i  278.4   28368   161539    219593   63976   7686 275455   36    66   72  55%     25  -57   63   42  150%
c -  278.9   28362   161539    220059   31336   7690 275458   39    74   33  52%     -5  -48   67   42  159%
c i  284.7   28361   161539    230283   40819   7731 275499   25    56   46  45%     87  -61   19   41   46%
c i  287.6   28360   161539    235102   45140   7767 275528   40    92   51  43%     -3  -22   51   41  124%
c i  287.6   28359   161539    235103   45140   7767 275528   40    92   51  43%     -3  -22   51   41  123%
c i  299.0   28356   161539    251838   59920   7878 275602   51   106   83  48%    168   -4   54   43  127%
c i  302.0   28355   161539    256231   63849   7909 275614   51   105   88  48%    -21   -4   36   43   84%
c i  303.2   28351   161539    257764   65198   7923 275631   50   104   88  48%    -52   -5   64   43  149%
c -  304.9   28259   161539    260279   34515   7941 275641   44    87   49  50%    -47  -21   37   43   87%
c i  305.6   28258   161539    261658   35746   7947 275649   42    80   56  53%    -28  -28   52   43  123%
c i  305.6   28257   161539    261659   35746   7947 275649   42    80   56  53%    -28  -28   52   43  122%
c i  310.9   27589   161539    271771   44913   8002 275697   43    91   65  48%     69  -15   52   43  121%
c i  315.0   27489   161539    279172   51520   8038 275735   38    73   70  52%     28  -30   41   42   98%
c i  315.0   27488   161539    279176   51523   8038 275735   38    73   70  52%     27  -30   41   42   96%
c i  316.2   27487   161539    280752   52917   8051 275738   45    90   71  50%    -38  -13   59   43  138%
c i  316.2   27486   161539    280755   52919   8051 275738   45    90   71  50%    -38  -13   58   43  137%
c i  321.8   27258   161539    290017   61241   8106 275769   35    71   78  49%     58  -29   21   42   51%
c 
c [simplification-23] limit 258168 conflicts (hard 290834) hit after 290837 conflicts
c [quatres-19] found 12928 quaternary clauses 47% in total
c [quatres-19-1] removed 1 duplicate quaternary clauses
c [quatres-19-2] added 3 single-self-subsuming ternary resolvents
c [quatres-19-2] added 18 quaternary resolvents
c [ternres-19] limit 55239367 with penalty 0 = 0 + 0
c [ternres-19] all 27255 free variables schedulable
c [ternres-19] 220 ternary resolvents (0 bin, 220 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-51] removed 1260 variables
c [treelook-8] limit 5523936 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 38303 literals 71%
c [treelook-8] scheduling used 759166 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 5523936 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 5552135 steps
c [treelook-8] 37953 literals remain 70%
c [treelook-8] 4797 variables remain to probed next time 18%
c [treelook-8] removed 11 variables, found 20273 hbrs
c [unhide-23] limit 5523936 with penalty 1 = 0 + 1
c [unhide-23-47] 2 units, 295 failed, 18385 tauts, 0 hbrs, 981351 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 266 transitive binary clauses
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 26765 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 618 variables 2% in round 1 in 10013857 steps
c [elim-19-1] backward subsumption/strengthening limit 10013800
c [elim-19-1-1] backward checking 3270 touched variables 12%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 10 and strengthened 24 clauses in 550885 steps
c [elim-19-1] rescheduled 120 variables 0% by backward subsumption
c [elim-19-2] eliminated 1 variables 0% in round 2 in 40853 steps
c [elim-19-2] backward subsumption/strengthening limit 40800
c [elim-19-2-1] backward checking 45 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 27074 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 619 = 2% variables out of 26765 scheduled
c [bca-19] limit of 10000000 steps and 289462 added (scaled 2)
c [bca-19] 30429 out of 52294 literals actually usable 58%
c [bca-19] added 16 blocked clauses in 118054 steps
c [sort-queue-23] sorted 26146 enqueued variables after 290837 conflicts
c [score-dist-23] active 0 (0%), one 22842 (87%), zero 3304 (13%)
c [score-dist-23] max exp 1, different 2 (100%)
c [score-dist-23] median active exp 0, avg 0.0
c [simplification-23] removed 1109 variables 4.1% (26146 remain 12%)
c [simplification-23] removed 17758 irredundant clauses 11.0% (143781 remain 12%)
c [simplification-23] maximum reduction of 11% = max (4%, 11%)
c [simplification-23] large reduction 11% >= 5% limit
c [simplification-23] next conflict interval 2908 = min (290837/100, 65423)
c [simplification-23] penalized conflict interval 2908 = 1 * 2908
c [simplification-23] hard conflict limit 303745 (soft 293745 + delta 10000)
c [simplification-23] new conflict limit 293745 (hard 303745)
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  331.3   26145   143781    294059   54818   7505 236403   40    84   58  47%    -19  -15   42   42   99%
c i  331.4   26140   143781    294115   54871   7505 236403   39    84   58  47%    -22  -15   37   42   88%
c i  333.0   26139   143781    296901   57478   7520 236414   41    93   58  44%    -36   -5   42   42  101%
c 
c [simplification-24] limit 293745 conflicts (hard 303745) hit after 303746 conflicts
c [quatres-20] found 13879 quaternary clauses 46% in total
c [quatres-20-1] removed 18 duplicate quaternary clauses
c [quatres-20-2] added 8 single-self-subsuming ternary resolvents
c [quatres-20-2] added 9 quaternary resolvents
c [ternres-20] limit 56992632 with penalty 0 = 0 + 0
c [ternres-20] all 26139 free variables schedulable
c [ternres-20] 1054 ternary resolvents (0 bin, 1054 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-53] removed 10 variables
c [basicprobe-8] limit 284963161 penalty 0 = 0 + 0
c [basicprobe-8-0] 2016 sched 8%, 177 failed, 2 lifted, 8435 hbrs
c [decomp-54] removed 479 variables
c [basicprobe-8-1] 9672 sched 38%, 297 failed, 19 lifted, 22981 hbrs
c [decomp-55] removed 478 variables
c [basicprobe-8-2] 9424 sched 38%, 125 failed, 0 lifted, 10723 hbrs
c [decomp-56] removed 185 variables
c [basicprobe-8-3] 9417 sched 38%, 85 failed, 2 lifted, 3164 hbrs
c [decomp-57] removed 119 variables
c [basicprobe-8-4] 6830 probes remain 27% after last round
c [basicprobe-8-4] 718 units = 695 failed (97%) + 23 lifted (3%)
c [basicprobe-8-4] removed 1274 variables, found 45673 hbrs
c [bate-6] eliminated 343 asymmetric tautologies during probing
c [unhide-24] limit 5699263 with penalty 1 = 0 + 1
c [unhide-24-50] 0 units, 19 failed, 20322 tauts, 0 hbrs, 739309 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 327 transitive binary clauses
c [cce-10] limit of 71240790 steps penalty 2 = 2 + 0
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 17
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 15
c [cce-10-1] eliminated 3 clauses out of 6 (50%) of length 14
c [cce-10-1] eliminated 2 clauses out of 10 (20%) of length 13
c [cce-10-1] eliminated 4 clauses out of 13 (31%) of length 11
c [cce-10-1] eliminated 7 clauses out of 23 (30%) of length 10
c [cce-10-1] eliminated 8 clauses out of 22 (36%) of length 9
c [cce-10-1] eliminated 9 clauses out of 39 (23%) of length 8
c [cce-10-1] eliminated 11 clauses out of 58 (19%) of length 7
c [cce-10-1] eliminated 13 clauses out of 497 (3%) of length 6
c [cce-10-1] eliminated 38 clauses out of 4499 (1%) of length 5
c [cce-10-1] eliminated 327 clauses out of 10911 (3%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 424 large clauses in 63881848 steps
c [cce-10-1] allowing another 31940924 steps for small clauses
c [cce-10-1] scheduling 85491 clauses = 74778 binary + 10713 ternary
c [cce-10-1] tried to eliminate 11765 small clauses 14%
c [cce-10-1] eliminated 1401 binary clauses 2%
c [cce-10-1] eliminated 319 ternary clauses 3%
c [cce-10-1] eliminated 1720 small clauses 2%
c [cce-10-1] eliminated 1720 small clauses in 71240790 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 2144 covered clauses in round 1
c [cce-10] eliminated 2144 covered clauses in TOTAL during 1 rounds
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 24861 variables 100%
c [elim-20] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 680 variables 3% in round 1 in 8679913 steps
c [elim-20-1] backward subsumption/strengthening limit 8679900
c [elim-20-1-1] backward checking 4019 touched variables 16%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 3 and strengthened 79 clauses in 615522 steps
c [elim-20-1] rescheduled 193 variables 1% by backward subsumption
c [elim-20-2] eliminated 10 variables 0% in round 2 in 83461 steps
c [elim-20-2] backward subsumption/strengthening limit 83400
c [elim-20-2-1] backward checking 116 touched variables 0%
c [elim-20-2-1] fully completed backward checking in 1 rounds
c [elim-20-2] subsumed 11 and strengthened 5 clauses in 51439 steps
c [elim-20-2] rescheduled 36 variables 0% by backward subsumption
c [elim-20-3] eliminated 1 variables 0% in round 3 in 20643 steps
c [elim-20-3] backward subsumption/strengthening limit 20600
c [elim-20-3-1] backward checking 14 touched variables 0%
c [elim-20-3-1] incomplete backward checking 0 remain 0%
c [elim-20-3] subsumed 1 and strengthened 0 clauses in 20601 steps
c [elim-20] incomplete 3 not tried 0% in round 3
c [elim-20] transition to [ all 1 rem 1 ] state
c [elim-20] eliminated 691 = 3% variables out of 24861 scheduled
c [bca-20] limit of 10000000 steps and 256488 added (scaled 2)
c [bca-20] 27690 out of 48342 literals actually usable 57%
c [bca-20] added 21 blocked clauses in 106480 steps
c [sort-queue-24] sorted 24170 enqueued variables after 303746 conflicts
c [score-dist-24] active 0 (0%), one 21929 (91%), zero 2241 (9%)
c [score-dist-24] max exp 1, different 2 (100%)
c [score-dist-24] median active exp 0, avg 0.0
c [simplification-24] removed 1969 variables 7.5% (24170 remain 11%)
c [simplification-24] removed 16491 irredundant clauses 11.5% (127290 remain 11%)
c [simplification-24] maximum reduction of 11% = max (8%, 11%)
c [simplification-24] large reduction 11% >= 5% limit
c [simplification-24] next conflict interval 3037 = min (303746/100, 65423)
c [simplification-24] penalized conflict interval 3037 = 1 * 3037
c [simplification-24] hard conflict limit 316783 (soft 306783 + delta 10000)
c [simplification-24] new conflict limit 306783 (hard 316783)
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  359.9   24169   127290    310078   51618   7974 210613   36    78   47  46%    118  -19   19   41   47%
c i  359.9   24167   127290    310158   51692   7974 210613   35    77   47  46%    103  -20   18   41   43%
c i  360.4   24166   127290    310961   52390   7983 210620   35    76   47  46%     11  -21   19   41   46%
c 
c [simplification-25] limit 306783 conflicts (hard 316783) hit after 316783 conflicts
c [quatres-21] found 13136 quaternary clauses 46% in total
c [quatres-21-1] removed 4 duplicate quaternary clauses
c [quatres-21-2] added 19 quaternary resolvents
c [ternres-21] limit 58647953 with penalty 0 = 0 + 0
c [ternres-21] all 24098 free variables schedulable
c [ternres-21] 637 ternary resolvents (0 bin, 637 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-58] removed 73 variables
c [simpleprobe-9] all 24097 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-59] removed 63 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 63 variables, found 18223 hbrs, 3 units
c [unhide-25] limit 11729590 with penalty 0 = 0 + 0
c [unhide-25-58] 0 units, 2 failed, 26885 tauts, 0 hbrs, 595737 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 357 transitive binary clauses
c [elim-21] no untried remaining variables left
c [elim-21] scheduled 24012 variables 100%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 151 variables 1% in round 1 in 8393062 steps
c [elim-21-1] backward subsumption/strengthening limit 8393000
c [elim-21-1-1] backward checking 1193 touched variables 5%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 0 and strengthened 8 clauses in 170462 steps
c [elim-21-1] rescheduled 32 variables 0% by backward subsumption
c [elim-21-2] eliminated 1 variables 0% in round 2 in 14598 steps
c [elim-21-2] backward subsumption/strengthening limit 14500
c [elim-21-2-1] backward checking 16 touched variables 0%
c [elim-21-2-1] incomplete backward checking 0 remain 0%
c [elim-21-2] subsumed 0 and strengthened 2 clauses in 14501 steps
c [elim-21-2] rescheduled 8 variables 0% by backward subsumption
c [elim-21-3] eliminated 1 variables 0% in round 3 in 6749 steps
c [elim-21-3] backward subsumption/strengthening limit 6700
c [elim-21-3-1] backward checking 10 touched variables 0%
c [elim-21-3-1] incomplete backward checking 3 remain 30%
c [elim-21-3] subsumed 0 and strengthened 2 clauses in 6721 steps
c [elim-21] incomplete 8 not tried 0% in round 3
c [elim-21] transition to [ all 1 rem 1 ] state
c [elim-21] eliminated 153 = 1% variables out of 24012 scheduled
c [elim-21] 153 < 1/100 * 24012 = 240 considered unsuccessful
c [bca-21] limit of 10000000 steps and 250813 added (scaled 2)
c [bca-21] 26582 out of 47720 literals actually usable 56%
c [bca-21] added 23 blocked clauses in 109981 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 10996490 penalty 4 = 4 + 0
c [sweep-11-1] 2322 pos 11.1% + 18548 neg 88.9% = 20870 sched 87.5% ret 2989
c [sweep-11-1] 11008210 steps 240 queries 534.85 avg class size
c [sweep-11-1] 8277 decisions 237 SAT calls 196.48 avg env size
c [sweep-11-1] 16725 variables remain 70% (7131 retained 30%)
c [decomp-60] removed 23 variables
c [sweep-11-1] removed 23 vars (0 failed, 7 eqs, 17 impls)
c [sweep-11] removed 23 vars in TOTAL (1 rounds, 239 queries)
c [sort-queue-25] sorted 23836 enqueued variables after 316783 conflicts
c [score-dist-25] active 0 (0%), one 21874 (92%), zero 1962 (8%)
c [score-dist-25] max exp 1, different 2 (100%)
c [score-dist-25] median active exp 0, avg 0.0
c [simplification-25] removed 262 variables 1.1% (23836 remain 11%)
c [simplification-25] removed 2904 irredundant clauses 2.3% (124386 remain 11%)
c [simplification-25] maximum reduction of 2% = max (1%, 2%)
c [simplification-25] geometric conflict interval increment 21807 = 65423 / 3
c [simplification-25] new conflict interval 87230
c [simplification-25] penalized conflict interval 87230 = 1 * 87230
c [simplification-25] hard conflict limit 447628 (soft 404013 + delta 43615)
c [simplification-25] new conflict limit 404013 (hard 447628)
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  376.1   23835   124386    322835   57269   8267 200764   40    82   52  49%     94  -11   14   41   34%
c i  376.8   23638   124386    324129   58486   8273 200767   35    71   52  48%    -19  -22   15   40   37%
c i  381.3   23637   124386    332227   65928   8301 200786   36    69   53  52%     37  -20   58   39  146%
c i  381.3   23629   124386    332271   65949   8301 200788   36    69   53  52%     32  -21   50   39  127%
c -  382.3   23593   124386    333987   34319   8314 200796   32    61   30  53%    -40  -28   23   39   59%
c i  383.3   23592   124386    336100   36215   8325 200801   29    54   36  54%    -26  -34   26   38   67%
c i  383.4   22289   124386    336116   36220   8326 200804   29    54   36  54%    -26  -34   24   38   64%
c i  383.4   21960   124386    336119   36222   8326 200804   29    54   36  54%    -26  -34   24   38   63%
c i  383.4   21817   124386    336125   36224   8326 200807   29    54   36  54%    -27  -34   24   38   62%
c i  383.4   19630   124386    336126   36224   8326 200807   29    54   36  54%    -27  -34   24   38   61%
c i  383.4   19561   124386    336128   36225   8326 200807   29    54   36  54%    -27  -34   23   38   61%
c 0  383.4   18922   124386    336128   36225   8326 200807   29    54   36  54%    -27  -34   23   38   61%
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 
s UNSATISFIABLE
c
c bate: 2454 basic ate = 2312 trn 94% + 142 lrg 6% in 6 updates
c bcas: 21 count, 2861 added (811 skipped), 3950257 steps
c bkwd: tried 524233 clauses, 1047051 lits, 2.00 lits/clause
c bkwd: checked 14185691 occs, 27.06 occs/clause, 13.55 occs/lit
c bkwd: subsumed 57 binary, 431 ternary, 157 large
c bkwd: strengthened 13 binary, 2 ternary (100% self), 2046 large (0% self)
c blkd: 6 bces, 7671 removed, 7105120 resolutions, 19970010 steps
c blkd: 10755 blocking literals 2%, 10 pure
c bump: 335786 bumped seen, 118404936 lits 352.6 on average
c card: 6 count, 0 units, 0 am1, 76130957 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 74185 subsumed
c card: 16517 at-most-one constraints found, average size 4.78
c card: 16517 at-most-one constraints used 100%, average size 4.78
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: 10 cces, 52667 eliminated, 52344 ate 99%, 323 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: 4059127 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 194 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 60 decompositions, 7860 equivalent 4%
c deco: 15573 decision-only clauses 5%, 63% reduction
c decs: 4178038 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 21 elims, 95251 eliminated 42%, 260 pure 0%
c elms: 67 rounds, 3.2 rounds/bve
c elms: 81345 small 85%, 13636 large 14%
c elms: 258366 tried small, 81353 succeeded 31%, 177013 failed 69%
c elms: 35060 subsumed, 60037 strengthened, 2851 blocked
c elms: 22314063 copies, 21449899 resolutions, 7030700 ipos
c elms: 5138754 subchks, 3098554 strchks
c gaus: 6 extractions, 243 extracted, 2.6 size, 3 max
c gaus: exported 2 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12724696 steps, 6362348 extr 50%, 1762 elim 0%
c glue: 38.3 orig avg, 38.3 real avg, 4.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 889523 = 223880 simple 25% + 649164 trn 73% + 16479 lrg 2%, 4415 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 335786 clauses, 153.1 length
c lrnd: 51413009 lits = 79781379 orig - 28368370 removed 36%
c lrnd: 156998 uips 47%, 147192 flips 44%
c mins: 306803 mins 92%, 3800 bin 1%, 7584 size 2%
c mins: 152960240 poisoned searches, 31385823 hits, 21% hit rate
c mins: 188152798 used twice searches, 7052037 hits, 4% hit rate
c move: moved 31941, 21863 bin 68%, 10078 trn 32%
c otfs: 1000 driving 23%, 3364 restarting 77%
c otfs: str 4364, 4217 red 97%, 147 irr 3%
c otfs: str 4364, 0 bin 0%, 177 trn 4%, 4187 lrg 96%
c otfs: sub 11, 11 red 100%, 0 irr 0%
c otfs: sub 11, 0 bin 0%, 0 trn 0%, 11 lrg 100%
c phas: 10 computed, 156481 set, 0 pos (0%), 156481 neg (100%)
c prbs: 8 basic, 134387 probed, 3543 failed, 123 lifted
c prbs: 9 simple, 785816 probed, 852 failed, 1000 eqs
c prbs: 8 treelook, 677 probed, 42 failed, 0 lifted
c prom: 55551 locked 6% out of 997175 tried
c prps: 771087308 props, 167 props/dec
c prps: 91% srch, 9% simp, 0% lkhd
c quat: 21 count, 199 quat, 58 self1, 1 self2, 1090 dup
c queu: 25 sorted, 4178038 next (6 steps 0.00)
c queu: 119866315 enq (0 steps 0.00), 118404936 deq 99%
c redc: 9704 clauses 29%, 33048 tried 10%, 311 sat 1%
c redc: 23500 lits 6%, 375872 tried 0%, 311 sat 0%
c redc: 1414 times jump level reduced, 24.6 levels on average
c reds: 5 count, 67225.6 conflicts per reduce
c reds: 0 memlim 0%, 5 arith 100%
c reds: 130016 collected 75%, 43730 retired 25%
c rmbd: 43762 removed, 7188 red 16%
c rsts: 12284 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 25 count, 22 confs 88%, 0 vars 0%
c simp: 2 its 8%, 1 bin 4%, 0 trns 0%
c subl: 335786 count (370241 tried 1.1), 22454 sub out of 324247 (6.9%)
c swps: 11 count, 11 rounds, 818 queries (74.4/round)
c swps: 746 sat calls, 32 unsat (0.9% success rate)
c swps: 16043 decisions 21.5, 658 conflicts 0.9
c swps; 4093.4 avg class size, 120.8 avg environment size
c swps: 0 failed, 169 impls, 85 equivs
c swp0: 268 type 0 queries, 58 unsat (21.6%), 260 sat (97.0%)
c swp1: 550 type 1 queries, 305 unsat (55.5%), 473 sat (86.0%)
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: 9028784 calls to obtain time
c tops: 102536 fixed 46%, 663 its, 506.98 confs/it
c trds: 21 transitive reductions, 6307 removed, 48 failed
c trds: 39980 nodes, 117895 edges, 39565091 steps
c trim: 906091 words, 3.5 MB
c trnr: 21 count, 10 bin, 7280 trn, 133184885 steps
c unhd: 25 count, 58 rounds, 116948249 steps
c unhd: 1829 non-trivial sccs of average size 2.5
c unhd: 162 units, 162 bin, 0 trn, 0 lrg
c unhd: 8384 failed, 8313 stamp, 0 lits, 36 bin, 25 trn, 0 lrg
c unhd: 429746 tauts, 20898 bin 5%, 11340 trn 3%, 2494 lrg 1%
c unhd: 429746 tauts, 395014 stamp 92%, 353529 red 82%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 5022346 str, 162 bin 0%, 5416 trn 0%, 5016768 lrg 100%, 5002031 red 100%
c vars: 18922 remaining 8% and 205647 removed 92% out of 224569
c vars: 102536 fixed 46%, 95251 eliminated 42%, 7860 equivalent 4%
c vsts: 6768652991 visits, 90% srch, 10% simp, 0% lkhd
c vsts: 8.7 search visits per propagation, 18144.1 per conflict
c wchs: 1115854158 pushed, 45351003 enlarged, 279 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         324446        130016         43730      25441554       3137796        174429
c 
c  0 0         36999  11      6660   5         0   0  15087776  59   1313302  42     38565  22     1.3
c  1 5         12406   4      3777   3      1352   3   1767004   7<   229335   7     12011   7     0.7
c  2 6         31676  10     12275   9      3724   9   2496179  10    371828  12<    21813  13     2.4
c  3 9         36601  11     14967  12      4757  11   1918188   8    312303  10     20736  12     3.4
c  4 14        36907  11     17009  13      4971  11   1416954   6    258689   8     19054  11<    3.7
c  5 21        36322  11<    17307  13<     5158  12   1054947   4    218634   7     16679  10     3.8
c  6 30        33061  10     16527  13      5060  12<   715276   3    152778   5     13567   8     4.5
c  7 41        28171   9     14041  11      4497  10    409187   2    108965   3     11382   7     4.3
c  8 54        22587   7     11071   9      3859   9    202297   1     63405   2      7739   4     3.9
c  9 69        16130   5      7702   6      3066   7    206536   1     51937   2      5425   3     3.1
c 10 86        13810   4      5596   4      2787   6    119543   0     34640   1      4334   2     2.2
c 11 126       13746   4      2418   2      3006   7     39475   0     17416   1      2476   1     1.7
c 12 230        6012   2       665   1      1489   3      8171   0      4556   0       648   0     1.2
c 13 534          18   0         1   0         4   0        21   0         8   0         0   0     0.0
c 
c avg                  4.9           5.2           6.1           1.4           2.3           3.6
c std                  3.2           2.7           3.0           2.2           2.7           3.0
c 
c   42.496  11% unhide
c   40.324  11% probe
c   28.344   7% cce
c   19.351   5% elim
c   10.779   3% bump
c    4.692   1% sweep
c    2.761   1% bca
c    2.511   1% decide
c    2.386   1% transred
c 
c    5.618 < 1% rest (below)
c 
c    2.015   1% block
c    1.384   0% gauss
c    1.063   0% ternres
c    0.808   0% quatres
c    0.348   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    4.523   1% preprocessing     3%
c  151.226  39% inprocessing     97%
c ==================================
c  155.749  41% simplifying
c  227.610  59% search
c ==================================
c  383.363 100% all
c 
c        336128 conflicts,         876.8 confs/sec
c          5533 ternaries,          60.7 confs/ternary
c          5177 binaries,           64.9 confs/binary
c           663 iterations,        507.0 confs/iteration
c 
c             5 reductions,          0.0 redus/sec,  67225.6 confs/reduction
c         12284 restarts,           32.0 rests/sec,     27.4 confs/restart
c       4178038 decisions,       10898.4 decis/sec,     12.4 decis/conflict
c     771087308 propagations,  2011377.5 props/sec,    184.6 props/decision
c 
c 383.4 seconds, 96.3 MB
c launch: done
