c launch: /data/cnf/sc2014/app/E02F22.cnf.bz2
c host: atom03
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/E02F22.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/E02F22.cnf.bz2
c no embedded options
c found 'p cnf 13574 1301188' header
c read 13574 variables, 1301188 clauses, 11462079 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=0
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 13541 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] STATIC (--score=0)
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   13541  1300429         0       0      0     0    0     0  113   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 34 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 34 out of 34 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1120 variables
c [simpleprobe-1] all 12454 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 11598 variables remain 93% (856 retained 7%)
c [simpleprobe-1] removed 0 variables, found 1436 hbrs, 0 units
c [unhide-1] limit 81049 based on 1296798 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 5292 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 12454 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 1006 variables 8% in round 1 in 4451915 steps
c [elim-1-1] backward subsumption/strengthening limit 4451900
c [elim-1-1-1] backward checking 11401 touched variables 92%
c [elim-1-1-1] incomplete backward checking 11376 remain 100%
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 4484004 steps
c [elim-1-1] fully rescheduled 11448 variables 92%
c [elim-1-2] no variable eliminated in round 2 in 1425584 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 1006 = 8% variables out of 12454 scheduled
c [phase-count-1] 1235836 negative 95.8% of 1289517 except 53681 4.2%
c [phase-count-1] 105649 positive 8.2% of 1289517 except 1183868 91.8%
c [phase-count-1] less non-negative clauses 53681 than limit 128900 (10.0%)
c [phase-count-1] non-pos/non-neg = 1183868/53681 = 22.05 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 11448 negative 100%
c [sort-queue-1] sorted 11448 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 11448 (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 1094 variables 8.7% (11448 remain 85%)
c [simplification-1] removed 10912 irredundant clauses 0.8% (1289517 remain 99%)
c [simplification-1] maximum reduction of 9% = max (9%, 1%)
c [simplification-1] large reduction 9% >= 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 3 variables
c [treelook-1] limit 322377 based on 1289511 irredundant clauses
c [treelook-1] scheduled 4091 literals 18%
c [treelook-1] scheduling used 324202 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 322377 based on 1289511 irredundant clauses
c [treelook-1] used 340663 steps
c [treelook-1] 4065 literals remain 18%
c [treelook-1] 3986 variables remain to probed next time 35%
c [treelook-1] removed 2 variables, found 6 hbrs
c [basicprobe-1] limit 10315720 based on 1289465 irredundant clauses
c [basicprobe-1-0] 8378 probes remain 73% after last round
c [basicprobe-1-0] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 4 variables, found 4767 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 11439 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 2538 blocked clauses
c [block-1] 2538 < 1/100 * 1289465 = 12894 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 76
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 75
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 73
c [cce-1-1] eliminated 13 clauses out of 18 (72%) of length 66
c [cce-1-1] eliminated 61 clauses out of 66 (92%) of length 65
c [cce-1-1] eliminated 55 clauses out of 55 (100%) of length 64
c [cce-1-1] eliminated 23 clauses out of 35 (66%) of length 63
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 167 large clauses in 30002883 steps
c [cce-1-1] allowing another 15001441 steps for small clauses
c [cce-1-1] scheduling 39547 clauses = 29756 binary + 9791 ternary
c [cce-1-1] tried to eliminate 733 small clauses 2%
c [cce-1-1] eliminated 45 ternary clauses 0%
c [cce-1-1] eliminated 45 small clauses 0%
c [cce-1-1] eliminated 45 small clauses in 30023176 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 212 covered clauses in round 1
c [cce-1] eliminated 212 covered clauses in TOTAL during 1 rounds
c [cce-1] 212 < 1/100 * 1286919 = 12869 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 11439 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 2 variables 0% in round 1 in 1754619 steps
c [elim-2-1] backward subsumption/strengthening limit 1754600
c [elim-2-1-1] backward checking 52 touched variables 0%
c [elim-2-1-1] incomplete backward checking 32 remain 62%
c [elim-2-1] subsumed 0 and strengthened 0 clauses in 1774987 steps
c [elim-2-1] fully rescheduled 11437 variables 100%
c [elim-2-2] no variable eliminated in round 2 in 1575410 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 2 = 0% variables out of 11439 scheduled
c [elim-2] 2 < 1/100 * 11439 = 114 considered unsuccessful
c [bca-1] limit of 10000000 steps and 2573552 added (scaled 2)
c [bca-1] 14539 out of 22876 literals actually usable 64%
c [bca-1] added 0 blocked clauses in 33591 steps
c [sweep-1] limit 2573052 based on 1286526 irredundant clauses
c [sweep-1-1] 317 pos 2.8% + 11120 neg 97.2% = 11437 sched 100.0% ret 0
c [sweep-1-1] 2676503 steps 139 queries 592.41 avg class size
c [sweep-1-1] 2124 decisions 138 SAT calls 36.03 avg env size
c [sweep-1-1] 4364 variables remain 38% (7073 retained 62%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 138 queries)
c [sort-queue-2] sorted 11437 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 11437 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 11 variables 0.1% (11437 remain 84%)
c [simplification-2] removed 2991 irredundant clauses 0.2% (1286526 remain 99%)
c [simplification-2] maximum reduction of 0% = max (0%, 0%)
c [simplification-2] full geometric conflict interval increment 20000
c [simplification-2] new conflict interval 20000
c [simplification-2] penalized conflict interval 20000 = 1 * 20000
c [simplification-2] hard conflict limit 31000 (soft 21000 + delta 10000)
c [simplification-2] new conflict limit 21000 (hard 31000)
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.9   11436  1286526      1271    1187   2647  6392    5   191  105   3%      8  189   18    0 4619%
c i   19.4   11435  1286526      1648    1515   2666  6400    7   220  106   3%      7  217   18    0 3608%
c i   20.3   11434  1286526      2424    2211   2712  6405    9   319  106   3%      7  312   23    1 3099%
c i   22.2   11433  1286526      4011    3670   2794  6420   13   453  106   3%     13  437   23    1 1918%
c 
c [simplification-3] limit of 118 binary hit after 119 binaries
c [quatres-1] found 20947 quaternary clauses 2% in total
c [quatres-1-2] added 3 single-self-subsuming ternary resolvents
c [quatres-1-2] added 16 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 11433 free variables schedulable
c [ternres-1] 8567 ternary resolvents (0 bin, 8567 trn)
c [ternres-1] 673 variables remain 6% (10760 retained 94%)
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 72 at-most-one constraints of average size 3.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 72 out of 72 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 2 xors of average arity 2.0
c [gauss-1] connected 4 occurrences of 2 variables (average 2.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-6] removed 1 variables
c [simpleprobe-2] 10650 schedulable variables 93%
c [simpleprobe-2] limit 4191676 penalty 1 = 1 + 0
c [decomp-7] removed 2 variables
c [simpleprobe-2] 9480 variables remain 83% (1950 retained 17%)
c [simpleprobe-2] removed 2 variables, found 92 hbrs, 2 units
c [unhide-2] limit 80406 based on 1286510 irredundant clauses
c [unhide-2-2] 0 units, 3 failed, 118 tauts, 0 hbrs, 58505 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 55 transitive binary clauses
c [sweep-2] limit 2572980 based on 1286490 irredundant clauses
c [sweep-2-1] 151 pos 3.5% + 4211 neg 96.5% = 4362 sched 38.2% ret 7066
c [sweep-2-1] 2579804 steps 113 queries 179.77 avg class size
c [sweep-2-1] 3032 decisions 111 SAT calls 83.71 avg env size
c [sweep-2-1] 1423 variables remain 12% (10005 retained 88%)
c [decomp-8] removed 1 variables
c [sweep-2-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 1 vars in TOTAL (1 rounds, 112 queries)
c [sort-queue-3] sorted 11427 enqueued variables after 12306 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 11427 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 6 variables 0.1% (11427 remain 84%)
c [simplification-3] removed 37 irredundant clauses 0.0% (1286489 remain 99%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] forced so keeping old conflict interval 20000
c [simplification-3] conflict limit remains at 21000 (hard 31000)
c [simplification-3] 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   40.6   11426  1286489     14654   13548  11822  6952   20   613  110   3%    139  513   19    4  453%
c i   47.0   11425  1286489     19754   18307  12025  7007   19   632  112   3%     50  493   20    5  385%
c 
c [simplification-4] limit 21000 conflicts (hard 31000) hit after 21000 conflicts
c [quatres-2] found 22747 quaternary clauses 2% in total
c [quatres-2-2] added 3 single-self-subsuming ternary resolvents
c [quatres-2-2] added 15 quaternary resolvents
c [ternres-2] limit 5142824 based on 1285706 irredundant clauses
c [ternres-2] 673 schedulable variables 6%
c [ternres-2] 2146 ternary resolvents (0 bin, 2146 trn)
c [ternres-2] 602 variables remain 5% (10823 retained 95%)
c [decomp-9] removed 2 variables
c [treelook-2] limit 355959 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 5272 literals 23%
c [treelook-2] scheduling used 366604 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 355959 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 430214 steps
c [treelook-2] 5266 literals remain 23%
c [treelook-2] 2258 variables remain to probed next time 20%
c [treelook-2] removed 0 variables, found 6 hbrs
c [unhide-3] limit 88989 with penalty 3 = 0 + 3
c [unhide-3-3] 1 units, 0 failed, 1507 tauts, 0 hbrs, 28033 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 44 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 11424 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] incomplete 164 not tried 1%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 4 blocked clauses
c [block-2] 4 < 1/100 * 1284685 = 12846 considered unsuccessful
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 12 clauses out of 12 (100%) of length 63
c [cce-2-1] eliminated 20 clauses out of 20 (100%) of length 62
c [cce-2-1] eliminated 14 clauses out of 60 (23%) of length 61
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 46 large clauses in 15007744 steps
c [cce-2-1] allowing another 7503872 steps for small clauses
c [cce-2-1] scheduling 39515 clauses = 29725 binary + 9790 ternary
c [cce-2-1] tried to eliminate 353 small clauses 1%
c [cce-2-1] eliminated 2 ternary clauses 0%
c [cce-2-1] eliminated 2 small clauses 0%
c [cce-2-1] eliminated 2 small clauses in 15024583 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 48 covered clauses in round 1
c [cce-2] eliminated 48 covered clauses in TOTAL during 1 rounds
c [cce-2] 48 < 1/100 * 1284679 = 12846 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 11422 variables 100%
c [elim-3] limit of 35595942 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 34 variables 0% in round 1 in 6410781 steps
c [elim-3-1] backward subsumption/strengthening limit 6410700
c [elim-3-1-1] backward checking 808 touched variables 7%
c [elim-3-1-1] incomplete backward checking 807 remain 100%
c [elim-3-1] subsumed 42 and strengthened 0 clauses in 6411933 steps
c [elim-3-1] rescheduled 12 variables 0% by backward subsumption
c [elim-3-2] no variable eliminated in round 2 in 0 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 34 = 0% variables out of 11422 scheduled
c [elim-3] 34 < 1/100 * 11422 = 114 considered unsuccessful
c [bca-2] limit of 10000000 steps and 2568128 added (scaled 2)
c [bca-2] 8808 out of 22778 literals actually usable 39%
c [bca-2] added 0 blocked clauses in 33418 steps
c [sweep-3] limit 2567628 based on 1283814 irredundant clauses
c [sweep-3-1] 54 pos 3.8% + 1369 neg 96.2% = 1423 sched 12.5% ret 9965
c [sweep-3-1] 2640202 steps 58 queries 89.36 avg class size
c [sweep-3-1] 2696 decisions 57 SAT calls 154.60 avg env size
c [sweep-3-1] 779 variables remain 7% (10609 retained 93%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 57 queries)
c [sort-queue-4] sorted 11388 enqueued variables after 21000 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 11388 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 37 variables 0.3% (11388 remain 84%)
c [simplification-4] removed 2675 irredundant clauses 0.2% (1283814 remain 99%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 40000
c [simplification-4] penalized conflict interval 40000 = 1 * 40000
c [simplification-4] hard conflict limit 81000 (soft 61000 + delta 20000)
c [simplification-4] new conflict limit 61000 (hard 81000)
c 
c [simplification-5] limit of 1972 ternary hit after 1972 ternaries
c [quatres-3] found 22555 quaternary clauses 2% in total
c [quatres-3-2] added 4 single-self-subsuming ternary resolvents
c [quatres-3-2] added 31 quaternary resolvents
c [ternres-3] limit 9458842 with penalty 0 = 0 + 0
c [ternres-3] 602 schedulable variables 5%
c [ternres-3] 3185 ternary resolvents (0 bin, 3185 trn)
c [ternres-3] 492 variables remain 4% (10896 retained 96%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 2 xors of average arity 2.0
c [gauss-2] connected 4 occurrences of 4 variables (average 1.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 4 variables
c [basicprobe-2] limit 47294210 penalty 0 = 0 + 0
c [basicprobe-2-0] 1057 probes remain 9% after last round
c [basicprobe-2-0] 12 units = 12 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 16 variables, found 19267 hbrs
c [unhide-4] limit 236471 with penalty 3 = 0 + 3
c [unhide-4-4] 0 units, 0 failed, 504 tauts, 0 hbrs, 67403 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 146 transitive binary clauses
c [sweep-4] limit 2837652 penalty 0 = 0 + 0
c [sweep-4-1] 32 pos 4.1% + 743 neg 95.9% = 775 sched 6.8% ret 10593
c [sweep-4-1] 2887159 steps 49 queries 43.35 avg class size
c [sweep-4-1] 3238 decisions 48 SAT calls 274.62 avg env size
c [sweep-4-1] 316 variables remain 3% (11052 retained 97%)
c [decomp-13] removed 2 variables
c [sweep-4-1] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 2 vars in TOTAL (1 rounds, 48 queries)
c [sort-queue-5] sorted 11366 enqueued variables after 52495 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 11366 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 22 variables 0.2% (11366 remain 84%)
c [simplification-5] removed 583 irredundant clauses 0.0% (1283231 remain 99%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] forced so keeping old conflict interval 40000
c [simplification-5] conflict limit remains at 61000 (hard 81000)
c [simplification-5] new ternary interval 10000
c 
c [simplification-6] limit 61000 conflicts (hard 81000) hit after 61002 conflicts
c [quatres-4] found 23174 quaternary clauses 2% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [quatres-4-2] added 21 quaternary resolvents
c [ternres-4] limit 11134470 with penalty 0 = 0 + 0
c [ternres-4] 492 schedulable variables 4%
c [ternres-4] 7447 ternary resolvents (0 bin, 7447 trn)
c [ternres-4] 409 variables remain 4% (10957 retained 96%)
c [card-3] limit 1391808 penalty 2 = 2 + 0
c [card-3] found 13 at-most-one constraints of average size 3.8
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1391808 for elimination
c [card-3] 13 out of 13 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 9431 schedulable variables 83%
c [simpleprobe-3] limit 44537883 penalty 0 = 0 + 0
c [simpleprobe-3] 8440 variables remain 74% (2926 retained 26%)
c [simpleprobe-3] removed 0 variables, found 303 hbrs, 0 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 91 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 33403410 penalty 0 = 0 + 0
c [sweep-5-1] 5 pos 1.6% + 309 neg 98.4% = 314 sched 2.8% ret 11052
c [sweep-5-1] 8653327 steps 106 queries 10.18 avg class size
c [sweep-5-1] 7144 decisions 105 SAT calls 310.96 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 388 pos 3.4% + 10978 neg 96.6% = 11366 sched 100.0% ret 0
c [sweep-5-2] 16068597 steps 292 queries 117.58 avg class size
c [sweep-5-2] 15652 decisions 290 SAT calls 260.67 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-17] removed 1 variables
c [sweep-5-2] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-5-3] 388 pos 3.4% + 10977 neg 96.6% = 11365 sched 100.0% ret 0
c [sweep-5-3] 8842448 steps 187 queries 129.18 avg class size
c [sweep-5-3] 9701 decisions 186 SAT calls 217.04 avg env size
c [sweep-5-3] 350 variables remain 3% (11015 retained 97%)
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] 1 < 1/1000 * 11366 = 11 considered unsuccessful
c [sweep-5] removed 1 vars in TOTAL (3 rounds, 582 queries)
c [sort-queue-6] sorted 11365 enqueued variables after 61002 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 11365 (100%)
c [score-dist-6] max exp 0, different 1 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 1 variables 0.0% (11365 remain 84%)
c [simplification-6] removed 439 irredundant clauses 0.0% (1282792 remain 99%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 40000
c [simplification-6] new conflict interval 80000
c [simplification-6] penalized conflict interval 80000 = 1 * 80000
c [simplification-6] hard conflict limit 181002 (soft 141002 + delta 40000)
c [simplification-6] new conflict limit 141002 (hard 181002)
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  129.4   11364  1282792     61425   54990  25857 26767   23   574  131   4%    465  215   22   13  173%
c -  131.8   11364  1282792     63169    7465  25877 26770   23   583  110   4%    -44  218   22   13  172%
c i  154.8   11363  1282792     83392   26941  26173 26808   22   589  116   4%    151  166   18   15  120%
c i  178.4   11362  1282792    104697   47526  26418 26848   24   557  123   4%    141   86   26   18  150%
c -  193.8   11362  1282792    118086   14857  26564 26870   23   506  110   5%     29   24   19   19  104%
c i  200.6   11361  1282792    126486   23010  26615 26877   20   361  113   5%    149 -116   22   19  117%
c 
c [simplification-7] limit 141002 conflicts (hard 181002) hit after 141153 conflicts
c [quatres-5] found 23780 quaternary clauses 2% in total
c [quatres-5-2] added 5 single-self-subsuming ternary resolvents
c [quatres-5-2] added 30 quaternary resolvents
c [ternres-5] limit 25932631 with penalty 0 = 0 + 0
c [ternres-5] 409 schedulable variables 4%
c [ternres-5] 12992 ternary resolvents (0 bin, 12992 trn)
c [ternres-5] 288 variables remain 3% (11073 retained 97%)
c [decomp-19] removed 4 variables
c [unhide-5] limit 324157 with penalty 4 = 1 + 3
c [unhide-5-5] 1 units, 0 failed, 2144 tauts, 0 hbrs, 42252 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 126 transitive binary clauses
c [transred-5] found 1 units
c [block-3] 164 variables 1% will be scheduled this time
c [block-3] scheduled 164 variables 1%
c [block-3] limit of 64831577 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-3] limit of 32415788 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 46 clauses out of 46 (100%) of length 61
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 46 large clauses in 32419007 steps
c [cce-3-1] allowing another 16209503 steps for small clauses
c [cce-3-1] scheduling 44007 clauses = 29524 binary + 14483 ternary
c [cce-3-1] tried to eliminate 691 small clauses 2%
c [cce-3-1] eliminated 17 ternary clauses 0%
c [cce-3-1] eliminated 17 small clauses 0%
c [cce-3-1] eliminated 17 small clauses in 32418889 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 63 covered clauses in round 1
c [cce-3] eliminated 63 covered clauses in TOTAL during 1 rounds
c [cce-3] 63 < 1/100 * 1280846 = 12808 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 11359 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 2593263105 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 49 variables 0% in round 1 in 12315170 steps
c [elim-4-1] backward subsumption/strengthening limit 12315100
c [elim-4-1-1] backward checking 952 touched variables 8%
c [elim-4-1-1] incomplete backward checking 936 remain 98%
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 12324516 steps
c [elim-4-1] fully rescheduled 11310 variables 100%
c [elim-4-2] no variable eliminated in round 2 in 11661735 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 49 = 0% variables out of 11359 scheduled
c [elim-4] 49 < 1/100 * 11359 = 113 considered unsuccessful
c [bca-3] limit of 10000000 steps and 2561170 added (scaled 2)
c [bca-3] 7646 out of 22622 literals actually usable 34%
c [bca-3] added 0 blocked clauses in 48029 steps
c [sort-queue-7] sorted 11310 enqueued variables after 141153 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 11310 (100%)
c [score-dist-7] max exp 0, different 1 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 51 variables 0.4% (11310 remain 84%)
c [simplification-7] removed 2457 irredundant clauses 0.2% (1280335 remain 98%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 80000
c [simplification-7] new conflict interval 160000
c [simplification-7] penalized conflict interval 160000 = 1 * 160000
c [simplification-7] hard conflict limit 381153 (soft 301153 + delta 80000)
c [simplification-7] new conflict limit 301153 (hard 381153)
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  233.4   11309  1280335    154150   45150  39791 26481   22   453  120   5%    223   -6   31   20  157%
c -  252.5   11298  1280335    172796   18799  39932 26511   24   447  111   5%     91  -14   22   21  108%
c -  292.0   11298  1280335    221637   22701  40250 26574   22   372  111   6%    581  -53   18   22   81%
c -  326.9   11298  1280335    268961   26296  40474 26623   24   398  112   6%    809   10   23   22  106%
c 
c [simplification-8] limit 301153 conflicts (hard 381153) hit after 301286 conflicts
c [quatres-6] found 24717 quaternary clauses 2% in total
c [quatres-6-2] added 4 single-self-subsuming ternary resolvents
c [quatres-6-2] added 22 quaternary resolvents
c [ternres-6] limit 55398624 with penalty 0 = 0 + 0
c [ternres-6] 288 schedulable variables 3%
c [ternres-6] 15052 ternary resolvents (0 bin, 15052 trn)
c [ternres-6] 195 variables remain 2% (11103 retained 98%)
c [gauss-3] limit 2769931 penalty 2 = 2 + 0
c [gauss-3] extracted 13 xors of average arity 2.0
c [gauss-3] connected 26 occurrences of 18 variables (average 1.4)
c [gauss-3] limit 2769931 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 18 variables
c [treelook-3] limit 2769931 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 14357 literals 64%
c [treelook-3] scheduling used 2430969 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 2769931 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 2987904 steps
c [treelook-3] 14321 literals remain 63%
c [treelook-3] 2216 variables remain to probed next time 20%
c [decomp-21] removed 1 variables
c [treelook-3] removed 1 variables, found 89 hbrs
c [unhide-6] limit 1384965 with penalty 3 = 0 + 3
c [unhide-6-6] 0 units, 0 failed, 854 tauts, 0 hbrs, 119728 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 58 transitive binary clauses
c [sweep-6] limit 8309793 penalty 1 = 1 + 0
c [sweep-6-1] 19 pos 5.4% + 330 neg 94.6% = 349 sched 3.1% ret 10930
c [sweep-6-1] 8380897 steps 78 queries 12.51 avg class size
c [sweep-6-1] 4617 decisions 77 SAT calls 296.97 avg env size
c [sweep-6-1] 80 variables remain 1% (11199 retained 99%)
c [decomp-22] removed 1 variables
c [sweep-6-1] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-6] 1 < 1/1000 * 11279 = 11 considered unsuccessful
c [sweep-6] removed 1 vars in TOTAL (1 rounds, 77 queries)
c [sort-queue-8] sorted 11278 enqueued variables after 301286 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 11278 (100%)
c [score-dist-8] max exp 0, different 1 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 20 variables 0.2% (11278 remain 83%)
c [simplification-8] removed 74 irredundant clauses 0.0% (1280261 remain 98%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 160000
c [simplification-8] new conflict interval 320000
c [simplification-8] penalized conflict interval 320000 = 1 * 320000
c [simplification-8] hard conflict limit 781286 (soft 621286 + delta 160000)
c [simplification-8] new conflict limit 621286 (hard 781286)
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 -  368.8   11278  1280261    315080   28126  55252 26276   23   270  113   8%    918  -94   25   23  108%
c i  382.6   11277  1280261    334892   47424  55322 26294   22   294  123   7%    945  -52   17   23   77%
c -  404.8   11277  1280261    361977   30239  55434 26313   26   404  113   6%   -926   53   27   23  116%
c i  426.1   11276  1280261    389661   57201  55538 26339   25   325  128   8%   -254  -35   25   24  106%
c -  440.5   11276  1280261    408964   32140  55605 26347   24   290  114   8%   -575  -49   25   24  104%
c -  477.0   11276  1280261    456575   33868  55805 26380   26   354  114   7%    251   17   30   24  123%
c -  515.4   11276  1280261    505177   35288  55987 26412   26   336  113   8%    656   10   24   25   96%
c -  551.7   11276  1280261    554357   37456  56136 26440   26   347  115   8%    850   25   28   25  109%
c -  587.6   11276  1280261    603839   39758  56287 26465   27   356  115   8%    942   43   26   25  103%
c 
c [simplification-9] limit 621286 conflicts (hard 781286) hit after 635141 conflicts
c [quatres-7] found 26692 quaternary clauses 2% in total
c [quatres-7-2] added 13 single-self-subsuming ternary resolvents
c [quatres-7-2] added 26 quaternary resolvents
c [ternres-7] limit 120755535 with penalty 0 = 0 + 0
c [ternres-7] 195 schedulable variables 2%
c [ternres-7] 21807 ternary resolvents (0 bin, 21807 trn)
c [ternres-7] 79 variables remain 1% (11197 retained 99%)
c [decomp-23] removed 3 variables
c [basicprobe-3] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-3-0] 1037 sched 9%, 1 failed, 0 lifted, 2116 hbrs
c [decomp-24] removed 8 variables
c [basicprobe-3-1] 9726 sched 86%, 5 failed, 0 lifted, 1950 hbrs
c [decomp-25] removed 6 variables
c [basicprobe-3-2] 9674 sched 86%, 0 failed, 0 lifted, 262 hbrs
c [basicprobe-3-3] 9673 sched 86%, 0 failed, 0 lifted, 37 hbrs
c [basicprobe-3-4] 9673 sched 86%, 0 failed, 0 lifted, 18 hbrs
c [basicprobe-3-5] 9673 sched 86%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-3-6] 8883 probes remain 79% after last round
c [basicprobe-3-6] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-3-6] removed 14 variables, found 4396 hbrs
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 194 transitive binary clauses
c [sort-queue-9] sorted 11261 enqueued variables after 635141 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 11261 (100%)
c [score-dist-9] max exp 0, different 1 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 15 variables 0.1% (11261 remain 83%)
c [simplification-9] removed 84 irredundant clauses 0.0% (1280177 remain 98%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 320000
c [simplification-9] new conflict interval 640000
c [simplification-9] penalized conflict interval 640000 = 1 * 640000
c [simplification-9] hard conflict limit 1595141 (soft 1275141 + delta 320000)
c [simplification-9] new conflict limit 1275141 (hard 1595141)
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 -  668.9   11261  1280177    653394   41719  78142 30433   26   370  115   7%    986   53   28   25  109%
c -  705.5   11261  1280177    703082   43442  78262 30437   24   290  116   8%   1006  -13   21   25   85%
c -  744.9   11261  1280177    753364   44825  78394 30440   25   318  117   8%   1016   13   29   25  115%
c -  785.7   11261  1280177    804355   45920  78532 30443   26   333  117   8%   1020   20   26   25  102%
c -  826.0   11261  1280177    856815   48086  78634 30450   26   318  116   8%   1022    0   26   25  104%
c -  866.6   11261  1280177    909490   49961  78734 30453   25   257  116  10%   1023  -57   23   25   94%
c -  910.5   11261  1280177    962647   51145  78838 30459   26   329  117   8%   1024   23   25   25   99%
c -  955.4   11261  1280177   1016814   51696  78954 30464   27   409  116   7%   1024   85   30   26  117%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 3 count, 0 added (0 skipped), 115038 steps
c bkwd: tried 1906 clauses, 3770 lits, 1.98 lits/clause
c bkwd: checked 12496604 occs, 6556.46 occs/clause, 3314.75 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 42 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 3 bces, 2542 removed, 22518832 resolutions, 75688896 steps
c blkd: 2539 blocking literals 9%, 2 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 3 count, 0 units, 0 am1, 8934206 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 25 subsumed
c card: 119 at-most-one constraints found, average size 3.37
c card: 119 at-most-one constraints used 100%, average size 3.37
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, 323 eliminated, 323 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: 12763267 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 43 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 29 decompositions, 129 equivalent 1%
c deco: 803 decision-only clauses 0%, 56% reduction
c decs: 35660271 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 4 elims, 1093 eliminated 8%, 8 pure 1%
c elms: 8 rounds, 2.0 rounds/bve
c elms: 0 small 0%, 1083 large 99%
c elms: 0 tried small, 0 succeeded 0%, 0 failed 0%
c elms: 1801 subsumed, 22 strengthened, 1 blocked
c elms: 707462 copies, 1266233 resolutions, 0 ipos
c elms: 1313738 subchks, 1041751 strchks
c gaus: 3 extractions, 17 extracted, 2.0 size, 2 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 11565490 steps, 5782745 extr 50%, 78 elim 0%
c glue: 24.2 orig avg, 24.2 real avg, 4.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 32100 = 1831 simple 6% + 30206 trn 94% + 63 lrg 0%, 109 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1067612 clauses, 87.8 length
c lrnd: 93725926 lits = 120105442 orig - 26379516 removed 22%
c lrnd: 717383 uips 67%, 114276 flips 11%
c mins: 1049353 mins 98%, 931 bin 0%, 16287 size 2%
c mins: 156898765 poisoned searches, 43708311 hits, 28% hit rate
c mins: 231170765 used twice searches, 13957053 hits, 6% hit rate
c move: moved 3899, 0 bin 0%, 3899 trn 100%
c otfs: 4191 driving 25%, 12485 restarting 75%
c otfs: str 16676, 16508 red 99%, 168 irr 1%
c otfs: str 16676, 0 bin 0%, 60 trn 0%, 16616 lrg 100%
c otfs: sub 10, 10 red 100%, 0 irr 0%
c otfs: sub 10, 0 bin 0%, 6 trn 60%, 4 lrg 40%
c phas: 1 computed, 11448 set, 0 pos (0%), 11448 neg (100%)
c prbs: 3 basic, 118304 probed, 22 failed, 0 lifted
c prbs: 3 simple, 20867 probed, 2 failed, 0 eqs
c prbs: 3 treelook, 67 probed, 1 failed, 0 lifted
c prom: 199064 locked 12% out of 1650329 tried
c prps: 763894323 props, 21 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 7 count, 161 quat, 33 self1, 0 self2, 1634 dup
c queu: 9 sorted, 35660271 next (0 steps 0.00)
c queu: 115854 enq (115844 steps 1.00), 0 deq 0%
c redc: 19500 clauses 23%, 84277 tried 8%, 14 sat 0%
c redc: 57802 lits 5%, 1161424 tried 1%, 14 sat 0%
c redc: 2588 times jump level reduced, 82.1 levels on average
c reds: 20 count, 53503.9 conflicts per reduce
c reds: 0 memlim 0%, 20 arith 100%
c reds: 592619 collected 64%, 338373 retired 36%
c rmbd: 831 removed, 54 red 6%
c rsts: 16763 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 9 count, 7 confs 78%, 0 vars 0%
c simp: 0 its 0%, 1 bin 11%, 1 trns 11%
c subl: 1067612 count (1128388 tried 1.1), 16665 sub out of 1060386 (1.6%)
c swps: 6 count, 8 rounds, 1014 queries (126.8/round)
c swps: 1012 sat calls, 1 unsat (1.7% success rate)
c swps: 48204 decisions 47.6, 1724 conflicts 1.7
c swps; 168.2 avg class size, 205.3 avg environment size
c swps: 0 failed, 4 impls, 3 equivs
c swp0: 337 type 0 queries, 53 unsat (15.7%), 337 sat (100.0%)
c swp1: 677 type 1 queries, 174 unsat (25.7%), 674 sat (99.6%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 71320733 calls to obtain time
c tops: 1091 fixed 8%, 13 its, 82313.77 confs/it
c trds: 7 transitive reductions, 714 removed, 1 failed
c trds: 130100 nodes, 277126 edges, 12166556 steps
c trim: 187672 words, 0.7 MB
c trnr: 7 count, 0 bin, 71196 trn, 247822932 steps
c unhd: 6 count, 6 rounds, 84857502 steps
c unhd: 4 non-trivial sccs of average size 2.0
c unhd: 2 units, 2 bin, 0 trn, 0 lrg
c unhd: 3 failed, 3 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 10419 tauts, 23 bin 0%, 3183 trn 31%, 6394 lrg 61%
c unhd: 10419 tauts, 819 stamp 8%, 2887 red 28%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 315921 str, 2 bin 0%, 58 trn 0%, 315861 lrg 100%, 220628 red 70%
c vars: 11261 remaining 83% and 2313 removed 17% out of 13574
c vars: 1091 fixed 8%, 1093 eliminated 8%, 129 equivalent 1%
c vsts: 22409329861 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 29.2 search visits per propagation, 20482.0 per conflict
c wchs: 11243532369 pushed, 17191047 enlarged, 731 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1060547        592619        338373      40592764       7584743        502723
c 
c  0 0         47431   4     10156   2         0   0  24212132  60   3127203  41    110696  22     1.4
c  1 5         25404   2     15419   3      5530   2   3248391   8<   690182   9     36407   7     0.3
c  2 6         93467   9     59996  10     21864   6   5611516  14   1372121  18<    97909  19<    0.9
c  3 9        171901  16    107987  18     45890  14   4781764  12   1323785  17    135081  27     2.2
c  4 14       215895  20<   131481  22<    67558  20   1663154   4    581035   8     70232  14     3.4
c  5 21       198039  19    112508  19     70317  21<   554315   1    245262   3     29038   6     4.5
c  6 30       145006  14     76835  13     56435  17    265677   1    128071   2     12780   3     4.6
c  7 41        88985   8     44906   8     36528  11    146224   0     69061   1      6290   1     3.8
c  8 54        44821   4     21308   4     19596   6     68485   0     31205   0      2797   1     2.2
c  9 69        19067   2      8329   1      9038   3     27133   0     11608   0      1063   0     1.1
c 10 86         8321   1      3250   1      4313   1     11305   0      4413   0       358   0     0.7
c 11 126        1743   0       386   0      1002   0      2147   0       680   0        67   0     0.2
c 12 230         453   0        58   0       296   0       506   0       113   0         5   0     0.1
c 13 534          14   0         0   0         6   0        15   0         4   0         0   0     0.0
c 
c avg                  4.4           4.4           5.0           1.0           1.7           2.4
c std                  2.1           1.9           1.9           1.5           1.8           1.8
c 
c   57.461   6% probe
c   21.114   2% decide
c   10.126   1% block
c   10.011   1% unhide
c    7.019   1% sweep
c    6.308   1% elim
c 
c   13.094 < 1% rest (below)
c 
c    3.468   0% cce
c    2.573   0% gauss
c    2.223   0% quatres
c    1.899   0% bca
c    1.890   0% ternres
c    0.959   0% transred
c    0.084   0% card
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    6.051   1% preprocessing     5%
c  105.815  11% inprocessing     95%
c ==================================
c  111.867  11% simplifying
c  886.423  89% search
c ==================================
c  998.290 100% all
c 
c       1070079 conflicts,        1071.9 confs/sec
c          6138 ternaries,         174.3 confs/ternary
c          1030 binaries,         1038.9 confs/binary
c            13 iterations,      82313.8 confs/iteration
c 
c            20 reductions,          0.0 redus/sec,  53503.9 confs/reduction
c         16763 restarts,           16.8 rests/sec,     63.8 confs/restart
c      35660271 decisions,       35721.3 decis/sec,     33.3 decis/conflict
c     763894323 propagations,   765202.7 props/sec,     21.4 props/decision
c 
c 998.3 seconds, 469.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
