c launch: /data/cnf/sc2014/app/6s123.cnf.bz2
c host: atom11
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/6s123.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/6s123.cnf.bz2
c no embedded options
c found 'p cnf 903211 2605283' header
c read 903211 variables, 2605283 clauses, 6077901 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 846503 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  846503  2355303         0       0      0     0    0     0  150   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1000000 penalty 1 = 0 + 1
c [card-1] found 15 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1000000 for elimination
c [card-1] 15 out of 15 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 140790 variables
c [simpleprobe-1] all 761463 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 10000000 penalty 1 = 0 + 1
c [decomp-2] removed 1480 variables
c [simpleprobe-1] 538825 variables remain 71% (221158 retained 29%)
c [simpleprobe-1] removed 1480 variables, found 7413 hbrs, 366 units
c [unhide-1] limit 136177 based on 2178845 irredundant clauses
c [unhide-1-1] 1 units, 575 failed, 1014 tauts, 0 hbrs, 834 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 759572 variables 100%
c [elim-1] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 670350 not tried 88% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 89222 = 12% variables out of 759572 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 1753373 negative 87.7% of 1998385 except 245012 12.3%
c [phase-count-1] 1264584 positive 63.3% of 1998385 except 733801 36.7%
c [phase-1] phase bias: 18076 positive 3%, 652274 negative 97%
c [sort-queue-1] sorted 670350 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 670350 (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 176153 variables 20.8% (670350 remain 79%)
c [simplification-1] removed 356918 irredundant clauses 15.2% (1998385 remain 85%)
c [simplification-1] maximum reduction of 21% = max (21%, 15%)
c [simplification-1] large reduction 21% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [decomp-3] removed 398 variables
c [simpleprobe-2] 475189 schedulable variables 71%
c [simpleprobe-2] limit 3994990 based on 1997495 irredundant clauses
c [decomp-4] removed 363 variables
c [simpleprobe-2] 475972 variables remain 71% (193617 retained 29%)
c [simpleprobe-2] removed 363 variables, found 2866 hbrs, 0 units
c [treelook-1] limit 499098 based on 1996392 irredundant clauses
c [treelook-1] scheduled 135766 literals 10%
c [treelook-1] scheduling used 499319 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 499098 based on 1996392 irredundant clauses
c [treelook-1] used 503003 steps
c [treelook-1] 135135 literals remain 10%
c [treelook-1] 134827 variables remain to probed next time 20%
c [decomp-5] removed 38 variables
c [treelook-1] removed 38 variables, found 270 hbrs
c [basicprobe-1] limit 15971136 based on 1996392 irredundant clauses
c [basicprobe-1-0] 393999 probes remain 59% after last round
c [basicprobe-1-0] 16 units = 16 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 16 variables, found 38758 hbrs
c [unhide-2] limit 124774 based on 1996392 irredundant clauses
c [unhide-2-2] 0 units, 224 failed, 2373 tauts, 0 hbrs, 33727 literals
c [elim-2] 669385 variables 100% will be scheduled this time
c [elim-2] scheduled 669385 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 436779 not tried 65% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 232607 = 35% variables out of 669385 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 1348209 negative 88.1% of 1530565 except 182356 11.9%
c [phase-count-2] 1101903 positive 72.0% of 1530565 except 428662 28.0%
c [phase-2] phase bias: 21105 positive 97%, 641 negative 3%
c [sort-queue-2] sorted 433993 enqueued variables after 368 conflicts
c [score-dist-2] active 2785 (1%), one 0 (0%), zero 433993 (99%)
c [score-dist-2] max exp 504, different 4 (1%)
c [score-dist-2] median active exp 502, avg 502.4
c [simplification-2] removed 233572 variables 34.8% (436778 remain 52%)
c [simplification-2] removed 467820 irredundant clauses 23.4% (1530565 remain 65%)
c [simplification-2] maximum reduction of 35% = max (35%, 23%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1000 (hard 11000)
c [simplification-2] new binary interval 1000
c 
c [simplification-3] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 148 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 148 out of 148 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 7531 variables
c [treelook-2] limit 378379 based on 1513519 irredundant clauses
c [treelook-2] scheduled 71650 literals 8%
c [treelook-2] scheduling used 380973 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 378379 based on 1513519 irredundant clauses
c [treelook-2] used 428573 steps
c [treelook-2] 70664 literals remain 8%
c [treelook-2] 43861 variables remain to probed next time 10%
c [decomp-7] removed 35 variables
c [treelook-2] removed 37 variables, found 1405 hbrs
c [unhide-3] limit 94594 based on 1513511 irredundant clauses
c [unhide-3-3] 0 units, 1516 failed, 2786 tauts, 0 hbrs, 8029 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 428359 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 269686 not tried 63% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 158606 = 37% variables out of 428359 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 975539 negative 86.0% of 1133937 except 158398 14.0%
c [phase-count-3] 968043 positive 85.4% of 1133937 except 165894 14.6%
c [phase-3] phase bias: 1620 positive 84%, 305 negative 16%
c [sort-queue-3] sorted 264795 enqueued variables after 1000 conflicts
c [score-dist-3] active 4958 (2%), one 0 (0%), zero 264795 (98%)
c [score-dist-3] max exp 505, different 5 (1%)
c [score-dist-3] median active exp 502, avg 502.4
c [simplification-3] removed 167025 variables 38.2% (269753 remain 32%)
c [simplification-3] removed 396628 irredundant clauses 25.9% (1133937 remain 48%)
c [simplification-3] maximum reduction of 38% = max (38%, 26%)
c [simplification-3] large reduction 38% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-3] new conflict limit 3000 (hard 13000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   34.6  269752  1133935      1337     227    409 18795    1   355  120   0%      9  352    2    0 5241%
c i   36.2  269751  1133933      1575     350    464 18833    1   516  120   0%      8  511    3    0 4945%
c i   47.1  269750  1133927      2758     680    892 19084    1  1690  124   0%     10 1669    3    0 2821%
c i   47.8  269749  1133927      2788     692    896 19086    1  1787  124   0%      9 1766    3    0 2884%
c 
c [simplification-4] limit 3000 conflicts (hard 13000) hit after 3001 conflicts
c [decomp-8] removed 210 variables
c [basicprobe-2] limit 16754966 penalty 0 = 0 + 0
c [basicprobe-2-0] 171336 probes remain 64% after last round
c [basicprobe-2-0] 47 units = 47 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 47 variables, found 14558 hbrs
c [unhide-4] limit 167549 with penalty 2 = 0 + 2
c [unhide-4-4] 0 units, 527 failed, 1155 tauts, 0 hbrs, 5496 literals
c [elim-4] 269190 variables 100% will be scheduled this time
c [elim-4] scheduled 269190 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1340397300 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 115337 variables 43% in round 1 in 442644853 steps
c [elim-4-1] backward subsumption/strengthening limit 442644800
c [elim-4-1-1] backward checking 185330 touched variables 69%
c [elim-4-1-1] incomplete backward checking 160380 remain 87%
c [elim-4-1] subsumed 2115 and strengthened 8025 clauses in 442646558 steps
c [elim-4-1] rescheduled 12838 variables 5% by backward subsumption
c [elim-4-2] eliminated 2027 variables 1% in round 2 in 163141841 steps
c [elim-4-2] backward subsumption/strengthening limit 163141800
c [elim-4-2-1] backward checking 165757 touched variables 62%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 453 and strengthened 1828 clauses in 95911166 steps
c [elim-4-2] rescheduled 4056 variables 2% by backward subsumption
c [elim-4-3] eliminated 585 variables 0% in round 3 in 83530942 steps
c [elim-4-3] backward subsumption/strengthening limit 83530900
c [elim-4-3-1] backward checking 2906 touched variables 1%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 209 and strengthened 539 clauses in 35378656 steps
c [elim-4] incomplete 814 not tried 0% in round 3
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 119436 = 44% variables out of 269190 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 141703 enqueued variables after 3001 conflicts
c [score-dist-4] active 8139 (5%), one 0 (0%), zero 141703 (95%)
c [score-dist-4] max exp 508, different 8 (2%)
c [score-dist-4] median active exp 502, avg 502.5
c [simplification-4] removed 119907 variables 44.5% (149842 remain 18%)
c [simplification-4] removed 281534 irredundant clauses 24.8% (852390 remain 36%)
c [simplification-4] maximum reduction of 44% = max (44%, 25%)
c [simplification-4] large reduction 44% >= 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 15001 (soft 5001 + delta 10000)
c [simplification-4] new conflict limit 5001 (hard 15001)
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   82.2  149841   852390      3132     255    273 14091    1  2132  114   0%      7 2103    3    0 3022%
c i   85.7  149840   852386      3439     381    323 14094    1  2377  114   0%      6 2342    3    0 2841%
c i   88.4  149839   852386      4019     597    443 14121    2  2453  114   0%      5 2401    4    0 2567%
c i   90.5  149838   852386      4218     673    486 14127    2  2507  114   0%      5 2447    4    0 2472%
c i   93.6  149837   852386      4520     815    534 14131    2  2625  114   0%      4 2554    4    0 2315%
c 
c [simplification-5] limit 5001 conflicts (hard 15001) hit after 5002 conflicts
c [quatres-1] found 222089 quaternary clauses 60% in total
c [quatres-1-1] added 40 double-self-subsuming ternary resolvents
c [quatres-1-2] added 492 single-self-subsuming ternary resolvents
c [quatres-1-2] added 24098 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 27482010 with penalty 0 = 0 + 0
c [ternres-1] all 149837 free variables schedulable
c [ternres-1] 35984 ternary resolvents (40 bin, 35944 trn)
c [ternres-1] 62810 variables remain 42% (87027 retained 58%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 8047 xors of average arity 3.0
c [gauss-1] connected 23773 occurrences of 8601 variables (average 2.8)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-9] removed 619 variables
c [simpleprobe-3] 105752 schedulable variables 71%
c [simpleprobe-3] limit 21985609 penalty 0 = 0 + 0
c [decomp-10] removed 107 variables
c [simpleprobe-3] 107019 variables remain 72% (42092 retained 28%)
c [simpleprobe-3] removed 107 variables, found 3202 hbrs, 3 units
c [unhide-5] limit 549640 with penalty 1 = 0 + 1
c [unhide-5-5] 4 units, 27 failed, 2143 tauts, 0 hbrs, 3626 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 205 transitive binary clauses
c [transred-1] found 8 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 149085 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 549640220 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 76297 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 9 (11%) of length 34
c [cce-1-1] eliminated 4 clauses out of 8 (50%) of length 33
c [cce-1-1] eliminated 2 clauses out of 18 (11%) of length 32
c [cce-1-1] eliminated 2 clauses out of 14 (14%) of length 31
c [cce-1-1] eliminated 5 clauses out of 32 (16%) of length 30
c [cce-1-1] eliminated 19 clauses out of 59 (32%) of length 29
c [cce-1-1] eliminated 14 clauses out of 68 (21%) of length 28
c [cce-1-1] eliminated 30 clauses out of 115 (26%) of length 27
c [cce-1-1] eliminated 46 clauses out of 160 (29%) of length 26
c [cce-1-1] eliminated 46 clauses out of 178 (26%) of length 25
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 169 large clauses in 30000098 steps
c [cce-1-1] allowing another 15000049 steps for small clauses
c [cce-1-1] scheduling 232808 clauses = 74095 binary + 158713 ternary
c [cce-1-1] tried to eliminate 6684 small clauses 3%
c [cce-1-1] eliminated 32 binary clauses 0%
c [cce-1-1] eliminated 324 ternary clauses 0%
c [cce-1-1] eliminated 356 small clauses 0%
c [cce-1-1] eliminated 356 small clauses in 30000005 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 525 covered clauses in round 1
c [cce-1] eliminated 525 covered clauses in TOTAL during 1 rounds
c [cce-1] 525 < 1/100 * 773624 = 7736 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 149002 variables 100%
c [elim-5] limit of 109928045 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 961 not tried 1% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 17663 = 12% variables out of 149002 scheduled
c [bca-1] limit of 10000000 steps and 1449468 added (scaled 2)
c [bca-1] 229864 out of 262680 literals actually usable 88%
c [bca-1] added 24958 blocked clauses in 737327 steps
c [sweep-1] limit 1648920 penalty 0 = 0 + 0
c [sweep-1-1] 59516 pos 45.3% + 71823 neg 54.7% = 131339 sched 100.0% ret 0
c [sweep-1-1] 1666512 steps 91 queries 38988.75 avg class size
c [sweep-1-1] 903 decisions 75 SAT calls 24.47 avg env size
c [sweep-1-1] 131058 variables remain 100% (277 retained 0%)
c [decomp-11] removed 475 variables
c [sweep-1-1] removed 475 vars (0 failed, 21 eqs, 35 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 475 vars in TOTAL (1 rounds, 90 queries)
c [sort-queue-5] sorted 120900 enqueued variables after 5002 conflicts
c [score-dist-5] active 9964 (8%), one 0 (0%), zero 120900 (92%)
c [score-dist-5] max exp 510, different 10 (2%)
c [score-dist-5] median active exp 502, avg 502.7
c [simplification-5] removed 18973 variables 12.7% (130864 remain 15%)
c [simplification-5] removed 128847 irredundant clauses 15.1% (723535 remain 31%)
c [simplification-5] maximum reduction of 15% = max (13%, 15%)
c [simplification-5] large reduction 15% >= 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 17002 (soft 7002 + delta 10000)
c [simplification-5] new conflict limit 7002 (hard 17002)
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  119.5  130863   723532      5543   17435  40477 57892    2  3105  111   0%      7 2996    4    0 1907%
c i  123.4  130862   723517      6772   18111  40579 57941    3  2646  112   0%     10 2493    7    0 2236%
c 
c [simplification-6] limit 7002 conflicts (hard 17002) hit after 7002 conflicts
c [quatres-2] found 197056 quaternary clauses 56% in total
c [quatres-2-1] removed 132 duplicate quaternary clauses
c [quatres-2-1] added 568 double-self-subsuming ternary resolvents
c [quatres-2-2] added 2796 single-self-subsuming ternary resolvents
c [quatres-2-2] added 16357 quaternary resolvents
c [ternres-2] limit 6735218 with penalty 0 = 0 + 0
c [ternres-2] 54629 schedulable variables 42%
c [ternres-2] 8801 ternary resolvents (320 bin, 8481 trn)
c [ternres-2] 44123 variables remain 34% (86739 retained 66%)
c [card-3] limit 841902 penalty 2 = 2 + 0
c [card-3] found 1362 at-most-one constraints of average size 5.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 841902 for elimination
c [card-3] 1362 out of 1362 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 6036 xors of average arity 3.0
c [gauss-2] connected 18055 occurrences of 6280 variables (average 2.9)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 84 variables
c [treelook-3] limit 673521 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 20668 literals 8%
c [treelook-3] scheduling used 673530 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 673521 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 844284 steps
c [treelook-3] 19997 literals remain 8%
c [treelook-3] 6710 variables remain to probed next time 5%
c [decomp-13] removed 4 variables
c [treelook-3] removed 7 variables, found 1024 hbrs
c [unhide-6] limit 673521 with penalty 1 = 0 + 1
c [unhide-6-6] 133 units, 217 failed, 2335 tauts, 0 hbrs, 9900 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 25 transitive binary clauses
c [transred-2] found 7 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 130498 variables 100%
c [block-2] limit of 67352184 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 1418 blocked clauses
c [block-2] 1418 < 1/100 * 722331 = 7223 considered unsuccessful
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 130408 variables 100%
c [elim-6] limit of 134704369 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 534 not tried 0% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 4537 = 3% variables out of 130408 scheduled
c [bca-2] limit of 10000000 steps and 1419363 added (scaled 2)
c [bca-2] 213674 out of 251744 literals actually usable 85%
c [bca-2] added 1299 blocked clauses in 703453 steps
c [sweep-2] limit 2020565 penalty 0 = 0 + 0
c [sweep-2-1] 61312 pos 48.8% + 64346 neg 51.2% = 125658 sched 99.8% ret 213
c [sweep-2-1] 2042150 steps 102 queries 38110.00 avg class size
c [sweep-2-1] 1384 decisions 98 SAT calls 50.10 avg env size
c [sweep-2-1] 125331 variables remain 100% (537 retained 0%)
c [decomp-14] removed 175 variables
c [sweep-2-1] removed 175 vars (0 failed, 13 eqs, 13 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 175 vars in TOTAL (1 rounds, 101 queries)
c [sort-queue-6] sorted 114300 enqueued variables after 7002 conflicts
c [score-dist-6] active 11396 (9%), one 0 (0%), zero 114300 (91%)
c [score-dist-6] max exp 511, different 11 (2%)
c [score-dist-6] median active exp 503, avg 503.1
c [simplification-6] removed 5166 variables 3.9% (125696 remain 15%)
c [simplification-6] removed 20686 irredundant clauses 2.9% (702831 remain 30%)
c [simplification-6] maximum reduction of 4% = max (4%, 3%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 4000
c [simplification-6] penalized conflict interval 4000 = 1 * 4000
c [simplification-6] hard conflict limit 21002 (soft 11002 + delta 10000)
c [simplification-6] new conflict limit 11002 (hard 21002)
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  136.6  125695   702825      7209   30426  44735 54915    3  2449  112   0%      7 2283    6    0 1776%
c i  138.7  125694   702820      8854   31465  44816 54965    4  1961  112   0%     14 1751    6    0 1257%
c 
c [simplification-7] limit 11002 conflicts (hard 21002) hit after 11003 conflicts
c [quatres-3] found 203376 quaternary clauses 57% in total
c [quatres-3-1] removed 143 duplicate quaternary clauses
c [quatres-3-1] added 1023 double-self-subsuming ternary resolvents
c [quatres-3-2] added 3570 single-self-subsuming ternary resolvents
c [quatres-3-2] added 6125 quaternary resolvents
c [ternres-3] limit 8266239 with penalty 0 = 0 + 0
c [ternres-3] 42255 schedulable variables 34%
c [ternres-3] 8046 ternary resolvents (428 bin, 7618 trn)
c [ternres-3] 33082 variables remain 26% (92612 retained 74%)
c [decomp-15] removed 121 variables
c [basicprobe-3] limit 41331196 penalty 0 = 0 + 0
c [basicprobe-3-0] 874 probes remain 1% after last round
c [basicprobe-3-0] 579 units = 571 failed (99%) + 8 lifted (1%)
c [basicprobe-3-0] removed 575 variables, found 60099 hbrs
c [bate-1] eliminated 805 asymmetric tautologies during probing
c [unhide-7] limit 826623 with penalty 1 = 0 + 1
c [unhide-7-7] 6 units, 8 failed, 3126 tauts, 0 hbrs, 5552 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 215 transitive binary clauses
c [transred-3] found 1 units
c [cce-2] limit of 20665598 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 64
c [cce-2-1] eliminated 1 clauses out of 22 (5%) of length 30
c [cce-2-1] eliminated 1 clauses out of 46 (2%) of length 29
c [cce-2-1] eliminated 1 clauses out of 101 (1%) of length 26
c [cce-2-1] eliminated 9 clauses out of 216 (4%) of length 24
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 13 large clauses in 20665769 steps
c [cce-2-1] allowing another 10332884 steps for small clauses
c [cce-2-1] scheduling 235249 clauses = 68816 binary + 166433 ternary
c [cce-2-1] tried to eliminate 4003 small clauses 2%
c [cce-2-1] eliminated 19 binary clauses 0%
c [cce-2-1] eliminated 60 ternary clauses 0%
c [cce-2-1] eliminated 79 small clauses 0%
c [cce-2-1] eliminated 124 small clauses in 20665862 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 137 covered clauses in round 1
c [cce-2] eliminated 137 covered clauses in TOTAL during 1 rounds
c [cce-2] 137 < 1/100 * 698741 = 6987 considered unsuccessful
c [elim-7] 526 variables 0% will be scheduled this time
c [elim-7] scheduled 526 variables 0%
c [elim-7] limit of 165324787 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 129 not tried 0% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 1 = 0% variables out of 526 scheduled
c [elim-7] 1 < 1/100 * 526 = 5 considered unsuccessful
c [bca-3] limit of 10000000 steps and 1409080 added (scaled 2)
c [bca-3] 208651 out of 249974 literals actually usable 83%
c [bca-3] added 295 blocked clauses in 675241 steps
c [sweep-3] limit 2479871 penalty 0 = 0 + 0
c [sweep-3-1] 61370 pos 49.3% + 63118 neg 50.7% = 124488 sched 99.6% ret 498
c [sweep-3-1] 2486113 steps 128 queries 36928.92 avg class size
c [sweep-3-1] 1564 decisions 107 SAT calls 42.54 avg env size
c [sweep-3-1] 124052 variables remain 99% (933 retained 1%)
c [decomp-16] removed 1481 variables
c [sweep-3-1] removed 1481 vars (0 failed, 28 eqs, 28 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1481 vars in TOTAL (1 rounds, 127 queries)
c [sort-queue-7] sorted 108771 enqueued variables after 11003 conflicts
c [score-dist-7] active 14734 (12%), one 0 (0%), zero 108771 (88%)
c [score-dist-7] max exp 511, different 11 (2%)
c [score-dist-7] median active exp 503, avg 503.6
c [simplification-7] removed 2189 variables 1.7% (123505 remain 15%)
c [simplification-7] removed 5442 irredundant clauses 0.8% (697372 remain 30%)
c [simplification-7] maximum reduction of 2% = max (2%, 1%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 10666
c [simplification-7] penalized conflict interval 10666 = 1 * 10666
c [simplification-7] hard conflict limit 31669 (soft 21669 + delta 10000)
c [simplification-7] new conflict limit 21669 (hard 31669)
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  169.1  123504   697359     16504   37376  51763 96242    6  2156  114   0%     97 1795    5    1  405%
c i  174.0  123503   697355     17355   37903  51809 96261    6  2586  114   0%     42 2201    5    1  448%
c i  176.7  123501   697352     18342   38463  51887 96287    6  2422  114   0%     17 2009    5    1  391%
c i  178.7  123500   697351     18891   38811  51942 96306    6  2367  114   0%      9 1938    6    1  460%
c i  183.1  123499   697345     21292   40530  52012 96343    8  1854  115   0%     17 1368   19    2 1216%
c i  183.2  123498   697345     21322   40548  52016 96343    8  1844  115   0%     16 1358   20    2 1248%
c 
c [simplification-8] limit 21669 conflicts (hard 31669) hit after 21669 conflicts
c [quatres-4] found 203616 quaternary clauses 58% in total
c [quatres-4-1] removed 45 duplicate quaternary clauses
c [quatres-4-1] added 1084 double-self-subsuming ternary resolvents
c [quatres-4-2] added 4795 single-self-subsuming ternary resolvents
c [quatres-4-2] added 3811 quaternary resolvents
c [ternres-4] limit 12862319 with penalty 0 = 0 + 0
c [ternres-4] 32424 schedulable variables 26%
c [ternres-4] 11907 ternary resolvents (750 bin, 11157 trn)
c [ternres-4] 16470 variables remain 13% (107028 retained 87%)
c [gauss-3] limit 1286231 penalty 1 = 1 + 0
c [gauss-3] extracted 3124 xors of average arity 3.0
c [gauss-3] connected 9276 occurrences of 3548 variables (average 2.6)
c [gauss-3] limit 1286231 penalty 1 = 1 + 0
c [gauss-3] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-17] removed 232 variables
c [simpleprobe-4] 88846 schedulable variables 72%
c [simpleprobe-4] limit 51449278 penalty 0 = 0 + 0
c [decomp-18] removed 174 variables
c [simpleprobe-4] 65665 variables remain 53% (57427 retained 47%)
c [simpleprobe-4] removed 174 variables, found 2554 hbrs, 26 units
c [unhide-8] limit 1286231 with penalty 1 = 0 + 1
c [unhide-8-8] 2 units, 40 failed, 6934 tauts, 0 hbrs, 11866 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 106 transitive binary clauses
c [transred-4] found 2 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 123070 variables 100%
c [block-3] limit of 64311598 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 783 blocked clauses
c [block-3] 783 < 1/100 * 693382 = 6933 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1398824 added (scaled 2)
c [bca-4] 200620 out of 246040 literals actually usable 82%
c [bca-4] added 410 blocked clauses in 652781 steps
c [sweep-4] limit 3858695 penalty 0 = 0 + 0
c [sweep-4-1] 62687 pos 51.3% + 59435 neg 48.7% = 122122 sched 99.3% ret 897
c [sweep-4-1] 3867056 steps 199 queries 33532.43 avg class size
c [sweep-4-1] 2376 decisions 196 SAT calls 40.60 avg env size
c [sweep-4-1] 121471 variables remain 99% (1547 retained 1%)
c [decomp-19] removed 40 variables
c [sweep-4-1] removed 40 vars (0 failed, 27 eqs, 23 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 40 vars in TOTAL (1 rounds, 198 queries)
c [sort-queue-8] sorted 100465 enqueued variables after 21669 conflicts
c [score-dist-8] active 22514 (18%), one 0 (0%), zero 100465 (82%)
c [score-dist-8] max exp 512, different 12 (2%)
c [score-dist-8] median active exp 504, avg 504.2
c [simplification-8] removed 519 variables 0.4% (122979 remain 15%)
c [simplification-8] removed 4844 irredundant clauses 0.7% (692501 remain 29%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-8] new conflict interval 20666
c [simplification-8] penalized conflict interval 20666 = 1 * 20666
c [simplification-8] hard conflict limit 52668 (soft 42335 + delta 10333)
c [simplification-8] new conflict limit 42335 (hard 52668)
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  192.8  122978   692499     22941   38767  63117 93174    9  1549  115   1%     10 1035   11    2  605%
c i  192.9  122977   692499     23114   38877  63120 93176   10  1512  115   1%      7  995   14    2  721%
c i  197.0  122976   692487     28132   42498  63277 93238   10   903  115   1%     53  339   11    2  444%
c i  197.3  122975   692487     28700   42923  63285 93240   12   839  115   1%     28  273   26    3  983%
c i  198.1  122974   692487     29675   43595  63311 93256   11   822  115   1%     10  252    8    3  280%
c i  198.5  122973   692487     30684   44370  63323 93259   13   712  116   2%      3  139   15    3  507%
c i  200.0  122972   692481     31167   44649  63367 93288   12   971  116   1%     -0  397    7    3  240%
c i  202.4  122971   692474     31622   44957  63380 93304   12  1332  116   1%     -3  754    6    3  206%
c i  203.0  122970   692474     31766   45044  63390 93307   12  1387  116   1%     -3  808    7    3  230%
c i  217.5  122969   692442     36301   48347  63540 93380   11  2221  116   0%     44 1559   14    3  400%
c 
c [simplification-9] limit of 29 iterations hit after 29 iterations
c [quatres-5] found 200592 quaternary clauses 58% in total
c [quatres-5-1] removed 102 duplicate quaternary clauses
c [quatres-5-1] added 551 double-self-subsuming ternary resolvents
c [quatres-5-2] added 2670 single-self-subsuming ternary resolvents
c [quatres-5-2] added 2533 quaternary resolvents
c [ternres-5] limit 17833551 with penalty 0 = 0 + 0
c [ternres-5] 16347 schedulable variables 13%
c [ternres-5] 19660 ternary resolvents (1592 bin, 18068 trn)
c [ternres-5] 1229 variables remain 1% (121740 retained 99%)
c [gauss-4] limit 3566710 penalty 0 = 0 + 0
c [gauss-4] extracted 9655 xors of average arity 2.9
c [gauss-4] connected 28425 occurrences of 7408 variables (average 3.8)
c [gauss-4] limit 3566710 penalty 0 = 0 + 0
c [gauss-4] exported 0 unary, 0 binary and 7 ternary equations
c [decomp-20] removed 580 variables
c [treelook-4] limit 1783355 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 33985 literals 14%
c [treelook-4] scheduling used 1783357 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1783355 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1787982 steps
c [treelook-4] 33540 literals remain 14%
c [treelook-4] 6090 variables remain to probed next time 5%
c [decomp-21] removed 68 variables
c [treelook-4] removed 68 variables, found 2387 hbrs
c [unhide-9] limit 1783355 with penalty 1 = 0 + 1
c [unhide-9-9] 10 units, 27 failed, 2089 tauts, 0 hbrs, 6430 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 185 transitive binary clauses
c [transred-5] found 11 units
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 122289 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3566710300 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 5483 variables 4% in round 1 in 680346451 steps
c [elim-8-1] backward subsumption/strengthening limit 680346400
c [elim-8-1-1] backward checking 28253 touched variables 23%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 592 and strengthened 2349 clauses in 179946293 steps
c [elim-8-1] rescheduled 4136 variables 3% by backward subsumption
c [elim-8-2] eliminated 471 variables 0% in round 2 in 329722210 steps
c [elim-8-2] backward subsumption/strengthening limit 329722200
c [elim-8-2-1] backward checking 2428 touched variables 2%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 87 and strengthened 227 clauses in 23832554 steps
c [elim-8-2] rescheduled 468 variables 0% by backward subsumption
c [elim-8-3] eliminated 108 variables 0% in round 3 in 55556848 steps
c [elim-8-3] backward subsumption/strengthening limit 55556800
c [elim-8-3-1] backward checking 425 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 25 and strengthened 49 clauses in 13208672 steps
c [elim-8] incomplete 99 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 6146 = 5% variables out of 122289 scheduled
c [bca-5] limit of 10000000 steps and 1324545 added (scaled 2)
c [bca-5] 187896 out of 232288 literals actually usable 81%
c [bca-5] added 822 blocked clauses in 618302 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 53500650 penalty 0 = 0 + 0
c [sweep-5-1] 59980 pos 52.3% + 54712 neg 47.7% = 114692 sched 98.8% ret 1451
c [sweep-5-1] 53514755 steps 2599 queries 12175.30 avg class size
c [sweep-5-1] 31739 decisions 2670 SAT calls 27.35 avg env size
c [sweep-5-1] 100465 variables remain 87% (15660 retained 13%)
c [decomp-22] removed 1326 variables
c [sweep-5-1] removed 1326 vars (0 failed, 419 eqs, 232 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1326 vars in TOTAL (1 rounds, 2598 queries)
c [sort-queue-9] sorted 85115 enqueued variables after 36301 conflicts
c [score-dist-9] active 29702 (26%), one 0 (0%), zero 85115 (74%)
c [score-dist-9] max exp 512, different 12 (2%)
c [score-dist-9] median active exp 504, avg 504.6
c [simplification-9] removed 8152 variables 6.6% (114817 remain 14%)
c [simplification-9] removed 39082 irredundant clauses 5.6% (653360 remain 28%)
c [simplification-9] maximum reduction of 7% = max (7%, 6%)
c [simplification-9] forced so keeping old conflict interval 20666
c [simplification-9] conflict limit remains at 42335 (hard 52668)
c [simplification-9] 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  248.9  114816   653360     36305   38906  65867 91220   11  2223  113   0%     44 1561   14    3  396%
c i  250.3  114815   653349     36513   38999  65884 91224   10  2366  114   0%     34 1700    9    3  270%
c 
c [simplification-10] limit 42337 conflicts (hard 52668) hit after 42338 conflicts
c [quatres-6] found 181721 quaternary clauses 56% in total
c [quatres-6-1] removed 388 duplicate quaternary clauses
c [quatres-6-1] added 130 double-self-subsuming ternary resolvents
c [quatres-6-2] added 1490 single-self-subsuming ternary resolvents
c [quatres-6-2] added 6249 quaternary resolvents
c [ternres-6] limit 21027087 with penalty 0 = 0 + 0
c [ternres-6] 1106 schedulable variables 1%
c [ternres-6] 16712 ternary resolvents (647 bin, 16065 trn)
c [ternres-6] 87 variables remain 0% (114728 retained 100%)
c [card-4] limit 1314192 penalty 3 = 3 + 0
c [card-4] found 1393 at-most-one constraints of average size 4.8
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1314192 for elimination
c [card-4] 1393 out of 1393 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 4205417 penalty 0 = 0 + 0
c [gauss-5] extracted 9757 xors of average arity 3.0
c [gauss-5] connected 28851 occurrences of 6429 variables (average 4.5)
c [gauss-5] limit 4205417 penalty 0 = 0 + 0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 344 variables
c [basicprobe-4] limit 105135437 penalty 0 = 0 + 0
c [basicprobe-4-0] 5376 sched 5%, 14 failed, 0 lifted, 6179 hbrs
c [decomp-24] removed 17 variables
c [basicprobe-4-1] 50431 sched 44%, 346 failed, 3 lifted, 11594 hbrs
c [decomp-25] removed 452 variables
c [basicprobe-4-2] 49928 sched 44%, 18 failed, 0 lifted, 727 hbrs
c [decomp-26] removed 19 variables
c [basicprobe-4-3] 49924 sched 44%, 1 failed, 0 lifted, 63 hbrs
c [decomp-27] removed 2 variables
c [basicprobe-4-4] 46871 probes remain 41% after last round
c [basicprobe-4-4] 382 units = 379 failed (99%) + 3 lifted (1%)
c [basicprobe-4-4] removed 490 variables, found 18566 hbrs
c [bate-2] eliminated 291 asymmetric tautologies during probing
c [unhide-10] limit 2102708 with penalty 1 = 0 + 1
c [unhide-10-10] 0 units, 0 failed, 6612 tauts, 0 hbrs, 13938 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 148 transitive binary clauses
c [cce-3] limit of 26283859 steps penalty 2 = 2 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 13141930 steps for small clauses
c [cce-3-1] scheduling 217367 clauses = 61257 binary + 156110 ternary
c [cce-3-1] tried to eliminate 8 small clauses 0%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 1 small clauses 0%
c [cce-3-1] eliminated 1 small clauses in 26283860 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1 covered clauses in round 1
c [cce-3] eliminated 1 covered clauses in TOTAL during 1 rounds
c [cce-3] 1 < 1/100 * 650004 = 6500 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 113981 variables 100%
c [elim-9] limit of 420541750 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 24 not tried 0% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 3837 = 3% variables out of 113981 scheduled
c [bca-6] limit of 10000000 steps and 1270574 added (scaled 2)
c [bca-6] 175006 out of 220290 literals actually usable 79%
c [bca-6] added 767 blocked clauses in 583062 steps
c [sweep-6] limit 6308126 penalty 0 = 0 + 0
c [sweep-6-1] 49403 pos 51.8% + 45933 neg 48.2% = 95336 sched 86.6% ret 14808
c [sweep-6-1] 6316411 steps 392 queries 22409.50 avg class size
c [sweep-6-1] 3488 decisions 381 SAT calls 20.18 avg env size
c [sweep-6-1] 94204 variables remain 86% (15939 retained 14%)
c [decomp-28] removed 393 variables
c [sweep-6-1] removed 393 vars (0 failed, 39 eqs, 37 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 393 vars in TOTAL (1 rounds, 391 queries)
c [sort-queue-10] sorted 77121 enqueued variables after 42338 conflicts
c [score-dist-10] active 32630 (30%), one 0 (0%), zero 77121 (70%)
c [score-dist-10] max exp 512, different 12 (2%)
c [score-dist-10] median active exp 504, avg 504.7
c [simplification-10] removed 5064 variables 4.4% (109751 remain 13%)
c [simplification-10] removed 26052 irredundant clauses 4.0% (627290 remain 27%)
c [simplification-10] maximum reduction of 4% = max (4%, 4%)
c [simplification-10] geometric conflict interval increment 4133 = 20666 / 5
c [simplification-10] new conflict interval 24799
c [simplification-10] penalized conflict interval 24799 = 1 * 24799
c [simplification-10] hard conflict limit 79536 (soft 67137 + delta 12399)
c [simplification-10] new conflict limit 67137 (hard 79536)
c 
c [simplification-11] limit of 4360 ternary hit after 4360 ternaries
c [quatres-7] found 178405 quaternary clauses 56% in total
c [quatres-7-1] removed 92 duplicate quaternary clauses
c [quatres-7-1] added 161 double-self-subsuming ternary resolvents
c [quatres-7-2] added 1520 single-self-subsuming ternary resolvents
c [quatres-7-2] added 4976 quaternary resolvents
c [ternres-7] limit 28099019 with penalty 0 = 0 + 0
c [ternres-7] 83 schedulable variables 0%
c [ternres-7] 9214 ternary resolvents (49 bin, 9165 trn)
c [ternres-7] 17 variables remain 0% (109734 retained 100%)
c [decomp-29] removed 143 variables
c [simpleprobe-5] 58524 schedulable variables 53%
c [simpleprobe-5] limit 112396078 penalty 0 = 0 + 0
c [decomp-30] removed 282 variables
c [simpleprobe-5] 28469 variables remain 26% (80857 retained 74%)
c [simpleprobe-5] removed 282 variables, found 3926 hbrs, 21 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 303 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 109325 variables 100%
c [block-4] limit of 70247548 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 852 blocked clauses
c [block-4] 852 < 1/100 * 625805 = 6258 considered unsuccessful
c [elim-10] 24 variables 0% will be scheduled this time
c [elim-10] scheduled 24 variables 0%
c [elim-10] limit of 561980391 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] no variable eliminated in round 1 in 249940782 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 1 = 4% variables out of 24 scheduled
c [elim-10] 1 < 1/100 * 24 = 0 considered unsuccessful
c [bca-7] limit of 10000000 steps and 1263295 added (scaled 2)
c [bca-7] 163732 out of 218616 literals actually usable 75%
c [bca-7] added 52 blocked clauses in 554953 steps
c [sweep-7] limit 8429705 penalty 0 = 0 + 0
c [sweep-7-1] 48939 pos 52.4% + 44522 neg 47.6% = 93461 sched 85.5% ret 15846
c [sweep-7-1] 8443140 steps 491 queries 21803.45 avg class size
c [sweep-7-1] 5654 decisions 484 SAT calls 23.49 avg env size
c [sweep-7-1] 91621 variables remain 84% (17680 retained 16%)
c [decomp-31] removed 41 variables
c [sweep-7-1] removed 41 vars (0 failed, 31 eqs, 37 impls)
c [sweep-7] 41 < 1/1000 * 109307 = 109 considered unsuccessful
c [sweep-7] removed 41 vars in TOTAL (1 rounds, 490 queries)
c [sort-queue-11] sorted 65659 enqueued variables after 57431 conflicts
c [score-dist-11] active 43607 (40%), one 0 (0%), zero 65659 (60%)
c [score-dist-11] max exp 514, different 13 (3%)
c [score-dist-11] median active exp 504, avg 504.7
c [simplification-11] removed 485 variables 0.4% (109266 remain 13%)
c [simplification-11] removed 3052 irredundant clauses 0.5% (624201 remain 27%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] forced so keeping old conflict interval 24799
c [simplification-11] conflict limit remains at 67137 (hard 79536)
c [simplification-11] new ternary interval 10000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  347.2  109265   624177     62101   55660  80529 103682    6  3624  115   0%    312 2224    5    4  106%
c 
c [simplification-12] limit 67137 conflicts (hard 79536) hit after 67774 conflicts
c [quatres-8] found 180629 quaternary clauses 56% in total
c [quatres-8-1] removed 149 duplicate quaternary clauses
c [quatres-8-1] added 112 double-self-subsuming ternary resolvents
c [quatres-8-2] added 1427 single-self-subsuming ternary resolvents
c [quatres-8-2] added 1964 quaternary resolvents
c [ternres-8] limit 30898198 with penalty 0 = 0 + 0
c [ternres-8] 17 schedulable variables 0%
c [ternres-8] 1965 ternary resolvents (233 bin, 1732 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-6] limit 3089819 penalty 1 = 1 + 0
c [gauss-6] extracted 5640 xors of average arity 3.0
c [gauss-6] connected 16695 occurrences of 5231 variables (average 3.2)
c [gauss-6] limit 3089819 penalty 1 = 1 + 0
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 271 variables
c [treelook-5] limit 3089819 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 31594 literals 14%
c [treelook-5] scheduling used 1859708 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 3089819 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 3104485 steps
c [treelook-5] 29980 literals remain 14%
c [treelook-5] 5259 variables remain to probed next time 5%
c [decomp-33] removed 77 variables
c [treelook-5] removed 80 variables, found 1926 hbrs
c [unhide-11] limit 1544909 with penalty 2 = 1 + 1
c [unhide-11-11] 4 units, 13 failed, 2895 tauts, 0 hbrs, 6176 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 206 transitive binary clauses
c [bca-8] limit of 10000000 steps and 1260341 added (scaled 2)
c [bca-8] 162336 out of 217812 literals actually usable 75%
c [bca-8] added 201 blocked clauses in 554753 steps
c [sort-queue-12] sorted 64672 enqueued variables after 67774 conflicts
c [score-dist-12] active 44233 (41%), one 0 (0%), zero 64672 (59%)
c [score-dist-12] max exp 514, different 14 (3%)
c [score-dist-12] median active exp 504, avg 504.8
c [simplification-12] removed 360 variables 0.3% (108905 remain 13%)
c [simplification-12] removed 1405 irredundant clauses 0.2% (622770 remain 26%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 24799
c [simplification-12] new conflict interval 49598
c [simplification-12] penalized conflict interval 49598 = 1 * 49598
c [simplification-12] hard conflict limit 142171 (soft 117372 + delta 24799)
c [simplification-12] new conflict limit 117372 (hard 142171)
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  380.5  108904   622765     80836   65921  81225 104281   17  1786  116   1%    184  247   14    6  239%
c i  383.1  108903   622763     81959   66766  81237 104283   23  1693  117   1%      5  151   38    6  604%
c i  383.1  108902   622763     81960   66766  81237 104283   23  1692  117   1%      5  151   38    6  602%
c i  387.2  108901   622763     84175   68461  81251 104289   19  1737  117   1%    -61  188   13    7  203%
c i  397.4  108900   622761     93810   73143  81393 104339  154  1500  126  10%     45  -11    6   29   22%
c i  398.8  108899   622759     95600   74285  81450 104361  106  1925  126   6%    -50  406    6   28   20%
c -  413.1  108899   622750    116397   62839  81610 104387   17   929  114   2%    202 -557    6   25   25%
c i  428.3  108898   622741    133969   76691  81708 104404   15   749  119   2%    395 -558   14   24   60%
c i  430.5  108897   622741    135318   77624  81724 104407   23   826  119   3%    -26 -471   80   24  330%
c 
c [simplification-13] limit 117382 conflicts (hard 142171) hit after 142171 conflicts
c [quatres-9] found 180996 quaternary clauses 55% in total
c [quatres-9-1] removed 26 duplicate quaternary clauses
c [quatres-9-1] added 115 double-self-subsuming ternary resolvents
c [quatres-9-2] added 1290 single-self-subsuming ternary resolvents
c [quatres-9-2] added 6384 quaternary resolvents
c [ternres-9] limit 49268104 with penalty 0 = 0 + 0
c [ternres-9] all 108897 free variables schedulable
c [ternres-9] 31448 ternary resolvents (2147 bin, 29301 trn)
c [ternres-9] 2315 variables remain 2% (106582 retained 98%)
c [decomp-34] removed 794 variables
c [basicprobe-5] limit 246340520 penalty 0 = 0 + 0
c [basicprobe-5-0] 45069 sched 42%, 246 failed, 2 lifted, 3161 hbrs
c [decomp-35] removed 336 variables
c [basicprobe-5-1] 47658 sched 44%, 31 failed, 0 lifted, 433 hbrs
c [decomp-36] removed 39 variables
c [basicprobe-5-2] 47631 sched 44%, 1 failed, 0 lifted, 20 hbrs
c [decomp-37] removed 3 variables
c [basicprobe-5-3] 47629 sched 44%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-5-4] 47629 sched 44%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-5-5] 47629 sched 44%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-5-6] 47629 sched 44%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-5-7] 27061 probes remain 25% after last round
c [basicprobe-5-7] 280 units = 278 failed (99%) + 2 lifted (1%)
c [basicprobe-5-7] removed 378 variables, found 3641 hbrs
c [bate-3] eliminated 103 asymmetric tautologies during probing
c [unhide-12] limit 4926810 with penalty 1 = 0 + 1
c [unhide-12-13] 0 units, 0 failed, 13896 tauts, 0 hbrs, 48379 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 232 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 107733 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 32 not tried 0% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 3000 = 3% variables out of 107733 scheduled
c [bca-9] limit of 10000000 steps and 1217700 added (scaled 2)
c [bca-9] 152022 out of 209468 literals actually usable 73%
c [bca-9] added 604 blocked clauses in 542689 steps
c [sweep-8] limit 7390215 penalty 1 = 1 + 0
c [sweep-8-1] 45444 pos 51.9% + 42118 neg 48.1% = 87562 sched 83.6% ret 17171
c [sweep-8-1] 7398690 steps 478 queries 20106.03 avg class size
c [sweep-8-1] 4886 decisions 451 SAT calls 21.83 avg env size
c [sweep-8-1] 86059 variables remain 82% (18670 retained 18%)
c [decomp-42] removed 294 variables
c [sweep-8-1] removed 294 vars (0 failed, 82 eqs, 86 impls)
c [sweep-8] removed 294 vars in TOTAL (1 rounds, 477 queries)
c [sort-queue-13] sorted 54525 enqueued variables after 142171 conflicts
c [score-dist-13] active 49914 (48%), one 0 (0%), zero 54525 (52%)
c [score-dist-13] max exp 516, different 16 (3%)
c [score-dist-13] median active exp 505, avg 505.8
c [simplification-13] removed 4458 variables 4.1% (104439 remain 12%)
c [simplification-13] removed 21817 irredundant clauses 3.5% (600913 remain 26%)
c [simplification-13] maximum reduction of 4% = max (4%, 4%)
c [simplification-13] geometric conflict interval increment 9919 = 49598 / 5
c [simplification-13] new conflict interval 59517
c [simplification-13] penalized conflict interval 59517 = 1 * 59517
c [simplification-13] hard conflict limit 231446 (soft 201688 + delta 29758)
c [simplification-13] new conflict limit 201688 (hard 231446)
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  467.4  104438   600913    142313   75389  85133 97992   27  3707  118   1%    -85 2339    9   26   34%
c i  467.7  104437   600912    142621   75547  85151 97995   26  3803  119   1%   -108 2423    5   26   20%
c -  498.0  104437   600905    168241   68386  85381 98061   31  1106  114   3%    199 -480   20   26   75%
c i  509.9  104436   600902    182769   79706  85475 98094   20  1725  119   1%    363  208   15   25   58%
c i  515.6  104435   600902    189877   83727  85634 98161   13  1799  119   1%   -140  226    9   24   38%
c i  529.8  104434   600899    199316   91480  85735 98187   12  3173  120   0%    -82 1434    9   22   42%
c i  530.3  104433   600899    199500   91608  85738 98190   12  3196  120   0%   -103 1453    9   22   39%
c i  542.1  104432   600899    206320   97191  85790 98204   18  2206  121   1%   -107  392   13   22   60%
c i  542.1  104431   600899    206326   97191  85792 98206   18  2207  121   1%   -108  393   13   22   58%
c i  542.8  104430   600899    206430   97279  85795 98211   18  2254  121   1%   -116  440   12   22   52%
c i  545.3  104429   600899    207862   98442  85806 98216   15  2421  121   1%   -164  594   11   22   50%
c -  546.0  104429   600899    209079   71880  85810 98220   16  2183  114   1%   -174  348   25   22  116%
c i  547.8  104428   600895    209823   72430  85853 98230   16  2265  117   1%   -168  426   18   22   84%
c i  548.6  104427   600890    210365   72748  85877 98243   17  2377  117   1%   -173  534   23   22  104%
c 
c [simplification-14] limit 201689 conflicts (hard 231446) hit after 222289 conflicts
c [quatres-10] found 176200 quaternary clauses 55% in total
c [quatres-10-1] removed 237 duplicate quaternary clauses
c [quatres-10-1] added 154 double-self-subsuming ternary resolvents
c [quatres-10-2] added 1387 single-self-subsuming ternary resolvents
c [quatres-10-2] added 8443 quaternary resolvents
c [ternres-10] limit 68419825 with penalty 0 = 0 + 0
c [ternres-10] 2076 schedulable variables 2%
c [ternres-10] 12338 ternary resolvents (680 bin, 11658 trn)
c [ternres-10] 89 variables remain 0% (104338 retained 100%)
c [decomp-43] removed 265 variables
c [simpleprobe-6] 27122 schedulable variables 26%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-44] removed 718 variables
c [simpleprobe-6] 1760 variables remain 2% (101696 retained 98%)
c [simpleprobe-6] removed 718 variables, found 8248 hbrs, 40 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 341 transitive binary clauses
c [transred-10] found 2 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 427623908 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 20 (5%) of length 30
c [cce-4-1] eliminated 1 clauses out of 81 (1%) of length 26
c [cce-4-1] eliminated 38 clauses out of 136 (28%) of length 25
c [cce-4-1] eliminated 20 clauses out of 160 (12%) of length 24
c [cce-4-1] eliminated 35 clauses out of 180 (19%) of length 23
c [cce-4-1] eliminated 76 clauses out of 217 (35%) of length 22
c [cce-4-1] eliminated 84 clauses out of 233 (36%) of length 21
c [cce-4-1] eliminated 101 clauses out of 281 (36%) of length 20
c [cce-4-1] eliminated 96 clauses out of 284 (34%) of length 19
c [cce-4-1] eliminated 127 clauses out of 396 (32%) of length 18
c [cce-4-1] eliminated 169 clauses out of 471 (36%) of length 17
c [cce-4-1] eliminated 137 clauses out of 523 (26%) of length 16
c [cce-4-1] eliminated 157 clauses out of 774 (20%) of length 15
c [cce-4-1] eliminated 179 clauses out of 1007 (18%) of length 14
c [cce-4-1] eliminated 222 clauses out of 1235 (18%) of length 13
c [cce-4-1] eliminated 236 clauses out of 1312 (18%) of length 12
c [cce-4-1] eliminated 265 clauses out of 1178 (22%) of length 11
c [cce-4-1] eliminated 341 clauses out of 1628 (21%) of length 10
c [cce-4-1] eliminated 387 clauses out of 2466 (16%) of length 9
c [cce-4-1] eliminated 745 clauses out of 7075 (11%) of length 8
c [cce-4-1] eliminated 1277 clauses out of 9432 (14%) of length 7
c [cce-4-1] eliminated 3504 clauses out of 24667 (14%) of length 6
c [cce-4-1] eliminated 1029 clauses out of 76561 (1%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 9227 large clauses in 427624329 steps
c [cce-4-1] allowing another 213812164 steps for small clauses
c [cce-4-1] scheduling 183705 clauses = 55153 binary + 128552 ternary
c [cce-4-1] tried to eliminate 111287 small clauses 61%
c [cce-4-1] eliminated 1270 binary clauses 2%
c [cce-4-1] eliminated 6154 ternary clauses 5%
c [cce-4-1] eliminated 7424 small clauses 4%
c [cce-4-1] eliminated 7430 small clauses in 427624030 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 16657 covered clauses in round 1
c [cce-4] eliminated 16657 covered clauses in TOTAL during 1 rounds
c [elim-12] 32 variables 0% will be scheduled this time
c [elim-12] scheduled 32 variables 0%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] no variable eliminated in round 1 in 248254573 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 0 = 0% variables out of 32 scheduled
c [bca-10] limit of 10000000 steps and 1173756 added (scaled 2)
c [bca-10] 143099 out of 206910 literals actually usable 69%
c [bca-10] added 125 blocked clauses in 524858 steps
c [sweep-9] limit 20525947 penalty 0 = 0 + 0
c [sweep-9-1] 43477 pos 51.1% + 41534 neg 48.9% = 85011 sched 82.2% ret 18443
c [sweep-9-1] 20527775 steps 1244 queries 13690.42 avg class size
c [sweep-9-1] 15081 decisions 1204 SAT calls 27.62 avg env size
c [sweep-9-1] 79785 variables remain 77% (23661 retained 23%)
c [decomp-45] removed 199 variables
c [sweep-9-1] removed 199 vars (0 failed, 181 eqs, 179 impls)
c [sweep-9] removed 199 vars in TOTAL (1 rounds, 1243 queries)
c [sort-queue-14] sorted 47002 enqueued variables after 222289 conflicts
c [score-dist-14] active 56253 (54%), one 0 (0%), zero 47002 (46%)
c [score-dist-14] max exp 516, different 16 (3%)
c [score-dist-14] median active exp 506, avg 506.7
c [simplification-14] removed 1172 variables 1.1% (103255 remain 12%)
c [simplification-14] removed 21764 irredundant clauses 3.6% (579125 remain 25%)
c [simplification-14] maximum reduction of 4% = max (1%, 4%)
c [simplification-14] geometric conflict interval increment 11903 = 59517 / 5
c [simplification-14] new conflict interval 71420
c [simplification-14] penalized conflict interval 71420 = 1 * 71420
c [simplification-14] hard conflict limit 329419 (soft 293709 + delta 35710)
c [simplification-14] new conflict limit 293709 (hard 329419)
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 -  593.5  103255   579119    248068   79163 100381 106181   47  1098  115   4%    333 -687   48   27  177%
c i  595.3  103254   579119    250853   80994 100389 106187   50   969  118   5%    362 -785   53   28  187%
c -  618.2  103254   579117    308243   79646 100470 106237   56   161  115  35%    480 -793   67   38  175%
c i  619.5  103253   579117    316721   82650 100474 106237   58   161  119  36%    546 -698   48   40  121%
c i  619.5  103252   579117    317120   82904 100475 106237   55   161  119  34%    218 -693   31   40   77%
c 
c [simplification-15] limit 293709 conflicts (hard 329419) hit after 329421 conflicts
c [quatres-11] found 181442 quaternary clauses 57% in total
c [quatres-11-1] removed 389 duplicate quaternary clauses
c [quatres-11-1] added 259 double-self-subsuming ternary resolvents
c [quatres-11-2] added 1443 single-self-subsuming ternary resolvents
c [quatres-11-2] added 2430 quaternary resolvents
c [ternres-11] limit 81944632 with penalty 0 = 0 + 0
c [ternres-11] 81 schedulable variables 0%
c [ternres-11] 9092 ternary resolvents (421 bin, 8671 trn)
c [ternres-11] 3 variables remain 0% (103249 retained 100%)
c [card-5] limit 2560769 penalty 4 = 4 + 0
c [card-5] found 2075 at-most-one constraints of average size 4.6
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2560769 for elimination
c [card-5] 2075 out of 2075 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-7] limit 4097231 penalty 2 = 2 + 0
c [gauss-7] extracted 6887 xors of average arity 3.0
c [gauss-7] connected 20444 occurrences of 5475 variables (average 3.7)
c [gauss-7] limit 4097231 penalty 2 = 2 + 0
c [decomp-46] removed 193 variables
c [gauss-7] exported 0 unary, 3 binary and 0 ternary equations
c [treelook-6] limit 8194463 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 28464 literals 14%
c [treelook-6] scheduling used 1787484 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 8194463 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 8374414 steps
c [treelook-6] 24961 literals remain 12%
c [treelook-6] 4796 variables remain to probed next time 5%
c [decomp-48] removed 158 variables
c [treelook-6] removed 170 variables, found 5050 hbrs
c [unhide-13] limit 4097231 with penalty 2 = 1 + 1
c [unhide-13-14] 7 units, 28 failed, 3477 tauts, 0 hbrs, 14083 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 401 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 102870 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 1074 blocked clauses
c [block-5] 1074 < 1/100 * 577716 = 5777 considered unsuccessful
c [bca-11] limit of 10000000 steps and 1168418 added (scaled 2)
c [bca-11] 144537 out of 205540 literals actually usable 70%
c [bca-11] added 193 blocked clauses in 530559 steps
c [sweep-10] limit 24583389 penalty 0 = 0 + 0
c [sweep-10-1] 39341 pos 49.6% + 40051 neg 50.4% = 79392 sched 77.3% ret 23377
c [sweep-10-1] 24595526 steps 1664 queries 12631.78 avg class size
c [sweep-10-1] 17800 decisions 1702 SAT calls 24.14 avg env size
c [sweep-10-1] 73158 variables remain 71% (29606 retained 29%)
c [decomp-49] removed 228 variables
c [sweep-10-1] removed 228 vars (0 failed, 175 eqs, 113 impls)
c [sweep-10] removed 228 vars in TOTAL (1 rounds, 1663 queries)
c [sort-queue-15] sorted 46003 enqueued variables after 329421 conflicts
c [score-dist-15] active 56538 (55%), one 0 (0%), zero 46003 (45%)
c [score-dist-15] max exp 517, different 17 (3%)
c [score-dist-15] median active exp 507, avg 506.9
c [simplification-15] removed 711 variables 0.7% (102541 remain 12%)
c [simplification-15] removed 2725 irredundant clauses 0.5% (576391 remain 24%)
c [simplification-15] maximum reduction of 1% = max (1%, 0%)
c [simplification-15] geometric conflict interval increment 35710 = 71420 / 2
c [simplification-15] new conflict interval 107130
c [simplification-15] penalized conflict interval 107130 = 1 * 107130
c [simplification-15] hard conflict limit 490116 (soft 436551 + delta 53565)
c [simplification-15] new conflict limit 436551 (hard 490116)
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  633.2  102540   576391    330407   87849 102997 106652   58   166  119  35%   -217 -567   70   41  170%
c i  634.8  102539   576391    337235   90190 103019 106660   52   172  122  30%   -284 -506   25   42   58%
c i  634.8  102538   576391    337296   90229 103019 106660   52   172  122  30%   -289 -506   24   42   56%
c -  641.5  102538   576391    383573   79084 103011 106670   59   141  115  42%    325 -268   52   46  111%
c 
c [simplification-16] limit 436551 conflicts (hard 490116) hit after 490116 conflicts
c [quatres-12] found 180001 quaternary clauses 57% in total
c [quatres-12-1] removed 245 duplicate quaternary clauses
c [quatres-12-1] added 64 double-self-subsuming ternary resolvents
c [quatres-12-2] added 885 single-self-subsuming ternary resolvents
c [quatres-12-2] added 1410 quaternary resolvents
c [ternres-12] limit 86365371 with penalty 0 = 0 + 0
c [ternres-12] 3 schedulable variables 0%
c [ternres-12] 1060 ternary resolvents (72 bin, 988 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-50] removed 18 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 26269 sched 26%, 74 failed, 2 lifted, 1237 hbrs
c [decomp-51] removed 109 variables
c [basicprobe-6-1] 45039 sched 44%, 34 failed, 0 lifted, 886 hbrs
c [decomp-52] removed 47 variables
c [basicprobe-6-2] 44981 sched 44%, 1 failed, 0 lifted, 13 hbrs
c [decomp-53] removed 1 variables
c [basicprobe-6-3] 44979 sched 44%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-6-4] 44979 sched 44%, 0 failed, 0 lifted, 1 hbrs
c [decomp-55] removed 1 variables
c [basicprobe-6-5] 44978 sched 44%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-6-6] 44978 sched 44%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-6-7] 44978 sched 44%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-6-8] 44978 sched 44%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-8] round limit 8 hit
c [basicprobe-6-8] 111 units = 109 failed (98%) + 2 lifted (2%)
c [basicprobe-6-8] removed 158 variables, found 2146 hbrs
c [bate-4] eliminated 42 asymmetric tautologies during probing
c [unhide-14] limit 8636537 with penalty 1 = 0 + 1
c [unhide-14-17] 0 units, 0 failed, 14711 tauts, 0 hbrs, 19340 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 238 transitive binary clauses
c [cce-5] limit of 107956714 steps penalty 2 = 2 + 0
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] allowing another 53978357 steps for small clauses
c [cce-5-1] scheduling 175163 clauses = 52646 binary + 122517 ternary
c [cce-5-1] tried to eliminate 21 small clauses 0%
c [cce-5-1] eliminated 2 ternary clauses 0%
c [cce-5-1] eliminated 2 small clauses 0%
c [cce-5-1] eliminated 2 small clauses in 107956715 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2 covered clauses in round 1
c [cce-5] eliminated 2 covered clauses in TOTAL during 1 rounds
c [cce-5] 2 < 1/100 * 575113 = 5751 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 102365 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 5067 variables 5% in round 1 in 604678915 steps
c [elim-13-1] backward subsumption/strengthening limit 604678900
c [elim-13-1-1] backward checking 20291 touched variables 20%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 531 and strengthened 834 clauses in 71580656 steps
c [elim-13-1] rescheduled 2253 variables 2% by backward subsumption
c [elim-13-2] eliminated 261 variables 0% in round 2 in 259813185 steps
c [elim-13-2] backward subsumption/strengthening limit 259813100
c [elim-13-2-1] backward checking 1457 touched variables 1%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 74 and strengthened 189 clauses in 18775622 steps
c [elim-13-2] rescheduled 300 variables 0% by backward subsumption
c [elim-13-3] eliminated 66 variables 0% in round 3 in 84549677 steps
c [elim-13-3] backward subsumption/strengthening limit 84549600
c [elim-13-3-1] backward checking 240 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 23 and strengthened 43 clauses in 1036157 steps
c [elim-13] incomplete 101 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 5427 = 5% variables out of 102365 scheduled
c [bca-12] limit of 10000000 steps and 1126281 added (scaled 2)
c [bca-12] 140344 out of 193878 literals actually usable 72%
c [bca-12] added 594 blocked clauses in 505857 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 259096110 penalty 0 = 0 + 0
c [sweep-11-1] 34501 pos 50.0% + 34495 neg 50.0% = 68996 sched 71.2% ret 27942
c [sweep-11-1] 224301822 steps 22034 queries 1975.12 avg class size
c [sweep-11-1] 181408 decisions 21973 SAT calls 17.46 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-59] removed 4389 variables
c [sweep-11-1] removed 4389 vars (0 failed, 4359 eqs, 2841 impls)
c [sweep-11-2] 46173 pos 49.9% + 46376 neg 50.1% = 92549 sched 100.0% ret 0
c [sweep-11-2] 34813409 steps 1988 queries 10517.34 avg class size
c [sweep-11-2] 27191 decisions 2076 SAT calls 30.80 avg env size
c [sweep-11-2] 80225 variables remain 87% (12313 retained 13%)
c [decomp-60] removed 296 variables
c [sweep-11-2] removed 296 vars (0 failed, 280 eqs, 152 impls)
c [sweep-11] removed 4685 vars in TOTAL (2 rounds, 24020 queries)
c [sort-queue-16] sorted 35644 enqueued variables after 490116 conflicts
c [score-dist-16] active 56609 (61%), one 0 (0%), zero 35644 (39%)
c [score-dist-16] max exp 519, different 19 (4%)
c [score-dist-16] median active exp 506, avg 506.5
c [simplification-16] removed 10285 variables 10.0% (92253 remain 11%)
c [simplification-16] removed 27335 irredundant clauses 4.7% (549056 remain 23%)
c [simplification-16] maximum reduction of 10% = max (10%, 5%)
c [simplification-16] large reduction 10% >= 5% limit
c [simplification-16] next conflict interval 4901 = min (490116/100, 107130)
c [simplification-16] penalized conflict interval 4901 = 1 * 4901
c [simplification-16] hard conflict limit 505017 (soft 495017 + delta 10000)
c [simplification-16] new conflict limit 495017 (hard 505017)
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  725.7   92252   549033    495732   66398  74601 84976   45   133  113  34%    898  -40   48   47  102%
c 
c [simplification-17] limit 495017 conflicts (hard 505017) hit after 505017 conflicts
c [quatres-13] found 170824 quaternary clauses 56% in total
c [quatres-13-1] removed 1202 duplicate quaternary clauses
c [quatres-13-1] added 887 double-self-subsuming ternary resolvents
c [quatres-13-2] added 1112 single-self-subsuming ternary resolvents
c [quatres-13-2] added 6931 quaternary resolvents
c [ternres-13] limit 86922650 with penalty 0 = 0 + 0
c [ternres-13] all 92252 free variables schedulable
c [ternres-13] 23285 ternary resolvents (1424 bin, 21861 trn)
c [ternres-13] 251 variables remain 0% (92001 retained 100%)
c [gauss-8] limit 8692265 penalty 1 = 1 + 0
c [gauss-8] extracted 13456 xors of average arity 2.9
c [gauss-8] connected 38762 occurrences of 4677 variables (average 8.3)
c [gauss-8] limit 8692265 penalty 1 = 1 + 0
c [gauss-8] connected 12201 occurrences of 4677 variables (average 2.6)
c [gauss-8] fully completed
c [decomp-61] removed 469 variables
c [gauss-8] exported 0 unary, 14 binary and 3 ternary equations
c [simpleprobe-7] 1322 schedulable variables 1%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-63] removed 242 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 242 variables, found 2098 hbrs, 45 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 473 transitive binary clauses
c [transred-13] found 40 units
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 91499 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 5594 variables 6% in round 1 in 503682411 steps
c [elim-14-1] backward subsumption/strengthening limit 296317589
c [elim-14-1-1] backward checking 15316 touched variables 17%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 429 and strengthened 781 clauses in 89345468 steps
c [elim-14-1] rescheduled 1922 variables 2% by backward subsumption
c [elim-14] incomplete 2 not tried 0% in round 2
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 6205 = 7% variables out of 91499 scheduled
c [bca-13] limit of 10000000 steps and 1003254 added (scaled 2)
c [bca-13] 123507 out of 170590 literals actually usable 72%
c [bca-13] added 790 blocked clauses in 444224 steps
c [sweep-12] limit 26076795 penalty 0 = 0 + 0
c [sweep-12-1] 37351 pos 50.5% + 36591 neg 49.5% = 73942 sched 86.7% ret 11352
c [sweep-12-1] 26078286 steps 1812 queries 10139.49 avg class size
c [sweep-12-1] 21726 decisions 1858 SAT calls 25.94 avg env size
c [sweep-12-1] 65559 variables remain 77% (19730 retained 23%)
c [decomp-64] removed 243 variables
c [sweep-12-1] removed 243 vars (0 failed, 165 eqs, 80 impls)
c [sweep-12] removed 243 vars in TOTAL (1 rounds, 1811 queries)
c [sort-queue-17] sorted 33716 enqueued variables after 505017 conflicts
c [score-dist-17] active 51335 (60%), one 0 (0%), zero 33716 (40%)
c [score-dist-17] max exp 519, different 19 (4%)
c [score-dist-17] median active exp 506, avg 506.5
c [simplification-17] removed 7201 variables 7.8% (85051 remain 10%)
c [simplification-17] removed 55574 irredundant clauses 10.1% (493459 remain 21%)
c [simplification-17] maximum reduction of 10% = max (8%, 10%)
c [simplification-17] large reduction 10% >= 5% limit
c [simplification-17] next conflict interval 5050 = min (505017/100, 107130)
c [simplification-17] penalized conflict interval 5050 = 1 * 5050
c [simplification-17] hard conflict limit 520067 (soft 510067 + delta 10000)
c [simplification-17] new conflict limit 510067 (hard 520067)
c 
c [simplification-18] limit 510067 conflicts (hard 520067) hit after 520068 conflicts
c [quatres-14] found 155292 quaternary clauses 56% in total
c [quatres-14-1] removed 218 duplicate quaternary clauses
c [quatres-14-1] added 170 double-self-subsuming ternary resolvents
c [quatres-14-2] added 938 single-self-subsuming ternary resolvents
c [quatres-14-2] added 1830 quaternary resolvents
c [ternres-14] limit 88475681 with penalty 0 = 0 + 0
c [ternres-14] 233 schedulable variables 0%
c [ternres-14] 8963 ternary resolvents (919 bin, 8044 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-9] limit 17695136 penalty 0 = 0 + 0
c [gauss-9] extracted 68113 xors of average arity 3.7
c [gauss-9] connected 252415 occurrences of 22546 variables (average 11.2)
c [gauss-9] limit 17695136 penalty 0 = 0 + 0
c [gauss-9] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-65] removed 33 variables
c [treelook-7] limit 8847568 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 22894 literals 13%
c [treelook-7] scheduling used 1514196 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 8847568 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 8852713 steps
c [treelook-7] 17625 literals remain 10%
c [treelook-7] 3536 variables remain to probed next time 4%
c [decomp-66] removed 19 variables
c [treelook-7] removed 44 variables, found 2256 hbrs
c [unhide-15] limit 8847568 with penalty 1 = 1 + 0
c [unhide-15-20] 6 units, 103 failed, 15037 tauts, 0 hbrs, 17272 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 197 transitive binary clauses
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 84937 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 1568 variables 2% in round 1 in 487075778 steps
c [elim-15-1] backward subsumption/strengthening limit 312924222
c [elim-15-1-1] backward checking 5988 touched variables 7%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 138 and strengthened 268 clauses in 35091243 steps
c [elim-15-1] rescheduled 668 variables 1% by backward subsumption
c [elim-15-2] eliminated 121 variables 0% in round 2 in 129024747 steps
c [elim-15-2] backward subsumption/strengthening limit 129024700
c [elim-15-2-1] backward checking 542 touched variables 1%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 16 and strengthened 44 clauses in 7469845 steps
c [elim-15-2] rescheduled 117 variables 0% by backward subsumption
c [elim-15-3] eliminated 22 variables 0% in round 3 in 27845474 steps
c [elim-15-3] backward subsumption/strengthening limit 27845400
c [elim-15-3-1] backward checking 93 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 11 and strengthened 7 clauses in 428720 steps
c [elim-15] incomplete 29 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 1719 = 2% variables out of 84937 scheduled
c [bca-14] limit of 10000000 steps and 983775 added (scaled 2)
c [bca-14] 120856 out of 166438 literals actually usable 73%
c [bca-14] added 554 blocked clauses in 444460 steps
c [sweep-13] limit 26542704 penalty 0 = 0 + 0
c [sweep-13-1] 32544 pos 50.9% + 31449 neg 49.1% = 63993 sched 76.9% ret 19225
c [sweep-13-1] 26544922 steps 2112 queries 8926.51 avg class size
c [sweep-13-1] 22406 decisions 2200 SAT calls 21.36 avg env size
c [sweep-13-1] 55956 variables remain 67% (27256 retained 33%)
c [decomp-67] removed 236 variables
c [sweep-13-1] removed 236 vars (0 failed, 178 eqs, 67 impls)
c [sweep-13] removed 236 vars in TOTAL (1 rounds, 2111 queries)
c [sort-queue-18] sorted 32867 enqueued variables after 520068 conflicts
c [score-dist-18] active 50115 (60%), one 0 (0%), zero 32867 (40%)
c [score-dist-18] max exp 519, different 19 (4%)
c [score-dist-18] median active exp 506, avg 506.5
c [simplification-18] removed 2069 variables 2.4% (82982 remain 10%)
c [simplification-18] removed 9833 irredundant clauses 2.0% (483625 remain 21%)
c [simplification-18] maximum reduction of 2% = max (2%, 2%)
c [simplification-18] geometric conflict interval increment 35710 = 107130 / 3
c [simplification-18] new conflict interval 142840
c [simplification-18] penalized conflict interval 142840 = 1 * 142840
c [simplification-18] hard conflict limit 734328 (soft 662908 + delta 71420)
c [simplification-18] new conflict limit 662908 (hard 734328)
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  773.0   82981   483625    520106   61150  70887 72221   21   289  107   7%   -797  102   34   41   83%
c -  780.2   82981   483625    588969   66558  70903 72223   29   133  105  22%    252  -31   31   36   85%
c -  783.8   82981   483625    638499   67995  70905 72223   28    97  106  28%    661  -32   23   32   72%
c 
c [simplification-19] limit 662908 conflicts (hard 734328) hit after 664318 conflicts
c [quatres-15] found 151383 quaternary clauses 56% in total
c [quatres-15-1] removed 393 duplicate quaternary clauses
c [quatres-15-1] added 99 double-self-subsuming ternary resolvents
c [quatres-15-2] added 605 single-self-subsuming ternary resolvents
c [quatres-15-2] added 751 quaternary resolvents
c [ternres-15] limit 96409758 with penalty 0 = 0 + 0
c [ternres-15] all 82981 free variables schedulable
c [ternres-15] 15015 ternary resolvents (391 bin, 14624 trn)
c [ternres-15] 37 variables remain 0% (82944 retained 100%)
c [decomp-68] removed 94 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 35388 sched 43%, 68 failed, 1 lifted, 1387 hbrs
c [decomp-69] removed 85 variables
c [basicprobe-7-1] 35315 sched 43%, 1 failed, 0 lifted, 137 hbrs
c [decomp-70] removed 1 variables
c [basicprobe-7-2] 35313 sched 43%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-7-3] 35313 sched 43%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-7-4] 35312 sched 43%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-7-5] 35311 sched 43%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-7-5] fully completed probing
c [basicprobe-7-5] 70 units = 69 failed (99%) + 1 lifted (1%)
c [basicprobe-7-5] removed 86 variables, found 1533 hbrs
c [bate-5] eliminated 45 asymmetric tautologies during probing
c [unhide-16] limit 19281951 with penalty 0 = 0 + 0
c [unhide-16-26] 0 units, 0 failed, 16981 tauts, 0 hbrs, 24252 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 103 transitive binary clauses
c [cce-6] limit of 60256099 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 63
c [cce-6-1] eliminated 1 clauses out of 7 (14%) of length 34
c [cce-6-1] eliminated 1 clauses out of 8 (12%) of length 30
c [cce-6-1] eliminated 2 clauses out of 20 (10%) of length 29
c [cce-6-1] eliminated 2 clauses out of 30 (7%) of length 28
c [cce-6-1] eliminated 1 clauses out of 28 (4%) of length 27
c [cce-6-1] eliminated 2 clauses out of 37 (5%) of length 26
c [cce-6-1] eliminated 3 clauses out of 52 (6%) of length 25
c [cce-6-1] eliminated 5 clauses out of 78 (6%) of length 24
c [cce-6-1] eliminated 1 clauses out of 85 (1%) of length 23
c [cce-6-1] eliminated 2 clauses out of 91 (2%) of length 22
c [cce-6-1] eliminated 3 clauses out of 126 (2%) of length 21
c [cce-6-1] eliminated 5 clauses out of 130 (4%) of length 20
c [cce-6-1] eliminated 3 clauses out of 150 (2%) of length 19
c [cce-6-1] eliminated 5 clauses out of 217 (2%) of length 18
c [cce-6-1] eliminated 8 clauses out of 237 (3%) of length 17
c [cce-6-1] eliminated 14 clauses out of 337 (4%) of length 16
c [cce-6-1] eliminated 18 clauses out of 511 (4%) of length 15
c [cce-6-1] eliminated 15 clauses out of 652 (2%) of length 14
c [cce-6-1] eliminated 18 clauses out of 920 (2%) of length 13
c [cce-6-1] eliminated 16 clauses out of 925 (2%) of length 12
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 126 large clauses in 60256433 steps
c [cce-6-1] allowing another 30128216 steps for small clauses
c [cce-6-1] scheduling 154111 clauses = 41895 binary + 112216 ternary
c [cce-6-1] tried to eliminate 16166 small clauses 10%
c [cce-6-1] eliminated 134 binary clauses 0%
c [cce-6-1] eliminated 596 ternary clauses 1%
c [cce-6-1] eliminated 730 small clauses 0%
c [cce-6-1] eliminated 730 small clauses in 60256413 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 856 covered clauses in round 1
c [cce-6] eliminated 856 covered clauses in TOTAL during 1 rounds
c [cce-6] 856 < 1/100 * 482338 = 4823 considered unsuccessful
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 82802 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 868 variables 1% in round 1 in 470284840 steps
c [elim-16-1] backward subsumption/strengthening limit 329715160
c [elim-16-1-1] backward checking 4166 touched variables 5%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 113 and strengthened 167 clauses in 31336511 steps
c [elim-16-1] rescheduled 458 variables 1% by backward subsumption
c [elim-16-2] eliminated 75 variables 0% in round 2 in 109266395 steps
c [elim-16-2] backward subsumption/strengthening limit 109266300
c [elim-16-2-1] backward checking 388 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 14 and strengthened 29 clauses in 12345372 steps
c [elim-16-2] rescheduled 80 variables 0% by backward subsumption
c [elim-16-3] eliminated 18 variables 0% in round 3 in 50352799 steps
c [elim-16-3] backward subsumption/strengthening limit 50352700
c [elim-16-3-1] backward checking 94 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 23 and strengthened 23 clauses in 6408209 steps
c [elim-16] incomplete 60 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 973 = 1% variables out of 82802 scheduled
c [bca-15] limit of 10000000 steps and 968554 added (scaled 2)
c [bca-15] 121064 out of 163660 literals actually usable 74%
c [bca-15] added 449 blocked clauses in 463606 steps
c [sweep-14] limit 28922927 penalty 0 = 0 + 0
c [sweep-14-1] 27872 pos 50.5% + 27300 neg 49.5% = 55172 sched 67.4% ret 26657
c [sweep-14-1] 28956270 steps 2414 queries 7505.84 avg class size
c [sweep-14-1] 24771 decisions 2519 SAT calls 20.11 avg env size
c [sweep-14-1] 46530 variables remain 57% (35299 retained 43%)
c [decomp-74] removed 211 variables
c [sweep-14-1] removed 211 vars (0 failed, 208 eqs, 64 impls)
c [sweep-14] removed 211 vars in TOTAL (1 rounds, 2413 queries)
c [sort-queue-19] sorted 32079 enqueued variables after 664318 conflicts
c [score-dist-19] active 49539 (61%), one 0 (0%), zero 32079 (39%)
c [score-dist-19] max exp 520, different 20 (4%)
c [score-dist-19] median active exp 506, avg 506.5
c [simplification-19] removed 1363 variables 1.6% (81618 remain 10%)
c [simplification-19] removed 7686 irredundant clauses 1.6% (475939 remain 20%)
c [simplification-19] maximum reduction of 2% = max (2%, 2%)
c [simplification-19] geometric conflict interval increment 47613 = 142840 / 3
c [simplification-19] new conflict interval 190453
c [simplification-19] penalized conflict interval 190453 = 1 * 190453
c [simplification-19] hard conflict limit 949997 (soft 854771 + delta 95226)
c [simplification-19] new conflict limit 854771 (hard 949997)
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 -  828.0   81618   475939    693727   67116  67337 68803   16   325  105   5%    868   90   17   25   69%
c -  838.3   81618   475939    746576   66409  67347 68804   14   220  105   7%    954  -33   15   19   79%
c -  853.5   81618   475939    794033   68457  67401 68859   11   326  105   3%    990   91   15   16   94%
c -  876.5   81618   475939    837194   66757  67438 68875   16   777  105   2%   1007  491   21   15  143%
c 
c [simplification-20] limit 854771 conflicts (hard 949997) hit after 854771 conflicts
c [quatres-16] found 148765 quaternary clauses 56% in total
c [quatres-16-1] removed 164 duplicate quaternary clauses
c [quatres-16-1] added 49 double-self-subsuming ternary resolvents
c [quatres-16-2] added 340 single-self-subsuming ternary resolvents
c [quatres-16-2] added 983 quaternary resolvents
c [ternres-16] limit 119267161 with penalty 0 = 0 + 0
c [ternres-16] 35 schedulable variables 0%
c [ternres-16] 1875 ternary resolvents (77 bin, 1798 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-10] limit 11926716 penalty 1 = 1 + 0
c [gauss-10] extracted 18266 xors of average arity 3.0
c [gauss-10] connected 54382 occurrences of 4061 variables (average 13.4)
c [gauss-10] limit 11926716 penalty 1 = 1 + 0
c [gauss-10] connected 19702 occurrences of 4061 variables (average 4.9)
c [gauss-10] fully completed
c [gauss-10] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-75] removed 45 variables
c [simpleprobe-8] all 81573 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-76] removed 146 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 146 variables, found 4028 hbrs, 26 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 281 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 81427 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 437 blocked clauses
c [block-6] 437 < 1/100 * 474733 = 4747 considered unsuccessful
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 81377 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 451 variables 1% in round 1 in 456689450 steps
c [elim-17-1] backward subsumption/strengthening limit 343310550
c [elim-17-1-1] backward checking 2384 touched variables 3%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 83 and strengthened 105 clauses in 31351965 steps
c [elim-17-1] rescheduled 292 variables 0% by backward subsumption
c [elim-17-2] eliminated 63 variables 0% in round 2 in 74080721 steps
c [elim-17-2] backward subsumption/strengthening limit 74080700
c [elim-17-2-1] backward checking 306 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 18 and strengthened 45 clauses in 3043008 steps
c [elim-17-2] rescheduled 81 variables 0% by backward subsumption
c [elim-17-3] eliminated 13 variables 0% in round 3 in 4004227 steps
c [elim-17-3] backward subsumption/strengthening limit 4004200
c [elim-17-3-1] backward checking 76 touched variables 0%
c [elim-17-3-1] fully completed backward checking in 1 rounds
c [elim-17-3] subsumed 6 and strengthened 24 clauses in 775993 steps
c [elim-17] incomplete 35 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 541 = 1% variables out of 81377 scheduled
c [elim-17] 541 < 1/100 * 81377 = 813 considered unsuccessful
c [bca-16] limit of 10000000 steps and 958420 added (scaled 2)
c [bca-16] 119449 out of 161674 literals actually usable 74%
c [bca-16] added 180 blocked clauses in 459202 steps
c [sweep-15] limit 35780148 penalty 0 = 0 + 0
c [sweep-15-1] 23779 pos 51.6% + 22297 neg 48.4% = 46076 sched 57.0% ret 34760
c [sweep-15-1] 35790647 steps 3330 queries 5506.81 avg class size
c [sweep-15-1] 34740 decisions 3481 SAT calls 19.79 avg env size
c [sweep-15-1] 35101 variables remain 43% (45732 retained 57%)
c [decomp-77] removed 334 variables
c [sweep-15-1] removed 334 vars (0 failed, 298 eqs, 107 impls)
c [sweep-15] removed 334 vars in TOTAL (1 rounds, 3329 queries)
c [sort-queue-20] sorted 30961 enqueued variables after 854771 conflicts
c [score-dist-20] active 49541 (62%), one 0 (0%), zero 30961 (38%)
c [score-dist-20] max exp 520, different 20 (4%)
c [score-dist-20] median active exp 506, avg 506.7
c [simplification-20] removed 1116 variables 1.4% (80502 remain 10%)
c [simplification-20] removed 5213 irredundant clauses 1.1% (470726 remain 20%)
c [simplification-20] maximum reduction of 1% = max (1%, 1%)
c [simplification-20] geometric conflict interval increment 95226 = 190453 / 2
c [simplification-20] new conflict interval 285679
c [simplification-20] penalized conflict interval 285679 = 1 * 285679
c [simplification-20] hard conflict limit 1283289 (soft 1140450 + delta 142839)
c [simplification-20] new conflict limit 1140450 (hard 1283289)
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 -  920.1   80502   470725    930954   69226  67564 71441   38   393  104  10%   1020  134   57   30  191%
c -  935.7   80502   470725    969674   69608  67579 71441   15   364  104   4%   1022   40   14   27   53%
c -  945.1   80502   470725   1009157   69635  67581 71441   14   326  104   4%   1023   -5   13   21   62%
c -  952.6   80502   470725   1050337   69427  67583 71441   18   240  104   7%   1023  -78   17   19   93%
c -  966.1   80502   470725   1101093   71398  67590 71441   18   210  104   8%   1024  -61   17   18   95%
c -  976.9   80502   470716   1147170   72599  67607 71444   28   189  105  15%   1024  -59   34   18  189%
c 
c [simplification-21] limit 1140450 conflicts (hard 1283289) hit after 1178948 conflicts
c [quatres-17] found 148078 quaternary clauses 56% in total
c [quatres-17-1] removed 148 duplicate quaternary clauses
c [quatres-17-1] added 43 double-self-subsuming ternary resolvents
c [quatres-17-2] added 195 single-self-subsuming ternary resolvents
c [quatres-17-2] added 566 quaternary resolvents
c [ternres-17] limit 149513628 with penalty 0 = 0 + 0
c [ternres-17] all 80502 free variables schedulable
c [ternres-17] 15758 ternary resolvents (528 bin, 15230 trn)
c [ternres-17] 2 variables remain 0% (80500 retained 100%)
c [card-6] limit 4672300 penalty 4 = 4 + 0
c [card-6] found 3552 at-most-one constraints of average size 4.3
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 4672300 for elimination
c [card-6] 3552 out of 3552 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-78] removed 97 variables
c [treelook-8] limit 14951362 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 20501 literals 13%
c [treelook-8] scheduling used 1481037 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 14951362 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 14951369 steps
c [treelook-8] 11713 literals remain 7%
c [treelook-8] 2831 variables remain to probed next time 4%
c [decomp-79] removed 9 variables
c [treelook-8] removed 53 variables, found 1972 hbrs
c [unhide-17] limit 10000000 with penalty 1 = 1 + 0
c [unhide-17-29] 6 units, 43 failed, 12890 tauts, 0 hbrs, 41090 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 141 transitive binary clauses
c [bca-17] limit of 10000000 steps and 955864 added (scaled 2)
c [bca-17] 118109 out of 160666 literals actually usable 74%
c [bca-17] added 333 blocked clauses in 480503 steps
c [sweep-16] limit 44854088 penalty 0 = 0 + 0
c [sweep-16-1] 18084 pos 51.6% + 16942 neg 48.4% = 35026 sched 43.6% ret 45306
c [sweep-16-1] 44856697 steps 5695 queries 2990.78 avg class size
c [sweep-16-1] 47534 decisions 5906 SAT calls 16.42 avg env size
c [sweep-16-1] 17853 variables remain 22% (62475 retained 78%)
c [decomp-80] removed 445 variables
c [sweep-16-1] removed 445 vars (0 failed, 420 eqs, 156 impls)
c [sweep-16] removed 445 vars in TOTAL (1 rounds, 5694 queries)
c [sort-queue-21] sorted 29649 enqueued variables after 1178948 conflicts
c [score-dist-21] active 50238 (63%), one 0 (0%), zero 29649 (37%)
c [score-dist-21] max exp 520, different 20 (4%)
c [score-dist-21] median active exp 506, avg 506.9
c [simplification-21] removed 615 variables 0.8% (79887 remain 9%)
c [simplification-21] removed 1539 irredundant clauses 0.3% (469176 remain 20%)
c [simplification-21] maximum reduction of 1% = max (1%, 0%)
c [simplification-21] geometric conflict interval increment 142839 = 285679 / 2
c [simplification-21] new conflict interval 428518
c [simplification-21] penalized conflict interval 428518 = 1 * 428518
c [simplification-21] hard conflict limit 1821725 (soft 1607466 + delta 214259)
c [simplification-21] new conflict limit 1607466 (hard 1821725)
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  996.1   79886   469176   1180264   99676  70630 69572   28   777  114   4%   1024  543   16   19   83%
c i  997.4   79885   469170   1180771  100064  70632 69573   26   954  114   3%  -2989  715    9   19   49%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 1286 basic ate = 872 trn 68% + 414 lrg 32% in 5 updates
c bcas: 17 count, 32626 added (3501 skipped), 9475830 steps
c bkwd: tried 3218007 clauses, 6422830 lits, 2.00 lits/clause
c bkwd: checked 873858719 occs, 271.55 occs/clause, 136.06 occs/lit
c bkwd: subsumed 56 binary, 1316 ternary, 3588 large
c bkwd: strengthened 1272 binary, 1280 ternary (100% self), 13024 large (0% self)
c blkd: 6 bces, 80861 removed, 25235679 resolutions, 67936712 steps
c blkd: 26264 blocking literals 1%, 392 pure
c bump: 1182536 bumped seen, 117772109 lits 99.6 on average
c card: 6 count, 0 units, 0 am1, 33169384 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 18648 subsumed
c card: 8545 at-most-one constraints found, average size 4.55
c card: 8545 at-most-one constraints used 100%, average size 4.55
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: 6 cces, 18127 eliminated, 18125 ate 100%, 2 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 8683184 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 157 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 80 decompositions, 111637 equivalent 12%
c deco: 3586 decision-only clauses 0%, 47% reduction
c decs: 144676277 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 17 elims, 648203 eliminated 72%, 986 pure 0%
c elms: 36 rounds, 2.1 rounds/bve
c elms: 627954 small 97%, 18871 large 3%
c elms: 1143946 tried small, 627955 succeeded 55%, 515991 failed 45%
c elms: 74884 subsumed, 89054 strengthened, 5260 blocked
c elms: 41954490 copies, 54164868 resolutions, 49032336 ipos
c elms: 83951619 subchks, 43216571 strchks
c gaus: 10 extractions, 148981 extracted, 3.3 size, 4 max
c gaus: exported 0 units, 17 binary and 12 ternary equations
c gaus: 2 gc, 117123496 steps, 58561748 extr 50%, 46237408 elim 39%
c glue: 27.6 orig avg, 27.6 real avg, 4.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 200887 = 34335 simple 17% + 155655 trn 77% + 10897 lrg 5%, 7358 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1182536 clauses, 36.9 length
c lrnd: 43626610 lits = 83522995 orig - 39896385 removed 48%
c lrnd: 249079 uips 21%, 354286 flips 30%
c mins: 1147573 mins 97%, 2225 bin 0%, 28090 size 2%
c mins: 20957102 poisoned searches, 1555007 hits, 7% hit rate
c mins: 97816766 used twice searches, 21979523 hits, 22% hit rate
c move: moved 57996, 20510 bin 35%, 37486 trn 65%
c otfs: 36120 driving 46%, 41812 restarting 54%
c otfs: str 77932, 73765 red 95%, 4167 irr 5%
c otfs: str 77932, 0 bin 0%, 9221 trn 12%, 68711 lrg 88%
c otfs: sub 7392, 6800 red 92%, 592 irr 8%
c otfs: sub 7392, 0 bin 0%, 1301 trn 18%, 6091 lrg 82%
c phas: 3 computed, 694021 set, 40801 pos (6%), 653220 neg (94%)
c prbs: 7 basic, 2335419 probed, 1469 failed, 16 lifted
c prbs: 8 simple, 1097064 probed, 527 failed, 3466 eqs
c prbs: 8 treelook, 21848 probed, 89 failed, 0 lifted
c prom: 37650 locked 4% out of 970495 tried
c prps: 1729037251 props, 11 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 17 count, 95841 quat, 26955 self1, 5509 self2, 14375 dup
c queu: 21 sorted, 144676278 next (2947565 steps 0.02)
c queu: 121264652 enq (189472739 steps 1.56), 117772109 deq 97%
c redc: 6247 clauses 7%, 93838 tried 8%, 28 sat 0%
c redc: 9673 lits 1%, 673243 tried 1%, 28 sat 0%
c redc: 826 times jump level reduced, 136.2 levels on average
c reds: 18 count, 65623.4 conflicts per reduce
c reds: 0 memlim 0%, 18 arith 100%
c reds: 526765 collected 90%, 55630 retired 10%
c rmbd: 49363 removed, 26398 red 53%
c rsts: 19058 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 21 count, 18 confs 86%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 1 trns 5%
c subl: 1182536 count (1293481 tried 1.1), 431793 sub out of 1157750 (37.3%)
c swps: 16 count, 17 rounds, 46756 queries (2750.4/round)
c swps: 47381 sat calls, 7683 unsat (0.8% success rate)
c swps: 444651 decisions 9.4, 37434 conflicts 0.8
c swps; 5834.0 avg class size, 20.2 avg environment size
c swps: 0 failed, 4250 impls, 6924 equivs
c swp0: 15580 type 0 queries, 1719 unsat (11.0%), 15002 sat (96.3%)
c swp1: 31176 type 1 queries, 15104 unsat (48.4%), 24830 sat (79.6%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 291718128 calls to obtain time
c tops: 62528 fixed 7%, 62 its, 19051.97 confs/it
c trds: 17 transitive reductions, 3800 removed, 72 failed
c trds: 415205 nodes, 256873 edges, 34003858 steps
c trim: 3617565 words, 13.8 MB
c trnr: 17 count, 10718 bin, 220405 trn, 844683205 steps
c unhd: 17 count, 29 rounds, 136356635 steps
c unhd: 1822 non-trivial sccs of average size 2.1
c unhd: 179 units, 175 bin, 4 trn, 0 lrg
c unhd: 3348 failed, 3297 stamp, 0 lits, 11 bin, 33 trn, 0 lrg
c unhd: 110454 tauts, 1918 bin 2%, 69811 trn 63%, 6122 lrg 6%
c unhd: 110454 tauts, 32603 stamp 30%, 104557 red 95%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 269990 str, 175 bin 0%, 43069 trn 16%, 226746 lrg 84%, 157964 red 59%
c vars: 80843 remaining 9% and 822368 removed 91% out of 903211
c vars: 62528 fixed 7%, 648203 eliminated 72%, 111637 equivalent 12%
c vsts: 15892136507 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 9.3 search visits per propagation, 12716.8 per conflict
c wchs: 1050209202 pushed, 131874023 enlarged, 258 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1253591        526765         55630      50244684      10580309        477483
c 
c  0 0        148711  12       278   0         0   0  29685688  59   3532519  33     63430  13     1.6
c  1 5         21776   2      5353   1      6664  12   4270425   8<   609742   6     19634   4     0.3
c  2 6         69296   6     27318   5     14539  26   6386500  13   1269789  12<    65751  14     0.9
c  3 9        197938  16    119209  23     19209  35<  4722314   9   1530380  14    135552  28<    3.2
c  4 14       283016  23<   180754  34      9523  17   2995668   6   1846365  17    113837  24     3.6
c  5 21       107966   9     65226  12<     2724   5   1310171   3   1099120  10     49460  10     3.0
c  6 30       127722  10     57038  11      1454   3    311087   1    249637   2     16341   3     6.2
c  7 41       202683  16     29000   6       411   1    295070   1    254168   2      4268   1    21.5
c  8 54        55550   4     22550   4       401   1    163896   0    124296   1      4834   1     3.7
c  9 69        17705   1      9027   2       236   0     49040   0     24577   0       984   0     3.3
c 10 86        13868   1      8436   2       158   0     29168   0     18687   0       661   0     2.5
c 11 126        2980   0      2295   0       190   0     10132   0      6750   0       401   0     1.3
c 12 230        4217   0       276   0       102   0     15326   0     14161   0      2330   0     5.8
c 13 534         163   0         5   0        19   0       199   0       118   0         0   0     0.3
c 
c avg                  4.3           4.5           3.0           1.1           2.4           3.1
c std                  2.5           1.8           1.5           1.7           2.2           1.9
c 
c  137.119  14% elim
c   98.238  10% decide
c   82.843   8% sweep
c   57.320   6% probe
c   24.093   2% cce
c   19.346   2% bump
c   16.777   2% unhide
c   16.300   2% quatres
c   10.083   1% gauss
c    7.626   1% ternres
c 
c   16.929 < 1% rest (below)
c 
c    7.282   1% bca
c    7.169   1% block
c    1.624   0% transred
c    0.855   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    9.068   1% preprocessing     2%
c  378.496  38% inprocessing     98%
c ==================================
c  387.564  39% simplifying
c  610.941  61% search
c ==================================
c  998.521 100% all
c 
c       1181222 conflicts,        1183.0 confs/sec
c          7554 ternaries,         156.4 confs/ternary
c          1313 binaries,          899.6 confs/binary
c            62 iterations,      19052.0 confs/iteration
c 
c            18 reductions,          0.0 redus/sec,  65623.4 confs/reduction
c         19058 restarts,           19.1 rests/sec,     62.0 confs/restart
c     144676277 decisions,      144890.5 decis/sec,    122.5 decis/conflict
c    1729037251 propagations,  1731597.9 props/sec,     12.0 props/decision
c 
c 998.5 seconds, 281.7 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
