c launch: /data/cnf/sc2014/app/SAT_dat.k80-24_1_rule_1.cnf.bz2
c host: atom26
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/SAT_dat.k80-24_1_rule_1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k80-24_1_rule_1.cnf.bz2
c no embedded options
c found 'p cnf 1295022 5074584' header
c read 1295022 variables, 5074584 clauses, 12738687 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=3
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 1254609 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] SUM (--score=3)
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 1254609  5034037         0       0      0     0    0     0  269   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1258509 based on 5034037 irredundant clauses
c [card-1] found 1110 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1258509 for elimination
c [card-1] 1110 out of 1110 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 290169 variables
c [simpleprobe-1] all 1004853 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 8169634 based on 4084817 irredundant clauses
c [decomp-2] removed 4817 variables
c [simpleprobe-1] 841701 variables remain 84% (158335 retained 16%)
c [simpleprobe-1] removed 4817 variables, found 11413 hbrs, 890 units
c [unhide-1] limit 253649 based on 4058388 irredundant clauses
c [unhide-1-1] 1132 units, 1130 failed, 8597 tauts, 0 hbrs, 49436 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 994535 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 913954 not tried 92% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 80906 = 8% variables out of 994535 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3603833 negative 95.2% of 3785343 except 181510 4.8%
c [phase-count-1] 3544623 positive 93.6% of 3785343 except 240720 6.4%
c [phase-1] phase bias: 424252 positive 46%, 489377 negative 54%
c [sort-queue-1] sorted 913629 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 913629 (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 172545 variables 15.9% (913629 remain 73%)
c [simplification-1] removed 1248694 irredundant clauses 24.8% (3785343 remain 75%)
c [simplification-1] maximum reduction of 25% = max (16%, 25%)
c [simplification-1] large reduction 25% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   15.6  913628  3785343         5       3     11 10292    0     0  234   1%      0    0    0    0 25320%
c i   15.6  913491  3785343         7       4     11 10292    0     0  234   1%      0    0    0    0 25182%
c i   15.6  913490  3785343        18      10     11 10296    0     0  234   2%      0    0    0    0 24630%
c i   15.6  913439  3785343        19      10     11 10296    0     0  234   2%      0    0    0    0 24534%
c i   15.7  913437  3785343        54      30     20 10301    0     1  234   3%      0    1    0    0 23490%
c i   16.1  913204  3785343       286     191     51 10327    0     3  235   8%      0    3    2    0 15630%
c i   16.1  913194  3785343       287     191     51 10327    0     3  235   8%      0    3    2    0 15569%
c i   16.3  912894  3785343       361     245     58 10337    0     4  235   7%      0    4    2    0 13558%
c i   17.5  912893  3785343       647     452     92 10374    1     8  235   7%      1    8    4    0 10983%
c i   17.5  912892  3785343       667     467     92 10378    1     8  235   7%      1    8    4    0 10625%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 4409 variables
c [simpleprobe-2] 765538 schedulable variables 84%
c [simpleprobe-2] limit 7543718 based on 3771859 irredundant clauses
c [decomp-4] removed 2663 variables
c [simpleprobe-2] 770499 variables remain 85% (136058 retained 15%)
c [simpleprobe-2] removed 2663 variables, found 34887 hbrs, 144 units
c [treelook-1] limit 940293 based on 3761173 irredundant clauses
c [treelook-1] scheduled 187969 literals 10%
c [treelook-1] scheduling used 940344 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 940293 based on 3761173 irredundant clauses
c [treelook-1] used 940498 steps
c [treelook-1] 187605 literals remain 10%
c [treelook-1] 185342 variables remain to probed next time 20%
c [decomp-5] removed 121 variables
c [treelook-1] removed 179 variables, found 3259 hbrs
c [basicprobe-1] limit 30083960 based on 3760495 irredundant clauses
c [basicprobe-1-0] 817370 probes remain 91% after last round
c [basicprobe-1-0] 4127 units = 2199 failed (53%) + 1928 lifted (47%)
c [basicprobe-1-0] removed 8939 variables, found 197842 hbrs
c [unhide-2] limit 235030 based on 3760495 irredundant clauses
c [unhide-2-2] 818 units, 1299 failed, 12679 tauts, 0 hbrs, 34327 literals
c [elim-2] 895192 variables 100% will be scheduled this time
c [elim-2] scheduled 895192 variables 100%
c [elim-2] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 813063 not tried 91% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 82131 = 9% variables out of 895192 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 3347088 negative 95.1% of 3519384 except 172296 4.9%
c [phase-count-2] 3286773 positive 93.4% of 3519384 except 232611 6.6%
c [phase-2] phase bias: 1096 positive 31%, 2388 negative 69%
c [sort-queue-2] sorted 803262 enqueued variables after 667 conflicts
c [score-dist-2] active 9799 (1%), one 0 (0%), zero 803262 (99%)
c [score-dist-2] max exp 516, different 16 (3%)
c [score-dist-2] median active exp 511, avg 511.0
c [simplification-2] removed 99440 variables 10.9% (813061 remain 65%)
c [simplification-2] removed 265959 irredundant clauses 7.0% (3519384 remain 70%)
c [simplification-2] maximum reduction of 11% = max (11%, 7%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1027 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   39.3  813060  3519384       755     404     81 172575    1     9  228   8%      1    9    5    0 10918%
c i   39.3  813059  3519384       756     404     81 172575    1     9  228   8%      1    9    5    0 10876%
c i   39.5  813058  3519384       853     483     91 172578    1    10  228  11%      1   10    9    0 12181%
c 
c [simplification-3] limit 1037 conflicts (hard 11000) hit after 1040 conflicts
c [card-2] limit 879846 based on 3519384 irredundant clauses
c [card-2] found 782 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 879846 for elimination
c [card-2] 782 out of 782 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 5162 variables
c [treelook-2] limit 877670 based on 3510680 irredundant clauses
c [treelook-2] scheduled 165437 literals 10%
c [treelook-2] scheduling used 877709 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 877670 based on 3510680 irredundant clauses
c [treelook-2] used 882136 steps
c [treelook-2] 165330 literals remain 10%
c [treelook-2] 103907 variables remain to probed next time 13%
c [decomp-7] removed 191 variables
c [treelook-2] removed 231 variables, found 1661 hbrs
c [unhide-3] limit 219351 based on 3509620 irredundant clauses
c [unhide-3-3] 351 units, 590 failed, 16937 tauts, 0 hbrs, 17738 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 806614 variables 100%
c [elim-3] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 726234 not tried 90% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 80380 = 10% variables out of 806614 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 3146812 negative 95.0% of 3312756 except 165944 5.0%
c [phase-count-3] 3086122 positive 93.2% of 3312756 except 226634 6.8%
c [phase-3] phase bias: 681 positive 30%, 1627 negative 70%
c [sort-queue-3] sorted 714180 enqueued variables after 1040 conflicts
c [score-dist-3] active 12054 (2%), one 0 (0%), zero 714180 (98%)
c [score-dist-3] max exp 518, different 18 (3%)
c [score-dist-3] median active exp 512, avg 512.1
c [simplification-3] removed 86824 variables 10.7% (726234 remain 58%)
c [simplification-3] removed 206628 irredundant clauses 5.9% (3312756 remain 66%)
c [simplification-3] maximum reduction of 11% = max (11%, 6%)
c [simplification-3] large reduction 11% >= 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 13040 (soft 3040 + delta 10000)
c [simplification-3] new conflict limit 3040 (hard 13040)
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   55.0  726233  3312756      1277     692    108 142129    2    13  221  15%      2   13   10    0 7562%
c i   55.5  726232  3312756      1566     924    124 142141    3    15  221  18%      2   15   11    0 5728%
c i   55.7  726231  3312756      1621     959    135 142148    3    16  221  16%      2   16    9    0 4848%
c i   57.5  726230  3312756      2200    1426    189 142183    3    26  222  12%      3   25    9    0 3722%
c 
c [simplification-4] limit 3040 conflicts (hard 13040) hit after 3040 conflicts
c [decomp-8] removed 959 variables
c [basicprobe-2] limit 26482872 based on 3310359 irredundant clauses
c [basicprobe-2-0] 557342 probes remain 77% after last round
c [basicprobe-2-0] 1272 units = 1190 failed (94%) + 82 lifted (6%)
c [basicprobe-2-0] removed 2768 variables, found 126744 hbrs
c [unhide-4] limit 206897 based on 3310359 irredundant clauses
c [unhide-4-4] 365 units, 494 failed, 13128 tauts, 0 hbrs, 33914 literals
c [elim-4] 721633 variables 100% will be scheduled this time
c [elim-4] scheduled 721633 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 170366860 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 68020 not tried 9% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 403765 = 56% variables out of 721633 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 2223068 negative 95.8% of 2320437 except 97369 4.2%
c [phase-count-4] 2182441 positive 94.1% of 2320437 except 137996 5.9%
c [phase-4] phase bias: 3594 positive 42%, 4928 negative 58%
c [sort-queue-4] sorted 306063 enqueued variables after 3040 conflicts
c [score-dist-4] active 11805 (4%), one 0 (0%), zero 306063 (96%)
c [score-dist-4] max exp 521, different 20 (4%)
c [score-dist-4] median active exp 515, avg 514.8
c [simplification-4] removed 408362 variables 56.2% (317868 remain 25%)
c [simplification-4] removed 992319 irredundant clauses 30.0% (2320437 remain 46%)
c [simplification-4] maximum reduction of 56% = max (56%, 30%)
c [simplification-4] large reduction 56% >= 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 15040 (soft 5040 + delta 10000)
c [simplification-4] new conflict limit 5040 (hard 15040)
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   86.2  317867  2320437      3232     698    135 66953    5    47  202  10%      7   46    8    0 1949%
c i   86.4  317866  2320437      3287     740    137 66954    5    48  202  10%      7   47    8    0 1982%
c i   90.3  317865  2320435      4885    2196    216 66965    9    64  202  15%     13   62   26    1 3076%
c 
c [simplification-5] limit 5040 conflicts (hard 15040) hit after 5040 conflicts
c [quatres-1] found 276914 quaternary clauses 36% in total
c [quatres-1-1] removed 2 duplicate quaternary clauses
c [quatres-1-1] added 89 double-self-subsuming ternary resolvents
c [quatres-1-2] added 4625 single-self-subsuming ternary resolvents
c [quatres-1-2] added 8608 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 10000000 with penalty 1 = 0 + 1
c [ternres-1] all 317865 free variables schedulable
c [ternres-1] 41361 ternary resolvents (64 bin, 41297 trn)
c [ternres-1] 210731 variables remain 66% (107134 retained 34%)
c [gauss-1] limit 1159700 based on 2319401 irredundant clauses
c [gauss-1] extracted 5067 xors of average arity 3.0
c [gauss-1] connected 15055 occurrences of 5828 variables (average 2.6)
c [gauss-1] limit 1159691 based on 2319383 irredundant clauses
c [decomp-9] removed 1461 variables
c [gauss-1] exported 0 unary, 2 binary and 0 ternary equations
c [decomp-10] removed 4 variables
c [simpleprobe-3] 270116 schedulable variables 85%
c [simpleprobe-3] limit 5571223 penalty 1 = 0 + 1
c [decomp-11] removed 203 variables
c [simpleprobe-3] 271767 variables remain 86% (44430 retained 14%)
c [simpleprobe-3] removed 203 variables, found 10208 hbrs, 37 units
c [unhide-5] limit 144646 based on 2314336 irredundant clauses
c [unhide-5-5] 63 units, 175 failed, 83285 tauts, 0 hbrs, 125814 literals
c [transred-1] limit 2245510 based on 2245510 irredundant clauses
c [transred-1] removed 921 transitive binary clauses
c [transred-1] found 26 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 315951 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 250000000 steps penalty 1 = 0 + 1
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 24564 blocked clauses
c [cce-1] limit of 15000000 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 24
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 22
c [cce-1-1] eliminated 4 clauses out of 7 (57%) of length 21
c [cce-1-1] eliminated 6 clauses out of 23 (26%) of length 20
c [cce-1-1] eliminated 13 clauses out of 64 (20%) of length 19
c [cce-1-1] eliminated 271 clauses out of 1255 (22%) of length 18
c [cce-1-1] eliminated 262 clauses out of 1338 (20%) of length 17
c [cce-1-1] eliminated 274 clauses out of 643 (43%) of length 16
c [cce-1-1] eliminated 69 clauses out of 1846 (4%) of length 15
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 903 large clauses in 15000016 steps
c [cce-1-1] allowing another 7500008 steps for small clauses
c [cce-1-1] scheduling 1221102 clauses = 975086 binary + 246016 ternary
c [cce-1-1] tried to eliminate 2430 small clauses 0%
c [cce-1-1] eliminated 412 binary clauses 0%
c [cce-1-1] eliminated 81 ternary clauses 0%
c [cce-1-1] eliminated 493 small clauses 0%
c [cce-1-1] eliminated 493 small clauses in 15000229 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1396 covered clauses in round 1
c [cce-1] eliminated 1396 covered clauses in TOTAL during 1 rounds
c [cce-1] 1396 < 1/100 * 2217631 = 22176 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 315464 variables 100%
c [elim-5] limit of 27856119 steps penalty 1 = 0 + 1
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 185454 not tried 59% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 12358 = 4% variables out of 315464 scheduled
c [bca-1] limit of 10000000 steps and 4384074 added (scaled 2)
c [bca-1] 582085 out of 606214 literals actually usable 96%
c [bca-1] added 6941 blocked clauses in 1855136 steps
c [sweep-1] limit 4383574 based on 2191787 irredundant clauses
c [sweep-1-1] 99612 pos 32.9% + 203494 neg 67.1% = 303106 sched 100.0% ret 0
c [sweep-1-1] 4425945 steps 100 queries 99501.50 avg class size
c [sweep-1-1] 1142 decisions 88 SAT calls 32.18 avg env size
c [sweep-1-1] 302724 variables remain 100% (373 retained 0%)
c [decomp-12] removed 418 variables
c [sweep-1-1] removed 418 vars (0 failed, 25 eqs, 34 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 418 vars in TOTAL (1 rounds, 99 queries)
c [phase-count-5] 2096961 negative 95.7% of 2190829 except 93868 4.3%
c [phase-count-5] 2072378 positive 94.6% of 2190829 except 118451 5.4%
c [phase-5] phase bias: 1085 positive 52%, 985 negative 48%
c [sort-queue-5] sorted 284115 enqueued variables after 5040 conflicts
c [score-dist-5] active 18573 (6%), one 0 (0%), zero 284115 (94%)
c [score-dist-5] max exp 523, different 22 (4%)
c [score-dist-5] median active exp 516, avg 515.9
c [simplification-5] removed 15177 variables 4.8% (302688 remain 24%)
c [simplification-5] removed 129606 irredundant clauses 5.6% (2190829 remain 44%)
c [simplification-5] maximum reduction of 6% = max (5%, 6%)
c [simplification-5] large reduction 6% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 17040 (soft 7040 + delta 10000)
c [simplification-5] new conflict limit 7040 (hard 17040)
c 
c [simplification-6] limit 7040 conflicts (hard 17040) hit after 7043 conflicts
c [quatres-2] found 284830 quaternary clauses 38% in total
c [quatres-2-1] removed 14 duplicate quaternary clauses
c [quatres-2-1] added 52 double-self-subsuming ternary resolvents
c [quatres-2-2] added 2073 single-self-subsuming ternary resolvents
c [quatres-2-2] added 7451 quaternary resolvents
c [ternres-2] limit 8762708 based on 2190677 irredundant clauses
c [ternres-2] 200665 schedulable variables 66%
c [ternres-2] 36487 ternary resolvents (819 bin, 35668 trn)
c [ternres-2] 131352 variables remain 43% (171336 retained 57%)
c [card-3] limit 547669 based on 2190677 irredundant clauses
c [card-3] found 278 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 547669 for elimination
c [card-3] 278 out of 278 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 1095338 based on 2190677 irredundant clauses
c [gauss-2] extracted 4824 xors of average arity 3.0
c [gauss-2] connected 14424 occurrences of 5629 variables (average 2.6)
c [gauss-2] limit 1095338 based on 2190677 irredundant clauses
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 270 variables
c [treelook-3] limit 547566 based on 2190266 irredundant clauses
c [treelook-3] scheduled 64334 literals 11%
c [treelook-3] scheduling used 547617 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 547566 based on 2190266 irredundant clauses
c [treelook-3] used 548566 steps
c [treelook-3] 64156 literals remain 11%
c [treelook-3] 38314 variables remain to probed next time 13%
c [decomp-14] removed 18 variables
c [treelook-3] removed 25 variables, found 1166 hbrs
c [unhide-6] limit 136884 based on 2190155 irredundant clauses
c [unhide-6-6] 213 units, 407 failed, 3892 tauts, 0 hbrs, 65592 literals
c [transred-2] limit 2187919 based on 2187919 irredundant clauses
c [transred-2] removed 866 transitive binary clauses
c [transred-2] found 28 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 301731 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 0 + 1
c [block-2] incomplete 1415 not tried 0%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 8480 blocked clauses
c [block-2] 8480 < 1/100 * 2187228 = 21872 considered unsuccessful
c [elim-6] 66583 variables 22% will be scheduled this time
c [elim-6] scheduled 66583 variables 22%
c [elim-6] limit of 48169757 steps penalty 1 = 0 + 1
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 23832 not tried 8% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 808 = 1% variables out of 66583 scheduled
c [elim-6] 808 < 1/100 * 66583 = 665 considered unsuccessful
c [bca-2] limit of 10000000 steps and 4254888 added (scaled 2)
c [bca-2] 562781 out of 601676 literals actually usable 94%
c [bca-2] added 1887 blocked clauses in 1766346 steps
c [sweep-2] limit 4250918 based on 2125459 irredundant clauses
c [sweep-2-1] 116567 pos 38.8% + 183926 neg 61.2% = 300493 sched 99.9% ret 344
c [sweep-2-1] 4294236 steps 101 queries 95126.50 avg class size
c [sweep-2-1] 1566 decisions 95 SAT calls 35.63 avg env size
c [sweep-2-1] 299925 variables remain 100% (911 retained 0%)
c [decomp-15] removed 716 variables
c [sweep-2-1] removed 716 vars (0 failed, 13 eqs, 15 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 716 vars in TOTAL (1 rounds, 100 queries)
c [phase-count-6] 2029312 negative 95.6% of 2123755 except 94443 4.4%
c [phase-count-6] 2003335 positive 94.3% of 2123755 except 120420 5.7%
c [phase-6] phase bias: 115 positive 47%, 129 negative 53%
c [sort-queue-6] sorted 269280 enqueued variables after 7043 conflicts
c [score-dist-6] active 30841 (10%), one 0 (0%), zero 269280 (90%)
c [score-dist-6] max exp 523, different 22 (4%)
c [score-dist-6] median active exp 516, avg 516.1
c [simplification-6] removed 2567 variables 0.8% (300121 remain 24%)
c [simplification-6] removed 67071 irredundant clauses 3.1% (2123755 remain 42%)
c [simplification-6] maximum reduction of 3% = max (1%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 5000
c [simplification-6] penalized conflict interval 5000 = 1 * 5000
c [simplification-6] hard conflict limit 22043 (soft 12043 + delta 10000)
c [simplification-6] new conflict limit 12043 (hard 22043)
c 
c [simplification-7] limit 12043 conflicts (hard 22043) hit after 12043 conflicts
c [quatres-3] found 287188 quaternary clauses 41% in total
c [quatres-3-1] removed 4 duplicate quaternary clauses
c [quatres-3-1] added 24 double-self-subsuming ternary resolvents
c [quatres-3-2] added 939 single-self-subsuming ternary resolvents
c [quatres-3-2] added 4428 quaternary resolvents
c [ternres-3] limit 8494828 based on 2123707 irredundant clauses
c [ternres-3] 130086 schedulable variables 43%
c [ternres-3] 38081 ternary resolvents (1215 bin, 36866 trn)
c [ternres-3] 82980 variables remain 28% (217141 retained 72%)
c [decomp-16] removed 363 variables
c [basicprobe-3] limit 28464016 penalty 1 = 0 + 1
c [basicprobe-3-0] 183737 probes remain 62% after last round
c [basicprobe-3-0] 2337 units = 2168 failed (93%) + 169 lifted (7%)
c [basicprobe-3-0] removed 3321 variables, found 131864 hbrs
c [bate-1] eliminated 4507 asymmetric tautologies during probing
c [unhide-7] limit 284640 with penalty 3 = 0 + 3
c [unhide-7-7] 189 units, 276 failed, 43369 tauts, 0 hbrs, 37285 literals
c [transred-3] limit 2047130 based on 2047130 irredundant clauses
c [transred-3] removed 1287 transitive binary clauses
c [transred-3] found 12 units
c [cce-2] limit of 14232008 steps penalty 2 = 1 + 1
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 25
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 23
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 21
c [cce-2-1] eliminated 5 clauses out of 8 (62%) of length 20
c [cce-2-1] eliminated 9 clauses out of 16 (56%) of length 19
c [cce-2-1] eliminated 4 clauses out of 769 (1%) of length 18
c [cce-2-1] eliminated 31 clauses out of 1071 (3%) of length 17
c [cce-2-1] eliminated 21 clauses out of 763 (3%) of length 16
c [cce-2-1] eliminated 192 clauses out of 1610 (12%) of length 15
c [cce-2-1] eliminated 10 clauses out of 2359 (0%) of length 14
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 277 large clauses in 14232284 steps
c [cce-2-1] allowing another 7116142 steps for small clauses
c [cce-2-1] scheduling 1153312 clauses = 888102 binary + 265210 ternary
c [cce-2-1] tried to eliminate 3361 small clauses 0%
c [cce-2-1] eliminated 522 binary clauses 0%
c [cce-2-1] eliminated 154 ternary clauses 0%
c [cce-2-1] eliminated 676 small clauses 0%
c [cce-2-1] eliminated 5275 small clauses in 14232009 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 5552 covered clauses in round 1
c [cce-2] eliminated 5552 covered clauses in TOTAL during 1 rounds
c [cce-2] 5552 < 1/100 * 2046545 = 20465 considered unsuccessful
c [bca-3] limit of 10000000 steps and 4086900 added (scaled 2)
c [bca-3] 545488 out of 591884 literals actually usable 92%
c [bca-3] added 391 blocked clauses in 1668241 steps
c [sweep-3] limit 4081986 based on 2040993 irredundant clauses
c [sweep-3-1] 114747 pos 38.9% + 180301 neg 61.1% = 295048 sched 99.7% ret 893
c [sweep-3-1] 4093762 steps 92 queries 92142.03 avg class size
c [sweep-3-1] 951 decisions 87 SAT calls 33.45 avg env size
c [sweep-3-1] 294583 variables remain 100% (1358 retained 0%)
c [decomp-17] removed 3517 variables
c [sweep-3-1] removed 3517 vars (0 failed, 22 eqs, 27 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 3517 vars in TOTAL (1 rounds, 91 queries)
c [phase-count-7] 1940580 negative 95.3% of 2035385 except 94805 4.7%
c [phase-count-7] 1919076 positive 94.3% of 2035385 except 116309 5.7%
c [phase-7] phase bias: 145 positive 54%, 123 negative 46%
c [sort-queue-7] sorted 253983 enqueued variables after 12043 conflicts
c [score-dist-7] active 38441 (13%), one 0 (0%), zero 253983 (87%)
c [score-dist-7] max exp 526, different 24 (5%)
c [score-dist-7] median active exp 517, avg 517.6
c [simplification-7] removed 7697 variables 2.6% (292424 remain 23%)
c [simplification-7] removed 88368 irredundant clauses 4.2% (2035385 remain 40%)
c [simplification-7] maximum reduction of 4% = max (3%, 4%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 9000
c [simplification-7] penalized conflict interval 9000 = 1 * 9000
c [simplification-7] hard conflict limit 31043 (soft 21043 + delta 10000)
c [simplification-7] new conflict limit 21043 (hard 31043)
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  191.3  292423  2035385     12607   24866  87248 160596   47   140  200  33%     99  124   58    6 1050%
c 
c [simplification-8] limit 21043 conflicts (hard 31043) hit after 21044 conflicts
c [quatres-4] found 284104 quaternary clauses 42% in total
c [quatres-4-1] removed 23 duplicate quaternary clauses
c [quatres-4-1] added 33 double-self-subsuming ternary resolvents
c [quatres-4-2] added 800 single-self-subsuming ternary resolvents
c [quatres-4-2] added 3083 quaternary resolvents
c [ternres-4] limit 12763017 with penalty 1 = 0 + 1
c [ternres-4] 80658 schedulable variables 28%
c [ternres-4] 56739 ternary resolvents (2507 bin, 54232 trn)
c [ternres-4] 6471 variables remain 2% (285952 retained 98%)
c [gauss-3] limit 1276301 penalty 2 = 1 + 1
c [gauss-3] extracted 4662 xors of average arity 3.0
c [gauss-3] connected 13874 occurrences of 5508 variables (average 2.5)
c [gauss-3] limit 1276301 penalty 2 = 1 + 1
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 787 variables
c [simpleprobe-4] 250472 schedulable variables 86%
c [simpleprobe-4] limit 51052070 penalty 1 = 0 + 1
c [decomp-19] removed 3362 variables
c [simpleprobe-4] 183375 variables remain 64% (104899 retained 36%)
c [simpleprobe-4] removed 3362 variables, found 115161 hbrs, 713 units
c [unhide-8] limit 638150 with penalty 3 = 0 + 3
c [unhide-8-8] 235 units, 468 failed, 27653 tauts, 0 hbrs, 54248 literals
c [transred-4] limit 2008240 based on 2008240 irredundant clauses
c [transred-4] removed 1057 transitive binary clauses
c [transred-4] found 14 units
c [block-3] 1405 variables 0% will be scheduled this time
c [block-3] scheduled 1405 variables 0%
c [block-3] limit of 63815088 steps penalty 2 = 1 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 8 blocked clauses
c [block-3] 8 < 1/100 * 2007826 = 20078 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 287640 variables 100%
c [elim-7] limit of 127630177 steps penalty 2 = 1 + 1
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 16464 not tried 6% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 15533 = 5% variables out of 287640 scheduled
c [bca-4] limit of 10000000 steps and 3877075 added (scaled 2)
c [bca-4] 496855 out of 544216 literals actually usable 91%
c [bca-4] added 1086 blocked clauses in 1546124 steps
c [sweep-4] limit 7657810 penalty 0 = 0 + 0
c [sweep-4-1] 104209 pos 38.5% + 166668 neg 61.5% = 270877 sched 99.5% ret 1230
c [sweep-4-1] 7676905 steps 197 queries 70019.43 avg class size
c [sweep-4-1] 2183 decisions 177 SAT calls 32.80 avg env size
c [sweep-4-1] 269464 variables remain 99% (2639 retained 1%)
c [decomp-20] removed 681 variables
c [sweep-4-1] removed 681 vars (0 failed, 30 eqs, 47 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 681 vars in TOTAL (1 rounds, 196 queries)
c [phase-count-8] 1841781 negative 95.2% of 1933948 except 92167 4.8%
c [phase-count-8] 1822265 positive 94.2% of 1933948 except 111683 5.8%
c [phase-8] phase bias: 169 positive 46%, 202 negative 54%
c [sort-queue-8] sorted 228203 enqueued variables after 21044 conflicts
c [score-dist-8] active 43223 (16%), one 0 (0%), zero 228203 (84%)
c [score-dist-8] max exp 528, different 25 (5%)
c [score-dist-8] median active exp 518, avg 518.7
c [simplification-8] removed 20997 variables 7.2% (271426 remain 22%)
c [simplification-8] removed 101437 irredundant clauses 5.0% (1933948 remain 38%)
c [simplification-8] maximum reduction of 7% = max (7%, 5%)
c [simplification-8] large reduction 7% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 33044 (soft 23044 + delta 10000)
c [simplification-8] new conflict limit 23044 (hard 33044)
c 
c [simplification-9] limit 23044 conflicts (hard 33044) hit after 23044 conflicts
c [quatres-5] found 284883 quaternary clauses 43% in total
c [quatres-5-1] removed 214 duplicate quaternary clauses
c [quatres-5-1] added 19 double-self-subsuming ternary resolvents
c [quatres-5-2] added 1569 single-self-subsuming ternary resolvents
c [quatres-5-2] added 4331 quaternary resolvents
c [ternres-5] limit 29203465 with penalty 0 = 0 + 0
c [ternres-5] 5838 schedulable variables 2%
c [ternres-5] 76881 ternary resolvents (2854 bin, 74027 trn)
c [ternres-5] 321 variables remain 0% (271105 retained 100%)
c [decomp-21] removed 603 variables
c [treelook-4] limit 2920346 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 173665 literals 32%
c [treelook-4] scheduling used 2920350 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 2920346 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 2936564 steps
c [treelook-4] 173454 literals remain 32%
c [treelook-4] 33605 variables remain to probed next time 12%
c [decomp-22] removed 14 variables
c [treelook-4] removed 46 variables, found 3396 hbrs
c [unhide-9] limit 730086 with penalty 3 = 0 + 3
c [unhide-9-9] 83 units, 200 failed, 20727 tauts, 0 hbrs, 23412 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1181 transitive binary clauses
c [transred-5] found 8 units
c [elim-8] 15292 variables 6% will be scheduled this time
c [elim-8] scheduled 15292 variables 6%
c [elim-8] boosting limit by 20
c [elim-8] limit of 11681386040 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 13 variables 0% in round 1 in 568918180 steps
c [elim-8-1] backward subsumption/strengthening limit 568918100
c [elim-8-1-1] backward checking 55527 touched variables 21%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1341 and strengthened 1891 clauses in 96378873 steps
c [elim-8-1] rescheduled 7766 variables 3% by backward subsumption
c [elim-8-2] eliminated 427 variables 0% in round 2 in 114343407 steps
c [elim-8-2] backward subsumption/strengthening limit 114343400
c [elim-8-2-1] backward checking 4526 touched variables 2%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 282 and strengthened 435 clauses in 19037165 steps
c [elim-8-2] rescheduled 1973 variables 1% by backward subsumption
c [elim-8-3] eliminated 78 variables 0% in round 3 in 36034937 steps
c [elim-8-3] backward subsumption/strengthening limit 36034900
c [elim-8-3-1] backward checking 866 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 19 and strengthened 31 clauses in 4312717 steps
c [elim-8] incomplete 128 not tried 0% in round 3
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 664 = 4% variables out of 15292 scheduled
c [elim-8] 664 < 1/100 * 15292 = 152 considered unsuccessful
c [bca-5] limit of 10000000 steps and 3775242 added (scaled 2)
c [bca-5] 487097 out of 539682 literals actually usable 90%
c [bca-5] added 592 blocked clauses in 1517278 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 87610390 penalty 0 = 0 + 0
c [sweep-5-1] 102637 pos 38.4% + 164601 neg 61.6% = 267238 sched 99.0% ret 2602
c [sweep-5-1] 87618923 steps 1892 queries 26032.65 avg class size
c [sweep-5-1] 25178 decisions 1764 SAT calls 36.92 avg env size
c [sweep-5-1] 244531 variables remain 91% (24966 retained 9%)
c [decomp-23] removed 1700 variables
c [sweep-5-1] removed 1700 vars (0 failed, 352 eqs, 504 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1700 vars in TOTAL (1 rounds, 1891 queries)
c [phase-count-9] 1784431 negative 95.0% of 1877964 except 93533 5.0%
c [phase-count-9] 1767049 positive 94.1% of 1877964 except 110915 5.9%
c [phase-9] phase bias: 72 positive 57%, 55 negative 43%
c [sort-queue-9] sorted 219952 enqueued variables after 23044 conflicts
c [score-dist-9] active 48188 (18%), one 0 (0%), zero 219952 (82%)
c [score-dist-9] max exp 529, different 26 (5%)
c [score-dist-9] median active exp 518, avg 518.7
c [simplification-9] removed 3286 variables 1.2% (268140 remain 21%)
c [simplification-9] removed 55983 irredundant clauses 2.9% (1877964 remain 37%)
c [simplification-9] maximum reduction of 3% = max (1%, 3%)
c [simplification-9] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-9] new conflict interval 14000
c [simplification-9] penalized conflict interval 14000 = 1 * 14000
c [simplification-9] hard conflict limit 47044 (soft 37044 + delta 10000)
c [simplification-9] new conflict limit 37044 (hard 47044)
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  394.7  268139  1877964     30042   34241 150642 218591  156   219  207  71%    221  161  111   36  307%
c i  397.5  268104  1877964     30505   34512 150645 218599  152   218  207  70%    128  159  132   37  359%
c i  399.7  267898  1877964     31196   34639 150653 218600  155   215  207  72%     49  155  146   38  384%
c i  402.7  267897  1877964     31795   35078 150658 218605  146   213  207  68%     13  151  101   39  261%
c i  404.1  267896  1877964     32329   35283 150676 218612  143   211  207  68%     -6  148  116   39  295%
c i  404.3  267895  1877964     32383   35332 150679 218612  141   211  207  67%     -7  148   97   39  247%
c 
c [simplification-10] limit 37044 conflicts (hard 47044) hit after 37044 conflicts
c [quatres-6] found 280184 quaternary clauses 45% in total
c [quatres-6-1] removed 130 duplicate quaternary clauses
c [quatres-6-1] added 22 double-self-subsuming ternary resolvents
c [quatres-6-2] added 730 single-self-subsuming ternary resolvents
c [quatres-6-2] added 2669 quaternary resolvents
c [ternres-6] limit 46824136 with penalty 0 = 0 + 0
c [ternres-6] 304 schedulable variables 0%
c [ternres-6] 116077 ternary resolvents (2319 bin, 113758 trn)
c [ternres-6] 25 variables remain 0% (267870 retained 100%)
c [card-4] limit 2926508 penalty 3 = 3 + 0
c [card-4] found 1667 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2926508 for elimination
c [card-4] 1667 out of 1667 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-24] removed 874 variables
c [basicprobe-4] limit 234120684 penalty 0 = 0 + 0
c [basicprobe-4-0] 155278 sched 62%, 9353 failed, 745 lifted, 331121 hbrs
c [decomp-25] removed 23833 variables
c [basicprobe-4-1] 110499 probes remain 47% after last round
c [basicprobe-4-1] 11172 units = 10324 failed (92%) + 848 lifted (8%)
c [basicprobe-4-1] removed 29966 variables, found 369097 hbrs
c [bate-2] eliminated 7945 asymmetric tautologies during probing
c [unhide-10] limit 1170603 with penalty 3 = 0 + 3
c [unhide-10-10] 95 units, 132 failed, 48211 tauts, 0 hbrs, 47856 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 2528 transitive binary clauses
c [transred-6] found 4 units
c [cce-3] limit of 58530171 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 30
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 24
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 23
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 22
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 21
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 20
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 19
c [cce-3-1] eliminated 9 clauses out of 648 (1%) of length 18
c [cce-3-1] eliminated 26 clauses out of 525 (5%) of length 17
c [cce-3-1] eliminated 19 clauses out of 401 (5%) of length 16
c [cce-3-1] eliminated 17 clauses out of 986 (2%) of length 15
c [cce-3-1] eliminated 216 clauses out of 1259 (17%) of length 14
c [cce-3-1] eliminated 1166 clauses out of 3090 (38%) of length 13
c [cce-3-1] eliminated 2572 clauses out of 5877 (44%) of length 12
c [cce-3-1] eliminated 673 clauses out of 6684 (10%) of length 11
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 4714 large clauses in 58530237 steps
c [cce-3-1] allowing another 29265118 steps for small clauses
c [cce-3-1] scheduling 875447 clauses = 688943 binary + 186504 ternary
c [cce-3-1] tried to eliminate 11579 small clauses 1%
c [cce-3-1] eliminated 2903 binary clauses 0%
c [cce-3-1] eliminated 608 ternary clauses 0%
c [cce-3-1] eliminated 3511 small clauses 0%
c [cce-3-1] eliminated 4715 small clauses in 58530176 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 9429 covered clauses in round 1
c [cce-3] eliminated 9429 covered clauses in TOTAL during 1 rounds
c [cce-3] 9429 < 1/100 * 1628919 = 16289 considered unsuccessful
c [bca-6] limit of 10000000 steps and 3244928 added (scaled 2)
c [bca-6] 425166 out of 474256 literals actually usable 90%
c [bca-6] added 1156 blocked clauses in 1280702 steps
c [sweep-6] limit 14047241 penalty 0 = 0 + 0
c [sweep-6-1] 80755 pos 37.5% + 134735 neg 62.5% = 215490 sched 90.9% ret 21637
c [sweep-6-1] 14073531 steps 413 queries 45189.54 avg class size
c [sweep-6-1] 5010 decisions 393 SAT calls 33.97 avg env size
c [sweep-6-1] 212877 variables remain 90% (24223 retained 10%)
c [decomp-26] removed 3487 variables
c [sweep-6-1] removed 3487 vars (0 failed, 62 eqs, 68 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 3487 vars in TOTAL (1 rounds, 412 queries)
c [phase-count-10] 1524529 negative 94.6% of 1611111 except 86582 5.4%
c [phase-count-10] 1504997 positive 93.4% of 1611111 except 106114 6.6%
c [phase-10] phase bias: 192 positive 56%, 152 negative 44%
c [sort-queue-10] sorted 188401 enqueued variables after 37044 conflicts
c [score-dist-10] active 45239 (19%), one 0 (0%), zero 188401 (81%)
c [score-dist-10] max exp 530, different 27 (5%)
c [score-dist-10] median active exp 518, avg 519.3
c [simplification-10] removed 34255 variables 12.8% (233640 remain 19%)
c [simplification-10] removed 266853 irredundant clauses 14.2% (1611111 remain 32%)
c [simplification-10] maximum reduction of 14% = max (13%, 14%)
c [simplification-10] large reduction 14% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 49044 (soft 39044 + delta 10000)
c [simplification-10] new conflict limit 39044 (hard 49044)
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  449.5  233639  1611111     37812   35917 125477 323327  121   190  189  63%     32  116   31   45   69%
c i  449.8  233638  1611111     38092   36163 125479 323332  114   189  189  60%     15  114   28   45   61%
c i  451.1  233637  1611111     39100   37044 125500 323343   95   187  189  51%    -12  110   19   45   43%
c i  452.6  233593  1611111     39830   37692 125506 323343   84   184  190  45%    -22  107   29   45   66%
c i  453.0  233582  1611111     39979   37827 125509 323344   82   184  190  45%    -24  106   29   45   65%
c 
c [simplification-11] limit 39044 conflicts (hard 49044) hit after 43259 conflicts
c [quatres-7] found 250410 quaternary clauses 46% in total
c [quatres-7-1] removed 388 duplicate quaternary clauses
c [quatres-7-1] added 118 double-self-subsuming ternary resolvents
c [quatres-7-2] added 1419 single-self-subsuming ternary resolvents
c [quatres-7-2] added 2970 quaternary resolvents
c [ternres-7] limit 49650380 with penalty 0 = 0 + 0
c [ternres-7] 22 schedulable variables 0%
c [ternres-7] 42732 ternary resolvents (941 bin, 41791 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 2482519 penalty 2 = 2 + 0
c [gauss-4] extracted 6670 xors of average arity 3.0
c [gauss-4] connected 19906 occurrences of 6761 variables (average 2.9)
c [gauss-4] limit 2482519 penalty 2 = 2 + 0
c [decomp-27] removed 285 variables
c [gauss-4] exported 0 unary, 1 binary and 0 ternary equations
c [simpleprobe-5] 146183 schedulable variables 63%
c [simpleprobe-5] limit 198601522 penalty 0 = 0 + 0
c [decomp-29] removed 7654 variables
c [simpleprobe-5] 53670 variables remain 24% (171959 retained 76%)
c [simpleprobe-5] removed 7654 variables, found 268536 hbrs, 536 units
c [unhide-11] limit 1241259 with penalty 3 = 0 + 3
c [unhide-11-11] 28 units, 19 failed, 24582 tauts, 0 hbrs, 23355 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 3041 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 225589 variables 100%
c [block-4] limit of 124125951 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 23516 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 224727 variables 100%
c [elim-9] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 515 not tried 0% in round 1
c [gc-82] reconnected 527410 binary clauses (produced 0 empty 3 units)
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 20029 = 9% variables out of 224727 scheduled
c [bca-7] limit of 10000000 steps and 2902542 added (scaled 2)
c [bca-7] 363649 out of 409398 literals actually usable 89%
c [bca-7] added 1940 blocked clauses in 1143474 steps
c [sweep-7] limit 14895114 penalty 0 = 0 + 0
c [sweep-7-1] 67938 pos 37.1% + 115327 neg 62.9% = 183265 sched 89.5% ret 21433
c [sweep-7-1] 14922401 steps 386 queries 39365.01 avg class size
c [sweep-7-1] 5734 decisions 379 SAT calls 36.23 avg env size
c [sweep-7-1] 179829 variables remain 88% (24744 retained 12%)
c [decomp-30] removed 709 variables
c [sweep-7-1] removed 709 vars (0 failed, 69 eqs, 62 impls)
c [sweep-7] removed 709 vars in TOTAL (1 rounds, 385 queries)
c [phase-count-11] 1367980 negative 94.7% of 1445135 except 77155 5.3%
c [phase-count-11] 1349342 positive 93.4% of 1445135 except 95793 6.6%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 145 positive 42%, 197 negative 58%
c [sort-queue-11] sorted 162755 enqueued variables after 43259 conflicts
c [score-dist-11] active 41234 (20%), one 0 (0%), zero 162755 (80%)
c [score-dist-11] max exp 531, different 28 (5%)
c [score-dist-11] median active exp 518, avg 519.5
c [simplification-11] removed 29579 variables 12.7% (203989 remain 16%)
c [simplification-11] removed 165976 irredundant clauses 10.3% (1445135 remain 29%)
c [simplification-11] maximum reduction of 13% = max (13%, 10%)
c [simplification-11] large reduction 13% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 55259 (soft 45259 + delta 10000)
c [simplification-11] new conflict limit 45259 (hard 55259)
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  488.5  203988  1445135     43940   33102 114606 449714   46   151  179  30%     10   67   20   43   45%
c i  489.3  203987  1445135     44504   33618 114613 449715   43   142  179  30%     -8   58   23   43   54%
c i  490.6  203986  1445135     45345   34366 114633 449721   38   136  179  28%    -19   51   15   43   35%
c i  490.7  203985  1445135     45397   34415 114634 449722   38   136  179  28%    -20   52   15   43   36%
c i  490.8  203984  1445135     45398   34415 114634 449722   38   136  179  28%    -20   52   15   43   36%
c 
c [simplification-12] limit 45269 conflicts (hard 55259) hit after 48601 conflicts
c [quatres-8] found 236222 quaternary clauses 46% in total
c [quatres-8-1] removed 1684 duplicate quaternary clauses
c [quatres-8-1] added 16 double-self-subsuming ternary resolvents
c [quatres-8-2] added 359 single-self-subsuming ternary resolvents
c [quatres-8-2] added 4558 quaternary resolvents
c [ternres-8] limit 52439024 with penalty 0 = 0 + 0
c [ternres-8] all 203984 free variables schedulable
c [ternres-8] 42100 ternary resolvents (1359 bin, 40741 trn)
c [ternres-8] 895 variables remain 0% (203089 retained 100%)
c [decomp-31] removed 287 variables
c [treelook-5] limit 5243902 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 165566 literals 41%
c [treelook-5] scheduling used 3699230 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 5243902 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 5264529 steps
c [treelook-5] 164843 literals remain 40%
c [treelook-5] 23955 variables remain to probed next time 12%
c [decomp-32] removed 45 variables
c [treelook-5] removed 67 variables, found 4670 hbrs
c [unhide-12] limit 2621951 with penalty 2 = 0 + 2
c [unhide-12-12] 46 units, 220 failed, 70119 tauts, 0 hbrs, 37982 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2422 transitive binary clauses
c [transred-8] found 1 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 203340 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 5209 variables 3% in round 1 in 479063139 steps
c [elim-10-1] backward subsumption/strengthening limit 320936861
c [elim-10-1-1] backward checking 36560 touched variables 18%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 416 and strengthened 321 clauses in 51933191 steps
c [elim-10-1] rescheduled 2032 variables 1% by backward subsumption
c [elim-10-2] eliminated 107 variables 0% in round 2 in 40867362 steps
c [elim-10-2] backward subsumption/strengthening limit 40867300
c [elim-10-2-1] backward checking 823 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 69 and strengthened 58 clauses in 3436742 steps
c [elim-10-2] rescheduled 333 variables 0% by backward subsumption
c [elim-10-3] eliminated 14 variables 0% in round 3 in 10967422 steps
c [elim-10-3] backward subsumption/strengthening limit 10967400
c [elim-10-3-1] backward checking 129 touched variables 0%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 0 and strengthened 5 clauses in 1060074 steps
c [elim-10] incomplete 15 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 5385 = 3% variables out of 203340 scheduled
c [bca-8] limit of 10000000 steps and 2840586 added (scaled 2)
c [bca-8] 346668 out of 395912 literals actually usable 88%
c [bca-8] added 773 blocked clauses in 1093449 steps
c [sweep-8] limit 15731707 penalty 0 = 0 + 0
c [sweep-8-1] 64528 pos 37.1% + 109554 neg 62.9% = 174082 sched 87.9% ret 23873
c [sweep-8-1] 15748929 steps 530 queries 30942.98 avg class size
c [sweep-8-1] 6644 decisions 499 SAT calls 38.21 avg env size
c [sweep-8-1] 169386 variables remain 86% (27870 retained 14%)
c [decomp-33] removed 1239 variables
c [sweep-8-1] removed 1239 vars (0 failed, 74 eqs, 98 impls)
c [sweep-8] removed 1239 vars in TOTAL (1 rounds, 529 queries)
c [phase-count-12] 1332753 negative 94.5% of 1409671 except 76918 5.5%
c [phase-count-12] 1316307 positive 93.4% of 1409671 except 93364 6.6%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 92 positive 37%, 155 negative 63%
c [sort-queue-12] sorted 153977 enqueued variables after 48601 conflicts
c [score-dist-12] active 42739 (22%), one 0 (0%), zero 153977 (78%)
c [score-dist-12] max exp 531, different 28 (5%)
c [score-dist-12] median active exp 519, avg 519.7
c [simplification-12] removed 7268 variables 3.6% (196716 remain 16%)
c [simplification-12] removed 35464 irredundant clauses 2.5% (1409671 remain 28%)
c [simplification-12] maximum reduction of 4% = max (4%, 2%)
c [simplification-12] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-12] new conflict interval 18000
c [simplification-12] penalized conflict interval 18000 = 1 * 18000
c [simplification-12] hard conflict limit 76601 (soft 66601 + delta 10000)
c [simplification-12] new conflict limit 66601 (hard 76601)
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  521.8  196715  1409671     48854   37877 137068 367438   28   106  179  26%      4   19   22   42   52%
c i  521.8  196695  1409671     48857   37879 137068 367438   28   105  179  26%      4   19   21   42   51%
c i  523.2  196694  1409671     49489   38374 137074 367441   27    98  179  28%    -12   11   22   42   54%
c i  525.7  196693  1409671     50703   39375 137078 367447   25    89  179  28%    -20    1   17   41   42%
c i  526.8  196629  1409671     51115   39754 137088 367448   24    88  179  27%    -24    1   16   41   39%
c i  548.0  196628  1409671     58394   45739 137187 367490   54   134  185  40%     62   45   29   42   68%
c i  548.0  196627  1409671     58401   45744 137187 367491   54   135  185  40%     61   45   28   42   66%
c 
c [simplification-13] limit 66605 conflicts (hard 76601) hit after 66606 conflicts
c [quatres-9] found 233327 quaternary clauses 46% in total
c [quatres-9-1] removed 54 duplicate quaternary clauses
c [quatres-9-1] added 49 double-self-subsuming ternary resolvents
c [quatres-9-2] added 564 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1986 quaternary resolvents
c [ternres-9] limit 64338390 with penalty 0 = 0 + 0
c [ternres-9] 873 schedulable variables 0%
c [ternres-9] 31273 ternary resolvents (1577 bin, 29696 trn)
c [ternres-9] 5 variables remain 0% (196622 retained 100%)
c [gauss-5] limit 6433839 penalty 1 = 1 + 0
c [gauss-5] extracted 14445 xors of average arity 3.0
c [gauss-5] connected 43157 occurrences of 10658 variables (average 4.0)
c [gauss-5] limit 6433839 penalty 1 = 1 + 0
c [decomp-34] removed 281 variables
c [gauss-5] exported 0 unary, 1 binary and 0 ternary equations
c [decomp-35] removed 1 variables
c [basicprobe-5] limit 321691952 penalty 0 = 0 + 0
c [basicprobe-5-0] 87361 sched 46%, 2265 failed, 173 lifted, 61922 hbrs
c [decomp-36] removed 7039 variables
c [basicprobe-5-1] 122930 sched 66%, 1397 failed, 146 lifted, 28821 hbrs
c [decomp-37] removed 4026 variables
c [basicprobe-5-2] 88261 probes remain 48% after last round
c [basicprobe-5-2] 4069 units = 3750 failed (92%) + 319 lifted (8%)
c [basicprobe-5-2] removed 11265 variables, found 93247 hbrs
c [bate-3] eliminated 6178 asymmetric tautologies during probing
c [unhide-13] limit 3216919 with penalty 2 = 0 + 2
c [unhide-13-13] 14 units, 59 failed, 14876 tauts, 0 hbrs, 47049 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 2449 transitive binary clauses
c [transred-9] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 185042 variables 100%
c [block-5] limit of 321691952 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 11566 blocked clauses
c [block-5] 11566 < 1/100 * 1299325 = 12993 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 184444 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 8116 variables 4% in round 1 in 413732279 steps
c [elim-11-1] backward subsumption/strengthening limit 386267721
c [elim-11-1-1] backward checking 47565 touched variables 26%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 365 and strengthened 606 clauses in 50208160 steps
c [elim-11-1] rescheduled 2873 variables 2% by backward subsumption
c [elim-11-2] eliminated 92 variables 0% in round 2 in 31058884 steps
c [elim-11-2] backward subsumption/strengthening limit 31058800
c [elim-11-2-1] backward checking 903 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 36 and strengthened 81 clauses in 2275608 steps
c [elim-11-2] rescheduled 331 variables 0% by backward subsumption
c [elim-11-3] eliminated 21 variables 0% in round 3 in 6983035 steps
c [elim-11-3] backward subsumption/strengthening limit 6983000
c [elim-11-3-1] backward checking 173 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 4 and strengthened 16 clauses in 1090032 steps
c [elim-11] incomplete 60 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 8255 = 4% variables out of 184444 scheduled
c [bca-9] limit of 10000000 steps and 2519121 added (scaled 2)
c [bca-9] 302103 out of 352380 literals actually usable 86%
c [bca-9] added 717 blocked clauses in 963138 steps
c [sweep-9] limit 19301517 penalty 0 = 0 + 0
c [sweep-9-1] 56318 pos 37.2% + 95277 neg 62.8% = 151595 sched 86.0% ret 24594
c [sweep-9-1] 19329440 steps 667 queries 23501.86 avg class size
c [sweep-9-1] 8683 decisions 638 SAT calls 34.75 avg env size
c [sweep-9-1] 145950 variables remain 83% (30234 retained 17%)
c [decomp-38] removed 515 variables
c [sweep-9-1] removed 515 vars (0 failed, 85 eqs, 99 impls)
c [sweep-9] removed 515 vars in TOTAL (1 rounds, 666 queries)
c [phase-count-13] 1184768 negative 94.5% of 1254326 except 69558 5.5%
c [phase-count-13] 1167191 positive 93.1% of 1254326 except 87135 6.9%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 34 positive 49%, 35 negative 51%
c [sort-queue-13] sorted 127153 enqueued variables after 66606 conflicts
c [score-dist-13] active 48521 (28%), one 0 (0%), zero 127153 (72%)
c [score-dist-13] max exp 531, different 28 (5%)
c [score-dist-13] median active exp 520, avg 520.8
c [simplification-13] removed 20953 variables 10.7% (175674 remain 14%)
c [simplification-13] removed 155345 irredundant clauses 11.0% (1254326 remain 25%)
c [simplification-13] maximum reduction of 11% = max (11%, 11%)
c [simplification-13] large reduction 11% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 78606 (soft 68606 + delta 10000)
c [simplification-13] new conflict limit 68606 (hard 78606)
c 
c [simplification-14] limit 68606 conflicts (hard 78606) hit after 68607 conflicts
c [quatres-10] found 212873 quaternary clauses 46% in total
c [quatres-10-1] removed 199 duplicate quaternary clauses
c [quatres-10-1] added 18 double-self-subsuming ternary resolvents
c [quatres-10-2] added 317 single-self-subsuming ternary resolvents
c [quatres-10-2] added 2309 quaternary resolvents
c [ternres-10] limit 67430614 with penalty 0 = 0 + 0
c [ternres-10] 5 schedulable variables 0%
c [ternres-10] 10807 ternary resolvents (131 bin, 10676 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-6] limit 13486122 penalty 0 = 0 + 0
c [gauss-6] extracted 28003 xors of average arity 3.0
c [gauss-6] connected 83854 occurrences of 13244 variables (average 6.3)
c [gauss-6] limit 13486122 penalty 0 = 0 + 0
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-39] removed 20 variables
c [simpleprobe-6] 39623 schedulable variables 23%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-40] removed 3076 variables
c [simpleprobe-6] 19794 variables remain 11% (152784 retained 89%)
c [simpleprobe-6] removed 3076 variables, found 129212 hbrs, 129 units
c [unhide-14] limit 3371530 with penalty 2 = 0 + 2
c [unhide-14-14] 8 units, 62 failed, 77163 tauts, 0 hbrs, 75767 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2643 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 421441342 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 6 (17%) of length 21
c [cce-4-1] eliminated 3 clauses out of 7 (43%) of length 20
c [cce-4-1] eliminated 1 clauses out of 7 (14%) of length 19
c [cce-4-1] eliminated 1 clauses out of 597 (0%) of length 18
c [cce-4-1] eliminated 11 clauses out of 378 (3%) of length 17
c [cce-4-1] eliminated 15 clauses out of 331 (5%) of length 16
c [cce-4-1] eliminated 41 clauses out of 1104 (4%) of length 15
c [cce-4-1] eliminated 113 clauses out of 1084 (10%) of length 14
c [cce-4-1] eliminated 74 clauses out of 1673 (4%) of length 13
c [cce-4-1] eliminated 124 clauses out of 3661 (3%) of length 12
c [cce-4-1] eliminated 440 clauses out of 4131 (11%) of length 11
c [cce-4-1] eliminated 1243 clauses out of 6956 (18%) of length 10
c [cce-4-1] eliminated 2357 clauses out of 12153 (19%) of length 9
c [cce-4-1] eliminated 3807 clauses out of 21630 (18%) of length 8
c [cce-4-1] eliminated 4714 clauses out of 26989 (17%) of length 7
c [cce-4-1] eliminated 7712 clauses out of 50932 (15%) of length 6
c [cce-4-1] eliminated 19665 clauses out of 102995 (19%) of length 5
c [cce-4-1] eliminated 1425 clauses out of 189067 (1%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 41747 large clauses in 421441353 steps
c [cce-4-1] allowing another 210720676 steps for small clauses
c [cce-4-1] scheduling 658917 clauses = 485253 binary + 173664 ternary
c [cce-4-1] tried to eliminate 112259 small clauses 17%
c [cce-4-1] eliminated 12212 binary clauses 3%
c [cce-4-1] eliminated 5029 ternary clauses 3%
c [cce-4-1] eliminated 17241 small clauses 3%
c [cce-4-1] eliminated 17580 small clauses in 421441350 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 59327 covered clauses in round 1
c [cce-4] eliminated 59327 covered clauses in TOTAL during 1 rounds
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 172549 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 10926 variables 6% in round 1 in 341992501 steps
c [elim-12-1] backward subsumption/strengthening limit 341992500
c [elim-12-1-1] backward checking 58004 touched variables 34%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 722 and strengthened 1277 clauses in 51096315 steps
c [elim-12-1] rescheduled 5399 variables 3% by backward subsumption
c [elim-12-2] eliminated 241 variables 0% in round 2 in 48036214 steps
c [elim-12-2] backward subsumption/strengthening limit 48036200
c [elim-12-2-1] backward checking 2468 touched variables 1%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 148 and strengthened 175 clauses in 6320088 steps
c [elim-12-2] rescheduled 710 variables 0% by backward subsumption
c [elim-12-3] eliminated 35 variables 0% in round 3 in 11606452 steps
c [elim-12-3] backward subsumption/strengthening limit 11606400
c [elim-12-3-1] backward checking 298 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 28 and strengthened 21 clauses in 1205325 steps
c [elim-12] incomplete 77 not tried 0% in round 3
c [gc-108] reconnected 368679 binary clauses (produced 0 empty 1 units)
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 11247 = 7% variables out of 172549 scheduled
c [bca-10] limit of 10000000 steps and 2277477 added (scaled 2)
c [bca-10] 275933 out of 322606 literals actually usable 86%
c [bca-10] added 1645 blocked clauses in 862940 steps
c [sweep-10] limit 20229184 penalty 0 = 0 + 0
c [sweep-10-1] 49175 pos 36.8% + 84411 neg 63.2% = 133586 sched 82.8% ret 27716
c [sweep-10-1] 20251551 steps 752 queries 21814.82 avg class size
c [sweep-10-1] 10010 decisions 737 SAT calls 35.48 avg env size
c [sweep-10-1] 126912 variables remain 79% (34385 retained 21%)
c [decomp-41] removed 246 variables
c [sweep-10-1] removed 246 vars (0 failed, 76 eqs, 79 impls)
c [sweep-10] removed 246 vars in TOTAL (1 rounds, 751 queries)
c [phase-count-14] 1065866 negative 94.0% of 1133740 except 67874 6.0%
c [phase-count-14] 1054130 positive 93.0% of 1133740 except 79610 7.0%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 40 positive 52%, 37 negative 48%
c [sort-queue-14] sorted 114082 enqueued variables after 68607 conflicts
c [score-dist-14] active 46974 (29%), one 0 (0%), zero 114082 (71%)
c [score-dist-14] max exp 531, different 28 (5%)
c [score-dist-14] median active exp 520, avg 521.0
c [simplification-14] removed 14618 variables 8.3% (161056 remain 13%)
c [simplification-14] removed 120586 irredundant clauses 9.6% (1133740 remain 23%)
c [simplification-14] maximum reduction of 10% = max (8%, 10%)
c [simplification-14] large reduction 10% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 80607 (soft 70607 + delta 10000)
c [simplification-14] new conflict limit 70607 (hard 80607)
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  658.0  161055  1133740     68642   40745 122486 331684   34   164  166  21%    102   64   47   39  120%
c 
c [simplification-15] limit 70607 conflicts (hard 80607) hit after 72019 conflicts
c [quatres-11] found 204491 quaternary clauses 50% in total
c [quatres-11-1] removed 269 duplicate quaternary clauses
c [quatres-11-1] added 198 double-self-subsuming ternary resolvents
c [quatres-11-2] added 196 single-self-subsuming ternary resolvents
c [quatres-11-2] added 3789 quaternary resolvents
c [ternres-11] limit 71572114 with penalty 0 = 0 + 0
c [ternres-11] all 161052 free variables schedulable
c [ternres-11] 29126 ternary resolvents (1251 bin, 27875 trn)
c [ternres-11] 100 variables remain 0% (160952 retained 100%)
c [card-5] limit 2236628 penalty 4 = 4 + 0
c [card-5] found 1550 at-most-one constraints of average size 3.3
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2236628 for elimination
c [card-5] 1550 out of 1550 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-42] removed 75 variables
c [treelook-6] limit 7157211 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 135880 literals 42%
c [treelook-6] scheduling used 3004134 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 7157211 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 7247428 steps
c [treelook-6] 135520 literals remain 42%
c [treelook-6] 19275 variables remain to probed next time 12%
c [decomp-43] removed 28 variables
c [treelook-6] removed 36 variables, found 3023 hbrs
c [unhide-15] limit 3578605 with penalty 2 = 0 + 2
c [unhide-15-15] 6 units, 13 failed, 7065 tauts, 0 hbrs, 9260 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 2381 transitive binary clauses
c [transred-11] found 4 units
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 160864 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 1820 variables 1% in round 1 in 329289942 steps
c [elim-13-1] backward subsumption/strengthening limit 329289900
c [elim-13-1-1] backward checking 14168 touched variables 9%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 108 and strengthened 258 clauses in 21368564 steps
c [elim-13-1] rescheduled 813 variables 1% by backward subsumption
c [elim-13-2] eliminated 42 variables 0% in round 2 in 5379577 steps
c [elim-13-2] backward subsumption/strengthening limit 5379500
c [elim-13-2-1] backward checking 386 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 22 and strengthened 21 clauses in 1109286 steps
c [elim-13-2] rescheduled 102 variables 0% by backward subsumption
c [elim-13-3] eliminated 12 variables 0% in round 3 in 2059580 steps
c [elim-13-3] backward subsumption/strengthening limit 2059500
c [elim-13-3-1] backward checking 98 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 9 and strengthened 4 clauses in 579195 steps
c [elim-13] incomplete 32 not tried 0% in round 3
c [gc-115] reconnected 329399 binary clauses (produced 0 empty 8 units)
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 1886 = 1% variables out of 160864 scheduled
c [bca-11] limit of 10000000 steps and 2249436 added (scaled 2)
c [bca-11] 268508 out of 317958 literals actually usable 84%
c [bca-11] added 151 blocked clauses in 848850 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 214716340 penalty 0 = 0 + 0
c [sweep-11-1] 46029 pos 36.8% + 79140 neg 63.2% = 125169 sched 78.7% ret 33809
c [sweep-11-1] 214732054 steps 7199 queries 2750.80 avg class size
c [sweep-11-1] 81122 decisions 6828 SAT calls 30.17 avg env size
c [sweep-11-1] 54520 variables remain 34% (104331 retained 66%)
c [decomp-44] removed 1994 variables
c [sweep-11-1] removed 1994 vars (0 failed, 1470 eqs, 1329 impls)
c [sweep-11] removed 1994 vars in TOTAL (1 rounds, 7198 queries)
c [phase-count-15] 1043535 negative 93.7% of 1113732 except 70197 6.3%
c [phase-count-15] 1032976 positive 92.7% of 1113732 except 80756 7.3%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 4 positive 29%, 10 negative 71%
c [sort-queue-15] sorted 96414 enqueued variables after 72019 conflicts
c [score-dist-15] active 60570 (39%), one 0 (0%), zero 96414 (61%)
c [score-dist-15] max exp 531, different 28 (5%)
c [score-dist-15] median active exp 520, avg 520.8
c [simplification-15] removed 4068 variables 2.5% (156984 remain 13%)
c [simplification-15] removed 20008 irredundant clauses 1.8% (1113732 remain 22%)
c [simplification-15] maximum reduction of 3% = max (3%, 2%)
c [simplification-15] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-15] new conflict interval 23000
c [simplification-15] penalized conflict interval 23000 = 1 * 23000
c [simplification-15] hard conflict limit 106519 (soft 95019 + delta 11500)
c [simplification-15] new conflict limit 95019 (hard 106519)
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  820.6  156983  1113732     87143   58532 138377 324450   71    83  177  86%    206  -21   44   48   90%
c i  820.6  156978  1113732     87167   58555 138377 324450   71    83  177  86%    200  -21   42   48   87%
c i  828.5  156977  1113732     91133   62394 138403 324488   51    86  179  60%    -16  -16   31   48   65%
c i  829.8  156976  1113732     92210   63401 138419 324500   50    89  179  56%    -43  -12   54   48  113%
c i  830.3  156975  1113732     92658   63822 138420 324507   50    90  179  56%    -50  -12   51   48  108%
c i  830.4  156974  1113732     92785   63935 138422 324509   51    90  179  56%    -52  -12   56   48  117%
c i  831.1  156961  1113732     93363   64452 138427 324516   51    90  179  57%    -56  -12   55   48  116%
c i  834.6  156960  1113732     95379   66283 138457 324539   49    94  180  52%    -46   -8   49   48  102%
c i  835.4  156959  1113732     95871   66722 138458 324550   49    94  180  52%    -51   -8   49   48  103%
c i  836.1  156958  1113732     96383   67171 138465 324553   50    93  180  54%    -54   -8   61   48  127%
c i  836.3  156956  1113732     96546   67320 138466 324553   51    93  180  54%    -55   -8   63   48  131%
c i  836.6  156955  1113732     96778   67534 138469 324555   52    93  180  55%    -57   -8   64   48  134%
c i  838.0  156954  1113732     98121   68753 138479 324559   54    92  180  59%    -51  -10   57   48  117%
c i  845.2  156927  1113732    102374   72551 138509 324593   58    90  182  65%     -9  -11   58   49  118%
c i  846.8  156924  1113732    103942   73938 138520 324604   62    89  189  70%    -37  -11   71   49  143%
c i  847.5  156918  1113732    104280   74222 138524 324609   63    89  189  71%    -42  -11   71   50  144%
c 
c [simplification-16] limit 95019 conflicts (hard 106519) hit after 106519 conflicts
c [quatres-12] found 203826 quaternary clauses 50% in total
c [quatres-12-1] removed 104 duplicate quaternary clauses
c [quatres-12-1] added 43 double-self-subsuming ternary resolvents
c [quatres-12-2] added 779 single-self-subsuming ternary resolvents
c [quatres-12-2] added 1757 quaternary resolvents
c [ternres-12] limit 104879390 with penalty 0 = 0 + 0
c [ternres-12] 93 schedulable variables 0%
c [ternres-12] 10976 ternary resolvents (180 bin, 10796 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-7] limit 10487939 penalty 1 = 1 + 0
c [gauss-7] extracted 21105 xors of average arity 3.0
c [gauss-7] connected 63141 occurrences of 13352 variables (average 4.7)
c [gauss-7] limit 10487939 penalty 1 = 1 + 0
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-45] removed 90 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 75452 sched 49%, 734 failed, 61 lifted, 27881 hbrs
c [decomp-46] removed 2342 variables
c [basicprobe-6-1] 97611 sched 64%, 389 failed, 16 lifted, 13946 hbrs
c [decomp-47] removed 1294 variables
c [basicprobe-6-2] 86372 probes remain 56% after last round
c [basicprobe-6-2] 1206 units = 1129 failed (94%) + 77 lifted (6%)
c [basicprobe-6-2] removed 3644 variables, found 42348 hbrs
c [bate-4] eliminated 2329 asymmetric tautologies during probing
c [unhide-16] limit 5000000 with penalty 2 = 0 + 2
c [unhide-16-16] 1 units, 11 failed, 44639 tauts, 0 hbrs, 126585 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1965 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 153178 variables 100%
c [block-6] limit of 200000000 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 11719 blocked clauses
c [cce-5] limit of 131099238 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 20
c [cce-5-1] eliminated 6 clauses out of 539 (1%) of length 18
c [cce-5-1] eliminated 4 clauses out of 421 (1%) of length 17
c [cce-5-1] eliminated 5 clauses out of 483 (1%) of length 16
c [cce-5-1] eliminated 33 clauses out of 907 (4%) of length 15
c [cce-5-1] eliminated 43 clauses out of 790 (5%) of length 14
c [cce-5-1] eliminated 181 clauses out of 1424 (13%) of length 13
c [cce-5-1] eliminated 213 clauses out of 2128 (10%) of length 12
c [cce-5-1] eliminated 362 clauses out of 2068 (18%) of length 11
c [cce-5-1] eliminated 559 clauses out of 3800 (15%) of length 10
c [cce-5-1] eliminated 1271 clauses out of 11133 (11%) of length 9
c [cce-5-1] eliminated 2008 clauses out of 19703 (10%) of length 8
c [cce-5-1] eliminated 2069 clauses out of 22107 (9%) of length 7
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 6755 large clauses in 131099239 steps
c [cce-5-1] allowing another 65549619 steps for small clauses
c [cce-5-1] scheduling 544002 clauses = 403118 binary + 140884 ternary
c [cce-5-1] tried to eliminate 38601 small clauses 7%
c [cce-5-1] eliminated 6678 binary clauses 2%
c [cce-5-1] eliminated 2296 ternary clauses 2%
c [cce-5-1] eliminated 8974 small clauses 2%
c [cce-5-1] eliminated 8974 small clauses in 131099239 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 15729 covered clauses in round 1
c [cce-5] eliminated 15729 covered clauses in TOTAL during 1 rounds
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 153025 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 5295 variables 3% in round 1 in 293637667 steps
c [elim-14-1] backward subsumption/strengthening limit 293637600
c [elim-14-1-1] backward checking 36799 touched variables 24%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 391 and strengthened 485 clauses in 36323946 steps
c [elim-14-1] rescheduled 2303 variables 2% by backward subsumption
c [elim-14-2] eliminated 93 variables 0% in round 2 in 15953320 steps
c [elim-14-2] backward subsumption/strengthening limit 15953300
c [elim-14-2-1] backward checking 950 touched variables 1%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 55 and strengthened 89 clauses in 2434780 steps
c [elim-14-2] rescheduled 335 variables 0% by backward subsumption
c [elim-14-3] eliminated 11 variables 0% in round 3 in 3253647 steps
c [elim-14-3] backward subsumption/strengthening limit 3253600
c [elim-14-3-1] backward checking 125 touched variables 0%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 9 and strengthened 7 clauses in 779777 steps
c [elim-14] incomplete 32 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 5403 = 4% variables out of 153025 scheduled
c [bca-12] limit of 10000000 steps and 2058429 added (scaled 2)
c [bca-12] 241158 out of 295246 literals actually usable 82%
c [bca-12] added 2013 blocked clauses in 789811 steps
c [sweep-12] limit 31463817 penalty 0 = 0 + 0
c [sweep-12-1] 18725 pos 37.4% + 31276 neg 62.6% = 50001 sched 33.9% ret 97621
c [sweep-12-1] 31465095 steps 1952 queries 3623.18 avg class size
c [sweep-12-1] 19602 decisions 1753 SAT calls 27.92 avg env size
c [sweep-12-1] 42128 variables remain 29% (105486 retained 71%)
c [decomp-48] removed 655 variables
c [sweep-12-1] removed 655 vars (0 failed, 434 eqs, 457 impls)
c [sweep-12] removed 655 vars in TOTAL (1 rounds, 1951 queries)
c [phase-count-16] 960396 negative 93.8% of 1023587 except 63191 6.2%
c [phase-count-16] 945327 positive 92.4% of 1023587 except 78260 7.6%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 9 positive 47%, 10 negative 53%
c [sort-queue-16] sorted 86940 enqueued variables after 106519 conflicts
c [score-dist-16] active 60027 (41%), one 0 (0%), zero 86940 (59%)
c [score-dist-16] max exp 533, different 29 (5%)
c [score-dist-16] median active exp 520, avg 521.3
c [simplification-16] removed 9951 variables 6.3% (146967 remain 12%)
c [simplification-16] removed 90145 irredundant clauses 8.1% (1023587 remain 20%)
c [simplification-16] maximum reduction of 8% = max (6%, 8%)
c [simplification-16] large reduction 8% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 118519 (soft 108519 + delta 10000)
c [simplification-16] new conflict limit 108519 (hard 118519)
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 -  906.2  146967  1023587    111431   51327 129825 290459   66    91  160  72%     38   -9   71   51  140%
c i  907.3  146966  1023587    112643   52364 129837 290474   67    89  166  76%     56  -11   61   51  120%
c 
c [simplification-17] limit 108519 conflicts (hard 118519) hit after 118520 conflicts
c [quatres-13] found 191681 quaternary clauses 50% in total
c [quatres-13-1] removed 82 duplicate quaternary clauses
c [quatres-13-1] added 17 double-self-subsuming ternary resolvents
c [quatres-13-2] added 349 single-self-subsuming ternary resolvents
c [quatres-13-2] added 2159 quaternary resolvents
c [ternres-13] limit 109039460 with penalty 0 = 0 + 0
c [ternres-13] all 146966 free variables schedulable
c [ternres-13] 29579 ternary resolvents (1002 bin, 28577 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-49] removed 112 variables
c [simpleprobe-7] 15914 schedulable variables 11%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-50] removed 2149 variables
c [simpleprobe-7] 13671 variables remain 9% (131035 retained 91%)
c [simpleprobe-7] removed 2149 variables, found 109262 hbrs, 86 units
c [unhide-17] limit 5000000 with penalty 2 = 0 + 2
c [unhide-17-17] 1 units, 6 failed, 7422 tauts, 0 hbrs, 8972 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 2646 transitive binary clauses
c [transred-13] found 1 units
c [cce-6] limit of 272598651 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 30
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 23
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 22
c [cce-6-1] eliminated 10 clauses out of 10 (100%) of length 21
c [cce-6-1] eliminated 1 clauses out of 523 (0%) of length 18
c [cce-6-1] eliminated 34 clauses out of 858 (4%) of length 15
c [cce-6-1] eliminated 9 clauses out of 734 (1%) of length 14
c [cce-6-1] eliminated 52 clauses out of 1359 (4%) of length 13
c [cce-6-1] eliminated 100 clauses out of 2223 (4%) of length 12
c [cce-6-1] eliminated 82 clauses out of 1857 (4%) of length 11
c [cce-6-1] eliminated 89 clauses out of 3375 (3%) of length 10
c [cce-6-1] eliminated 161 clauses out of 9974 (2%) of length 9
c [cce-6-1] eliminated 265 clauses out of 17338 (2%) of length 8
c [cce-6-1] eliminated 1206 clauses out of 19712 (6%) of length 7
c [cce-6-1] eliminated 3308 clauses out of 42804 (8%) of length 6
c [cce-6-1] eliminated 4955 clauses out of 79097 (6%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 10277 large clauses in 272598673 steps
c [cce-6-1] allowing another 136299336 steps for small clauses
c [cce-6-1] scheduling 523286 clauses = 368535 binary + 154751 ternary
c [cce-6-1] tried to eliminate 88642 small clauses 17%
c [cce-6-1] eliminated 6721 binary clauses 2%
c [cce-6-1] eliminated 3922 ternary clauses 3%
c [cce-6-1] eliminated 10643 small clauses 2%
c [cce-6-1] eliminated 10764 small clauses in 272598745 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 21041 covered clauses in round 1
c [cce-6] eliminated 21041 covered clauses in TOTAL during 1 rounds
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 144699 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 3519 variables 2% in round 1 in 270757509 steps
c [elim-15-1] backward subsumption/strengthening limit 270757500
c [elim-15-1-1] backward checking 26141 touched variables 18%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 393 and strengthened 345 clauses in 27591786 steps
c [elim-15-1] rescheduled 2028 variables 1% by backward subsumption
c [elim-15-2] eliminated 76 variables 0% in round 2 in 25669090 steps
c [elim-15-2] backward subsumption/strengthening limit 25669000
c [elim-15-2-1] backward checking 621 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 50 and strengthened 40 clauses in 1488386 steps
c [elim-15-2] rescheduled 199 variables 0% by backward subsumption
c [elim-15-3] eliminated 11 variables 0% in round 3 in 1628802 steps
c [elim-15-3] backward subsumption/strengthening limit 1628800
c [elim-15-3-1] backward checking 82 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 5 and strengthened 1 clauses in 536574 steps
c [elim-15] incomplete 13 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 3607 = 2% variables out of 144699 scheduled
c [bca-13] limit of 10000000 steps and 1949370 added (scaled 2)
c [bca-13] 229749 out of 282186 literals actually usable 81%
c [bca-13] added 446 blocked clauses in 732773 steps
c [sweep-13] limit 32711838 penalty 0 = 0 + 0
c [sweep-13-1] 14978 pos 37.5% + 24984 neg 62.5% = 39962 sched 28.3% ret 101130
c [sweep-13-1] 32713461 steps 2295 queries 2983.10 avg class size
c [sweep-13-1] 21973 decisions 2105 SAT calls 26.89 avg env size
c [sweep-13-1] 31659 variables remain 22% (109339 retained 78%)
c [decomp-51] removed 751 variables
c [sweep-13-1] removed 751 vars (0 failed, 494 eqs, 426 impls)
c [sweep-13] removed 751 vars in TOTAL (1 rounds, 2294 queries)
c [phase-count-17] 906407 negative 93.7% of 967155 except 60748 6.3%
c [phase-count-17] 890724 positive 92.1% of 967155 except 76431 7.9%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 8 positive 73%, 3 negative 27%
c [sort-queue-17] sorted 80560 enqueued variables after 118520 conflicts
c [score-dist-17] active 59781 (43%), one 0 (0%), zero 80560 (57%)
c [score-dist-17] max exp 534, different 30 (6%)
c [score-dist-17] median active exp 520, avg 521.4
c [simplification-17] removed 6625 variables 4.5% (140341 remain 11%)
c [simplification-17] removed 56432 irredundant clauses 5.5% (967155 remain 19%)
c [simplification-17] maximum reduction of 6% = max (5%, 6%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 130520 (soft 120520 + delta 10000)
c [simplification-17] new conflict limit 120520 (hard 130520)
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  943.5  140340   967155    119252   54168 146940 353192   70    82  165  86%     29  -17   65   53  122%
c i  944.4  140322   967155    120150   54963 146948 353195   69    80  165  86%    -17  -18   68   53  127%
c i  952.0  140321   967155    125555   59732 146966 353199   65    77  166  85%     12  -20   45   54   84%
c i  952.0  140311   967155    125571   59745 146966 353199   65    77  166  85%     11  -20   44   54   81%
c 
c [simplification-18] limit 120520 conflicts (hard 130520) hit after 130520 conflicts
c [quatres-14] found 187619 quaternary clauses 51% in total
c [quatres-14-1] removed 106 duplicate quaternary clauses
c [quatres-14-1] added 49 double-self-subsuming ternary resolvents
c [quatres-14-2] added 598 single-self-subsuming ternary resolvents
c [quatres-14-2] added 1632 quaternary resolvents
c [ternres-14] limit 112982475 with penalty 0 = 0 + 0
c [ternres-14] all 140297 free variables schedulable
c [ternres-14] 22719 ternary resolvents (464 bin, 22255 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-52] removed 148 variables
c [treelook-7] limit 11298247 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 124417 literals 44%
c [treelook-7] scheduling used 2773734 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 11298247 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 11331336 steps
c [treelook-7] 123689 literals remain 44%
c [treelook-7] 16687 variables remain to probed next time 12%
c [decomp-53] removed 24 variables
c [treelook-7] removed 48 variables, found 20437 hbrs
c [unhide-18] limit 5000000 with penalty 2 = 0 + 2
c [unhide-18-18] 3 units, 79 failed, 74438 tauts, 0 hbrs, 62279 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 1792 transitive binary clauses
c [transred-14] found 1 units
c [block-7] scheduling all variables this time
c [block-7] scheduled 140076 variables 100%
c [block-7] limit of 400000000 steps penalty 1 = 1 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 4251 blocked clauses
c [block-7] 4251 < 1/100 * 964823 = 9648 considered unsuccessful
c [cce-7] limit of 564912375 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 2 clauses out of 499 (0%) of length 18
c [cce-7-1] eliminated 1 clauses out of 524 (0%) of length 16
c [cce-7-1] eliminated 3 clauses out of 775 (0%) of length 15
c [cce-7-1] eliminated 6 clauses out of 721 (1%) of length 14
c [cce-7-1] eliminated 23 clauses out of 1240 (2%) of length 13
c [cce-7-1] eliminated 43 clauses out of 2087 (2%) of length 12
c [cce-7-1] eliminated 64 clauses out of 1783 (4%) of length 11
c [cce-7-1] eliminated 116 clauses out of 2785 (4%) of length 10
c [cce-7-1] eliminated 134 clauses out of 8729 (2%) of length 9
c [cce-7-1] eliminated 214 clauses out of 18224 (1%) of length 8
c [cce-7-1] eliminated 772 clauses out of 18991 (4%) of length 7
c [cce-7-1] eliminated 2314 clauses out of 38938 (6%) of length 6
c [cce-7-1] eliminated 6104 clauses out of 72238 (8%) of length 5
c [cce-7-1] eliminated 36358 clauses out of 162102 (22%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 46154 large clauses in 480561926 steps
c [cce-7-1] allowing another 240280963 steps for small clauses
c [cce-7-1] scheduling 481754 clauses = 350117 binary + 131637 ternary
c [cce-7-1] tried to eliminate 211790 small clauses 44%
c [cce-7-1] eliminated 29342 binary clauses 8%
c [cce-7-1] eliminated 10958 ternary clauses 8%
c [cce-7-1] eliminated 40300 small clauses 8%
c [cce-7-1] eliminated 40300 small clauses in 564912376 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 86454 covered clauses in round 1
c [cce-7] eliminated 86454 covered clauses in TOTAL during 1 rounds
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 140009 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 10522 variables 8% in round 1 in 234880570 steps
c [elim-16-1] backward subsumption/strengthening limit 234880500
c [elim-16-1-1] backward checking 46151 touched variables 33%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 344 and strengthened 878 clauses in 32092159 steps
c [elim-16-1] rescheduled 3144 variables 2% by backward subsumption
c [elim-16-2] eliminated 115 variables 0% in round 2 in 27020731 steps
c [elim-16-2] backward subsumption/strengthening limit 27020700
c [elim-16-2-1] backward checking 953 touched variables 1%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 29 and strengthened 72 clauses in 2094198 steps
c [elim-16-2] rescheduled 277 variables 0% by backward subsumption
c [elim-16-3] eliminated 4 variables 0% in round 3 in 2131910 steps
c [elim-16-3] backward subsumption/strengthening limit 2131900
c [elim-16-3-1] backward checking 49 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 4 and strengthened 5 clauses in 667840 steps
c [elim-16] incomplete 23 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 10643 = 8% variables out of 140009 scheduled
c [bca-14] limit of 10000000 steps and 1712147 added (scaled 2)
c [bca-14] 209484 out of 258734 literals actually usable 81%
c [bca-14] added 3016 blocked clauses in 685063 steps
c [sweep-14] limit 33894742 penalty 0 = 0 + 0
c [sweep-14-1] 10859 pos 37.9% + 17798 neg 62.1% = 28657 sched 22.2% ret 100709
c [sweep-14-1] 33902290 steps 3285 queries 1640.33 avg class size
c [sweep-14-1] 32192 decisions 3105 SAT calls 26.24 avg env size
c [sweep-14-1] 18155 variables remain 14% (111082 retained 86%)
c [decomp-54] removed 962 variables
c [sweep-14-1] removed 962 vars (0 failed, 638 eqs, 528 impls)
c [sweep-14] removed 962 vars in TOTAL (1 rounds, 3284 queries)
c [phase-count-18] 795849 negative 93.8% of 848117 except 52268 6.2%
c [phase-count-18] 779749 positive 91.9% of 848117 except 68368 8.1%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 5 positive 42%, 7 negative 58%
c [sort-queue-18] sorted 69778 enqueued variables after 130520 conflicts
c [score-dist-18] active 58626 (46%), one 0 (0%), zero 69778 (54%)
c [score-dist-18] max exp 534, different 30 (6%)
c [score-dist-18] median active exp 520, avg 521.5
c [simplification-18] removed 11893 variables 8.5% (128404 remain 10%)
c [simplification-18] removed 119038 irredundant clauses 12.3% (848117 remain 17%)
c [simplification-18] maximum reduction of 12% = max (8%, 12%)
c [simplification-18] large reduction 12% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 142520 (soft 132520 + delta 10000)
c [simplification-18] new conflict limit 132520 (hard 142520)
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 20959 basic ate = 15765 trn 75% + 5194 lrg 25% in 4 updates
c bcas: 14 count, 22754 added (10390 skipped), 16753325 steps
c bkwd: tried 3916704 clauses, 7826019 lits, 2.00 lits/clause
c bkwd: checked 283880579 occs, 72.48 occs/clause, 36.27 occs/lit
c bkwd: subsumed 30 binary, 1708 ternary, 3111 large
c bkwd: strengthened 55 binary, 44 ternary (100% self), 7023 large (0% self)
c blkd: 7 bces, 84104 removed, 44749028 resolutions, 117677411 steps
c blkd: 61804 blocking literals 2%, 2253 pure
c bump: 149924 bumped seen, 77284697 lits 515.5 on average
c card: 5 count, 0 units, 0 am1, 101081493 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 12911 subsumed
c card: 5387 at-most-one constraints found, average size 3.12
c card: 5387 at-most-one constraints used 100%, average size 3.12
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: 7 cces, 192665 eliminated, 159346 ate 83%, 33319 abce 17%
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: 17813271 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 148 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 54 decompositions, 143048 equivalent 11%
c deco: 15528 decision-only clauses 10%, 59% reduction
c decs: 1713685 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 744438 eliminated 57%, 11383 pure 2%
c elms: 40 rounds, 2.5 rounds/bve
c elms: 638487 small 86%, 92315 large 12%
c elms: 862067 tried small, 638487 succeeded 74%, 223580 failed 26%
c elms: 308235 subsumed, 404392 strengthened, 0 blocked
c elms: 64569527 copies, 79998858 resolutions, 17703795 ipos
c elms: 56703315 subchks, 101738705 strchks
c gaus: 7 extractions, 84776 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 4 binary and 0 ternary equations
c gaus: 0 gc, 72885004 steps, 36442502 extr 50%, 36538821 elim 50%
c glue: 57.7 orig avg, 57.7 real avg, 6.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1722576 = 678679 simple 39% + 1032770 trn 60% + 11127 lrg 1%, 46264 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 149924 clauses, 86.3 length
c lrnd: 12934504 lits = 26415099 orig - 13480595 removed 51%
c lrnd: 41513 uips 28%, 69616 flips 46%
c mins: 125345 mins 84%, 3131 bin 2%, 5590 size 4%
c mins: 26646756 poisoned searches, 2389385 hits, 9% hit rate
c mins: 43028621 used twice searches, 3518467 hits, 8% hit rate
c move: moved 194040, 97199 bin 50%, 96841 trn 50%
c otfs: 1965 driving 44%, 2525 restarting 56%
c otfs: str 4490, 3555 red 79%, 935 irr 21%
c otfs: str 4490, 0 bin 0%, 1762 trn 39%, 2728 lrg 61%
c otfs: sub 147, 133 red 90%, 14 irr 10%
c otfs: sub 147, 0 bin 0%, 71 trn 48%, 76 lrg 52%
c phas: 18 computed, 932158 set, 431738 pos (46%), 500420 neg (54%)
c prbs: 6 basic, 1473919 probed, 20760 failed, 3423 lifted
c prbs: 7 simple, 1797433 probed, 2535 failed, 24326 eqs
c prbs: 7 treelook, 2543 probed, 113 failed, 0 lifted
c prom: 311 locked 0% out of 475315 tried
c prps: 1817205274 props, 995 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 14 count, 51730 quat, 15317 self1, 747 self2, 6436 dup
c queu: 18 sorted, 1713685 next (91990 steps 0.05)
c queu: 83652446 enq (191227540 steps 2.29), 77284697 deq 92%
c redc: 3704 clauses 15%, 24984 tried 19%, 200 sat 1%
c redc: 6530 lits 4%, 159794 tried 1%, 200 sat 0%
c redc: 586 times jump level reduced, 37.1 levels on average
c reds: 1 count, 131558.0 conflicts per reduce
c reds: 0 memlim 0%, 1 arith 100%
c reds: 25006 collected 91%, 2578 retired 9%
c rmbd: 380695 removed, 272161 red 71%
c rsts: 5363 restarts 88%, 721 skipped 12%
c rsts: 721 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 18 count, 17 confs 94%, 0 vars 0%
c simp: 1 its 6%, 0 bin 0%, 0 trns 0%
c subl: 149924 count (343657 tried 2.3), 27608 sub out of 137200 (20.1%)
c swps: 14 count, 14 rounds, 19847 queries (1417.6/round)
c swps: 18648 sat calls, 2725 unsat (1.1% success rate)
c swps: 221990 decisions 11.9, 20331 conflicts 1.1
c swps; 10708.5 avg class size, 30.4 avg environment size
c swps: 0 failed, 3773 impls, 3844 equivs
c swp0: 6611 type 0 queries, 1411 unsat (21.3%), 6163 sat (93.2%)
c swp1: 13236 type 1 queries, 8590 unsat (64.9%), 9840 sat (74.3%)
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: 3727641 calls to obtain time
c tops: 279132 fixed 22%, 66 its, 1993.30 confs/it
c trds: 14 transitive reductions, 27179 removed, 101 failed
c trds: 332261 nodes, 556753 edges, 28491034 steps
c trim: 708338 words, 2.7 MB
c trnr: 14 count, 16683 bin, 568255 trn, 697166583 steps
c unhd: 18 count, 18 rounds, 220019841 steps
c unhd: 26434 non-trivial sccs of average size 2.5
c unhd: 3651 units, 3611 bin, 37 trn, 3 lrg
c unhd: 5640 failed, 4946 stamp, 0 lits, 23 bin, 578 trn, 3 lrg
c unhd: 598782 tauts, 10932 bin 2%, 131178 trn 22%, 45109 lrg 8%
c unhd: 598782 tauts, 411563 stamp 69%, 430140 red 72%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 880871 str, 3611 bin 0%, 68712 trn 8%, 808548 lrg 92%, 357710 red 41%
c vars: 128404 remaining 10% and 1166618 removed 90% out of 1295022
c vars: 279132 fixed 22%, 744438 eliminated 57%, 143048 equivalent 11%
c vsts: 12287315950 visits, 92% srch, 8% simp, 0% lkhd
c vsts: 6.6 search visits per propagation, 86077.8 per conflict
c wchs: 1517679558 pushed, 204391654 enlarged, 220 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         188930         25006          2578      14055327       4050697         54916
c 
c  0 0         68390  36        17   0         0   0  10674946  76   2257053  56     14712  27     0.8
c  1 5          2526   1        10   0       291  11    655997   5<   319271   8      2864   5     0.1
c  2 6          4961   3        49   0       393  15    936429   7    496320  12<     5759  10     0.2
c  3 9          5594   3       229   1       326  13    576854   4    329183   8      4424   8     0.4
c  4 14         9793   5      2292   9       267  10    388528   3    189235   5      2898   5<    2.0
c  5 21        10127   5<     2027   8       301  12<   250737   2    127560   3      2615   5     1.4
c  6 30         8601   5      1796   7       230   9    136163   1     67471   2      2053   4     1.1
c  7 41         6058   3      3176  13        99   4    108978   1     43135   1      2567   5     1.8
c  8 54        11121   6      1166   5<       76   3    138242   1     86860   2      6051  11     1.6
c  9 69        36639  19      9870  39       415  16    124642   1     85830   2      4951   9     7.6
c 10 86         9667   5      4342  17       173   7     33609   0     28243   1      4736   9     2.8
c 11 126       14351   8        32   0         7   0     28817   0     19428   0      1254   2     7.0
c 12 230        1102   1         0   0         0   0      1385   0      1108   0        32   0     0.4
c 
c avg                  4.8           7.8           5.0           0.8           1.6           4.3
c std                  4.2           2.0           2.9           1.9           2.4           3.7
c 
c  112.492  11% elim
c   98.925  10% probe
c   85.935   9% sweep
c   50.491   5% cce
c   32.171   3% unhide
c   20.636   2% bump
c   17.888   2% block
c   14.539   1% bca
c   14.030   1% gauss
c   11.568   1% quatres
c 
c   13.440 < 1% rest (below)
c 
c    9.380   1% ternres
c    1.860   0% transred
c    1.536   0% decide
c    0.664   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   15.371   2% preprocessing     3%
c  481.514  48% inprocessing     97%
c ==================================
c  496.885  50% simplifying
c  499.678  50% search
c ==================================
c  996.586 100% all
c 
c        131558 conflicts,         132.0 confs/sec
c          1669 ternaries,          78.8 confs/ternary
c           942 binaries,          139.7 confs/binary
c            66 iterations,       1993.3 confs/iteration
c 
c             1 reductions,          0.0 redus/sec, 131558.0 confs/reduction
c          5363 restarts,            5.4 rests/sec,     24.5 confs/restart
c       1713685 decisions,        1719.6 decis/sec,     13.0 decis/conflict
c    1817205274 propagations,  1823430.4 props/sec,   1060.4 props/decision
c 
c 996.6 seconds, 502.7 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
