c launch: /data/cnf/sc2014/app/atco_enc3_opt1_13_48.cnf.bz2
c host: atom05
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/atco_enc3_opt1_13_48.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc3_opt1_13_48.cnf.bz2
c no embedded options
c found 'p cnf 1614656 6435344' header
c read 1614656 variables, 6435344 clauses, 16056542 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 1607603 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0 1607603  6411548         0       0      0     0    0     0  399   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1602887 based on 6411548 irredundant clauses
c [card-1] found 843 at-most-one constraints of average size 3.6
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1602887 for elimination
c [card-1] 843 out of 843 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 120003 variables
c [simpleprobe-1] all 1494653 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 11911610 based on 5955805 irredundant clauses
c [decomp-2] removed 41 variables
c [simpleprobe-1] 1494612 variables remain 100% (0 retained 0%)
c [simpleprobe-1] removed 41 variables, found 702 hbrs, 0 units
c [unhide-1] limit 372229 based on 5955674 irredundant clauses
c [unhide-1-1] 5 units, 161 failed, 4604 tauts, 0 hbrs, 706 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1492884 variables 100%
c [elim-1] limit of 5943756 steps based on 5943756 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 1460040 not tried 98% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 30518 = 2% variables out of 1492884 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 5902833 negative 99.9% of 5909262 except 6429 0.1%
c [phase-count-1] 5864268 positive 99.2% of 5909262 except 44994 0.8%
c [phase-count-1] less non-negative clauses 6429 than limit 590900 (10.0%)
c [phase-count-1] non-pos/non-neg = 44994/6429 = 7.00 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 1462366 negative 100%
c [sort-queue-1] sorted 1462366 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1462366 (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 33998 variables 2.3% (1462366 remain 91%)
c [simplification-1] removed 502286 irredundant clauses 7.8% (5909262 remain 92%)
c [simplification-1] maximum reduction of 8% = max (2%, 8%)
c [simplification-1] large reduction 8% >= 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   35.9 1462365  5909262       933     473    389   526    1    65  416   1%      5   65    3    0 8012%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 134 variables
c [simpleprobe-2] all 1462232 free variables schedulable
c [simpleprobe-2] limit 11817396 based on 5908698 irredundant clauses
c [decomp-4] removed 72 variables
c [simpleprobe-2] 1462160 variables remain 100% (0 retained 0%)
c [simpleprobe-2] removed 72 variables, found 432 hbrs, 0 units
c [treelook-1] limit 1477103 based on 5908412 irredundant clauses
c [treelook-1] scheduled 155877 literals 5%
c [treelook-1] scheduling used 1478998 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1477103 based on 5908412 irredundant clauses
c [treelook-1] used 1477135 steps
c [treelook-1] 154649 literals remain 5%
c [treelook-1] 153864 variables remain to probed next time 11%
c [decomp-5] removed 68 variables
c [treelook-1] removed 74 variables, found 295 hbrs
c [basicprobe-1] limit 47264872 based on 5908109 irredundant clauses
c [basicprobe-1-0] 12217 probes remain 1% after last round
c [basicprobe-1-0] 60 units = 51 failed (85%) + 9 lifted (15%)
c [basicprobe-1-0] removed 1436 variables, found 41716 hbrs
c [unhide-2] limit 369256 based on 5908109 irredundant clauses
c [unhide-2-2] 5 units, 681 failed, 19621 tauts, 0 hbrs, 2990 literals
c [elim-2] 1450689 variables 100% will be scheduled this time
c [elim-2] scheduled 1450689 variables 100%
c [elim-2] limit of 15890371 steps penalty 3 = 0 + 3
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 1385700 not tried 95% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 64808 = 4% variables out of 1450689 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 5834893 negative 99.9% of 5841606 except 6713 0.1%
c [phase-count-2] 5794396 positive 99.2% of 5841606 except 47210 0.8%
c [phase-count-2] less non-negative clauses 6713 than limit 584100 (10.0%)
c [phase-count-2] non-pos/non-neg = 47210/6713 = 7.03 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 74791 negative 100%
c [sort-queue-2] sorted 1388206 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 8752 (1%), zero 1379454 (99%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 74132 variables 5.1% (1388206 remain 86%)
c [simplification-2] removed 67656 irredundant clauses 1.1% (5841606 remain 91%)
c [simplification-2] maximum reduction of 5% = max (5%, 1%)
c [simplification-2] large reduction 5% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
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   83.8 1388205  5841606      2814    1162   1330 16392    1   115  413   1%     16  112    3    0 2335%
c 
c [simplification-3] limit of 136 binary hit after 136 binaries
c [card-2] limit 1460401 based on 5841606 irredundant clauses
c [card-2] found 726 at-most-one constraints of average size 3.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1460401 for elimination
c [card-2] 726 out of 726 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 2692 variables
c [treelook-2] limit 1457520 based on 5830081 irredundant clauses
c [treelook-2] scheduled 262348 literals 9%
c [treelook-2] scheduling used 1761710 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1457520 based on 5830081 irredundant clauses
c [treelook-2] used 1470402 steps
c [treelook-2] 261740 literals remain 9%
c [treelook-2] 31619 variables remain to probed next time 2%
c [decomp-7] removed 8 variables
c [treelook-2] removed 604 variables, found 652 hbrs
c [unhide-3] limit 364168 based on 5826699 irredundant clauses
c [unhide-3-3] 1 units, 64 failed, 27892 tauts, 0 hbrs, 970 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1384102 variables 100%
c [elim-3] limit of 33042567 steps penalty 3 = 0 + 3
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 1241481 not tried 90% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 139917 = 10% variables out of 1384102 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 5764118 negative 99.9% of 5770880 except 6762 0.1%
c [phase-count-3] 5725372 positive 99.2% of 5770880 except 45508 0.8%
c [phase-count-3] less non-negative clauses 6762 than limit 577000 (10.0%)
c [phase-count-3] non-pos/non-neg = 45508/6762 = 6.73 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 45099 negative 100%
c [sort-queue-3] sorted 1244185 enqueued variables after 2815 conflicts
c [score-dist-3] active 0 (0%), one 18327 (1%), zero 1225858 (99%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 141649 variables 10.2% (1244185 remain 77%)
c [simplification-3] removed 70726 irredundant clauses 1.2% (5770880 remain 90%)
c [simplification-3] maximum reduction of 10% = max (10%, 1%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3001 (hard 13001)
c [simplification-3] new binary interval 1000
c 
c [simplification-4] limit 3001 conflicts (hard 13001) hit after 3002 conflicts
c [decomp-8] removed 50 variables
c [basicprobe-2] limit 46166200 based on 5770775 irredundant clauses
c [basicprobe-2-0] 6503 probes remain 1% after last round
c [basicprobe-2-0] 60 units = 60 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1221 variables, found 21359 hbrs
c [unhide-4] limit 360673 based on 5770775 irredundant clauses
c [unhide-4-4] 1 units, 818 failed, 9428 tauts, 0 hbrs, 2621 literals
c [elim-4] 1237447 variables 100% will be scheduled this time
c [elim-4] scheduled 1237447 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 753529832 steps penalty 3 = 0 + 3
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 4216 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 369319 = 30% variables out of 1237447 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 5639019 negative 99.8% of 5648359 except 9340 0.2%
c [phase-count-4] 5604197 positive 99.2% of 5648359 except 44162 0.8%
c [phase-count-4] less non-negative clauses 9340 than limit 564800 (10.0%)
c [phase-count-4] non-pos/non-neg = 44162/9340 = 4.73 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 26967 negative 100%
c [sort-queue-4] sorted 871190 enqueued variables after 3002 conflicts
c [score-dist-4] active 0 (0%), one 13208 (2%), zero 857982 (98%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 372995 variables 30.0% (871190 remain 54%)
c [simplification-4] removed 122521 irredundant clauses 2.1% (5648359 remain 88%)
c [simplification-4] maximum reduction of 30% = max (30%, 2%)
c [simplification-4] large reduction 30% >= 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 15002 (soft 5002 + delta 10000)
c [simplification-4] new conflict limit 5002 (hard 15002)
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  190.6  871189  5648359      3585     859    567 15671    2   171  426   1%     11  167    4    0 2364%
c i  202.1  870883  5648359      4329    1286    730 15748    2   201  426   1%      8  194    3    0 1665%
c 
c [simplification-5] limit 5002 conflicts (hard 15002) hit after 5002 conflicts
c [quatres-1] found 1041617 quaternary clauses 99% in total
c [quatres-1-1] removed 54 duplicate quaternary clauses
c [quatres-1-2] added 56 single-self-subsuming ternary resolvents
c [quatres-1-2] added 137 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 22593292 based on 5648323 irredundant clauses
c [ternres-1] all 870398 free variables schedulable
c [ternres-1] 1969 ternary resolvents (0 bin, 1969 trn)
c [ternres-1] 848428 variables remain 97% (21970 retained 3%)
c [gauss-1] limit 2824161 based on 5648323 irredundant clauses
c [gauss-1] extracted 268 xors of average arity 2.7
c [gauss-1] connected 733 occurrences of 715 variables (average 1.0)
c [gauss-1] limit 2821479 based on 5642959 irredundant clauses
c [gauss-1] fully completed
c [decomp-9] removed 506 variables
c [gauss-1] exported 0 unary, 1 binary and 0 ternary equations
c [decomp-10] removed 13 variables
c [simpleprobe-3] all 869879 free variables schedulable
c [simpleprobe-3] limit 11829959 penalty 3 = 0 + 3
c [decomp-11] removed 19 variables
c [simpleprobe-3] 869860 variables remain 100% (0 retained 0%)
c [simpleprobe-3] removed 19 variables, found 224 hbrs, 0 units
c [unhide-5] limit 352601 based on 5641630 irredundant clauses
c [unhide-5-5] 1 units, 39 failed, 26184 tauts, 0 hbrs, 657 literals
c [transred-1] limit 5614184 based on 5614184 irredundant clauses
c [transred-1] removed 2 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 869279 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 295748976 steps penalty 3 = 0 + 3
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 9392 blocked clauses
c [block-1] 9392 < 1/100 * 5614182 = 56141 considered unsuccessful
c [cce-1] limit of 14787448 steps penalty 3 = 0 + 3
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 33
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-1-1] eliminated 7 clauses out of 324 (2%) of length 16
c [cce-1-1] eliminated 12 clauses out of 432 (3%) of length 15
c [cce-1-1] eliminated 3 clauses out of 107 (3%) of length 14
c [cce-1-1] eliminated 19 clauses out of 123 (15%) of length 13
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 43 large clauses in 14787824 steps
c [cce-1-1] allowing another 7393912 steps for small clauses
c [cce-1-1] scheduling 2863348 clauses = 1805461 binary + 1057887 ternary
c [cce-1-1] tried to eliminate 41 small clauses 0%
c [cce-1-1] eliminated 1 binary clauses 0%
c [cce-1-1] eliminated 1 small clauses 0%
c [cce-1-1] eliminated 1 small clauses in 14787448 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 44 covered clauses in round 1
c [cce-1] eliminated 44 covered clauses in TOTAL during 1 rounds
c [cce-1] 44 < 1/100 * 5601044 = 56010 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 869277 variables 100%
c [elim-5] limit of 59149795 steps penalty 3 = 0 + 3
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 610886 not tried 70% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 5272 = 1% variables out of 869277 scheduled
c [elim-5] 5272 < 1/100 * 869277 = 8692 considered unsuccessful
c [bca-1] limit of 10000000 steps and 11192564 added (scaled 2)
c [bca-1] 1721650 out of 1728012 literals actually usable 100%
c [bca-1] added 19014 blocked clauses in 3526483 steps
c [sweep-1] limit 11192064 based on 5596032 irredundant clauses
c [sweep-1-1] 452629 pos 52.4% + 411376 neg 47.6% = 864005 sched 100.0% ret 0
c [sweep-1-1] 11516888 steps 38 queries 215610.82 avg class size
c [sweep-1-1] 189 decisions 30 SAT calls 30.03 avg env size
c [sweep-1-1] 862742 variables remain 100% (134 retained 0%)
c [decomp-12] removed 1186 variables
c [sweep-1-1] removed 1186 vars (0 failed, 7 eqs, 9 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1186 vars in TOTAL (1 rounds, 37 queries)
c [phase-count-5] 5578753 negative 99.8% of 5588109 except 9356 0.2%
c [phase-count-5] 5546773 positive 99.3% of 5588109 except 41336 0.7%
c [phase-count-5] less non-negative clauses 9356 than limit 558800 (10.0%)
c [phase-count-5] non-pos/non-neg = 41336/9356 = 4.42 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 7071 negative 100%
c [sort-queue-5] sorted 862819 enqueued variables after 5002 conflicts
c [score-dist-5] active 0 (0%), one 24842 (3%), zero 837977 (97%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 7579 variables 0.9% (862819 remain 54%)
c [simplification-5] removed 60250 irredundant clauses 1.1% (5588109 remain 87%)
c [simplification-5] maximum reduction of 1% = max (1%, 1%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 10000
c [simplification-5] penalized conflict interval 10000 = 1 * 10000
c [simplification-5] hard conflict limit 25002 (soft 15002 + delta 10000)
c [simplification-5] new conflict limit 15002 (hard 25002)
c 
c [simplification-6] limit of 2911 ternary hit after 2911 ternaries
c [quatres-2] found 1035541 quaternary clauses 99% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-2] added 44 single-self-subsuming ternary resolvents
c [quatres-2-2] added 51 quaternary resolvents
c [ternres-2] limit 22352364 based on 5588091 irredundant clauses
c [ternres-2] 841026 schedulable variables 97%
c [ternres-2] 2052 ternary resolvents (0 bin, 2052 trn)
c [ternres-2] 820436 variables remain 95% (42383 retained 5%)
c [card-3] limit 1397022 based on 5588091 irredundant clauses
c [card-3] found 724 at-most-one constraints of average size 3.4
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1397022 for elimination
c [card-3] 724 out of 724 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2794045 based on 5588091 irredundant clauses
c [gauss-2] extracted 202 xors of average arity 3.0
c [gauss-2] connected 603 occurrences of 591 variables (average 1.0)
c [gauss-2] limit 2794045 based on 5588091 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 85 variables
c [treelook-3] limit 1396949 based on 5587799 irredundant clauses
c [treelook-3] scheduled 110816 literals 6%
c [treelook-3] scheduling used 1397772 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1396949 based on 5587799 irredundant clauses
c [treelook-3] used 2144101 steps
c [treelook-3] 110704 literals remain 6%
c [treelook-3] 18453 variables remain to probed next time 2%
c [treelook-3] removed 108 variables, found 488 hbrs
c [unhide-6] limit 491377 with penalty 4 = 0 + 4
c [unhide-6-6] 5 units, 443 failed, 1606 tauts, 0 hbrs, 31522 literals
c [transred-2] limit 5583720 based on 5583720 irredundant clauses
c [transred-2] removed 0 transitive binary clauses
c [bca-2] limit of 10000000 steps and 11154481 added (scaled 2)
c [bca-2] 1707965 out of 1721424 literals actually usable 99%
c [bca-2] added 575 blocked clauses in 3483181 steps
c [sweep-2] limit 11144474 based on 5572237 irredundant clauses
c [sweep-2-1] 476332 pos 55.3% + 384250 neg 44.7% = 860582 sched 100.0% ret 129
c [sweep-2-1] 11551488 steps 37 queries 175232.97 avg class size
c [sweep-2-1] 320 decisions 33 SAT calls 62.73 avg env size
c [sweep-2-1] 860456 variables remain 100% (255 retained 0%)
c [decomp-15] removed 56 variables
c [sweep-2-1] removed 56 vars (0 failed, 3 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 56 vars in TOTAL (1 rounds, 36 queries)
c [phase-count-6] 5562580 negative 99.8% of 5572095 except 9515 0.2%
c [phase-count-6] 5530605 positive 99.3% of 5572095 except 41490 0.7%
c [phase-count-6] less non-negative clauses 9515 than limit 557200 (10.0%)
c [phase-count-6] non-pos/non-neg = 41490/9515 = 4.36 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 3205 negative 100%
c [sort-queue-6] sorted 860655 enqueued variables after 9345 conflicts
c [score-dist-6] active 0 (0%), one 42265 (5%), zero 818390 (95%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 2164 variables 0.3% (860655 remain 54%)
c [simplification-6] removed 16014 irredundant clauses 0.3% (5572095 remain 87%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] forced so keeping old conflict interval 10000
c [simplification-6] conflict limit remains at 15002 (hard 25002)
c [simplification-6] new ternary interval 10000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  339.5  860654  5572095      9502    4258   8130 35438    4   260  423   1%     62  238    4    0  891%
c i  389.7  858616  5572095     14943    7891   9272 35894    4   224  423   2%     64  186    5    1  584%
c 
c [simplification-7] limit 15002 conflicts (hard 25002) hit after 15003 conflicts
c [quatres-3] found 996206 quaternary clauses 99% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 16 single-self-subsuming ternary resolvents
c [quatres-3-2] added 17 quaternary resolvents
c [ternres-3] limit 22288360 based on 5572090 irredundant clauses
c [ternres-3] 814459 schedulable variables 95%
c [ternres-3] 3528 ternary resolvents (0 bin, 3528 trn)
c [ternres-3] 794167 variables remain 93% (62374 retained 7%)
c [decomp-16] removed 4168 variables
c [basicprobe-3] limit 44353912 based on 5544239 irredundant clauses
c [basicprobe-3-0] 4381 probes remain 1% after last round
c [basicprobe-3-0] 255 units = 145 failed (57%) + 110 lifted (43%)
c [basicprobe-3-0] removed 1008 variables, found 12123 hbrs
c [bate-1] eliminated 327 asymmetric tautologies during probing
c [unhide-7] limit 692241 with penalty 4 = 0 + 4
c [unhide-7-7] 16 units, 128 failed, 14925 tauts, 0 hbrs, 1014 literals
c [block-2] scheduling all variables this time
c [block-2] scheduled 854233 variables 100%
c [block-2] limit of 34612089 steps penalty 4 = 1 + 3
c [block-2] incomplete 40724 not tried 5%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 251 blocked clauses
c [block-2] 251 < 1/100 * 5523693 = 55236 considered unsuccessful
c [cce-2] limit of 17306044 steps penalty 4 = 1 + 3
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 24
c [cce-2-1] eliminated 2 clauses out of 382 (1%) of length 15
c [cce-2-1] eliminated 4 clauses out of 129 (3%) of length 13
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 7 large clauses in 17306047 steps
c [cce-2-1] allowing another 8653023 steps for small clauses
c [cce-2-1] scheduling 3457089 clauses = 1775518 binary + 1681571 ternary
c [cce-2-1] tried to eliminate 44 small clauses 0%
c [cce-2-1] eliminated 2 binary clauses 0%
c [cce-2-1] eliminated 2 ternary clauses 0%
c [cce-2-1] eliminated 4 small clauses 0%
c [cce-2-1] eliminated 4 small clauses in 17306044 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 11 covered clauses in round 1
c [cce-2] eliminated 11 covered clauses in TOTAL during 1 rounds
c [cce-2] 11 < 1/100 * 5515994 = 55159 considered unsuccessful
c [elim-6] 4160 variables 0% will be scheduled this time
c [elim-6] scheduled 4160 variables 0%
c [elim-6] limit of 50000000 steps penalty 4 = 1 + 3
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 4049 not tried 0% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 4160 scheduled
c [bca-3] limit of 10000000 steps and 11042082 added (scaled 2)
c [bca-3] 1688685 out of 1708416 literals actually usable 99%
c [bca-3] added 11 blocked clauses in 3442791 steps
c [sweep-3] limit 11031788 based on 5515894 irredundant clauses
c [sweep-3-1] 457209 pos 53.5% + 396749 neg 46.5% = 853958 sched 100.0% ret 249
c [sweep-3-1] 11291109 steps 33 queries 194564.82 avg class size
c [sweep-3-1] 275 decisions 26 SAT calls 99.19 avg env size
c [sweep-3-1] 853877 variables remain 100% (330 retained 0%)
c [decomp-17] removed 349 variables
c [sweep-3-1] removed 349 vars (0 failed, 6 eqs, 9 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 349 vars in TOTAL (1 rounds, 32 queries)
c [phase-count-7] 5506262 negative 99.8% of 5515527 except 9265 0.2%
c [phase-count-7] 5474439 positive 99.3% of 5515527 except 41088 0.7%
c [phase-count-7] less non-negative clauses 9265 than limit 551500 (10.0%)
c [phase-count-7] non-pos/non-neg = 41088/9265 = 4.43 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 3178 negative 100%
c [sort-queue-7] sorted 853858 enqueued variables after 15003 conflicts
c [score-dist-7] active 0 (0%), one 56000 (7%), zero 797858 (93%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 2683 variables 0.3% (853858 remain 53%)
c [simplification-7] removed 56568 irredundant clauses 1.0% (5515527 remain 86%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-7] new conflict interval 20000
c [simplification-7] penalized conflict interval 20000 = 1 * 20000
c [simplification-7] hard conflict limit 45003 (soft 35003 + delta 10000)
c [simplification-7] new conflict limit 35003 (hard 45003)
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  485.4  853857  5515527     19759   11233  13690 44319    5   275  423   2%     52  222    5    1  436%
c i  524.3  851661  5515527     22499   13181  14132 44562    5   284  423   2%     23  223    6    1  448%
c i  541.0  850286  5515527     23622   14025  14294 44643    5   291  423   2%      8  226    5    1  370%
c 
c [simplification-8] limit of 2247 binary hit after 2247 binaries
c [quatres-4] found 962654 quaternary clauses 98% in total
c [quatres-4-1] removed 4 duplicate quaternary clauses
c [quatres-4-2] added 18 single-self-subsuming ternary resolvents
c [quatres-4-2] added 20 quaternary resolvents
c [ternres-4] limit 22062044 based on 5515511 irredundant clauses
c [ternres-4] 788359 schedulable variables 92%
c [ternres-4] 6332 ternary resolvents (0 bin, 6332 trn)
c [ternres-4] 771727 variables remain 91% (78528 retained 9%)
c [gauss-3] limit 2757755 based on 5515511 irredundant clauses
c [gauss-3] extracted 212 xors of average arity 2.9
c [gauss-3] connected 614 occurrences of 585 variables (average 1.0)
c [gauss-3] limit 2746166 based on 5492332 irredundant clauses
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 345 variables
c [simpleprobe-4] all 849910 free variables schedulable
c [simpleprobe-4] limit 25000000 penalty 3 = 0 + 3
c [decomp-19] removed 99 variables
c [simpleprobe-4] 837753 variables remain 99% (12058 retained 1%)
c [simpleprobe-4] removed 99 variables, found 473 hbrs, 11 units
c [unhide-8] limit 1250000 with penalty 4 = 0 + 4
c [unhide-8-8] 22 units, 800 failed, 3497 tauts, 0 hbrs, 127257 literals
c [transred-3] limit 5484334 based on 5484334 irredundant clauses
c [transred-3] removed 4 transitive binary clauses
c [bca-4] limit of 10000000 steps and 10933350 added (scaled 2)
c [bca-4] 1663826 out of 1691912 literals actually usable 98%
c [bca-4] added 495 blocked clauses in 3395399 steps
c [sweep-4] limit 10923050 based on 5461525 irredundant clauses
c [sweep-4-1] 468532 pos 55.4% + 377101 neg 44.6% = 845633 sched 100.0% ret 322
c [sweep-4-1] 11022705 steps 45 queries 177847.71 avg class size
c [sweep-4-1] 375 decisions 36 SAT calls 114.56 avg env size
c [sweep-4-1] 844692 variables remain 100% (441 retained 0%)
c [decomp-20] removed 1167 variables
c [sweep-4-1] removed 1167 vars (0 failed, 8 eqs, 11 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 1167 vars in TOTAL (1 rounds, 44 queries)
c [phase-count-8] 5446050 negative 99.8% of 5455531 except 9481 0.2%
c [phase-count-8] 5415946 positive 99.3% of 5455531 except 39585 0.7%
c [phase-count-8] less non-negative clauses 9481 than limit 545500 (10.0%)
c [phase-count-8] non-pos/non-neg = 39585/9481 = 4.18 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 2617 negative 100%
c [sort-queue-8] sorted 844788 enqueued variables after 27473 conflicts
c [score-dist-8] active 0 (0%), one 71384 (8%), zero 773404 (92%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 5467 variables 0.6% (844788 remain 53%)
c [simplification-8] removed 59996 irredundant clauses 1.1% (5455531 remain 85%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] forced so keeping old conflict interval 20000
c [simplification-8] conflict limit remains at 35003 (hard 45003)
c [simplification-8] new binary interval 10000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  654.8  844787  5455531     30778   19334  21420 40305    6   277  420   2%     83  190    6    2  323%
c 
c [simplification-9] limit 35003 conflicts (hard 45003) hit after 35003 conflicts
c [quatres-5] found 805177 quaternary clauses 98% in total
c [quatres-5-1] removed 2 duplicate quaternary clauses
c [quatres-5-2] added 13 single-self-subsuming ternary resolvents
c [quatres-5-2] added 12 quaternary resolvents
c [ternres-5] limit 21821972 based on 5455493 irredundant clauses
c [ternres-5] 766711 schedulable variables 91%
c [ternres-5] 12538 ternary resolvents (0 bin, 12538 trn)
c [ternres-5] 744455 variables remain 88% (100274 retained 12%)
c [decomp-21] removed 183 variables
c [treelook-4] limit 1642570 penalty 3 = 0 + 3 boost 1
c [treelook-4] scheduled 152164 literals 9%
c [treelook-4] scheduling used 1642573 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1642570 penalty 3 = 0 + 3 boost 1
c [treelook-4] used 1806724 steps
c [treelook-4] 151862 literals remain 9%
c [treelook-4] 5577 variables remain to probed next time 1%
c [decomp-22] removed 3 variables
c [treelook-4] removed 286 variables, found 487 hbrs
c [unhide-9] limit 1250000 with penalty 4 = 0 + 4
c [unhide-9-9] 4 units, 149 failed, 11863 tauts, 0 hbrs, 3837 literals
c [transred-4] limit 5441860 based on 5441860 irredundant clauses
c [transred-4] removed 2 transitive binary clauses
c [transred-4] found 1 units
c [bca-5] limit of 10000000 steps and 10877413 added (scaled 2)
c [bca-5] 1653334 out of 1685772 literals actually usable 98%
c [bca-5] added 18 blocked clauses in 3378384 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 49277112 penalty 3 = 0 + 3
c [sweep-5-1] 463928 pos 55.1% + 378529 neg 44.9% = 842457 sched 99.9% ret 428
c [sweep-5-1] 49321267 steps 170 queries 77973.99 avg class size
c [sweep-5-1] 1380 decisions 128 SAT calls 69.38 avg env size
c [sweep-5-1] 840044 variables remain 100% (1022 retained 0%)
c [decomp-23] removed 2201 variables
c [sweep-5-1] removed 2201 vars (0 failed, 44 eqs, 41 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 2201 vars in TOTAL (1 rounds, 169 queries)
c [phase-count-9] 5411267 negative 99.8% of 5420383 except 9116 0.2%
c [phase-count-9] 5381905 positive 99.3% of 5420383 except 38478 0.7%
c [phase-count-9] less non-negative clauses 9116 than limit 542000 (10.0%)
c [phase-count-9] non-pos/non-neg = 38478/9116 = 4.22 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 1031 negative 100%
c [sort-queue-9] sorted 840684 enqueued variables after 35003 conflicts
c [score-dist-9] active 0 (0%), one 78996 (9%), zero 761688 (91%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 4045 variables 0.5% (840684 remain 52%)
c [simplification-9] removed 35148 irredundant clauses 0.6% (5420383 remain 85%)
c [simplification-9] maximum reduction of 1% = max (0%, 1%)
c [simplification-9] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-9] new conflict interval 30000
c [simplification-9] penalized conflict interval 30000 = 1 * 30000
c [simplification-9] hard conflict limit 80003 (soft 65003 + delta 15000)
c [simplification-9] new conflict limit 65003 (hard 80003)
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  752.4  840683  5420383     35840   23218  34450 41095    6   281  420   2%     48  180    7    2  310%
c i  850.6  836744  5420383     43200   29029  35483 41428    7   284  420   2%     79  165    7    3  264%
c i  869.3  835900  5420383     44548   30132  35633 41483    7   284  420   2%     16  161    7    3  256%
c i  956.4  834464  5420383     50632   35183  36245 41734    7   288  420   3%     57  150    6    3  206%
c i  973.8  833492  5420383     51749   36118  36368 41765    7   296  421   2%     11  155    7    3  208%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 327 basic ate = 221 trn 68% + 106 lrg 32% in 1 updates
c bcas: 5 count, 20113 added (1159 skipped), 17226238 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: 2 bces, 9643 removed, 30112982 resolutions, 87838194 steps
c blkd: 8797 blocking literals 0%, 28 pure
c bump: 52414 bumped seen, 2154350 lits 41.1 on average
c card: 3 count, 0 units, 0 am1, 9955740 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 4257 subsumed
c card: 2293 at-most-one constraints found, average size 3.50
c card: 2293 at-most-one constraints used 100%, average size 3.50
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: 2 cces, 55 eliminated, 55 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 22491886 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 54 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 23 decompositions, 4727 equivalent 0%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 3112167 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 609845 eliminated 38%, 206 pure 0%
c elms: 6 rounds, 1.0 rounds/bve
c elms: 605398 small 99%, 4213 large 1%
c elms: 1680470 tried small, 605398 succeeded 36%, 1075072 failed 64%
c elms: 32173 subsumed, 19874 strengthened, 0 blocked
c elms: 33245846 copies, 26818812 resolutions, 88911181 ipos
c elms: 4854054 subchks, 2451345 strchks
c gaus: 3 extractions, 682 extracted, 2.9 size, 3 max
c gaus: exported 0 units, 1 binary and 0 ternary equations
c gaus: 0 gc, 16753016 steps, 8376508 extr 50%, 2824 elim 0%
c glue: 5.7 orig avg, 5.7 real avg, 1.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 82244 = 1831 simple 2% + 80009 trn 97% + 404 lrg 0%, 8649 sub 11%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 52413 clauses, 12.9 length
c lrnd: 677454 lits = 808049 orig - 130595 removed 16%
c lrnd: 27088 uips 52%, 17018 flips 32%
c mins: 39950 mins 76%, 3001 bin 6%, 9463 size 18%
c mins: 1445407 poisoned searches, 197938 hits, 14% hit rate
c mins: 1975010 used twice searches, 139453 hits, 7% hit rate
c move: moved 14966, 1350 bin 9%, 13616 trn 91%
c otfs: 1030 driving 58%, 755 restarting 42%
c otfs: str 1785, 742 red 42%, 1043 irr 58%
c otfs: str 1785, 0 bin 0%, 286 trn 16%, 1499 lrg 84%
c otfs: sub 1, 1 red 100%, 0 irr 0%
c otfs: sub 1, 0 bin 0%, 0 trn 0%, 1 lrg 100%
c phas: 9 computed, 1626325 set, 0 pos (0%), 1626325 neg (100%)
c prbs: 3 basic, 20836 probed, 256 failed, 119 lifted
c prbs: 4 simple, 2147538 probed, 11 failed, 36 eqs
c prbs: 4 treelook, 1272 probed, 18 failed, 0 lifted
c prom: 0 locked 0% out of 8592 tried
c prps: 2733460022 props, 872 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 5 count, 237 quat, 147 self1, 0 self2, 241 dup
c queu: 9 sorted, 3112167 next (137 steps 0.00)
c queu: 12997757 enq (0 steps 0.00), 2154350 deq 17%
c redc: 4954 clauses 21%, 23971 tried 45%, 42 sat 0%
c redc: 7549 lits 4%, 190252 tried 24%, 42 sat 0%
c redc: 561 times jump level reduced, 40.2 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: 17659 removed, 1199 red 7%
c rsts: 5069 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 9 count, 6 confs 67%, 0 vars 0%
c simp: 0 its 0%, 2 bin 22%, 1 trns 11%
c subl: 52413 count (13497 tried 0.3), 903 sub out of 39620 (2.3%)
c swps: 5 count, 5 rounds, 318 queries (63.6/round)
c swps: 253 sat calls, 8 unsat (0.6% success rate)
c swps: 2539 decisions 10.0, 158 conflicts 0.6
c swps; 133195.6 avg class size, 73.3 avg environment size
c swps: 0 failed, 71 impls, 68 equivs
c swp0: 104 type 0 queries, 18 unsat (17.3%), 103 sat (99.0%)
c swp1: 214 type 1 queries, 168 unsat (78.5%), 147 sat (68.7%)
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: 6329324 calls to obtain time
c tops: 168710 fixed 10%, 15 its, 3552.40 confs/it
c trds: 4 transitive reductions, 8 removed, 1 failed
c trds: 2242 nodes, 2245 edges, 22145565 steps
c trim: 9363 words, 0.0 MB
c trnr: 5 count, 0 bin, 26419 trn, 111118034 steps
c unhd: 9 count, 9 rounds, 260556813 steps
c unhd: 153 non-trivial sccs of average size 3.1
c unhd: 60 units, 58 bin, 0 trn, 2 lrg
c unhd: 3283 failed, 3074 stamp, 0 lits, 106 bin, 87 trn, 2 lrg
c unhd: 119620 tauts, 360 bin 0%, 21226 trn 18%, 588 lrg 0%
c unhd: 119620 tauts, 97446 stamp 81%, 45051 red 38%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 171574 str, 58 bin 0%, 8279 trn 5%, 163237 lrg 95%, 15710 red 9%
c vars: 831374 remaining 51% and 783282 removed 49% out of 1614656
c vars: 168710 fixed 10%, 609845 eliminated 38%, 4727 equivalent 0%
c vsts: 20837032374 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 7.6 search visits per propagation, 388023.8 per conflict
c wchs: 1044840955 pushed, 236674836 enlarged, 86 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          39857             0             0       1804036         80882          9690
c 
c  0 0         16965  43         0   0<        0   0<  1508599  84<    51527  64      3508  36     0.5
c  1 5          3558   9<        0   0         0   0     92437   5      6079   8<      754   8<    0.2
c  2 6          9079  23         0   0         0   0    129187   7     14484  18      3549  37     0.7
c  3 9          5806  15         0   0         0   0     44059   2      5466   7      1141  12     0.6
c  4 14         3070   8         0   0         0   0     24274   1      2521   3       589   6     0.4
c  5 21         1027   3         0   0         0   0      4867   0       633   1       126   1     0.2
c  6 30          278   1         0   0         0   0       531   0       137   0        20   0     0.1
c  7 41           58   0         0   0         0   0        63   0        25   0         2   0     0.0
c  8 54           11   0         0   0         0   0        14   0         7   0         0   0     0.0
c  9 69            5   0         0   0         0   0         5   0         3   0         1   0     0.0
c 
c avg                  1.5           0.0           0.0           0.3           0.8           1.5
c std                  1.5           0.0           0.0           0.9           1.2           1.3
c 
c   86.232   9% elim
c   35.211   4% quatres
c   33.470   3% probe
c   23.084   2% unhide
c   22.762   2% sweep
c   11.148   1% bca
c    9.713   1% block
c    8.878   1% gauss
c 
c   13.600 < 1% rest (below)
c 
c    5.591   1% cce
c    2.874   0% decide
c    2.646   0% transred
c    1.375   0% ternres
c    1.011   0% card
c    0.102   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   15.395   2% preprocessing     5%
c  272.381  27% inprocessing     95%
c ==================================
c  287.776  29% simplifying
c  708.273  71% search
c ==================================
c  996.078 100% all
c 
c         53286 conflicts,          53.5 confs/sec
c          9253 ternaries,           5.8 confs/ternary
c          3400 binaries,           15.7 confs/binary
c            15 iterations,       3552.4 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          5069 restarts,            5.1 rests/sec,     10.5 confs/restart
c       3112167 decisions,        3124.4 decis/sec,     58.4 decis/conflict
c    2733460022 propagations,  2744221.9 props/sec,    878.3 props/decision
c 
c 996.1 seconds, 635.9 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
