c launch: /data/cnf/sc2014/app/atco_enc3_opt1_04_50.cnf.bz2
c host: atom24
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/atco_enc3_opt1_04_50.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc3_opt1_04_50.cnf.bz2
c no embedded options
c found 'p cnf 1613160 6429816' header
c read 1613160 variables, 6429816 clauses, 16042866 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 1557441 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 1557441  6170180         0       0      0     0    0     0  412   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1542545 based on 6170180 irredundant clauses
c [card-1] found 873 at-most-one constraints of average size 3.6
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1542545 for elimination
c [card-1] 873 out of 873 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 273550 variables
c [simpleprobe-1] all 1339610 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 10677216 based on 5338608 irredundant clauses
c [decomp-2] removed 194 variables
c [simpleprobe-1] 1086527 variables remain 81% (252889 retained 19%)
c [simpleprobe-1] removed 194 variables, found 475 hbrs, 4 units
c [unhide-1] limit 333623 based on 5337983 irredundant clauses
c [unhide-1-1] 6 units, 288 failed, 4449 tauts, 0 hbrs, 832 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1337940 variables 100%
c [elim-1] limit of 5327219 steps based on 5327219 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 1308348 not tried 98% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 27527 = 2% variables out of 1337940 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 5289572 negative 99.9% of 5295234 except 5662 0.1%
c [phase-count-1] 5256899 positive 99.3% of 5295234 except 38335 0.7%
c [phase-count-1] less non-negative clauses 5662 than limit 529500 (10.0%)
c [phase-count-1] non-pos/non-neg = 38335/5662 = 6.77 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 1310413 negative 100%
c [sort-queue-1] sorted 1310413 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1310413 (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 30822 variables 2.3% (1310413 remain 84%)
c [simplification-1] removed 874946 irredundant clauses 14.2% (5295234 remain 86%)
c [simplification-1] maximum reduction of 14% = max (2%, 14%)
c [simplification-1] large reduction 14% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 120 variables
c [simpleprobe-2] 1062773 schedulable variables 81%
c [simpleprobe-2] limit 10589544 based on 5294772 irredundant clauses
c [decomp-4] removed 95 variables
c [simpleprobe-2] 1062904 variables remain 81% (247294 retained 19%)
c [simpleprobe-2] removed 95 variables, found 438 hbrs, 1 units
c [treelook-1] limit 1323593 based on 5294375 irredundant clauses
c [treelook-1] scheduled 203627 literals 8%
c [treelook-1] scheduling used 1399274 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1323593 based on 5294375 irredundant clauses
c [treelook-1] used 1450128 steps
c [treelook-1] 203491 literals remain 8%
c [treelook-1] 202339 variables remain to probed next time 15%
c [decomp-5] removed 73 variables
c [treelook-1] removed 205 variables, found 686 hbrs
c [basicprobe-1] limit 42346744 based on 5293343 irredundant clauses
c [basicprobe-1-0] 10513 probes remain 1% after last round
c [basicprobe-1-0] 64 units = 39 failed (61%) + 25 lifted (39%)
c [basicprobe-1-0] removed 1156 variables, found 34555 hbrs
c [unhide-2] limit 330833 based on 5293343 irredundant clauses
c [unhide-2-2] 0 units, 1710 failed, 16533 tauts, 0 hbrs, 2724 literals
c [elim-2] 1298160 variables 100% will be scheduled this time
c [elim-2] scheduled 1298160 variables 100%
c [elim-2] limit of 14974750 steps penalty 3 = 0 + 3
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 1236196 not tried 95% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 61720 = 5% variables out of 1298160 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 5215028 negative 99.9% of 5221020 except 5992 0.1%
c [phase-count-2] 5180580 positive 99.2% of 5221020 except 40440 0.8%
c [phase-count-2] less non-negative clauses 5992 than limit 522100 (10.0%)
c [phase-count-2] non-pos/non-neg = 40440/5992 = 6.75 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 129202 negative 100%
c [sort-queue-2] sorted 1227535 enqueued variables after 1000 conflicts
c [score-dist-2] active 10969 (1%), one 0 (0%), zero 1227535 (99%)
c [score-dist-2] max exp 515, different 14 (3%)
c [score-dist-2] median active exp 511, avg 511.1
c [simplification-2] removed 71909 variables 5.5% (1238504 remain 80%)
c [simplification-2] removed 74214 irredundant clauses 1.4% (5221020 remain 85%)
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 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit of 153 binary hit after 153 binaries
c [card-2] limit 1305255 based on 5221020 irredundant clauses
c [card-2] found 632 at-most-one constraints of average size 3.4
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1305255 for elimination
c [card-2] 632 out of 632 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 81 variables
c [treelook-2] limit 1305214 based on 5220859 irredundant clauses
c [treelook-2] scheduled 215417 literals 9%
c [treelook-2] scheduling used 1582543 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1305214 based on 5220859 irredundant clauses
c [treelook-2] used 1342245 steps
c [treelook-2] 214357 literals remain 9%
c [treelook-2] 41475 variables remain to probed next time 3%
c [decomp-7] removed 19 variables
c [treelook-2] removed 1025 variables, found 675 hbrs
c [unhide-3] limit 325976 based on 5215626 irredundant clauses
c [unhide-3-3] 2 units, 46 failed, 26379 tauts, 0 hbrs, 963 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1236752 variables 100%
c [elim-3] limit of 32676123 steps penalty 3 = 0 + 3
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 1099467 not tried 89% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 134412 = 11% variables out of 1236752 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 5136270 negative 99.9% of 5142357 except 6087 0.1%
c [phase-count-3] 5103334 positive 99.2% of 5142357 except 39023 0.8%
c [phase-count-3] less non-negative clauses 6087 than limit 514200 (10.0%)
c [phase-count-3] non-pos/non-neg = 39023/6087 = 6.41 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 108070 negative 100%
c [sort-queue-3] sorted 1081872 enqueued variables after 2468 conflicts
c [score-dist-3] active 20468 (2%), one 0 (0%), zero 1081872 (98%)
c [score-dist-3] max exp 518, different 17 (3%)
c [score-dist-3] median active exp 513, avg 513.0
c [simplification-3] removed 136164 variables 11.0% (1102340 remain 71%)
c [simplification-3] removed 78663 irredundant clauses 1.5% (5142357 remain 83%)
c [simplification-3] maximum reduction of 11% = max (11%, 2%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3000 (hard 13000)
c [simplification-3] new binary interval 1000
c 
c [simplification-4] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [decomp-8] removed 37 variables
c [basicprobe-2] limit 41138224 based on 5142278 irredundant clauses
c [basicprobe-2-0] 5806 probes remain 1% after last round
c [basicprobe-2-0] 64 units = 64 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1104 variables, found 21426 hbrs
c [unhide-4] limit 321392 based on 5142278 irredundant clauses
c [unhide-4-4] 2 units, 1165 failed, 10484 tauts, 0 hbrs, 6215 literals
c [elim-4] 1094937 variables 100% will be scheduled this time
c [elim-4] scheduled 1094937 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 772291372 steps penalty 3 = 0 + 3
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 3472 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 322405 = 29% variables out of 1094937 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 5016976 negative 99.8% of 5025322 except 8346 0.2%
c [phase-count-4] 4987967 positive 99.3% of 5025322 except 37355 0.7%
c [phase-count-4] less non-negative clauses 8346 than limit 502500 (10.0%)
c [phase-count-4] non-pos/non-neg = 37355/8346 = 4.48 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 77039 negative 100%
c [sort-queue-4] sorted 760198 enqueued variables after 3000 conflicts
c [score-dist-4] active 15475 (2%), one 0 (0%), zero 760198 (98%)
c [score-dist-4] max exp 520, different 19 (4%)
c [score-dist-4] median active exp 514, avg 513.7
c [simplification-4] removed 326667 variables 29.6% (775673 remain 50%)
c [simplification-4] removed 117035 irredundant clauses 2.3% (5025322 remain 81%)
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 15000 (soft 5000 + delta 10000)
c [simplification-4] new conflict limit 5000 (hard 15000)
c 
c [simplification-5] limit 5000 conflicts (hard 15000) hit after 5002 conflicts
c [quatres-1] found 915735 quaternary clauses 99% in total
c [quatres-1-1] removed 47 duplicate quaternary clauses
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 49 single-self-subsuming ternary resolvents
c [quatres-1-2] added 135 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20101132 based on 5025283 irredundant clauses
c [ternres-1] all 775673 free variables schedulable
c [ternres-1] 1954 ternary resolvents (0 bin, 1954 trn)
c [ternres-1] 756045 variables remain 97% (19628 retained 3%)
c [gauss-1] limit 2512641 based on 5025283 irredundant clauses
c [gauss-1] extracted 219 xors of average arity 2.7
c [gauss-1] connected 598 occurrences of 580 variables (average 1.0)
c [gauss-1] limit 2512641 based on 5025283 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 496 variables
c [simpleprobe-3] 628628 schedulable variables 81%
c [simpleprobe-3] limit 12398255 penalty 3 = 0 + 3
c [decomp-10] removed 1 variables
c [simpleprobe-3] 628895 variables remain 81% (146281 retained 19%)
c [simpleprobe-3] removed 1 variables, found 515 hbrs, 0 units
c [unhide-5] limit 314011 based on 5024189 irredundant clauses
c [unhide-5-5] 1 units, 200 failed, 26660 tauts, 0 hbrs, 1040 literals
c [transred-1] limit 4996177 based on 4996177 irredundant clauses
c [transred-1] removed 3 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 774754 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 619912760 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 6981 blocked clauses
c [block-1] 6981 < 1/100 * 4996174 = 49961 considered unsuccessful
c [cce-1] limit of 30995638 steps penalty 2 = 0 + 2
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 23
c [cce-1-1] eliminated 5 clauses out of 48 (10%) of length 19
c [cce-1-1] eliminated 3 clauses out of 70 (4%) of length 18
c [cce-1-1] eliminated 3 clauses out of 367 (1%) of length 14
c [cce-1-1] eliminated 5 clauses out of 176 (3%) of length 13
c [cce-1-1] eliminated 4 clauses out of 434 (1%) of length 12
c [cce-1-1] eliminated 3 clauses out of 173 (2%) of length 11
c [cce-1-1] eliminated 37 clauses out of 208 (18%) of length 10
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 62 large clauses in 30995644 steps
c [cce-1-1] allowing another 15497822 steps for small clauses
c [cce-1-1] scheduling 3116668 clauses = 1615617 binary + 1501051 ternary
c [cce-1-1] tried to eliminate 92 small clauses 0%
c [cce-1-1] eliminated 3 binary clauses 0%
c [cce-1-1] eliminated 3 small clauses 0%
c [cce-1-1] eliminated 3 small clauses in 30995640 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 65 covered clauses in round 1
c [cce-1] eliminated 65 covered clauses in TOTAL during 1 rounds
c [cce-1] 65 < 1/100 * 4986549 = 49865 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 774754 variables 100%
c [elim-5] limit of 123982552 steps penalty 2 = 0 + 2
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 315257 not tried 41% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 8254 = 1% variables out of 774754 scheduled
c [bca-1] limit of 10000000 steps and 9959286 added (scaled 2)
c [bca-1] 1529441 out of 1533002 literals actually usable 100%
c [bca-1] added 13976 blocked clauses in 3127212 steps
c [sweep-1] limit 9958786 based on 4979393 irredundant clauses
c [sweep-1-1] 396217 pos 51.7% + 370283 neg 48.3% = 766500 sched 100.0% ret 0
c [sweep-1-1] 10143502 steps 35 queries 170309.40 avg class size
c [sweep-1-1] 346 decisions 26 SAT calls 77.27 avg env size
c [sweep-1-1] 766423 variables remain 100% (77 retained 0%)
c [decomp-11] removed 20 variables
c [sweep-1-1] removed 20 vars (0 failed, 8 eqs, 13 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 20 vars in TOTAL (1 rounds, 34 queries)
c [phase-count-5] 4970892 negative 99.8% of 4979380 except 8488 0.2%
c [phase-count-5] 4944066 positive 99.3% of 4979380 except 35314 0.7%
c [phase-count-5] less non-negative clauses 8488 than limit 497900 (10.0%)
c [phase-count-5] non-pos/non-neg = 35314/8488 = 4.16 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 66211 negative 100%
c [sort-queue-5] sorted 747581 enqueued variables after 5002 conflicts
c [score-dist-5] active 18899 (2%), one 0 (0%), zero 747581 (98%)
c [score-dist-5] max exp 523, different 22 (4%)
c [score-dist-5] median active exp 515, avg 515.2
c [simplification-5] removed 9193 variables 1.2% (766480 remain 49%)
c [simplification-5] removed 45942 irredundant clauses 0.9% (4979380 remain 81%)
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 15002 conflicts (hard 25002) hit after 15003 conflicts
c [quatres-2] found 911356 quaternary clauses 99% in total
c [quatres-2-1] removed 4 duplicate quaternary clauses
c [quatres-2-2] added 68 single-self-subsuming ternary resolvents
c [quatres-2-2] added 393 quaternary resolvents
c [ternres-2] limit 19917492 based on 4979373 irredundant clauses
c [ternres-2] 747085 schedulable variables 97%
c [ternres-2] 2406 ternary resolvents (2 bin, 2404 trn)
c [ternres-2] 728395 variables remain 95% (38085 retained 5%)
c [card-3] limit 2063403 penalty 4 = 2 + 2
c [card-3] found 1029 at-most-one constraints of average size 3.4
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 2063403 for elimination
c [card-3] 1029 out of 1029 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 44 variables
c [treelook-3] limit 1650723 penalty 2 = 0 + 2 boost 1
c [treelook-3] scheduled 139710 literals 9%
c [treelook-3] scheduling used 1655070 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1650723 penalty 2 = 0 + 2 boost 1
c [treelook-3] used 2231913 steps
c [treelook-3] 139563 literals remain 9%
c [treelook-3] 14223 variables remain to probed next time 2%
c [treelook-3] removed 133 variables, found 289 hbrs
c [unhide-6] limit 825361 with penalty 4 = 0 + 4
c [unhide-6-6] 10 units, 700 failed, 1599 tauts, 0 hbrs, 34607 literals
c [transred-2] limit 4976107 based on 4976107 irredundant clauses
c [transred-2] removed 5 transitive binary clauses
c [elim-6] 3415 variables 0% will be scheduled this time
c [elim-6] scheduled 3415 variables 0%
c [elim-6] limit of 200000000 steps penalty 2 = 0 + 2
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 3085 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 3415 scheduled
c [bca-2] limit of 10000000 steps and 9951846 added (scaled 2)
c [bca-2] 1524122 out of 1531424 literals actually usable 100%
c [bca-2] added 528 blocked clauses in 3114466 steps
c [sweep-2] limit 9944358 based on 4972179 irredundant clauses
c [sweep-2-1] 397811 pos 52.0% + 367834 neg 48.0% = 765645 sched 100.0% ret 66
c [sweep-2-1] 10179322 steps 24 queries 196791.33 avg class size
c [sweep-2-1] 229 decisions 21 SAT calls 83.90 avg env size
c [sweep-2-1] 765572 variables remain 100% (139 retained 0%)
c [decomp-14] removed 61 variables
c [sweep-2-1] removed 61 vars (0 failed, 2 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 61 vars in TOTAL (1 rounds, 23 queries)
c [phase-count-6] 4963575 negative 99.8% of 4972080 except 8505 0.2%
c [phase-count-6] 4936890 positive 99.3% of 4972080 except 35190 0.7%
c [phase-count-6] less non-negative clauses 8505 than limit 497200 (10.0%)
c [phase-count-6] non-pos/non-neg = 35190/8505 = 4.14 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 65990 negative 100%
c [sort-queue-6] sorted 741076 enqueued variables after 15003 conflicts
c [score-dist-6] active 24574 (3%), one 0 (0%), zero 741076 (97%)
c [score-dist-6] max exp 527, different 26 (5%)
c [score-dist-6] median active exp 517, avg 517.5
c [simplification-6] removed 830 variables 0.1% (765650 remain 49%)
c [simplification-6] removed 7300 irredundant clauses 0.1% (4972080 remain 81%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 20000
c [simplification-6] new conflict interval 30000
c [simplification-6] penalized conflict interval 30000 = 1 * 30000
c [simplification-6] hard conflict limit 60003 (soft 45003 + delta 15000)
c [simplification-6] new conflict limit 45003 (hard 60003)
c 
c [simplification-7] limit 45003 conflicts (hard 60003) hit after 45004 conflicts
c [quatres-3] found 881065 quaternary clauses 99% in total
c [quatres-3-1] removed 3 duplicate quaternary clauses
c [quatres-3-2] added 12 single-self-subsuming ternary resolvents
c [quatres-3-2] added 19 quaternary resolvents
c [ternres-3] limit 50000000 with penalty 2 = 0 + 2
c [ternres-3] 727603 schedulable variables 95%
c [ternres-3] 7105 ternary resolvents (1 bin, 7104 trn)
c [ternres-3] 678947 variables remain 89% (86703 retained 11%)
c [gauss-2] limit 5151506 penalty 3 = 1 + 2
c [gauss-2] extracted 320 xors of average arity 3.0
c [gauss-2] connected 955 occurrences of 889 variables (average 1.1)
c [gauss-2] limit 5151506 penalty 3 = 1 + 2
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 23 variables
c [basicprobe-3] limit 100000000 penalty 2 = 0 + 2
c [basicprobe-3-0] 654 probes remain 0% after last round
c [basicprobe-3-0] 216 units = 216 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 2415 variables, found 19644 hbrs
c [bate-1] eliminated 688 asymmetric tautologies during probing
c [unhide-7] limit 1250000 with penalty 4 = 0 + 4
c [unhide-7-7] 30 units, 154 failed, 16971 tauts, 0 hbrs, 26027 literals
c [transred-3] limit 4939313 based on 4939313 irredundant clauses
c [transred-3] removed 6 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 761646 variables 100%
c [block-2] limit of 100000000 steps penalty 3 = 1 + 2
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 271 blocked clauses
c [block-2] 271 < 1/100 * 4939308 = 49393 considered unsuccessful
c [cce-2] limit of 128787655 steps penalty 3 = 1 + 2
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 36
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 30
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 25
c [cce-2-1] eliminated 1 clauses out of 507 (0%) of length 12
c [cce-2-1] eliminated 2 clauses out of 198 (1%) of length 11
c [cce-2-1] eliminated 587 clauses out of 2788 (21%) of length 9
c [cce-2-1] eliminated 58 clauses out of 143 (41%) of length 8
c [cce-2-1] eliminated 119 clauses out of 1425 (8%) of length 7
c [cce-2-1] eliminated 135 clauses out of 495 (27%) of length 6
c [cce-2-1] eliminated 3 clauses out of 3519 (0%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 908 large clauses in 128787664 steps
c [cce-2-1] allowing another 64393832 steps for small clauses
c [cce-2-1] scheduling 2544213 clauses = 1592560 binary + 951653 ternary
c [cce-2-1] tried to eliminate 512 small clauses 0%
c [cce-2-1] eliminated 40 binary clauses 0%
c [cce-2-1] eliminated 46 ternary clauses 0%
c [cce-2-1] eliminated 86 small clauses 0%
c [cce-2-1] eliminated 86 small clauses in 128787657 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 994 covered clauses in round 1
c [cce-2] eliminated 994 covered clauses in TOTAL during 1 rounds
c [cce-2] 994 < 1/100 * 4929645 = 49296 considered unsuccessful
c [bca-3] limit of 10000000 steps and 9865054 added (scaled 2)
c [bca-3] 1513959 out of 1523236 literals actually usable 99%
c [bca-3] added 209 blocked clauses in 3099418 steps
c [sweep-3] limit 15454518 penalty 2 = 0 + 2
c [sweep-3-1] 395205 pos 51.9% + 366281 neg 48.1% = 761486 sched 100.0% ret 131
c [sweep-3-1] 15581734 steps 51 queries 128981.12 avg class size
c [sweep-3-1] 474 decisions 44 SAT calls 71.27 avg env size
c [sweep-3-1] 761288 variables remain 100% (329 retained 0%)
c [decomp-16] removed 456 variables
c [sweep-3-1] removed 456 vars (0 failed, 7 eqs, 6 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 456 vars in TOTAL (1 rounds, 50 queries)
c [phase-count-7] 4920395 negative 99.8% of 4928317 except 7922 0.2%
c [phase-count-7] 4893465 positive 99.3% of 4928317 except 34852 0.7%
c [phase-count-7] less non-negative clauses 7922 than limit 492800 (10.0%)
c [phase-count-7] non-pos/non-neg = 34852/7922 = 4.40 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 61456 negative 100%
c [sort-queue-7] sorted 732847 enqueued variables after 45004 conflicts
c [score-dist-7] active 28314 (4%), one 0 (0%), zero 732847 (96%)
c [score-dist-7] max exp 531, different 30 (6%)
c [score-dist-7] median active exp 519, avg 519.5
c [simplification-7] removed 4489 variables 0.6% (761161 remain 49%)
c [simplification-7] removed 43763 irredundant clauses 0.9% (4928317 remain 80%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-7] new conflict interval 45000
c [simplification-7] penalized conflict interval 45000 = 1 * 45000
c [simplification-7] hard conflict limit 112504 (soft 90004 + delta 22500)
c [simplification-7] new conflict limit 90004 (hard 112504)
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 688 basic ate = 577 trn 84% + 111 lrg 16% in 1 updates
c bcas: 3 count, 14713 added (1153 skipped), 9341096 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, 7252 removed, 31679027 resolutions, 92797708 steps
c blkd: 6606 blocking literals 0%, 29 pure
c bump: 52602 bumped seen, 22937511 lits 436.1 on average
c card: 3 count, 0 units, 0 am1, 10441434 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 5172 subsumed
c card: 2534 at-most-one constraints found, average size 3.50
c card: 2534 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, 1059 eliminated, 1059 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: 22472682 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 39 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 16 decompositions, 3306 equivalent 0%
c deco: 22487 decision-only clauses 43%, 69% reduction
c decs: 969496 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 554334 eliminated 34%, 218 pure 0%
c elms: 6 rounds, 1.0 rounds/bve
c elms: 550653 small 99%, 3434 large 1%
c elms: 1727095 tried small, 550653 succeeded 32%, 1176442 failed 68%
c elms: 37010 subsumed, 17999 strengthened, 0 blocked
c elms: 35575689 copies, 28268448 resolutions, 94013268 ipos
c elms: 8471614 subchks, 3083398 strchks
c gaus: 2 extractions, 539 extracted, 2.9 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 15330076 steps, 7665038 extr 50%, 2630 elim 0%
c glue: 72.0 orig avg, 72.0 real avg, 7.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 79562 = 1428 simple 2% + 77957 trn 98% + 177 lrg 0%, 8515 sub 11%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 52602 clauses, 95.9 length
c lrnd: 5044356 lits = 12484975 orig - 7440619 removed 60%
c lrnd: 20776 uips 39%, 23255 flips 44%
c mins: 28085 mins 53%, 781 bin 1%, 1249 size 2%
c mins: 6181910 poisoned searches, 747862 hits, 12% hit rate
c mins: 8741854 used twice searches, 704188 hits, 8% hit rate
c move: moved 11682, 987 bin 8%, 10695 trn 92%
c otfs: 616 driving 70%, 269 restarting 30%
c otfs: str 885, 489 red 55%, 396 irr 45%
c otfs: str 885, 0 bin 0%, 35 trn 4%, 850 lrg 96%
c otfs: sub 6, 6 red 100%, 0 irr 0%
c otfs: sub 6, 0 bin 0%, 0 trn 0%, 6 lrg 100%
c phas: 7 computed, 1818381 set, 0 pos (0%), 1818381 neg (100%)
c prbs: 3 basic, 23692 probed, 319 failed, 25 lifted
c prbs: 3 simple, 917352 probed, 5 failed, 156 eqs
c prbs: 3 treelook, 65 probed, 13 failed, 0 lifted
c prom: 0 locked 0% out of 45404 tried
c prps: 2778341787 props, 2845 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 3 count, 547 quat, 129 self1, 1 self2, 159 dup
c queu: 7 sorted, 969496 next (78015 steps 0.08)
c queu: 31152193 enq (52806131 steps 1.70), 22937511 deq 74%
c redc: 848 clauses 22%, 3887 tried 7%, 9 sat 0%
c redc: 1186 lits 3%, 41090 tried 0%, 9 sat 0%
c redc: 155 times jump level reduced, 60.9 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: 19036 removed, 1529 red 8%
c rsts: 4457 restarts 95%, 212 skipped 5%
c rsts: 212 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: 7 count, 6 confs 86%, 0 vars 0%
c simp: 0 its 0%, 1 bin 14%, 0 trns 0%
c subl: 52602 count (87819 tried 1.7), 22527 sub out of 50291 (44.8%)
c swps: 3 count, 3 rounds, 107 queries (35.7/round)
c swps: 91 sat calls, 1 unsat (0.8% success rate)
c swps: 1049 decisions 11.5, 76 conflicts 0.8
c swps; 161325.8 avg class size, 75.9 avg environment size
c swps: 0 failed, 20 impls, 17 equivs
c swp0: 34 type 0 queries, 2 unsat (5.9%), 33 sat (97.1%)
c swp1: 73 type 1 queries, 53 unsat (72.6%), 57 sat (78.1%)
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: 2044310 calls to obtain time
c tops: 294359 fixed 18%, 0 its, 0.00 confs/it
c trds: 3 transitive reductions, 14 removed, 0 failed
c trds: 1419 nodes, 1460 edges, 14932684 steps
c trim: 281868 words, 1.1 MB
c trnr: 3 count, 3 bin, 11462 trn, 90018627 steps
c unhd: 7 count, 7 rounds, 184857593 steps
c unhd: 94 non-trivial sccs of average size 3.4
c unhd: 51 units, 49 bin, 1 trn, 1 lrg
c unhd: 4263 failed, 4107 stamp, 0 lits, 75 bin, 73 trn, 1 lrg
c unhd: 103075 tauts, 239 bin 0%, 15571 trn 15%, 523 lrg 1%
c unhd: 103075 tauts, 86742 stamp 84%, 36603 red 36%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 72408 str, 49 bin 0%, 4268 trn 6%, 68091 lrg 94%, 36323 red 50%
c vars: 761161 remaining 47% and 851999 removed 53% out of 1613160
c vars: 294359 fixed 18%, 554334 eliminated 34%, 3306 equivalent 0%
c vsts: 23603020131 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 8.5 search visits per propagation, 440968.3 per conflict
c wchs: 671065702 pushed, 160154465 enlarged, 62 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          50838             0             0       2982836        731025         16762
c 
c  0 0          2877   6         0   0<        0   0<  1438835  48    207142  28      3188  19     0.1
c  1 5           883   2         0   0         0   0    337594  11     72171  10      1356   8     0.0
c  2 6          1872   4         0   0         0   0    429275  14<   119290  16      1845  11     0.1
c  3 9          2305   5         0   0         0   0    250500   8     73254  10<     1805  11     0.2
c  4 14         2597   5         0   0         0   0    164993   6     70841  10      1114   7     0.4
c  5 21         6138  12         0   0         0   0     76831   3     39412   5      1241   7<    1.1
c  6 30         3290   6         0   0         0   0     98312   3     43689   6       624   4     0.7
c  7 41         1210   2<        0   0         0   0     46594   2     22461   3       541   3     0.5
c  8 54         1996   4         0   0         0   0     32874   1     19064   3       926   6     1.1
c  9 69         1484   3         0   0         0   0     17563   1     10192   1       580   3     0.9
c 10 86        18188  36         0   0         0   0     74943   3     46326   6      3193  19     8.6
c 11 126        7998  16         0   0         0   0     14522   0      7183   1       349   2     2.0
c 
c avg                  7.5           0.0           0.0           1.8           3.0           4.6
c std                  3.4           0.0           0.0           2.5           3.1           3.8
c 
c   90.438   9% elim
c   25.422   3% probe
c   19.296   2% quatres
c   17.448   2% unhide
c    9.501   1% cce
c    9.390   1% block
c    8.726   1% sweep
c    6.300   1% bca
c 
c   13.690 < 1% rest (below)
c 
c    6.174   1% bump
c    3.080   0% gauss
c    1.754   0% transred
c    1.041   0% card
c    0.992   0% ternres
c    0.649   0% decide
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   14.103   1% preprocessing     6%
c  209.682  21% inprocessing     94%
c ==================================
c  223.785  22% simplifying
c  772.229  78% search
c ==================================
c  996.043 100% all
c 
c         53142 conflicts,          53.4 confs/sec
c          1440 ternaries,          36.9 confs/ternary
c           806 binaries,           65.9 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          4457 restarts,            4.5 rests/sec,     11.9 confs/restart
c        969496 decisions,         973.3 decis/sec,     18.2 decis/conflict
c    2778341787 propagations,  2789379.3 props/sec,   2865.8 props/decision
c 
c 996.0 seconds, 579.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
