c launch: /data/cnf/sc2014/app/SAT_dat.k95-24_1_rule_1.cnf.bz2
c host: atom02
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.k95-24_1_rule_1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k95-24_1_rule_1.cnf.bz2
c no embedded options
c found 'p cnf 1540077 6036174' header
c read 1540077 variables, 6036174 clauses, 15152847 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 1492299 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 1492299  5988262         0       0      0     0    0     0  291   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1497065 based on 5988262 irredundant clauses
c [card-1] found 1331 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1497065 for elimination
c [card-1] 1331 out of 1331 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 311739 variables
c [simpleprobe-1] all 1228338 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 9996544 based on 4998272 irredundant clauses
c [decomp-2] removed 2331 variables
c [simpleprobe-1] 1226007 variables remain 100% (0 retained 0%)
c [simpleprobe-1] removed 2331 variables, found 46597 hbrs, 554 units
c [unhide-1] limit 311511 based on 4984188 irredundant clauses
c [unhide-1-1] 1879 units, 1375 failed, 10904 tauts, 0 hbrs, 62108 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1220765 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 1140827 not tried 93% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 80237 = 7% variables out of 1220765 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 4464960 negative 95.2% of 4690418 except 225458 4.8%
c [phase-count-1] 4393387 positive 93.7% of 4690418 except 297031 6.3%
c [phase-1] phase bias: 530218 positive 46%, 610310 negative 54%
c [sort-queue-1] sorted 1140528 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1140528 (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 182331 variables 13.8% (1140528 remain 76%)
c [simplification-1] removed 1297844 irredundant clauses 21.7% (4690418 remain 78%)
c [simplification-1] maximum reduction of 22% = max (14%, 22%)
c [simplification-1] large reduction 22% >= 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   18.7 1140527  4690418         3       2     15 41008    0     0  281   0%      0    0    0    0 25451%
c i   18.8 1140264  4690418        15       2     20 41014    0     0  281   1%      0    0    0    0 24783%
c i   18.9 1140217  4690418       132      78     36 41037    0     1  282   8%      0    1    1    0 20557%
c i   19.0 1140174  4690418       233     147     53 41046    0     2  282   9%      0    2    2    0 17044%
c i   19.0 1140173  4690418       253     162     55 41047    0     2  282   9%      0    2    2    0 16728%
c i   20.7 1139218  4690418       573     407     90 41082    0    10  283   5%      1   10    4    0 11628%
c i   20.8 1139217  4690418       583     414     92 41082    0    11  283   5%      1   10    4    0 11429%
c i   21.0 1139216  4690418       614     438     94 41084    0    12  283   4%      1   12    4    0 10729%
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [decomp-3] removed 5454 variables
c [simpleprobe-2] all 1135074 free variables schedulable
c [simpleprobe-2] limit 9350356 based on 4675178 irredundant clauses
c [decomp-4] removed 2138 variables
c [simpleprobe-2] 956805 variables remain 84% (176131 retained 16%)
c [simpleprobe-2] removed 2138 variables, found 16524 hbrs, 502 units
c [treelook-1] limit 1166604 based on 4666417 irredundant clauses
c [treelook-1] scheduled 233762 literals 10%
c [treelook-1] scheduling used 1166610 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1166604 based on 4666417 irredundant clauses
c [treelook-1] used 1181690 steps
c [treelook-1] 233666 literals remain 10%
c [treelook-1] 230790 variables remain to probed next time 20%
c [decomp-5] removed 121 variables
c [treelook-1] removed 136 variables, found 5740 hbrs
c [basicprobe-1] limit 37326360 based on 4665795 irredundant clauses
c [basicprobe-1-0] 1027387 probes remain 92% after last round
c [basicprobe-1-0] 5602 units = 2493 failed (45%) + 3109 lifted (55%)
c [basicprobe-1-0] removed 12438 variables, found 225464 hbrs
c [unhide-2] limit 291612 based on 4665795 irredundant clauses
c [unhide-2-2] 856 units, 1344 failed, 14277 tauts, 0 hbrs, 39506 literals
c [elim-2] 1117809 variables 100% will be scheduled this time
c [elim-2] scheduled 1117809 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 1035668 not tried 93% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 82140 = 7% variables out of 1117809 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 4188052 negative 95.1% of 4403081 except 215029 4.9%
c [phase-count-2] 4115719 positive 93.5% of 4403081 except 287362 6.5%
c [phase-2] phase bias: 898 positive 31%, 1992 negative 69%
c [sort-queue-2] sorted 1015960 enqueued variables after 729 conflicts
c [score-dist-2] active 19709 (2%), one 0 (0%), zero 1015960 (98%)
c [score-dist-2] max exp 515, different 15 (3%)
c [score-dist-2] median active exp 510, avg 510.7
c [simplification-2] removed 103547 variables 9.1% (1035669 remain 69%)
c [simplification-2] removed 287337 irredundant clauses 6.1% (4403081 remain 74%)
c [simplification-2] maximum reduction of 9% = max (9%, 6%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1004 (hard 11000)
c [simplification-2] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   49.0 1035668  4403081       735     401     71 212986    1    16  275   4%      1   16    4    0 9031%
c i   49.8 1035667  4403081       825     460     88 212997    1    21  276   3%      1   21    3    0 7813%
c 
c [simplification-3] limit 1004 conflicts (hard 11000) hit after 1005 conflicts
c [card-2] limit 1100770 based on 4403081 irredundant clauses
c [card-2] found 985 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1100770 for elimination
c [card-2] 985 out of 985 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 6335 variables
c [treelook-2] limit 1098278 based on 4393113 irredundant clauses
c [treelook-2] scheduled 206680 literals 10%
c [treelook-2] scheduling used 1098393 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1098278 based on 4393113 irredundant clauses
c [treelook-2] used 1106910 steps
c [treelook-2] 206490 literals remain 10%
c [treelook-2] 127985 variables remain to probed next time 12%
c [decomp-7] removed 175 variables
c [treelook-2] removed 194 variables, found 3743 hbrs
c [unhide-3] limit 274518 based on 4392300 irredundant clauses
c [unhide-3-3] 315 units, 645 failed, 19009 tauts, 0 hbrs, 19337 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1027971 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 952956 not tried 93% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 75015 = 7% variables out of 1027971 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 3993507 negative 95.0% of 4202505 except 208998 5.0%
c [phase-count-3] 3920779 positive 93.3% of 4202505 except 281726 6.7%
c [phase-3] phase bias: 439 positive 28%, 1115 negative 72%
c [sort-queue-3] sorted 932673 enqueued variables after 1005 conflicts
c [score-dist-3] active 20283 (2%), one 0 (0%), zero 932673 (98%)
c [score-dist-3] max exp 516, different 16 (3%)
c [score-dist-3] median active exp 511, avg 510.9
c [simplification-3] removed 82711 variables 8.0% (952956 remain 64%)
c [simplification-3] removed 200576 irredundant clauses 4.6% (4202505 remain 70%)
c [simplification-3] maximum reduction of 8% = max (8%, 5%)
c [simplification-3] large reduction 8% >= 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 13005 (soft 3005 + delta 10000)
c [simplification-3] new conflict limit 3005 (hard 13005)
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   74.0  952955  4202505      1402     785    203 183922    1    33  269   3%      3   33    3    0 4134%
c i   74.1  952917  4202505      1405     786    204 183922    1    33  269   3%      3   33    3    0 4108%
c i   80.1  952860  4202505      2112    1333    299 183969    2    47  269   5%      4   47   12    0 6443%
c 
c [simplification-4] limit 3008 conflicts (hard 13005) hit after 3011 conflicts
c [decomp-8] removed 1070 variables
c [basicprobe-2] limit 33598608 based on 4199826 irredundant clauses
c [basicprobe-2-0] 743566 probes remain 78% after last round
c [basicprobe-2-0] 1698 units = 1558 failed (92%) + 140 lifted (8%)
c [basicprobe-2-0] removed 3637 variables, found 169869 hbrs
c [unhide-4] limit 262489 based on 4199826 irredundant clauses
c [unhide-4-4] 501 units, 765 failed, 16311 tauts, 0 hbrs, 35133 literals
c [elim-4] 947004 variables 100% will be scheduled this time
c [elim-4] scheduled 947004 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 399378155 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 7938 not tried 1% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 556102 = 59% variables out of 947004 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 2606926 negative 95.6% of 2727982 except 121056 4.4%
c [phase-count-4] 2557359 positive 93.7% of 2727982 except 170623 6.3%
c [phase-4] phase bias: 2834 positive 40%, 4244 negative 60%
c [sort-queue-4] sorted 370348 enqueued variables after 3011 conflicts
c [score-dist-4] active 20555 (5%), one 0 (0%), zero 370348 (95%)
c [score-dist-4] max exp 519, different 18 (3%)
c [score-dist-4] median active exp 513, avg 513.1
c [simplification-4] removed 561957 variables 59.0% (390903 remain 26%)
c [simplification-4] removed 1474523 irredundant clauses 35.1% (2727982 remain 46%)
c [simplification-4] maximum reduction of 59% = max (59%, 35%)
c [simplification-4] large reduction 59% >= 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 15011 (soft 5011 + delta 10000)
c [simplification-4] new conflict limit 5011 (hard 15011)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  130.6  390902  2727975      4156    1450    289 80180    8    79  232  11%     18   76   26    1 3811%
c i  132.3  390901  2727975      4427    1651    309 80192    9    80  232  11%     14   77   22    1 2908%
c 
c [simplification-5] limit 5011 conflicts (hard 15011) hit after 5012 conflicts
c [quatres-1] found 338994 quaternary clauses 40% in total
c [quatres-1-1] removed 7 duplicate quaternary clauses
c [quatres-1-1] added 122 double-self-subsuming ternary resolvents
c [quatres-1-2] added 3570 single-self-subsuming ternary resolvents
c [quatres-1-2] added 11556 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 14938547 with penalty 1 = 0 + 1
c [ternres-1] all 390901 free variables schedulable
c [ternres-1] 73199 ternary resolvents (379 bin, 72820 trn)
c [ternres-1] 216197 variables remain 55% (174704 retained 45%)
c [gauss-1] limit 1363920 based on 2727840 irredundant clauses
c [gauss-1] extracted 6491 xors of average arity 3.0
c [gauss-1] connected 19241 occurrences of 7646 variables (average 2.5)
c [gauss-1] limit 1363912 based on 2727825 irredundant clauses
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 2171 variables
c [simpleprobe-3] 328874 schedulable variables 85%
c [simpleprobe-3] limit 11950838 penalty 1 = 0 + 1
c [decomp-10] removed 815 variables
c [simpleprobe-3] 274671 variables remain 71% (113244 retained 29%)
c [simpleprobe-3] removed 815 variables, found 48123 hbrs, 262 units
c [unhide-5] limit 169871 based on 2717948 irredundant clauses
c [unhide-5-5] 201 units, 300 failed, 61726 tauts, 0 hbrs, 88353 literals
c [transred-1] limit 2667336 based on 2667336 irredundant clauses
c [transred-1] removed 1238 transitive binary clauses
c [transred-1] found 27 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 387307 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 298770960 steps penalty 1 = 0 + 1
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 29774 blocked clauses
c [cce-1] limit of 15000000 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 3 clauses out of 4 (75%) of length 24
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 23
c [cce-1-1] eliminated 5 clauses out of 17 (29%) of length 22
c [cce-1-1] eliminated 4 clauses out of 8 (50%) of length 21
c [cce-1-1] eliminated 5 clauses out of 8 (62%) of length 20
c [cce-1-1] eliminated 18 clauses out of 26 (69%) of length 19
c [cce-1-1] eliminated 343 clauses out of 1300 (26%) of length 18
c [cce-1-1] eliminated 139 clauses out of 1430 (10%) of length 17
c [cce-1-1] eliminated 344 clauses out of 916 (38%) of length 16
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 862 large clauses in 15015220 steps
c [cce-1-1] allowing another 7507610 steps for small clauses
c [cce-1-1] scheduling 1531452 clauses = 1185195 binary + 346257 ternary
c [cce-1-1] tried to eliminate 3331 small clauses 0%
c [cce-1-1] eliminated 561 binary clauses 0%
c [cce-1-1] eliminated 138 ternary clauses 0%
c [cce-1-1] eliminated 699 small clauses 0%
c [cce-1-1] eliminated 699 small clauses in 15000019 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1561 covered clauses in round 1
c [cce-1] eliminated 1561 covered clauses in TOTAL during 1 rounds
c [cce-1] 1561 < 1/100 * 2630954 = 26309 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 386696 variables 100%
c [elim-5] limit of 59754192 steps penalty 1 = 0 + 1
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 153261 not tried 40% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 20758 = 5% variables out of 386696 scheduled
c [bca-1] limit of 10000000 steps and 5165354 added (scaled 2)
c [bca-1] 701871 out of 731878 literals actually usable 96%
c [bca-1] added 9500 blocked clauses in 2223142 steps
c [sweep-1] limit 5164854 based on 2582427 irredundant clauses
c [sweep-1-1] 123852 pos 33.8% + 242086 neg 66.2% = 365938 sched 100.0% ret 0
c [sweep-1-1] 5198017 steps 100 queries 109171.38 avg class size
c [sweep-1-1] 1359 decisions 97 SAT calls 36.78 avg env size
c [sweep-1-1] 365321 variables remain 100% (453 retained 0%)
c [decomp-11] removed 710 variables
c [sweep-1-1] removed 710 vars (0 failed, 21 eqs, 20 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 710 vars in TOTAL (1 rounds, 99 queries)
c [phase-count-5] 2465505 negative 95.6% of 2579633 except 114128 4.4%
c [phase-count-5] 2436412 positive 94.4% of 2579633 except 143221 5.6%
c [phase-5] phase bias: 1105 positive 47%, 1259 negative 53%
c [sort-queue-5] sorted 338529 enqueued variables after 5012 conflicts
c [score-dist-5] active 26699 (7%), one 0 (0%), zero 338529 (93%)
c [score-dist-5] max exp 523, different 22 (4%)
c [score-dist-5] median active exp 515, avg 515.0
c [simplification-5] removed 25673 variables 6.6% (365228 remain 24%)
c [simplification-5] removed 148341 irredundant clauses 5.4% (2579633 remain 43%)
c [simplification-5] maximum reduction of 7% = max (7%, 5%)
c [simplification-5] large reduction 7% >= 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 17012 (soft 7012 + delta 10000)
c [simplification-5] new conflict limit 7012 (hard 17012)
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  165.8  365227  2579633      5257   11128  54962 121399   11    87  233  13%     10   83   21    1 2078%
c 
c [simplification-6] limit 7012 conflicts (hard 17012) hit after 7013 conflicts
c [quatres-2] found 346731 quaternary clauses 41% in total
c [quatres-2-1] removed 25 duplicate quaternary clauses
c [quatres-2-1] added 23 double-self-subsuming ternary resolvents
c [quatres-2-2] added 1985 single-self-subsuming ternary resolvents
c [quatres-2-2] added 8610 quaternary resolvents
c [ternres-2] limit 10317956 based on 2579489 irredundant clauses
c [ternres-2] 201599 schedulable variables 55%
c [ternres-2] 47516 ternary resolvents (1182 bin, 46334 trn)
c [ternres-2] 127574 variables remain 35% (237653 retained 65%)
c [card-3] limit 644872 based on 2579489 irredundant clauses
c [card-3] found 326 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 644872 for elimination
c [card-3] 326 out of 326 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 374 variables
c [treelook-3] limit 644776 based on 2579106 irredundant clauses
c [treelook-3] scheduled 74500 literals 10%
c [treelook-3] scheduling used 645274 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 644776 based on 2579106 irredundant clauses
c [treelook-3] used 645587 steps
c [treelook-3] 74405 literals remain 10%
c [treelook-3] 44925 variables remain to probed next time 12%
c [decomp-13] removed 6 variables
c [treelook-3] removed 10 variables, found 1324 hbrs
c [unhide-6] limit 247563 with penalty 3 = 0 + 3
c [unhide-6-6] 241 units, 650 failed, 8797 tauts, 0 hbrs, 56593 literals
c [transred-2] limit 2576454 based on 2576454 irredundant clauses
c [transred-2] removed 1038 transitive binary clauses
c [transred-2] found 17 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 364006 variables 100%
c [block-2] limit of 49512617 steps penalty 1 = 0 + 1
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 9859 blocked clauses
c [block-2] 9859 < 1/100 * 2575744 = 25757 considered unsuccessful
c [elim-6] 7807 variables 2% will be scheduled this time
c [elim-6] scheduled 7807 variables 2%
c [elim-6] limit of 99025234 steps penalty 1 = 0 + 1
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 3902 not tried 1% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 30 = 0% variables out of 7807 scheduled
c [elim-6] 30 < 1/100 * 7807 = 78 considered unsuccessful
c [bca-2] limit of 10000000 steps and 5103034 added (scaled 2)
c [bca-2] 683002 out of 727562 literals actually usable 94%
c [bca-2] added 526 blocked clauses in 2142921 steps
c [sweep-2] limit 5097784 based on 2548892 irredundant clauses
c [sweep-2-1] 123457 pos 34.0% + 239891 neg 66.0% = 363348 sched 99.9% ret 432
c [sweep-2-1] 5120055 steps 99 queries 116996.17 avg class size
c [sweep-2-1] 1252 decisions 95 SAT calls 31.52 avg env size
c [sweep-2-1] 362862 variables remain 100% (905 retained 0%)
c [decomp-14] removed 712 variables
c [sweep-2-1] removed 712 vars (0 failed, 22 eqs, 27 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 712 vars in TOTAL (1 rounds, 98 queries)
c [phase-count-6] 2433425 negative 95.5% of 2546916 except 113491 4.5%
c [phase-count-6] 2402755 positive 94.3% of 2546916 except 144161 5.7%
c [phase-6] phase bias: 366 positive 43%, 495 negative 57%
c [sort-queue-6] sorted 333839 enqueued variables after 7013 conflicts
c [score-dist-6] active 29229 (8%), one 0 (0%), zero 333839 (92%)
c [score-dist-6] max exp 525, different 24 (5%)
c [score-dist-6] median active exp 516, avg 516.3
c [simplification-6] removed 2159 variables 0.6% (363068 remain 24%)
c [simplification-6] removed 32717 irredundant clauses 1.3% (2546916 remain 43%)
c [simplification-6] maximum reduction of 1% = max (1%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 10000
c [simplification-6] penalized conflict interval 10000 = 1 * 10000
c [simplification-6] hard conflict limit 27013 (soft 17013 + delta 10000)
c [simplification-6] new conflict limit 17013 (hard 27013)
c 
c [simplification-7] limit 17013 conflicts (hard 27013) hit after 17013 conflicts
c [quatres-3] found 349589 quaternary clauses 42% in total
c [quatres-3-1] removed 20 duplicate quaternary clauses
c [quatres-3-1] added 24 double-self-subsuming ternary resolvents
c [quatres-3-2] added 1005 single-self-subsuming ternary resolvents
c [quatres-3-2] added 3374 quaternary resolvents
c [ternres-3] limit 22355280 with penalty 1 = 0 + 1
c [ternres-3] 126634 schedulable variables 35%
c [ternres-3] 90485 ternary resolvents (3840 bin, 86645 trn)
c [ternres-3] 6879 variables remain 2% (356189 retained 98%)
c [gauss-2] limit 2235528 penalty 2 = 1 + 1
c [gauss-2] extracted 8882 xors of average arity 3.0
c [gauss-2] connected 26441 occurrences of 9572 variables (average 2.8)
c [gauss-2] limit 2235528 penalty 2 = 1 + 1
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 1201 variables
c [basicprobe-3] limit 111776401 penalty 1 = 0 + 1
c [basicprobe-3-0] 139585 probes remain 40% after last round
c [basicprobe-3-0] 8408 units = 7495 failed (89%) + 913 lifted (11%)
c [basicprobe-3-0] removed 10072 variables, found 373662 hbrs
c [bate-1] eliminated 9289 asymmetric tautologies during probing
c [unhide-7] limit 1117764 with penalty 3 = 0 + 3
c [unhide-7-7] 128 units, 200 failed, 40709 tauts, 0 hbrs, 45959 literals
c [transred-3] limit 2382675 based on 2382675 irredundant clauses
c [transred-3] removed 2186 transitive binary clauses
c [transred-3] found 9 units
c [cce-2] limit of 55888200 steps penalty 2 = 1 + 1
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 22
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 21
c [cce-2-1] eliminated 3 clauses out of 4 (75%) of length 20
c [cce-2-1] eliminated 2 clauses out of 7 (29%) of length 19
c [cce-2-1] eliminated 2 clauses out of 825 (0%) of length 18
c [cce-2-1] eliminated 10 clauses out of 809 (1%) of length 17
c [cce-2-1] eliminated 12 clauses out of 848 (1%) of length 16
c [cce-2-1] eliminated 191 clauses out of 1831 (10%) of length 15
c [cce-2-1] eliminated 679 clauses out of 2603 (26%) of length 14
c [cce-2-1] eliminated 1514 clauses out of 4867 (31%) of length 13
c [cce-2-1] eliminated 878 clauses out of 6801 (13%) of length 12
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 3297 large clauses in 55888214 steps
c [cce-2-1] allowing another 27944107 steps for small clauses
c [cce-2-1] scheduling 1296288 clauses = 1027641 binary + 268647 ternary
c [cce-2-1] tried to eliminate 12804 small clauses 1%
c [cce-2-1] eliminated 1715 binary clauses 0%
c [cce-2-1] eliminated 531 ternary clauses 0%
c [cce-2-1] eliminated 2246 small clauses 0%
c [cce-2-1] eliminated 5164 small clauses in 55888202 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 8461 covered clauses in round 1
c [cce-2] eliminated 8461 covered clauses in TOTAL during 1 rounds
c [cce-2] 8461 < 1/100 * 2382062 = 23820 considered unsuccessful
c [bca-3] limit of 10000000 steps and 4752715 added (scaled 2)
c [bca-3] 655956 out of 702926 literals actually usable 93%
c [bca-3] added 998 blocked clauses in 1966511 steps
c [sweep-3] limit 6706584 penalty 1 = 0 + 1
c [sweep-3-1] 117660 pos 33.6% + 232936 neg 66.4% = 350596 sched 99.8% ret 866
c [sweep-3-1] 6790833 steps 125 queries 105690.54 avg class size
c [sweep-3-1] 1437 decisions 100 SAT calls 32.57 avg env size
c [sweep-3-1] 350044 variables remain 100% (1411 retained 0%)
c [decomp-16] removed 9442 variables
c [sweep-3-1] removed 9442 vars (0 failed, 36 eqs, 43 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 9442 vars in TOTAL (1 rounds, 124 queries)
c [phase-count-7] 2240615 negative 95.0% of 2358530 except 117915 5.0%
c [phase-count-7] 2219565 positive 94.1% of 2358530 except 138965 5.9%
c [phase-7] phase bias: 1482 positive 58%, 1078 negative 42%
c [sort-queue-7] sorted 313237 enqueued variables after 17013 conflicts
c [score-dist-7] active 28783 (8%), one 0 (0%), zero 313237 (92%)
c [score-dist-7] max exp 528, different 27 (5%)
c [score-dist-7] median active exp 516, avg 517.7
c [simplification-7] removed 21048 variables 5.8% (342020 remain 23%)
c [simplification-7] removed 188386 irredundant clauses 7.4% (2358530 remain 39%)
c [simplification-7] maximum reduction of 7% = max (6%, 7%)
c [simplification-7] large reduction 7% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 29013 (soft 19013 + delta 10000)
c [simplification-7] new conflict limit 19013 (hard 29013)
c 
c [simplification-8] limit 19013 conflicts (hard 29013) hit after 19013 conflicts
c [quatres-4] found 335642 quaternary clauses 43% in total
c [quatres-4-1] removed 61 duplicate quaternary clauses
c [quatres-4-1] added 68 double-self-subsuming ternary resolvents
c [quatres-4-2] added 1605 single-self-subsuming ternary resolvents
c [quatres-4-2] added 4306 quaternary resolvents
c [ternres-4] limit 25118635 with penalty 1 = 0 + 1
c [ternres-4] 6251 schedulable variables 2%
c [ternres-4] 86331 ternary resolvents (3176 bin, 83155 trn)
c [ternres-4] 593 variables remain 0% (341427 retained 100%)
c [decomp-17] removed 717 variables
c [simpleprobe-4] 241036 schedulable variables 71%
c [simpleprobe-4] limit 100000000 penalty 1 = 0 + 1
c [decomp-18] removed 5332 variables
c [simpleprobe-4] 137867 variables remain 41% (198104 retained 59%)
c [simpleprobe-4] removed 5332 variables, found 177589 hbrs, 841 units
c [unhide-8] limit 1255931 with penalty 3 = 0 + 3
c [unhide-8-8] 170 units, 274 failed, 56541 tauts, 0 hbrs, 53327 literals
c [transred-4] limit 2317400 based on 2317400 irredundant clauses
c [transred-4] removed 1918 transitive binary clauses
c [transred-4] found 8 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 335563 variables 100%
c [block-3] limit of 125593175 steps penalty 2 = 1 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 19971 blocked clauses
c [block-3] 19971 < 1/100 * 2316898 = 23168 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 335145 variables 100%
c [elim-7] limit of 200000000 steps penalty 2 = 1 + 1
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 8948 not tried 3% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 24741 = 7% variables out of 335145 scheduled
c [bca-4] limit of 10000000 steps and 4393756 added (scaled 2)
c [bca-4] 574517 out of 620810 literals actually usable 93%
c [bca-4] added 2428 blocked clauses in 1812848 steps
c [sweep-4] limit 7535590 penalty 1 = 0 + 1
c [sweep-4-1] 101194 pos 32.7% + 208005 neg 67.3% = 309199 sched 99.6% ret 1205
c [sweep-4-1] 7602375 steps 162 queries 93722.20 avg class size
c [sweep-4-1] 2177 decisions 163 SAT calls 32.63 avg env size
c [sweep-4-1] 308074 variables remain 99% (2329 retained 1%)
c [decomp-19] removed 939 variables
c [sweep-4-1] removed 939 vars (0 failed, 24 eqs, 26 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 939 vars in TOTAL (1 rounds, 161 queries)
c [phase-count-8] 2082954 negative 95.1% of 2191414 except 108460 4.9%
c [phase-count-8] 2058820 positive 93.9% of 2191414 except 132594 6.1%
c [phase-8] phase bias: 1149 positive 44%, 1435 negative 56%
c [sort-queue-8] sorted 281828 enqueued variables after 19013 conflicts
c [score-dist-8] active 27637 (9%), one 0 (0%), zero 281828 (91%)
c [score-dist-8] max exp 529, different 27 (5%)
c [score-dist-8] median active exp 516, avg 518.1
c [simplification-8] removed 32555 variables 9.5% (309465 remain 21%)
c [simplification-8] removed 167116 irredundant clauses 7.1% (2191414 remain 37%)
c [simplification-8] maximum reduction of 10% = max (10%, 7%)
c [simplification-8] large reduction 10% >= 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 31013 (soft 21013 + delta 10000)
c [simplification-8] new conflict limit 21013 (hard 31013)
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  487.6  309464  2191414     20828   24961 152585 366872  117   153  229  76%    203  119  104   30  346%
c 
c [simplification-9] limit 21013 conflicts (hard 31013) hit after 21015 conflicts
c [quatres-5] found 334513 quaternary clauses 44% in total
c [quatres-5-1] removed 351 duplicate quaternary clauses
c [quatres-5-1] added 29 double-self-subsuming ternary resolvents
c [quatres-5-2] added 1158 single-self-subsuming ternary resolvents
c [quatres-5-2] added 5640 quaternary resolvents
c [ternres-5] limit 27026270 with penalty 1 = 0 + 1
c [ternres-5] 529 schedulable variables 0%
c [ternres-5] 107165 ternary resolvents (2497 bin, 104668 trn)
c [ternres-5] 65 variables remain 0% (309399 retained 100%)
c [decomp-20] removed 536 variables
c [treelook-4] limit 2702627 penalty 1 = 0 + 1 boost 1
c [treelook-4] scheduled 172109 literals 28%
c [treelook-4] scheduling used 2702630 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 2702627 penalty 1 = 0 + 1 boost 1
c [treelook-4] used 2707171 steps
c [treelook-4] 171825 literals remain 28%
c [treelook-4] 35626 variables remain to probed next time 12%
c [decomp-21] removed 32 variables
c [treelook-4] removed 51 variables, found 2942 hbrs
c [unhide-9] limit 1351313 with penalty 3 = 0 + 3
c [unhide-9-9] 96 units, 247 failed, 20642 tauts, 0 hbrs, 21603 literals
c [transred-5] limit 2172988 based on 2172988 irredundant clauses
c [transred-5] removed 1585 transitive binary clauses
c [transred-5] found 10 units
c [elim-8] 3785 variables 1% will be scheduled this time
c [elim-8] scheduled 3785 variables 1%
c [elim-8] boosting limit by 20
c [elim-8] limit of 8000000000 steps penalty 1 = 0 + 1
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 488273287 steps
c [elim-8] fully completed in 1 rounds
c [gc-65] reconnected 361525 binary clauses (produced 0 empty 2 units)
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 29 = 1% variables out of 3785 scheduled
c [elim-8] 29 < 1/100 * 3785 = 37 considered unsuccessful
c [bca-5] limit of 10000000 steps and 4322182 added (scaled 2)
c [bca-5] 563064 out of 617122 literals actually usable 91%
c [bca-5] added 455 blocked clauses in 1772772 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 81078810 penalty 1 = 0 + 1
c [sweep-5-1] 100359 pos 32.8% + 205900 neg 67.2% = 306259 sched 99.3% ret 2301
c [sweep-5-1] 81108112 steps 1628 queries 36031.90 avg class size
c [sweep-5-1] 21993 decisions 1536 SAT calls 37.65 avg env size
c [sweep-5-1] 288485 variables remain 94% (19953 retained 6%)
c [decomp-22] removed 1282 variables
c [sweep-5-1] removed 1282 vars (0 failed, 268 eqs, 356 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1282 vars in TOTAL (1 rounds, 1627 queries)
c [phase-count-9] 2044746 negative 95.0% of 2153445 except 108699 5.0%
c [phase-count-9] 2022332 positive 93.9% of 2153445 except 131113 6.1%
c [phase-9] phase bias: 238 positive 53%, 211 negative 47%
c [sort-queue-9] sorted 272481 enqueued variables after 21015 conflicts
c [score-dist-9] active 34797 (11%), one 0 (0%), zero 272481 (89%)
c [score-dist-9] max exp 529, different 27 (5%)
c [score-dist-9] median active exp 517, avg 518.3
c [simplification-9] removed 2186 variables 0.7% (307278 remain 21%)
c [simplification-9] removed 37969 irredundant clauses 1.7% (2153445 remain 36%)
c [simplification-9] maximum reduction of 2% = max (1%, 2%)
c [simplification-9] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-9] new conflict interval 16666
c [simplification-9] penalized conflict interval 16666 = 1 * 16666
c [simplification-9] hard conflict limit 47681 (soft 37681 + delta 10000)
c [simplification-9] new conflict limit 37681 (hard 47681)
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  583.8  307277  2153445     24924   30804 200004 366590  118   140  232  84%     25   99  111   35  312%
c i  684.0  307276  2153445     35251   33781 200067 366615   88   130  236  68%    111   76   52   45  116%
c i  690.4  307266  2153445     37226   35500 200112 366636   68   125  236  54%      3   69   38   45   84%
c i  693.5  307265  2153445     38416   36555 200125 366643   59   124  236  48%    -15   66   44   45   98%
c i  698.6  307264  2153445     40472   38473 200138 366645   50   116  237  43%    -13   56   35   44   78%
c 
c [simplification-10] limit 37681 conflicts (hard 47681) hit after 43523 conflicts
c [quatres-6] found 338799 quaternary clauses 45% in total
c [quatres-6-1] removed 61 duplicate quaternary clauses
c [quatres-6-1] added 31 double-self-subsuming ternary resolvents
c [quatres-6-2] added 595 single-self-subsuming ternary resolvents
c [quatres-6-2] added 2505 quaternary resolvents
c [ternres-6] limit 47317979 with penalty 1 = 0 + 1
c [ternres-6] 60 schedulable variables 0%
c [ternres-6] 58893 ternary resolvents (1208 bin, 57685 trn)
c [ternres-6] 1 variables remain 0% (307263 retained 100%)
c [card-4] limit 2957373 penalty 4 = 3 + 1
c [card-4] found 1648 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2957373 for elimination
c [card-4] 1648 out of 1648 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 2365898 penalty 3 = 2 + 1
c [gauss-3] extracted 5735 xors of average arity 3.0
c [gauss-3] connected 17101 occurrences of 6887 variables (average 2.5)
c [gauss-3] limit 2365898 penalty 3 = 2 + 1
c [decomp-23] removed 346 variables
c [gauss-3] exported 0 unary, 1 binary and 0 ternary equations
c [basicprobe-4] limit 200000000 penalty 1 = 0 + 1
c [basicprobe-4-0] 112533 sched 38%, 6230 failed, 368 lifted, 211906 hbrs
c [decomp-25] removed 17392 variables
c [basicprobe-4-1] 95922 probes remain 35% after last round
c [basicprobe-4-1] 8673 units = 8192 failed (94%) + 481 lifted (6%)
c [basicprobe-4-1] removed 29441 variables, found 264751 hbrs
c [bate-2] eliminated 7287 asymmetric tautologies during probing
c [unhide-10] limit 2365898 with penalty 3 = 0 + 3
c [unhide-10-10] 113 units, 181 failed, 53405 tauts, 0 hbrs, 68905 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 2165 transitive binary clauses
c [transred-6] found 3 units
c [cce-3] limit of 118294947 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 22
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 21
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 20
c [cce-3-1] eliminated 7 clauses out of 11 (64%) of length 19
c [cce-3-1] eliminated 13 clauses out of 795 (2%) of length 18
c [cce-3-1] eliminated 13 clauses out of 743 (2%) of length 17
c [cce-3-1] eliminated 19 clauses out of 518 (4%) of length 16
c [cce-3-1] eliminated 19 clauses out of 1334 (1%) of length 15
c [cce-3-1] eliminated 83 clauses out of 1391 (6%) of length 14
c [cce-3-1] eliminated 878 clauses out of 3325 (26%) of length 13
c [cce-3-1] eliminated 1776 clauses out of 5837 (30%) of length 12
c [cce-3-1] eliminated 1952 clauses out of 8452 (23%) of length 11
c [cce-3-1] eliminated 4092 clauses out of 27454 (15%) of length 10
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 8859 large clauses in 118294972 steps
c [cce-3-1] allowing another 59147486 steps for small clauses
c [cce-3-1] scheduling 1014941 clauses = 798257 binary + 216684 ternary
c [cce-3-1] tried to eliminate 27291 small clauses 3%
c [cce-3-1] eliminated 5316 binary clauses 1%
c [cce-3-1] eliminated 1436 ternary clauses 1%
c [cce-3-1] eliminated 6752 small clauses 1%
c [cce-3-1] eliminated 8427 small clauses in 118294962 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 17286 covered clauses in round 1
c [cce-3] eliminated 17286 covered clauses in TOTAL during 1 rounds
c [cce-3] 17286 < 1/100 * 1912397 = 19123 considered unsuccessful
c [bca-6] limit of 10000000 steps and 3797675 added (scaled 2)
c [bca-6] 500481 out of 554502 literals actually usable 90%
c [bca-6] added 1495 blocked clauses in 1533911 steps
c [sweep-6] limit 28390787 penalty 0 = 0 + 0
c [sweep-6-1] 83594 pos 32.2% + 176113 neg 67.8% = 259707 sched 93.7% ret 17543
c [sweep-6-1] 28426252 steps 687 queries 53808.67 avg class size
c [sweep-6-1] 8141 decisions 635 SAT calls 31.48 avg env size
c [sweep-6-1] 254548 variables remain 92% (22600 retained 8%)
c [decomp-26] removed 4185 variables
c [sweep-6-1] removed 4185 vars (0 failed, 115 eqs, 142 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 4185 vars in TOTAL (1 rounds, 686 queries)
c [phase-count-10] 1783986 negative 94.7% of 1884684 except 100698 5.3%
c [phase-count-10] 1760238 positive 93.4% of 1884684 except 124446 6.6%
c [phase-10] phase bias: 852 positive 45%, 1062 negative 55%
c [sort-queue-10] sorted 235532 enqueued variables after 43523 conflicts
c [score-dist-10] active 37533 (14%), one 0 (0%), zero 235532 (86%)
c [score-dist-10] max exp 531, different 28 (5%)
c [score-dist-10] median active exp 519, avg 519.8
c [simplification-10] removed 34199 variables 11.1% (273065 remain 18%)
c [simplification-10] removed 268761 irredundant clauses 12.5% (1884684 remain 31%)
c [simplification-10] maximum reduction of 12% = max (11%, 12%)
c [simplification-10] large reduction 12% >= 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 55523 (soft 45523 + delta 10000)
c [simplification-10] new conflict limit 45523 (hard 55523)
c 
c [simplification-11] limit 45523 conflicts (hard 55523) hit after 45523 conflicts
c [quatres-7] found 304279 quaternary clauses 46% in total
c [quatres-7-1] removed 198 duplicate quaternary clauses
c [quatres-7-1] added 158 double-self-subsuming ternary resolvents
c [quatres-7-2] added 1420 single-self-subsuming ternary resolvents
c [quatres-7-2] added 3483 quaternary resolvents
c [ternres-7] limit 96729429 with penalty 0 = 0 + 0
c [ternres-7] 1 schedulable variables 0%
c [ternres-7] 31586 ternary resolvents (724 bin, 30862 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 132 variables
c [simpleprobe-5] 108191 schedulable variables 40%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-28] removed 7323 variables
c [simpleprobe-5] 60412 variables remain 23% (205198 retained 77%)
c [simpleprobe-5] removed 7323 variables, found 256151 hbrs, 571 units
c [unhide-11] limit 2418235 with penalty 3 = 0 + 3
c [unhide-11-11] 30 units, 37 failed, 24186 tauts, 0 hbrs, 33952 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 3379 transitive binary clauses
c [transred-7] found 4 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 265545 variables 100%
c [block-4] limit of 200000000 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 28282 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 264627 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 1137 not tried 0% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 21656 = 8% variables out of 264627 scheduled
c [bca-7] limit of 10000000 steps and 3440089 added (scaled 2)
c [bca-7] 433717 out of 485944 literals actually usable 89%
c [bca-7] added 2800 blocked clauses in 1388253 steps
c [sweep-7] limit 29018828 penalty 0 = 0 + 0
c [sweep-7-1] 70144 pos 31.5% + 152759 neg 68.5% = 222903 sched 91.7% ret 20068
c [sweep-7-1] 29018849 steps 746 queries 40187.34 avg class size
c [sweep-7-1] 11390 decisions 706 SAT calls 42.28 avg env size
c [sweep-7-1] 216170 variables remain 89% (26796 retained 11%)
c [decomp-29] removed 585 variables
c [sweep-7-1] removed 585 vars (0 failed, 99 eqs, 109 impls)
c [sweep-7] removed 585 vars in TOTAL (1 rounds, 745 queries)
c [phase-count-11] 1624259 negative 94.7% of 1714438 except 90179 5.3%
c [phase-count-11] 1599794 positive 93.3% of 1714438 except 114644 6.7%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 840 positive 43%, 1116 negative 57%
c [sort-queue-11] sorted 204558 enqueued variables after 45523 conflicts
c [score-dist-11] active 37828 (16%), one 0 (0%), zero 204558 (84%)
c [score-dist-11] max exp 531, different 28 (5%)
c [score-dist-11] median active exp 519, avg 520.0
c [simplification-11] removed 30679 variables 11.2% (242386 remain 16%)
c [simplification-11] removed 170246 irredundant clauses 9.0% (1714438 remain 29%)
c [simplification-11] maximum reduction of 11% = max (11%, 9%)
c [simplification-11] large reduction 11% >= 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 57523 (soft 47523 + delta 10000)
c [simplification-11] new conflict limit 47523 (hard 57523)
c 
c [simplification-12] limit 47523 conflicts (hard 57523) hit after 47523 conflicts
c [quatres-8] found 288288 quaternary clauses 46% in total
c [quatres-8-1] removed 1805 duplicate quaternary clauses
c [quatres-8-1] added 29 double-self-subsuming ternary resolvents
c [quatres-8-2] added 614 single-self-subsuming ternary resolvents
c [quatres-8-2] added 4745 quaternary resolvents
c [ternres-8] limit 100962240 with penalty 0 = 0 + 0
c [ternres-8] all 242386 free variables schedulable
c [ternres-8] 68705 ternary resolvents (3008 bin, 65697 trn)
c [ternres-8] 147 variables remain 0% (242239 retained 100%)
c [gauss-4] limit 10096224 penalty 1 = 1 + 0
c [gauss-4] extracted 20486 xors of average arity 3.0
c [gauss-4] connected 61014 occurrences of 11280 variables (average 5.4)
c [gauss-4] limit 10096224 penalty 1 = 1 + 0
c [decomp-30] removed 578 variables
c [gauss-4] exported 0 unary, 7 binary and 0 ternary equations
c [treelook-5] limit 10096224 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 194250 literals 40%
c [treelook-5] scheduling used 4373254 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 10096224 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 10110795 steps
c [treelook-5] 192965 literals remain 40%
c [treelook-5] 27465 variables remain to probed next time 11%
c [decomp-32] removed 91 variables
c [treelook-5] removed 135 variables, found 8804 hbrs
c [unhide-12] limit 2500000 with penalty 3 = 0 + 3
c [unhide-12-12] 28 units, 330 failed, 81025 tauts, 0 hbrs, 33834 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2482 transitive binary clauses
c [elim-10] 1134 variables 0% will be scheduled this time
c [elim-10] scheduled 1134 variables 0%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] no variable eliminated in round 1 in 184468451 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 69 = 6% variables out of 1134 scheduled
c [elim-10] 69 < 1/100 * 1134 = 11 considered unsuccessful
c [bca-8] limit of 10000000 steps and 3421979 added (scaled 2)
c [bca-8] 424537 out of 482736 literals actually usable 88%
c [bca-8] added 821 blocked clauses in 1344295 steps
c [sweep-8] limit 30288672 penalty 0 = 0 + 0
c [sweep-8-1] 68321 pos 31.8% + 146482 neg 68.2% = 214803 sched 89.0% ret 26564
c [sweep-8-1] 30320984 steps 806 queries 33907.07 avg class size
c [sweep-8-1] 10613 decisions 759 SAT calls 38.23 avg env size
c [sweep-8-1] 208733 variables remain 86% (32625 retained 14%)
c [decomp-33] removed 689 variables
c [sweep-8-1] removed 689 vars (0 failed, 155 eqs, 184 impls)
c [sweep-8] removed 689 vars in TOTAL (1 rounds, 805 queries)
c [phase-count-12] 1611919 negative 94.6% of 1704175 except 92256 5.4%
c [phase-count-12] 1588372 positive 93.2% of 1704175 except 115803 6.8%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 440 positive 44%, 564 negative 56%
c [sort-queue-12] sorted 199501 enqueued variables after 47523 conflicts
c [score-dist-12] active 41177 (17%), one 0 (0%), zero 199501 (83%)
c [score-dist-12] max exp 531, different 28 (5%)
c [score-dist-12] median active exp 519, avg 520.0
c [simplification-12] removed 1708 variables 0.7% (240678 remain 16%)
c [simplification-12] removed 10263 irredundant clauses 0.6% (1704175 remain 28%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-12] new conflict interval 26666
c [simplification-12] penalized conflict interval 26666 = 1 * 26666
c [simplification-12] hard conflict limit 87522 (soft 74189 + delta 13333)
c [simplification-12] new conflict limit 74189 (hard 87522)
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  896.7  240677  1704175     54220   45101 187379 450184   67   107  216  63%    153   37   71   47  151%
c i  908.4  240676  1704175     55305   45697 187383 450187   70   105  216  67%     28   34   75   48  157%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 16576 basic ate = 12628 trn 76% + 3948 lrg 24% in 2 updates
c bcas: 8 count, 19023 added (13955 skipped), 14184653 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 4 bces, 87886 removed, 44725481 resolutions, 117677709 steps
c blkd: 41665 blocking literals 1%, 2143 pure
c bump: 66242 bumped seen, 77103159 lits 1164.0 on average
c card: 4 count, 0 units, 0 am1, 56691395 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 10512 subsumed
c card: 4290 at-most-one constraints found, average size 3.05
c card: 4290 at-most-one constraints used 100%, average size 3.05
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: 3 cces, 22715 eliminated, 18392 ate 81%, 4323 abce 19%
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: 21189021 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 91 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 33 decompositions, 150083 equivalent 10%
c deco: 26422 decision-only clauses 40%, 69% reduction
c decs: 626919 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 10 elims, 862102 eliminated 56%, 11712 pure 1%
c elms: 10 rounds, 1.0 rounds/bve
c elms: 747922 small 87%, 100325 large 12%
c elms: 876900 tried small, 747922 succeeded 85%, 128978 failed 15%
c elms: 354299 subsumed, 482956 strengthened, 2240 blocked
c elms: 36945645 copies, 46691726 resolutions, 15320935 ipos
c elms: 24169300 subchks, 43706119 strchks
c gaus: 4 extractions, 41594 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 8 binary and 0 ternary equations
c gaus: 0 gc, 32124756 steps, 16062378 extr 50%, 16107733 elim 50%
c glue: 81.8 orig avg, 81.8 real avg, 7.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1621040 = 544984 simple 34% + 1067575 trn 66% + 8481 lrg 1%, 39180 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 66242 clauses, 97.4 length
c lrnd: 6451336 lits = 18370102 orig - 11918766 removed 65%
c lrnd: 12118 uips 18%, 44661 flips 67%
c mins: 36797 mins 56%, 1177 bin 2%, 1846 size 3%
c mins: 6757586 poisoned searches, 523090 hits, 8% hit rate
c mins: 12295467 used twice searches, 973596 hits, 8% hit rate
c move: moved 110543, 49577 bin 45%, 60966 trn 55%
c otfs: 444 driving 43%, 594 restarting 57%
c otfs: str 1038, 851 red 82%, 187 irr 18%
c otfs: str 1038, 0 bin 0%, 364 trn 35%, 674 lrg 65%
c otfs: sub 31, 20 red 65%, 11 irr 35%
c otfs: sub 31, 0 bin 0%, 7 trn 23%, 24 lrg 77%
c phas: 12 computed, 1165742 set, 540861 pos (46%), 624881 neg (54%)
c prbs: 4 basic, 848042 probed, 19738 failed, 4643 lifted
c prbs: 5 simple, 2317468 probed, 2730 failed, 15470 eqs
c prbs: 5 treelook, 1876 probed, 100 failed, 0 lifted
c prom: 0 locked 0% out of 267994 tried
c prps: 2258908398 props, 3540 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 8 count, 44219 quat, 11952 self1, 484 self2, 3528 dup
c queu: 12 sorted, 626919 next (19905 steps 0.03)
c queu: 84282250 enq (151269318 steps 1.79), 77103159 deq 91%
c redc: 1315 clauses 16%, 8286 tried 13%, 53 sat 1%
c redc: 2469 lits 4%, 59277 tried 0%, 53 sat 0%
c redc: 225 times jump level reduced, 34.5 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 374154 removed, 251797 red 67%
c rsts: 2823 restarts 69%, 1298 skipped 31%
c rsts: 1298 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: 12 count, 11 confs 92%, 0 vars 0%
c simp: 0 its 0%, 1 bin 8%, 0 trns 0%
c subl: 66242 count (116448 tried 1.8), 30546 sub out of 62422 (48.9%)
c swps: 8 count, 8 rounds, 4345 queries (543.1/round)
c swps: 4091 sat calls, 508 unsat (1.1% success rate)
c swps: 58362 decisions 14.3, 4605 conflicts 1.1
c swps; 46911.3 avg class size, 37.1 avg environment size
c swps: 0 failed, 907 impls, 740 equivs
c swp0: 1445 type 0 queries, 102 unsat (7.1%), 1419 sat (98.2%)
c swp1: 2900 type 1 queries, 1823 unsat (62.9%), 2186 sat (75.4%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 1386564 calls to obtain time
c tops: 287216 fixed 19%, 24 its, 2586.75 confs/it
c trds: 8 transitive reductions, 15991 removed, 78 failed
c trds: 228667 nodes, 373757 edges, 18130799 steps
c trim: 928887 words, 3.5 MB
c trnr: 8 count, 16014 bin, 547866 trn, 344766338 steps
c unhd: 12 count, 12 rounds, 205836014 steps
c unhd: 37097 non-trivial sccs of average size 2.4
c unhd: 4558 units, 4540 bin, 18 trn, 0 lrg
c unhd: 6348 failed, 5510 stamp, 0 lits, 38 bin, 703 trn, 0 lrg
c unhd: 407532 tauts, 9527 bin 2%, 94422 trn 23%, 20921 lrg 5%
c unhd: 407532 tauts, 282662 stamp 69%, 272290 red 67%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 558610 str, 4540 bin 1%, 76968 trn 14%, 477102 lrg 85%, 121395 red 22%
c vars: 240676 remaining 16% and 1299401 removed 84% out of 1540077
c vars: 287216 fixed 19%, 862102 eliminated 56%, 150083 equivalent 10%
c vsts: 14269077786 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 6.3 search visits per propagation, 224377.1 per conflict
c wchs: 1339203880 pushed, 202670394 enlarged, 136 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         106641             0             0       7806319       2491093         20336
c 
c  0 0         50021  47         0   0<        0   0<  5890402  75   1287726  52      3971  20     0.8
c  1 5          1011   1         0   0         0   0    363862   5<   188373   8      1327   7     0.0
c  2 6          2691   3         0   0         0   0    469983   6    255637  10<     1620   8     0.2
c  3 9          3133   3         0   0         0   0    365328   5    229675   9      1448   7     0.3
c  4 14         2189   2         0   0         0   0    229766   3    145408   6      1132   6     0.2
c  5 21         2052   2<        0   0         0   0    178265   2    130513   5      1218   6<    0.3
c  6 30         2354   2         0   0         0   0     62881   1     52725   2      1028   5     0.6
c  7 41         2927   3         0   0         0   0     54082   1     47987   2      2490  12     0.7
c  8 54         1596   1         0   0         0   0     55646   1     44062   2      2048  10     0.5
c  9 69         2384   2         0   0         0   0     44574   1     36638   1      1765   9     0.9
c 10 86        13715  13         0   0         0   0     50027   1     36495   1      1403   7     4.8
c 11 126       22568  21         0   0         0   0     41503   1     35854   1       886   4     6.3
c 
c avg                  4.6           0.0           0.0           0.9           1.9           4.9
c std                  4.9           0.0           0.0           2.0           2.7           3.6
c 
c   71.078   7% elim
c   63.530   6% probe
c   49.625   5% sweep
c   29.066   3% unhide
c   19.401   2% bump
c   16.429   2% block
c   12.174   1% bca
c   10.603   1% cce
c    9.553   1% gauss
c 
c   15.033 < 1% rest (below)
c 
c    8.522   1% quatres
c    4.114   0% ternres
c    1.135   0% transred
c    0.708   0% card
c    0.555   0% decide
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   18.495   2% preprocessing     6%
c  303.309  30% inprocessing     94%
c ==================================
c  321.804  32% simplifying
c  674.107  68% search
c ==================================
c  995.938 100% all
c 
c         62082 conflicts,          62.3 confs/sec
c           922 ternaries,          67.3 confs/ternary
c           557 binaries,          111.5 confs/binary
c            24 iterations,       2586.8 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          2823 restarts,            2.8 rests/sec,     22.0 confs/restart
c        626919 decisions,         629.5 decis/sec,     10.1 decis/conflict
c    2258908398 propagations,  2268121.6 props/sec,   3603.2 props/decision
c 
c 995.9 seconds, 613.4 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
