c launch: /data/cnf/sc2014/app/6s13-opt.cnf.bz2
c host: atom29
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/6s13-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/6s13-opt.cnf.bz2
c no embedded options
c found 'p cnf 52436 153557' header
c read 52436 variables, 153557 clauses, 358297 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 51981 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   51981   151783         0       0      0     0    0     0    9   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 83 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] 83 out of 83 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 57 at-most-one constraints, 57 used 100%
c [card-1] exported 61 binary clauses, 1.1 per/constraint
c [decomp-1] removed 888 variables
c [simpleprobe-1] all 51538 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 1183 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1183 variables, found 2119 hbrs, 156 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 8 tauts, 0 hbrs, 11 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 50355 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 37049 variables 74% in round 1 in 10576975 steps
c [elim-1-1] backward subsumption/strengthening limit 9423025
c [elim-1-1-1] backward checking 36067 touched variables 72%
c [elim-1-1-1] incomplete backward checking 35910 remain 100%
c [elim-1-1] subsumed 8 and strengthened 128 clauses in 9425504 steps
c [elim-1] incomplete 313 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 37051 = 74% variables out of 50355 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 66921 negative 90.6% of 73865 except 6944 9.4%
c [phase-count-1] 62289 positive 84.3% of 73865 except 11576 15.7%
c [phase-1] phase bias: 3169 positive 24%, 10135 negative 76%
c [sort-queue-1] sorted 13304 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 13304 (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 38677 variables 74.4% (13304 remain 26%)
c [simplification-1] removed 77918 irredundant clauses 51.3% (73865 remain 49%)
c [simplification-1] maximum reduction of 74% = max (74%, 51%)
c [simplification-1] large reduction 74% >= 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 1001 conflicts
c [decomp-3] removed 7 variables
c [simpleprobe-2] all 13297 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 4 variables
c [simpleprobe-2] 6621 variables remain 50% (6672 retained 50%)
c [simpleprobe-2] removed 4 variables, found 538 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 26586 literals 100%
c [treelook-1] scheduling used 300002 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 303816 steps
c [treelook-1] 26521 literals remain 100%
c [treelook-1] 13293 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 2268 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 6498 probes remain 49% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1 variables, found 4102 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 13292 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 209 variables 2% in round 1 in 11795543 steps
c [elim-2-1] backward subsumption/strengthening limit 8204457
c [elim-2-1-1] backward checking 2225 touched variables 17%
c [elim-2-1-1] incomplete backward checking 2146 remain 96%
c [elim-2-1] subsumed 2 and strengthened 26 clauses in 8205251 steps
c [elim-2] incomplete 66 not tried 0% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 210 = 2% variables out of 13292 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 13082 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 4265 (33%), zero 8817 (67%)
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 222 variables 1.7% (13082 remain 25%)
c [simplification-2] removed 752 irredundant clauses 1.0% (73112 remain 48%)
c [simplification-2] maximum reduction of 2% = max (2%, 1%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 6666
c [simplification-2] penalized conflict interval 6666 = 1 * 6666
c [simplification-2] hard conflict limit 17667 (soft 7667 + delta 10000)
c [simplification-2] new conflict limit 7667 (hard 17667)
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    3.6   13081    73112      7478    5922    682  6824    5   115    8   4%     96  107    6    1  937%
c 
c [simplification-3] limit 7667 conflicts (hard 17667) hit after 7668 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 176 at-most-one constraints of average size 3.0
c [card-2] found 4 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 180 out of 180 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 46 at-most-one constraints, 21 used 46%
c [card-2] exported 23 binary clauses, 1.1 per/constraint
c [decomp-6] removed 27 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 1 units, 1 failed, 744 tauts, 0 hbrs, 3451 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 13053 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 112 variables 1% in round 1 in 14679426 steps
c [elim-3-1] backward subsumption/strengthening limit 5320574
c [elim-3-1-1] backward checking 886 touched variables 7%
c [elim-3-1-1] incomplete backward checking 869 remain 98%
c [elim-3-1] subsumed 0 and strengthened 5 clauses in 5324239 steps
c [elim-3] incomplete 16 not tried 0% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 112 = 1% variables out of 13053 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 12941 enqueued variables after 7668 conflicts
c [score-dist-3] active 0 (0%), one 9264 (72%), zero 3677 (28%)
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 140 variables 1.1% (12941 remain 25%)
c [simplification-3] removed 285 irredundant clauses 0.4% (72827 remain 48%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 16666
c [simplification-3] penalized conflict interval 16666 = 1 * 16666
c [simplification-3] hard conflict limit 34334 (soft 24334 + delta 10000)
c [simplification-3] new conflict limit 24334 (hard 34334)
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    5.1   12940    72827     13273   10484   1022  5955    7   131    9   5%     66  114    6    1  494%
c i    5.2   12939    72827     13983   11095   1064  5969    7   131    9   5%     31  113    7    1  547%
c 
c [simplification-4] limit of 207 binary hit after 207 binaries
c [decomp-7] removed 22 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 13815 literals 53%
c [treelook-2] scheduling used 150005 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 355557 steps
c [treelook-2] 13799 literals remain 53%
c [treelook-2] 10458 variables remain to probed next time 81%
c [treelook-2] removed 0 variables, found 1080 hbrs
c [unhide-3] limit 186465 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 1 failed, 182 tauts, 0 hbrs, 5651 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 12918 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 64 variables 0% in round 1 in 14663291 steps
c [elim-4-1] backward subsumption/strengthening limit 14663200
c [elim-4-1-1] backward checking 458 touched variables 4%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 5 clauses in 4051940 steps
c [elim-4-1] rescheduled 15 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 40311 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 64 = 0% variables out of 12918 scheduled
c [elim-4] 64 < 1/100 * 12918 = 129 considered unsuccessful
c [sort-queue-4] sorted 12854 enqueued variables after 21777 conflicts
c [score-dist-4] active 0 (0%), one 10825 (84%), zero 2029 (16%)
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 85 variables 0.7% (12854 remain 25%)
c [simplification-4] removed 316 irredundant clauses 0.4% (72509 remain 48%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] forced so keeping old conflict interval 16666
c [simplification-4] conflict limit remains at 24334 (hard 34334)
c [simplification-4] new binary interval 1000
c 
c [simplification-5] limit 24334 conflicts (hard 34334) hit after 24335 conflicts
c [quatres-1] found 17682 quaternary clauses 50% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 130 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1752 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 12854 free variables schedulable
c [ternres-1] 8202 ternary resolvents (153 bin, 8049 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 5099 xors of average arity 3.0
c [gauss-1] connected 15462 occurrences of 1090 variables (average 14.2)
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-9] removed 31 variables
c [basicprobe-2] limit 5314979 penalty 0 = 0 + 0
c [basicprobe-2-0] 1858 probes remain 14% after last round
c [basicprobe-2-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 9 variables, found 12812 hbrs
c [bate-1] eliminated 37 asymmetric tautologies during probing
c [unhide-4] limit 212599 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 2064 tauts, 0 hbrs, 6289 literals
c [transred-1] limit 1062995 with penalty 0 = 0 + 0
c [transred-1] removed 415 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 12814 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 2017 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 64 (3%) of length 13
c [cce-1-1] eliminated 6 clauses out of 90 (7%) of length 12
c [cce-1-1] eliminated 4 clauses out of 113 (4%) of length 11
c [cce-1-1] eliminated 10 clauses out of 208 (5%) of length 10
c [cce-1-1] eliminated 15 clauses out of 374 (4%) of length 9
c [cce-1-1] eliminated 35 clauses out of 622 (6%) of length 8
c [cce-1-1] eliminated 84 clauses out of 1233 (7%) of length 7
c [cce-1-1] eliminated 342 clauses out of 3385 (10%) of length 6
c [cce-1-1] eliminated 251 clauses out of 6925 (4%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 749 large clauses in 30000011 steps
c [cce-1-1] allowing another 15000005 steps for small clauses
c [cce-1-1] scheduling 22855 clauses = 14108 binary + 8747 ternary
c [cce-1-1] tried to eliminate 10504 small clauses 46%
c [cce-1-1] eliminated 73 binary clauses 1%
c [cce-1-1] eliminated 229 ternary clauses 3%
c [cce-1-1] eliminated 302 small clauses 1%
c [cce-1-1] eliminated 302 small clauses in 30000130 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1051 covered clauses in round 1
c [cce-1] eliminated 1051 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 139120 added (scaled 2)
c [bca-1] 10100 out of 25630 literals actually usable 39%
c [bca-1] added 3 blocked clauses in 44801 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 5607 pos 43.8% + 7207 neg 56.2% = 12814 sched 100.0% ret 0
c [sweep-1-1] 1080906 steps 75 queries 1070.12 avg class size
c [sweep-1-1] 1528 decisions 71 SAT calls 45.14 avg env size
c [sweep-1-1] 11669 variables remain 91% (1145 retained 9%)
c [decomp-10] removed 96 variables
c [sweep-1-1] removed 96 vars (0 failed, 9 eqs, 7 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 96 vars in TOTAL (1 rounds, 74 queries)
c [sort-queue-5] sorted 12718 enqueued variables after 24335 conflicts
c [score-dist-5] active 0 (0%), one 10937 (86%), zero 1781 (14%)
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 136 variables 1.1% (12718 remain 24%)
c [simplification-5] removed 3217 irredundant clauses 4.4% (69292 remain 46%)
c [simplification-5] maximum reduction of 4% = max (1%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 20666
c [simplification-5] penalized conflict interval 20666 = 1 * 20666
c [simplification-5] hard conflict limit 55334 (soft 45001 + delta 10333)
c [simplification-5] new conflict limit 45001 (hard 55334)
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    9.4   12717    69292     25160   21781  10355 17689    7   137   12   5%    139  101    6    2  289%
c i    9.4   12716    69292     25232   21813  10364 17694    7   136   12   5%    128  100    6    2  264%
c i   10.7   12715    69291     33155   28804  10564 17746    8   133   12   6%     82   87    7    3  254%
c i   10.7   12714    69291     33170   28807  10568 17749    8   133   12   6%     81   86    7    3  247%
c i   10.8   12713    69291     33758   29328  10589 17752    8   134   12   6%     36   86    8    3  280%
c i   11.3   12712    69291     35855   31182  10640 17762    8   139   12   6%      0   89    8    3  249%
c i   11.4   12711    69291     36307   31535  10666 17768    8   137   12   6%     -8   86    7    3  237%
c i   11.4   12710    69290     36518   31670  10686 17772    8   145   12   5%    -11   94    6    3  198%
c i   11.9   12709    69290     39314   34078  10787 17800    8   132   12   6%      4   78    8    3  240%
c 
c [simplification-6] limit 45001 conflicts (hard 55334) hit after 45002 conflicts
c [quatres-2] found 19811 quaternary clauses 50% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-1] added 4 double-self-subsuming ternary resolvents
c [quatres-2-2] added 133 single-self-subsuming ternary resolvents
c [quatres-2-2] added 784 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 12709 free variables schedulable
c [ternres-2] 1439 ternary resolvents (63 bin, 1376 trn)
c [ternres-2] 5 variables remain 0% (12704 retained 100%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 131 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 131 out of 131 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 38 variables
c [simpleprobe-3] 6293 schedulable variables 50%
c [simpleprobe-3] limit 8930419 penalty 0 = 0 + 0
c [decomp-12] removed 57 variables
c [simpleprobe-3] 768 variables remain 6% (11855 retained 94%)
c [simpleprobe-3] removed 57 variables, found 3079 hbrs, 0 units
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 1526 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 12623 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 89 blocked clauses
c [block-2] 89 < 1/100 * 68944 = 689 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 4 clauses out of 1129 (0%) of length 7
c [cce-2-1] eliminated 7 clauses out of 3055 (0%) of length 6
c [cce-2-1] eliminated 41 clauses out of 6659 (1%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 52 large clauses in 30000009 steps
c [cce-2-1] allowing another 15000004 steps for small clauses
c [cce-2-1] scheduling 32660 clauses = 13786 binary + 18874 ternary
c [cce-2-1] tried to eliminate 11549 small clauses 35%
c [cce-2-1] eliminated 63 binary clauses 0%
c [cce-2-1] eliminated 270 ternary clauses 1%
c [cce-2-1] eliminated 333 small clauses 1%
c [cce-2-1] eliminated 333 small clauses in 30000609 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 385 covered clauses in round 1
c [cce-2] eliminated 385 covered clauses in TOTAL during 1 rounds
c [cce-2] 385 < 1/100 * 68855 = 688 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 12609 variables 100%
c [elim-5] limit of 22326048 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 528 variables 4% in round 1 in 15766086 steps
c [elim-5-1] backward subsumption/strengthening limit 6559962
c [elim-5-1-1] backward checking 2843 touched variables 23%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 7 and strengthened 32 clauses in 3564109 steps
c [elim-5-1] rescheduled 97 variables 1% by backward subsumption
c [elim-5-2] eliminated 2 variables 0% in round 2 in 1865139 steps
c [elim-5-2] backward subsumption/strengthening limit 1130714
c [elim-5-2-1] backward checking 18 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 47809 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 530 = 4% variables out of 12609 scheduled
c [bca-2] limit of 10000000 steps and 135811 added (scaled 2)
c [bca-2] 7031 out of 24160 literals actually usable 29%
c [bca-2] added 46 blocked clauses in 53850 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4856 pos 44.1% + 6155 neg 55.9% = 11011 sched 91.2% ret 1068
c [sweep-2-1] 1027419 steps 36 queries 928.89 avg class size
c [sweep-2-1] 1042 decisions 35 SAT calls 58.03 avg env size
c [sweep-2-1] 10430 variables remain 86% (1649 retained 14%)
c [decomp-13] removed 2 variables
c [sweep-2-1] removed 2 vars (0 failed, 2 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 2 vars in TOTAL (1 rounds, 35 queries)
c [sort-queue-6] sorted 12077 enqueued variables after 45002 conflicts
c [score-dist-6] active 0 (0%), one 11581 (96%), zero 496 (4%)
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 632 variables 5.0% (12077 remain 23%)
c [simplification-6] removed 1635 irredundant clauses 2.4% (67655 remain 45%)
c [simplification-6] maximum reduction of 5% = max (5%, 2%)
c [simplification-6] large reduction 5% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 57002 (soft 47002 + delta 10000)
c [simplification-6] new conflict limit 47002 (hard 57002)
c 
c [simplification-7] limit 47002 conflicts (hard 57002) hit after 47002 conflicts
c [quatres-3] found 20092 quaternary clauses 49% in total
c [quatres-3-1] removed 13 duplicate quaternary clauses
c [quatres-3-1] added 4 double-self-subsuming ternary resolvents
c [quatres-3-2] added 42 single-self-subsuming ternary resolvents
c [quatres-3-2] added 578 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 5 schedulable variables 0%
c [ternres-3] 719 ternary resolvents (18 bin, 701 trn)
c [ternres-3] 1 variables remain 0% (12076 retained 100%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1836 xors of average arity 3.0
c [gauss-2] connected 5504 occurrences of 803 variables (average 6.9)
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-14] removed 3 variables
c [unhide-5] limit 232017 with penalty 1 = 1 + 0
c [unhide-5-5] 0 units, 0 failed, 289 tauts, 0 hbrs, 9980 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 580 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 12074 variables 100%
c [elim-6] limit of 46403576 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 27 variables 0% in round 1 in 15523632 steps
c [elim-6-1] backward subsumption/strengthening limit 15523600
c [elim-6-1-1] backward checking 237 touched variables 2%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 2032569 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 27 = 0% variables out of 12074 scheduled
c [elim-6] 27 < 1/100 * 12074 = 120 considered unsuccessful
c [bca-3] limit of 10000000 steps and 135634 added (scaled 2)
c [bca-3] 6741 out of 24096 literals actually usable 28%
c [bca-3] added 2 blocked clauses in 55092 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 4545 pos 43.7% + 5858 neg 56.3% = 10403 sched 86.4% ret 1644
c [sweep-3-1] 1033897 steps 60 queries 851.28 avg class size
c [sweep-3-1] 1193 decisions 54 SAT calls 41.85 avg env size
c [sweep-3-1] 9818 variables remain 82% (2227 retained 18%)
c [decomp-15] removed 19 variables
c [sweep-3-1] removed 19 vars (0 failed, 8 eqs, 9 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 19 vars in TOTAL (1 rounds, 59 queries)
c [sort-queue-7] sorted 12028 enqueued variables after 47002 conflicts
c [score-dist-7] active 0 (0%), one 11573 (96%), zero 455 (4%)
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 49 variables 0.4% (12028 remain 23%)
c [simplification-7] removed 120 irredundant clauses 0.2% (67535 remain 44%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20666
c [simplification-7] new conflict interval 41332
c [simplification-7] penalized conflict interval 41332 = 1 * 41332
c [simplification-7] hard conflict limit 109000 (soft 88334 + delta 20666)
c [simplification-7] new conflict limit 88334 (hard 109000)
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   16.7   12027    67535     49165   41368  11781 17716    8   121   14   7%    106   57    7    4  172%
c i   18.6   12026    67534     58737   49795  12021 17765    8   117   15   7%     96   45    8    5  174%
c i   20.8   12025    67534     70031   59597  12323 17834    8   122   15   7%    115   43    7    5  145%
c i   22.5   12024    67534     78083   66665  12505 17862    8   128   16   7%     62   42    8    5  141%
c -   23.1   12024    67534     80272   29084  12558 17884    8   122   13   7%    -15   36    8    6  141%
c i   23.2   12023    67534     80830   29572  12578 17891    8   124   14   7%    -13   37    8    6  135%
c i   24.0   12022    67534     85081   33314  12677 17928    8   109   14   7%      4   21    8    6  140%
c 
c [simplification-8] limit 88334 conflicts (hard 109000) hit after 88973 conflicts
c [quatres-4] found 22135 quaternary clauses 45% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 9 double-self-subsuming ternary resolvents
c [quatres-4-2] added 183 single-self-subsuming ternary resolvents
c [quatres-4-2] added 478 quaternary resolvents
c [ternres-4] limit 5052103 with penalty 0 = 0 + 0
c [ternres-4] 1 schedulable variables 0%
c [ternres-4] 367 ternary resolvents (0 bin, 367 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-16] removed 46 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 325 transitive binary clauses
c [transred-4] found 5 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 11977 variables 100%
c [block-3] limit of 25260518 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 54 blocked clauses
c [block-3] 54 < 1/100 * 67462 = 674 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3-1] scheduling 30334 clauses = 13042 binary + 17292 ternary
c [cce-3-1] tried to eliminate 701 small clauses 2%
c [cce-3-1] eliminated 7 binary clauses 0%
c [cce-3-1] eliminated 10 ternary clauses 0%
c [cce-3-1] eliminated 17 small clauses 0%
c [cce-3-1] eliminated 17 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 17 covered clauses in round 1
c [cce-3] eliminated 17 covered clauses in TOTAL during 1 rounds
c [cce-3] 17 < 1/100 * 67396 = 673 considered unsuccessful
c [bca-4] limit of 10000000 steps and 135283 added (scaled 2)
c [bca-4] 5078 out of 23944 literals actually usable 21%
c [bca-4] added 0 blocked clauses in 48196 steps
c [sweep-4] limit 1515631 penalty 0 = 0 + 0
c [sweep-4-1] 4266 pos 43.7% + 5494 neg 56.3% = 9760 sched 81.5% ret 2211
c [sweep-4-1] 1521676 steps 102 queries 446.18 avg class size
c [sweep-4-1] 2069 decisions 96 SAT calls 43.02 avg env size
c [sweep-4-1] 8614 variables remain 72% (3357 retained 28%)
c [decomp-17] removed 15 variables
c [sweep-4-1] removed 15 vars (0 failed, 11 eqs, 8 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 15 vars in TOTAL (1 rounds, 101 queries)
c [sort-queue-8] sorted 11956 enqueued variables after 88973 conflicts
c [score-dist-8] active 0 (0%), one 11937 (100%), zero 19 (0%)
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 66 variables 0.5% (11956 remain 23%)
c [simplification-8] removed 167 irredundant clauses 0.2% (67367 remain 44%)
c [simplification-8] maximum reduction of 1% = max (1%, 0%)
c [simplification-8] geometric conflict interval increment 20666 = 41332 / 2
c [simplification-8] new conflict interval 61998
c [simplification-8] penalized conflict interval 61998 = 1 * 61998
c [simplification-8] hard conflict limit 181970 (soft 150971 + delta 30999)
c [simplification-8] new conflict limit 150971 (hard 181970)
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   28.3   11955    67365     96281   43480  13241 17641    8   120   13   7%    107   27    8    6  128%
c i   28.3   11954    67365     96283   43480  13242 17641    8   120   13   7%    106   27    8    6  127%
c i   29.1   11953    67365    100930   47548  13337 17662    8   105   14   8%      6   12    9    6  139%
c i   29.5   11952    67364    102976   49333  13383 17675    8   113   14   7%    -26   19    7    6  120%
c i   30.1   11951    67363    106124   52121  13465 17696    8   117   14   7%    -16   23    7    6  116%
c i   30.4   11950    67363    107951   53745  13507 17704    8   104   15   8%    -29    9    8    6  129%
c i   30.8   11949    67363    110079   55638  13543 17721    8   112   16   7%    -27   16    8    6  120%
c i   31.3   11948    67363    112853   58141  13608 17733    8   102   16   8%    -18    6    8    6  122%
c i   33.6   11947    67363    125501   69577  13791 17776    8    97   17   9%    127   -1    8    7  122%
c i   35.3   11946    67363    133872   77094  13936 17800    8   106   17   8%     58    7    8    7  121%
c 
c [simplification-9] limit of 28 iterations hit after 28 iterations
c [quatres-5] found 23574 quaternary clauses 42% in total
c [quatres-5-1] removed 7 duplicate quaternary clauses
c [quatres-5-1] added 11 double-self-subsuming ternary resolvents
c [quatres-5-2] added 190 single-self-subsuming ternary resolvents
c [quatres-5-2] added 386 quaternary resolvents
c [ternres-5] limit 7712107 with penalty 0 = 0 + 0
c [ternres-5] all 11946 free variables schedulable
c [ternres-5] 2729 ternary resolvents (123 bin, 2606 trn)
c [ternres-5] 3 variables remain 0% (11943 retained 100%)
c [decomp-18] removed 56 variables
c [treelook-3] limit 192802 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 11036 literals 46%
c [treelook-3] scheduling used 192884 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 192802 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 192809 steps
c [treelook-3] 10999 literals remain 46%
c [treelook-3] 8021 variables remain to probed next time 67%
c [decomp-19] removed 4 variables
c [treelook-3] removed 5 variables, found 280 hbrs
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 338 transitive binary clauses
c [transred-5] found 7 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 11888 variables 100%
c [elim-7] limit of 77121076 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 104 variables 1% in round 1 in 25052522 steps
c [elim-7-1] backward subsumption/strengthening limit 25052500
c [elim-7-1-1] backward checking 618 touched variables 5%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 1 and strengthened 8 clauses in 2157713 steps
c [elim-7-1] rescheduled 31 variables 0% by backward subsumption
c [elim-7-2] eliminated 1 variables 0% in round 2 in 49680 steps
c [elim-7-2] backward subsumption/strengthening limit 49600
c [elim-7-2-1] backward checking 10 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 34722 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 106 = 1% variables out of 11888 scheduled
c [elim-7] 106 < 1/100 * 11888 = 118 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 23136320 penalty 0 = 0 + 0
c [sweep-5-1] 3660 pos 43.2% + 4804 neg 56.8% = 8464 sched 71.8% ret 3318
c [sweep-5-1] 23210838 steps 764 queries 48.60 avg class size
c [sweep-5-1] 15046 decisions 670 SAT calls 57.96 avg env size
c [sweep-5-1] 1570 variables remain 13% (10209 retained 87%)
c [decomp-20] removed 251 variables
c [sweep-5-1] removed 251 vars (0 failed, 235 eqs, 238 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 251 vars in TOTAL (1 rounds, 763 queries)
c [sort-queue-9] sorted 11531 enqueued variables after 133872 conflicts
c [score-dist-9] active 0 (0%), one 11528 (100%), zero 3 (0%)
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 415 variables 3.5% (11531 remain 22%)
c [simplification-9] removed 884 irredundant clauses 1.3% (66479 remain 44%)
c [simplification-9] maximum reduction of 3% = max (3%, 1%)
c [simplification-9] forced so keeping old conflict interval 61998
c [simplification-9] conflict limit remains at 150976 (hard 181970)
c [simplification-9] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   37.4   11530    66479    134307   76855  15119 17969    8   107   20   8%     19    8    8    7  113%
c i   37.8   11529    66477    136167   78459  15143 17982    9   106   20   8%    -29    7    8    7  115%
c -   38.1   11529    66475    137735   42720  15168 17988    9   105   14   8%    -38    5    9    7  128%
c 
c [simplification-10] limit 150976 conflicts (hard 181970) hit after 154160 conflicts
c [quatres-6] found 23902 quaternary clauses 40% in total
c [quatres-6-1] removed 17 duplicate quaternary clauses
c [quatres-6-1] added 17 double-self-subsuming ternary resolvents
c [quatres-6-2] added 220 single-self-subsuming ternary resolvents
c [quatres-6-2] added 330 quaternary resolvents
c [ternres-6] limit 8498423 with penalty 0 = 0 + 0
c [ternres-6] 2 schedulable variables 0%
c [ternres-6] 524 ternary resolvents (10 bin, 514 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 531151 penalty 3 = 3 + 0
c [card-4] found 154 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 531151 for elimination
c [card-4] 154 out of 154 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 697 xors of average arity 3.0
c [gauss-3] connected 2077 occurrences of 606 variables (average 3.4)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-21] removed 10 variables
c [basicprobe-3] limit 42492119 penalty 0 = 0 + 0
c [basicprobe-3-0] 1949 sched 17%, 13 failed, 0 lifted, 3834 hbrs
c [decomp-22] removed 24 variables
c [basicprobe-3-1] 6555 sched 57%, 33 failed, 0 lifted, 4970 hbrs
c [decomp-23] removed 67 variables
c [basicprobe-3-2] 6434 sched 56%, 0 failed, 0 lifted, 468 hbrs
c [basicprobe-3-3] 6427 sched 56%, 0 failed, 0 lifted, 73 hbrs
c [basicprobe-3-4] 4211 probes remain 37% after last round
c [basicprobe-3-4] 46 units = 46 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 91 variables, found 9346 hbrs
c [bate-2] eliminated 31 asymmetric tautologies during probing
c [unhide-6] limit 424921 with penalty 2 = 2 + 0
c [unhide-6-6] 0 units, 0 failed, 3707 tauts, 0 hbrs, 37329 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 706 transitive binary clauses
c [bca-5] limit of 10000000 steps and 132383 added (scaled 2)
c [bca-5] 3830 out of 22858 literals actually usable 17%
c [bca-5] added 0 blocked clauses in 64788 steps
c [sweep-6] limit 2549527 penalty 0 = 0 + 0
c [sweep-6-1] 698 pos 45.7% + 829 neg 54.3% = 1527 sched 13.4% ret 9901
c [sweep-6-1] 2576255 steps 192 queries 76.64 avg class size
c [sweep-6-1] 2604 decisions 162 SAT calls 41.63 avg env size
c [sweep-6-1] 1116 variables remain 10% (10312 retained 90%)
c [decomp-26] removed 95 variables
c [sweep-6-1] removed 95 vars (0 failed, 66 eqs, 53 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 95 vars in TOTAL (1 rounds, 191 queries)
c [sort-queue-10] sorted 11333 enqueued variables after 154160 conflicts
c [score-dist-10] active 0 (0%), one 11331 (100%), zero 2 (0%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 196 variables 1.7% (11333 remain 22%)
c [simplification-10] removed 631 irredundant clauses 0.9% (65841 remain 43%)
c [simplification-10] maximum reduction of 2% = max (2%, 1%)
c [simplification-10] geometric conflict interval increment 20666 = 61998 / 3
c [simplification-10] new conflict interval 82664
c [simplification-10] penalized conflict interval 82664 = 1 * 82664
c [simplification-10] hard conflict limit 278156 (soft 236824 + delta 41332)
c [simplification-10] new conflict limit 236824 (hard 278156)
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 -   45.6   11333    65831    190629   59520  14390 21605    8    96   21   8%    546    5    7    7   92%
c i   46.7   11332    65831    202820   70840  14427 21616    8    76   24  10%    627  -10    8    7  113%
c i   51.0   11331    65828    231302   97275  14625 21648    8    75   21  10%     82   -3    4    7   62%
c -   51.1   11331    65828    232136   66964  14627 21648    8   102   16   8%   -153   24    7    7  103%
c i   53.2   11330    65827    248046   81389  14708 21670    8    50   19  15%    -56  -28    6    7   86%
c -   55.9   11330    65827    272607   73050  14773 21678    7    35   24  20%     99  -31    8    7  112%
c 
c [simplification-11] limit 236824 conflicts (hard 278156) hit after 276402 conflicts
c [quatres-7] found 25035 quaternary clauses 33% in total
c [quatres-7-1] removed 29 duplicate quaternary clauses
c [quatres-7-1] added 15 double-self-subsuming ternary resolvents
c [quatres-7-2] added 280 single-self-subsuming ternary resolvents
c [quatres-7-2] added 488 quaternary resolvents
c [ternres-7] limit 13407145 with penalty 0 = 0 + 0
c [ternres-7] all 11330 free variables schedulable
c [ternres-7] 5669 ternary resolvents (231 bin, 5438 trn)
c [ternres-7] 1 variables remain 0% (11329 retained 100%)
c [decomp-27] removed 92 variables
c [simpleprobe-4] 652 schedulable variables 6%
c [simpleprobe-4] limit 53628580 penalty 0 = 0 + 0
c [decomp-28] removed 38 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 38 variables, found 3325 hbrs, 6 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 997 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 11203 variables 100%
c [block-4] limit of 33517862 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 1011 blocked clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 167589312 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 1 clauses out of 91 (1%) of length 12
c [cce-4-1] eliminated 5 clauses out of 119 (4%) of length 11
c [cce-4-1] eliminated 6 clauses out of 225 (3%) of length 10
c [cce-4-1] eliminated 20 clauses out of 402 (5%) of length 9
c [cce-4-1] eliminated 26 clauses out of 722 (4%) of length 8
c [cce-4-1] eliminated 63 clauses out of 1417 (4%) of length 7
c [cce-4-1] eliminated 228 clauses out of 2921 (8%) of length 6
c [cce-4-1] eliminated 777 clauses out of 6559 (12%) of length 5
c [cce-4-1] eliminated 1482 clauses out of 14583 (10%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 2608 large clauses in 91149278 steps
c [cce-4-1] allowing another 45574639 steps for small clauses
c [cce-4-1] scheduling 28625 clauses = 12395 binary + 16230 ternary
c [cce-4-1] tried to eliminate 28625 small clauses 100%
c [cce-4-1] eliminated 283 binary clauses 2%
c [cce-4-1] eliminated 760 ternary clauses 5%
c [cce-4-1] eliminated 1043 small clauses 4%
c [cce-4-1] eliminated 1043 small clauses in 103120258 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 3651 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 32234528 steps for small clauses
c [cce-4-2] scheduling 27582 clauses = 12112 binary + 15470 ternary
c [cce-4-2] tried to eliminate 7722 small clauses 28%
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 3651 covered clauses in TOTAL during 2 rounds
c [sweep-7] limit 4022143 penalty 0 = 0 + 0
c [sweep-7-1] 385 pos 37.7% + 637 neg 62.3% = 1022 sched 9.2% ret 10067
c [sweep-7-1] 4022354 steps 124 queries 85.48 avg class size
c [sweep-7-1] 2099 decisions 109 SAT calls 39.80 avg env size
c [sweep-7-1] 780 variables remain 7% (10309 retained 93%)
c [decomp-29] removed 39 variables
c [sweep-7-1] removed 39 vars (0 failed, 35 eqs, 32 impls)
c [sweep-7] removed 39 vars in TOTAL (1 rounds, 123 queries)
c [sort-queue-11] sorted 11050 enqueued variables after 276402 conflicts
c [score-dist-11] active 0 (0%), one 11048 (100%), zero 2 (0%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 280 variables 2.5% (11050 remain 21%)
c [simplification-11] removed 5119 irredundant clauses 7.8% (60708 remain 40%)
c [simplification-11] maximum reduction of 8% = max (2%, 8%)
c [simplification-11] large reduction 8% >= 5% limit
c [simplification-11] next conflict interval 2764 = min (276402/100, 82664)
c [simplification-11] penalized conflict interval 2764 = 1 * 2764
c [simplification-11] hard conflict limit 289166 (soft 279166 + delta 10000)
c [simplification-11] new conflict limit 279166 (hard 289166)
c 
c [simplification-12] limit 279166 conflicts (hard 289166) hit after 279166 conflicts
c [quatres-8] found 23341 quaternary clauses 32% in total
c [quatres-8-1] removed 48 duplicate quaternary clauses
c [quatres-8-1] added 14 double-self-subsuming ternary resolvents
c [quatres-8-2] added 191 single-self-subsuming ternary resolvents
c [quatres-8-2] added 225 quaternary resolvents
c [ternres-8] limit 13557963 with penalty 0 = 0 + 0
c [ternres-8] 1 schedulable variables 0%
c [ternres-8] 795 ternary resolvents (28 bin, 767 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-30] removed 15 variables
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 698 transitive binary clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 11035 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1355796325 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 664 variables 6% in round 1 in 20907110 steps
c [elim-8-1] backward subsumption/strengthening limit 20907100
c [elim-8-1-1] backward checking 2927 touched variables 27%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 2 and strengthened 42 clauses in 2445573 steps
c [elim-8-1] rescheduled 79 variables 1% by backward subsumption
c [elim-8-2] eliminated 3 variables 0% in round 2 in 519773 steps
c [elim-8-2] backward subsumption/strengthening limit 519700
c [elim-8-2-1] backward checking 27 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 6 clauses in 85229 steps
c [elim-8-2] rescheduled 9 variables 0% by backward subsumption
c [elim-8-3] eliminated 2 variables 0% in round 3 in 196541 steps
c [elim-8-3] backward subsumption/strengthening limit 196500
c [elim-8-3-1] backward checking 7 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 1 and strengthened 2 clauses in 62137 steps
c [elim-8] incomplete 7 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 670 = 6% variables out of 11035 scheduled
c [sweep-8] limit 4067388 penalty 0 = 0 + 0
c [sweep-8-1] 269 pos 38.9% + 422 neg 61.1% = 691 sched 6.7% ret 9674
c [sweep-8-1] 4098947 steps 211 queries 29.27 avg class size
c [sweep-8-1] 2886 decisions 187 SAT calls 39.59 avg env size
c [sweep-8-1] 282 variables remain 3% (10083 retained 97%)
c [decomp-31] removed 57 variables
c [sweep-8-1] removed 57 vars (0 failed, 54 eqs, 47 impls)
c [sweep-8] removed 57 vars in TOTAL (1 rounds, 210 queries)
c [sort-queue-12] sorted 10308 enqueued variables after 279166 conflicts
c [score-dist-12] active 0 (0%), one 10308 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 742 variables 6.7% (10308 remain 20%)
c [simplification-12] removed 1962 irredundant clauses 3.2% (58746 remain 39%)
c [simplification-12] maximum reduction of 7% = max (7%, 3%)
c [simplification-12] large reduction 7% >= 5% limit
c [simplification-12] next conflict interval 2791 = min (279166/100, 82664)
c [simplification-12] penalized conflict interval 2791 = 1 * 2791
c [simplification-12] hard conflict limit 291957 (soft 281957 + delta 10000)
c [simplification-12] new conflict limit 281957 (hard 291957)
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   62.6   10307    58746    280067   71383  19114 18390    8    70   18  11%    198    5    9    7  119%
c i   63.0   10306    58746    285728   76510  19171 18413    7    69   18  11%   -197    4    8    7  104%
c i   63.0   10305    58746    285729   76510  19171 18413    7    69   18  11%   -197    4    8    7  104%
c 
c [simplification-13] limit 281967 conflicts (hard 291957) hit after 291957 conflicts
c [quatres-9] found 22923 quaternary clauses 32% in total
c [quatres-9-1] removed 15 duplicate quaternary clauses
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 78 single-self-subsuming ternary resolvents
c [quatres-9-2] added 373 quaternary resolvents
c [ternres-9] limit 13981190 with penalty 0 = 0 + 0
c [ternres-9] all 10305 free variables schedulable
c [ternres-9] 2419 ternary resolvents (128 bin, 2291 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-32] removed 37 variables
c [treelook-4] limit 699059 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 16397 literals 80%
c [treelook-4] scheduling used 465134 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 699059 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 706340 steps
c [treelook-4] 16320 literals remain 79%
c [treelook-4] 6796 variables remain to probed next time 66%
c [decomp-33] removed 1 variables
c [treelook-4] removed 4 variables, found 1841 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 577 transitive binary clauses
c [transred-9] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 10266 variables 100%
c [block-5] limit of 69905951 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 654 blocked clauses
c [cce-5] limit of 34952975 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 1 clauses out of 35 (3%) of length 14
c [cce-5-1] eliminated 4 clauses out of 80 (5%) of length 12
c [cce-5-1] eliminated 4 clauses out of 141 (3%) of length 11
c [cce-5-1] eliminated 11 clauses out of 209 (5%) of length 10
c [cce-5-1] eliminated 18 clauses out of 395 (5%) of length 9
c [cce-5-1] eliminated 49 clauses out of 754 (6%) of length 8
c [cce-5-1] eliminated 17 clauses out of 1357 (1%) of length 7
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 104 large clauses in 34952979 steps
c [cce-5-1] allowing another 17476489 steps for small clauses
c [cce-5-1] scheduling 19236 clauses = 11049 binary + 8187 ternary
c [cce-5-1] tried to eliminate 2999 small clauses 16%
c [cce-5-1] eliminated 53 binary clauses 0%
c [cce-5-1] eliminated 100 ternary clauses 1%
c [cce-5-1] eliminated 153 small clauses 1%
c [cce-5-1] eliminated 153 small clauses in 34952975 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 257 covered clauses in round 1
c [cce-5] eliminated 257 covered clauses in TOTAL during 1 rounds
c [cce-5] 257 < 1/100 * 57960 = 579 considered unsuccessful
c [bca-6] limit of 10000000 steps and 115931 added (scaled 2)
c [bca-6] 2910 out of 20456 literals actually usable 14%
c [bca-6] added 8 blocked clauses in 88107 steps
c [sweep-9] limit 4194357 penalty 0 = 0 + 0
c [sweep-9-1] 101 pos 36.7% + 174 neg 63.3% = 275 sched 2.7% ret 9952
c [sweep-9-1] 3295253 steps 179 queries 14.35 avg class size
c [sweep-9-1] 2402 decisions 148 SAT calls 34.27 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-34] removed 57 variables
c [sweep-9-1] removed 57 vars (0 failed, 54 eqs, 45 impls)
c [sweep-9-2] 4554 pos 44.8% + 5616 neg 55.2% = 10170 sched 100.0% ret 0
c [sweep-9-2] 914716 steps 28 queries 1434.71 avg class size
c [sweep-9-2] 902 decisions 26 SAT calls 108.58 avg env size
c [sweep-9-2] 9847 variables remain 97% (323 retained 3%)
c [decomp-35] removed 4 variables
c [sweep-9-2] removed 4 vars (0 failed, 3 eqs, 3 impls)
c [sweep-9] removed 61 vars in TOTAL (2 rounds, 205 queries)
c [sort-queue-13] sorted 10166 enqueued variables after 291957 conflicts
c [score-dist-13] active 0 (0%), one 10166 (100%), zero 0 (0%)
c [score-dist-13] max exp 1, different 1 (50%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 139 variables 1.3% (10166 remain 20%)
c [simplification-13] removed 1156 irredundant clauses 2.0% (57588 remain 38%)
c [simplification-13] maximum reduction of 2% = max (1%, 2%)
c [simplification-13] geometric conflict interval increment 27554 = 82664 / 3
c [simplification-13] new conflict interval 110218
c [simplification-13] penalized conflict interval 110218 = 1 * 110218
c [simplification-13] hard conflict limit 457284 (soft 402175 + delta 55109)
c [simplification-13] new conflict limit 402175 (hard 457284)
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   67.3   10165    57588    292178   81793  20609 18734    7   100   20   7%   -166   35    8    7  114%
c i   68.9   10164    57582    304076   92940  20640 18740    7    46   20  16%    -54  -18    8    7  115%
c i   68.9   10163    57582    304077   92940  20640 18740    7    46   20  16%    -54  -18    8    7  114%
c -   71.9   10163    57581    319558   73459  20737 18768    9    67   16  14%     24    2   10    7  130%
c -   79.2   10163    57581    361249   77429  20900 18801    9    47   24  19%    495  -13   10    8  130%
c i   85.6   10162    57581    399491  113581  20966 18810   10    44   30  22%    729   -5   10    8  126%
c -   86.6   10162    57581    402107   81157  20979 18811   10    45   24  22%   -598   -4   10    8  120%
c -   93.4   10162    57581    444089   86506  21033 18819    9    37   25  25%    108   -7   10    8  117%
c 
c [simplification-14] limit 402185 conflicts (hard 457284) hit after 445573 conflicts
c [quatres-10] found 23820 quaternary clauses 28% in total
c [quatres-10-1] removed 26 duplicate quaternary clauses
c [quatres-10-1] added 6 double-self-subsuming ternary resolvents
c [quatres-10-2] added 137 single-self-subsuming ternary resolvents
c [quatres-10-2] added 220 quaternary resolvents
c [ternres-10] limit 23529470 with penalty 0 = 0 + 0
c [ternres-10] all 10162 free variables schedulable
c [ternres-10] 2674 ternary resolvents (104 bin, 2570 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 588236 penalty 3 = 3 + 0
c [gauss-4] extracted 618 xors of average arity 3.0
c [gauss-4] connected 1836 occurrences of 486 variables (average 3.8)
c [gauss-4] limit 588236 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 32 variables
c [basicprobe-4] limit 117647350 penalty 0 = 0 + 0
c [basicprobe-4-0] 3973 sched 39%, 28 failed, 8 lifted, 3840 hbrs
c [decomp-37] removed 52 variables
c [basicprobe-4-1] 5799 sched 58%, 9 failed, 0 lifted, 1933 hbrs
c [decomp-38] removed 18 variables
c [basicprobe-4-2] 5784 sched 57%, 0 failed, 0 lifted, 192 hbrs
c [basicprobe-4-3] 5781 sched 57%, 0 failed, 0 lifted, 46 hbrs
c [basicprobe-4-4] 5783 sched 57%, 0 failed, 0 lifted, 14 hbrs
c [decomp-41] removed 1 variables
c [basicprobe-4-5] 5782 sched 57%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-4-6] 5782 sched 57%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-4-7] 5783 sched 57%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-4-8] 5783 sched 57%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 45 units = 37 failed (82%) + 8 lifted (18%)
c [basicprobe-4-8] removed 71 variables, found 6052 hbrs
c [bate-3] eliminated 33 asymmetric tautologies during probing
c [unhide-7] limit 588236 with penalty 3 = 3 + 0
c [unhide-7-7] 0 units, 0 failed, 664 tauts, 0 hbrs, 18781 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 695 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 10059 variables 100%
c [block-6] limit of 235294701 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 2401 blocked clauses
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 9801 variables 100%
c [elim-9] limit of 235294701 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 553 variables 6% in round 1 in 19000599 steps
c [elim-9-1] backward subsumption/strengthening limit 19000500
c [elim-9-1-1] backward checking 1771 touched variables 18%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 6 and strengthened 6 clauses in 1869668 steps
c [elim-9-1] rescheduled 34 variables 0% by backward subsumption
c [elim-9-2] eliminated 3 variables 0% in round 2 in 87631 steps
c [elim-9-2] backward subsumption/strengthening limit 87600
c [elim-9-2-1] backward checking 13 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 1 and strengthened 0 clauses in 38866 steps
c [elim-9-2] rescheduled 4 variables 0% by backward subsumption
c [elim-9-3] eliminated 3 variables 0% in round 3 in 3097 steps
c [elim-9-3] backward subsumption/strengthening limit 3000
c [elim-9-3-1] backward checking 8 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 0 and strengthened 0 clauses in 3001 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 559 = 6% variables out of 9801 scheduled
c [sweep-10] limit 7058841 penalty 0 = 0 + 0
c [sweep-10-1] 3913 pos 43.8% + 5021 neg 56.2% = 8934 sched 96.7% ret 308
c [sweep-10-1] 7108542 steps 213 queries 288.07 avg class size
c [sweep-10-1] 4706 decisions 195 SAT calls 68.47 avg env size
c [sweep-10-1] 5619 variables remain 61% (3623 retained 39%)
c [decomp-45] removed 38 variables
c [sweep-10-1] removed 38 vars (0 failed, 35 eqs, 38 impls)
c [sweep-10] removed 38 vars in TOTAL (1 rounds, 212 queries)
c [sort-queue-14] sorted 9204 enqueued variables after 445573 conflicts
c [score-dist-14] active 0 (0%), one 9204 (100%), zero 0 (0%)
c [score-dist-14] max exp 1, different 1 (50%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 958 variables 9.4% (9204 remain 18%)
c [simplification-14] removed 4748 irredundant clauses 8.2% (52833 remain 35%)
c [simplification-14] maximum reduction of 9% = max (9%, 8%)
c [simplification-14] large reduction 9% >= 5% limit
c [simplification-14] next conflict interval 4455 = min (445573/100, 110218)
c [simplification-14] penalized conflict interval 4455 = 1 * 4455
c [simplification-14] hard conflict limit 460028 (soft 450028 + delta 10000)
c [simplification-14] new conflict limit 450028 (hard 460028)
c 
c [simplification-15] limit 450028 conflicts (hard 460028) hit after 450029 conflicts
c [quatres-11] found 22429 quaternary clauses 28% in total
c [quatres-11-1] removed 21 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 99 single-self-subsuming ternary resolvents
c [quatres-11-2] added 277 quaternary resolvents
c [ternres-11] limit 23690625 with penalty 0 = 0 + 0
c [ternres-11] all 9204 free variables schedulable
c [ternres-11] 1647 ternary resolvents (98 bin, 1549 trn)
c [ternres-11] 1 variables remain 0% (9203 retained 100%)
c [card-5] limit 740332 penalty 4 = 4 + 0
c [card-5] found 172 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 740332 for elimination
c [card-5] 172 out of 172 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-46] removed 15 variables
c [simpleprobe-5] all 9189 free variables schedulable
c [simpleprobe-5] limit 94762501 penalty 0 = 0 + 0
c [decomp-47] removed 30 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 30 variables, found 2399 hbrs, 1 units
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 889 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 9159 variables 100%
c [block-7] limit of 236906253 steps penalty 0 = 0 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 2061 blocked clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 8926 variables 100%
c [elim-10] limit of 473812507 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 347 variables 4% in round 1 in 16956989 steps
c [elim-10-1] backward subsumption/strengthening limit 16956900
c [elim-10-1-1] backward checking 987 touched variables 11%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 6 and strengthened 2 clauses in 1457571 steps
c [elim-10-1] rescheduled 28 variables 0% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 27884 steps
c [elim-10-2] backward subsumption/strengthening limit 27800
c [elim-10-2-1] backward checking 9 touched variables 0%
c [elim-10-2-1] incomplete backward checking 4 remain 44%
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 29029 steps
c [elim-10-2] fully rescheduled 8578 variables 96%
c [elim-10-3] eliminated 192 variables 2% in round 3 in 16051380 steps
c [elim-10-3] backward subsumption/strengthening limit 16051300
c [elim-10-3-1] backward checking 414 touched variables 5%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 0 and strengthened 5 clauses in 6402556 steps
c [elim-10] incomplete 15 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 540 = 6% variables out of 8926 scheduled
c [bca-7] limit of 10000000 steps and 97161 added (scaled 2)
c [bca-7] 2624 out of 16774 literals actually usable 16%
c [bca-7] added 70 blocked clauses in 90713 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 71071870 penalty 0 = 0 + 0
c [sweep-11-1] 2251 pos 45.7% + 2674 neg 54.3% = 4925 sched 58.7% ret 3461
c [sweep-11-1] 27553175 steps 1005 queries 28.10 avg class size
c [sweep-11-1] 16182 decisions 906 SAT calls 52.61 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-48] removed 244 variables
c [sweep-11-1] removed 244 vars (0 failed, 262 eqs, 250 impls)
c [sweep-11-2] 3514 pos 43.2% + 4628 neg 56.8% = 8142 sched 100.0% ret 0
c [sweep-11-2] 26146020 steps 995 queries 33.85 avg class size
c [sweep-11-2] 16596 decisions 948 SAT calls 53.88 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-49] removed 145 variables
c [sweep-11-2] removed 145 vars (0 failed, 171 eqs, 140 impls)
c [sweep-11-3] 3452 pos 43.2% + 4545 neg 56.8% = 7997 sched 100.0% ret 0
c [sweep-11-3] 17380330 steps 656 queries 47.39 avg class size
c [sweep-11-3] 12221 decisions 648 SAT calls 58.25 avg env size
c [sweep-11-3] 639 variables remain 8% (7357 retained 92%)
c [decomp-50] removed 41 variables
c [sweep-11-3] removed 41 vars (0 failed, 53 eqs, 30 impls)
c [sweep-11] removed 430 vars in TOTAL (3 rounds, 2653 queries)
c [sort-queue-15] sorted 7956 enqueued variables after 450029 conflicts
c [score-dist-15] active 0 (0%), one 7956 (100%), zero 0 (0%)
c [score-dist-15] max exp 1, different 1 (50%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 1248 variables 13.6% (7956 remain 15%)
c [simplification-15] removed 4888 irredundant clauses 9.3% (47944 remain 32%)
c [simplification-15] maximum reduction of 14% = max (14%, 9%)
c [simplification-15] large reduction 14% >= 5% limit
c [simplification-15] next conflict interval 4500 = min (450029/100, 110218)
c [simplification-15] penalized conflict interval 4500 = 1 * 4500
c [simplification-15] hard conflict limit 464529 (soft 454529 + delta 10000)
c [simplification-15] new conflict limit 454529 (hard 464529)
c 
c [simplification-16] limit 454529 conflicts (hard 464529) hit after 464529 conflicts
c [quatres-12] found 20607 quaternary clauses 26% in total
c [quatres-12-1] removed 133 duplicate quaternary clauses
c [quatres-12-1] added 5 double-self-subsuming ternary resolvents
c [quatres-12-2] added 120 single-self-subsuming ternary resolvents
c [quatres-12-2] added 446 quaternary resolvents
c [ternres-12] limit 24414602 with penalty 0 = 0 + 0
c [ternres-12] 1 schedulable variables 0%
c [ternres-12] 2777 ternary resolvents (17 bin, 2760 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-51] removed 1 variables
c [treelook-5] limit 2441460 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 13002 literals 82%
c [treelook-5] scheduling used 459261 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2441460 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2446713 steps
c [treelook-5] 12525 literals remain 79%
c [treelook-5] 5332 variables remain to probed next time 67%
c [decomp-52] removed 2 variables
c [treelook-5] removed 6 variables, found 2879 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1277 transitive binary clauses
c [transred-12] found 3 units
c [block-8] scheduling all variables this time
c [block-8] scheduled 7946 variables 100%
c [block-8] limit of 244146029 steps penalty 0 = 0 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 658 blocked clauses
c [cce-6] limit of 30518253 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 2 clauses out of 18 (11%) of length 15
c [cce-6-1] eliminated 4 clauses out of 28 (14%) of length 14
c [cce-6-1] eliminated 2 clauses out of 51 (4%) of length 13
c [cce-6-1] eliminated 3 clauses out of 75 (4%) of length 12
c [cce-6-1] eliminated 13 clauses out of 118 (11%) of length 11
c [cce-6-1] eliminated 29 clauses out of 173 (17%) of length 10
c [cce-6-1] eliminated 27 clauses out of 353 (8%) of length 9
c [cce-6-1] eliminated 39 clauses out of 616 (6%) of length 8
c [cce-6-1] eliminated 118 clauses out of 1123 (11%) of length 7
c [cce-6-1] eliminated 299 clauses out of 2456 (12%) of length 6
c [cce-6-1] eliminated 514 clauses out of 4865 (11%) of length 5
c [cce-6-1] eliminated 182 clauses out of 10393 (2%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 1232 large clauses in 30518261 steps
c [cce-6-1] allowing another 15259130 steps for small clauses
c [cce-6-1] scheduling 19822 clauses = 8800 binary + 11022 ternary
c [cce-6-1] tried to eliminate 8716 small clauses 44%
c [cce-6-1] eliminated 83 binary clauses 1%
c [cce-6-1] eliminated 223 ternary clauses 2%
c [cce-6-1] eliminated 306 small clauses 2%
c [cce-6-1] eliminated 306 small clauses in 30519589 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1538 covered clauses in round 1
c [cce-6] eliminated 1538 covered clauses in TOTAL during 1 rounds
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 7894 variables 100%
c [elim-11] limit of 488292058 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 418 variables 5% in round 1 in 13321437 steps
c [elim-11-1] backward subsumption/strengthening limit 13321400
c [elim-11-1-1] backward checking 1625 touched variables 21%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 6 and strengthened 8 clauses in 2080388 steps
c [elim-11-1] rescheduled 54 variables 1% by backward subsumption
c [elim-11-2] eliminated 4 variables 0% in round 2 in 2725703 steps
c [elim-11-2] backward subsumption/strengthening limit 2725700
c [elim-11-2-1] backward checking 36 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 2 clauses in 763008 steps
c [elim-11-2] rescheduled 10 variables 0% by backward subsumption
c [elim-11-3] eliminated 2 variables 0% in round 3 in 13141 steps
c [elim-11-3] backward subsumption/strengthening limit 13100
c [elim-11-3-1] backward checking 28 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 0 and strengthened 0 clauses in 13101 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 424 = 5% variables out of 7894 scheduled
c [bca-8] limit of 10000000 steps and 87512 added (scaled 2)
c [bca-8] 2393 out of 14942 literals actually usable 16%
c [bca-8] added 59 blocked clauses in 98919 steps
c [sweep-12] limit 7324380 penalty 0 = 0 + 0
c [sweep-12-1] 241 pos 42.5% + 326 neg 57.5% = 567 sched 7.6% ret 6903
c [sweep-12-1] 7048370 steps 274 queries 13.52 avg class size
c [sweep-12-1] 4142 decisions 253 SAT calls 55.27 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-53] removed 30 variables
c [sweep-12-1] removed 30 vars (0 failed, 38 eqs, 26 impls)
c [sweep-12-2] 3143 pos 42.2% + 4297 neg 57.8% = 7440 sched 100.0% ret 0
c [sweep-12-2] 305416 steps 10 queries 1230.20 avg class size
c [sweep-12-2] 149 decisions 9 SAT calls 83.33 avg env size
c [sweep-12-2] 7390 variables remain 99% (50 retained 1%)
c [sweep-12-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-12] removed 30 vars in TOTAL (2 rounds, 282 queries)
c [sort-queue-16] sorted 7440 enqueued variables after 464529 conflicts
c [score-dist-16] active 0 (0%), one 7440 (100%), zero 0 (0%)
c [score-dist-16] max exp 1, different 1 (50%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 516 variables 6.5% (7440 remain 14%)
c [simplification-16] removed 4485 irredundant clauses 9.4% (43458 remain 29%)
c [simplification-16] maximum reduction of 9% = max (6%, 9%)
c [simplification-16] large reduction 9% >= 5% limit
c [simplification-16] next conflict interval 4645 = min (464529/100, 110218)
c [simplification-16] penalized conflict interval 4645 = 1 * 4645
c [simplification-16] hard conflict limit 479174 (soft 469174 + delta 10000)
c [simplification-16] new conflict limit 469174 (hard 479174)
c 
c [simplification-17] limit 469174 conflicts (hard 479174) hit after 474622 conflicts
c [quatres-13] found 19244 quaternary clauses 26% in total
c [quatres-13-1] removed 26 duplicate quaternary clauses
c [quatres-13-1] added 10 double-self-subsuming ternary resolvents
c [quatres-13-2] added 94 single-self-subsuming ternary resolvents
c [quatres-13-2] added 273 quaternary resolvents
c [ternres-13] limit 25137545 with penalty 0 = 0 + 0
c [ternres-13] all 7440 free variables schedulable
c [ternres-13] 1914 ternary resolvents (72 bin, 1842 trn)
c [ternres-13] 7 variables remain 0% (7433 retained 100%)
c [decomp-55] removed 2 variables
c [basicprobe-5] limit 125687726 penalty 0 = 0 + 0
c [basicprobe-5-0] 4221 sched 57%, 6 failed, 0 lifted, 778 hbrs
c [decomp-56] removed 11 variables
c [basicprobe-5-1] 4183 sched 56%, 0 failed, 0 lifted, 35 hbrs
c [basicprobe-5-2] 4182 sched 56%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-5-3] 4182 sched 56%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-5-4] 4182 sched 56%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-5] 4182 sched 56%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-5-6] 4182 sched 56%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-5-7] 4182 sched 56%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-7] fully completed probing
c [basicprobe-5-7] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-5-7] removed 11 variables, found 838 hbrs
c [bate-4] eliminated 32 asymmetric tautologies during probing
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 830 transitive binary clauses
c [block-9] scheduling all variables this time
c [block-9] scheduled 7427 variables 100%
c [block-9] limit of 251375452 steps penalty 0 = 0 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 139 blocked clauses
c [block-9] 139 < 1/100 * 43353 = 433 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 7407 variables 100%
c [elim-12] limit of 502750905 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 100 variables 1% in round 1 in 12853754 steps
c [elim-12-1] backward subsumption/strengthening limit 12853700
c [elim-12-1-1] backward checking 440 touched variables 6%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 4 and strengthened 1 clauses in 979661 steps
c [elim-12-1] rescheduled 20 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 677797 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 100 = 1% variables out of 7407 scheduled
c [bca-9] limit of 10000000 steps and 86256 added (scaled 2)
c [bca-9] 2262 out of 14616 literals actually usable 15%
c [bca-9] added 19 blocked clauses in 107619 steps
c [sweep-13] limit 7541263 penalty 0 = 0 + 0
c [sweep-13-1] 3106 pos 42.8% + 4151 neg 57.2% = 7257 sched 99.3% ret 50
c [sweep-13-1] 7544372 steps 180 queries 120.11 avg class size
c [sweep-13-1] 4956 decisions 179 SAT calls 78.72 avg env size
c [sweep-13-1] 3643 variables remain 50% (3664 retained 50%)
c [decomp-63] removed 7 variables
c [sweep-13-1] removed 7 vars (0 failed, 7 eqs, 2 impls)
c [sweep-13] removed 7 vars in TOTAL (1 rounds, 179 queries)
c [sort-queue-17] sorted 7300 enqueued variables after 474622 conflicts
c [score-dist-17] active 0 (0%), one 7300 (100%), zero 0 (0%)
c [score-dist-17] max exp 1, different 1 (50%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 140 variables 1.9% (7300 remain 14%)
c [simplification-17] removed 630 irredundant clauses 1.4% (42827 remain 28%)
c [simplification-17] maximum reduction of 2% = max (2%, 1%)
c [simplification-17] geometric conflict interval increment 36739 = 110218 / 3
c [simplification-17] new conflict interval 146957
c [simplification-17] penalized conflict interval 146957 = 1 * 146957
c [simplification-17] hard conflict limit 695057 (soft 621579 + delta 73478)
c [simplification-17] new conflict limit 621579 (hard 695057)
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 -  115.1    7300    42827    490172   83151  20127 17668    8    43   16  19%    570   -1    8    8  103%
c -  121.5    7300    42826    531969   89024  20162 17669    7    35   25  20%    784   -6    7    8   92%
c -  129.0    7300    42826    569202   88599  20201 17676    8    84   25  10%    888   37   10    8  120%
c -  138.2    7300    42826    609916   88892  20233 17681    9    40   25  23%    951   -4    8    9   95%
c 
c [simplification-18] limit 621579 conflicts (hard 695057) hit after 628796 conflicts
c [quatres-14] found 19480 quaternary clauses 23% in total
c [quatres-14-1] removed 4 duplicate quaternary clauses
c [quatres-14-1] added 9 double-self-subsuming ternary resolvents
c [quatres-14-2] added 88 single-self-subsuming ternary resolvents
c [quatres-14-2] added 168 quaternary resolvents
c [ternres-14] limit 36081365 with penalty 0 = 0 + 0
c [ternres-14] 7 schedulable variables 0%
c [ternres-14] 2198 ternary resolvents (37 bin, 2161 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-64] removed 2 variables
c [simpleprobe-6] all 7298 free variables schedulable
c [simpleprobe-6] limit 144325461 penalty 0 = 0 + 0
c [decomp-65] removed 20 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 20 variables, found 1964 hbrs, 0 units
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 1093 transitive binary clauses
c [cce-7] limit of 90203413 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 3 clauses out of 25 (12%) of length 14
c [cce-7-1] eliminated 3 clauses out of 48 (6%) of length 13
c [cce-7-1] eliminated 5 clauses out of 78 (6%) of length 12
c [cce-7-1] eliminated 11 clauses out of 103 (11%) of length 11
c [cce-7-1] eliminated 9 clauses out of 145 (6%) of length 10
c [cce-7-1] eliminated 19 clauses out of 334 (6%) of length 9
c [cce-7-1] eliminated 65 clauses out of 643 (10%) of length 8
c [cce-7-1] eliminated 102 clauses out of 1076 (9%) of length 7
c [cce-7-1] eliminated 210 clauses out of 2165 (10%) of length 6
c [cce-7-1] eliminated 378 clauses out of 4251 (9%) of length 5
c [cce-7-1] eliminated 963 clauses out of 9674 (10%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 1768 large clauses in 56973028 steps
c [cce-7-1] allowing another 28486514 steps for small clauses
c [cce-7-1] scheduling 14265 clauses = 8018 binary + 6247 ternary
c [cce-7-1] tried to eliminate 14265 small clauses 100%
c [cce-7-1] eliminated 429 binary clauses 5%
c [cce-7-1] eliminated 646 ternary clauses 10%
c [cce-7-1] eliminated 1075 small clauses 8%
c [cce-7-1] eliminated 1075 small clauses in 56403090 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 2843 covered clauses in round 1
c [cce-7-2] eliminated 1 clauses out of 45 (2%) of length 13
c [cce-7-2] eliminated 1 clauses out of 73 (1%) of length 12
c [cce-7-2] eliminated 3 clauses out of 92 (3%) of length 11
c [cce-7-2] eliminated 2 clauses out of 136 (1%) of length 10
c [cce-7-2] eliminated 4 clauses out of 315 (1%) of length 9
c [cce-7-2] eliminated 4 clauses out of 578 (1%) of length 8
c [cce-7-2] eliminated 6 clauses out of 974 (1%) of length 7
c [cce-7-2] eliminated 11 clauses out of 1955 (1%) of length 6
c [cce-7-2] eliminated 38 clauses out of 3873 (1%) of length 5
c [cce-7-2] eliminated 11 clauses out of 8711 (0%) of length 4
c [cce-7-2] incomplete large round (ACCE)
c [cce-7-2] eliminated 81 large clauses in 33800399 steps
c [cce-7-2] allowing another 16900199 steps for small clauses
c [cce-7-2] scheduling 13190 clauses = 7589 binary + 5601 ternary
c [cce-7-2] tried to eliminate 6962 small clauses 53%
c [cce-7-2] eliminated 25 binary clauses 0%
c [cce-7-2] eliminated 16 ternary clauses 0%
c [cce-7-2] eliminated 41 small clauses 0%
c [cce-7-2] eliminated 41 small clauses in 33800333 steps
c [cce-7-2] incomplete small round (ACCE)
c [cce-7-2] eliminated 122 covered clauses in round 2
c [cce-7] eliminated 2965 covered clauses in TOTAL during 2 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 7278 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 520 variables 7% in round 1 in 10974707 steps
c [elim-13-1] backward subsumption/strengthening limit 10974700
c [elim-13-1-1] backward checking 1449 touched variables 20%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 2 and strengthened 10 clauses in 1095811 steps
c [elim-13-1] rescheduled 51 variables 1% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 936318 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 520 = 7% variables out of 7278 scheduled
c [bca-10] limit of 10000000 steps and 78405 added (scaled 2)
c [bca-10] 2048 out of 13518 literals actually usable 15%
c [bca-10] added 17 blocked clauses in 107983 steps
c [sweep-14] limit 10824409 penalty 0 = 0 + 0
c [sweep-14-1] 1381 pos 42.3% + 1885 neg 57.7% = 3266 sched 48.3% ret 3492
c [sweep-14-1] 10849187 steps 326 queries 51.57 avg class size
c [sweep-14-1] 6673 decisions 327 SAT calls 55.61 avg env size
c [sweep-14-1] 944 variables remain 14% (5814 retained 86%)
c [decomp-66] removed 24 variables
c [sweep-14-1] removed 24 vars (0 failed, 23 eqs, 16 impls)
c [sweep-14] removed 24 vars in TOTAL (1 rounds, 325 queries)
c [sort-queue-18] sorted 6734 enqueued variables after 628796 conflicts
c [score-dist-18] active 0 (0%), one 6734 (100%), zero 0 (0%)
c [score-dist-18] max exp 1, different 1 (50%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 566 variables 7.8% (6734 remain 13%)
c [simplification-18] removed 3938 irredundant clauses 9.2% (38888 remain 26%)
c [simplification-18] maximum reduction of 9% = max (8%, 9%)
c [simplification-18] large reduction 9% >= 5% limit
c [simplification-18] next conflict interval 6287 = min (628796/100, 146957)
c [simplification-18] penalized conflict interval 6287 = 1 * 6287
c [simplification-18] hard conflict limit 645083 (soft 635083 + delta 10000)
c [simplification-18] new conflict limit 635083 (hard 645083)
c 
c [simplification-19] limit 635083 conflicts (hard 645083) hit after 642860 conflicts
c [quatres-15] found 17880 quaternary clauses 22% in total
c [quatres-15-1] removed 18 duplicate quaternary clauses
c [quatres-15-1] added 1 double-self-subsuming ternary resolvents
c [quatres-15-2] added 94 single-self-subsuming ternary resolvents
c [quatres-15-2] added 242 quaternary resolvents
c [ternres-15] limit 36961469 with penalty 0 = 0 + 0
c [ternres-15] all 6734 free variables schedulable
c [ternres-15] 2107 ternary resolvents (68 bin, 2039 trn)
c [ternres-15] 1 variables remain 0% (6733 retained 100%)
c [gauss-5] limit 462018 penalty 4 = 4 + 0
c [gauss-5] extracted 183 xors of average arity 3.0
c [gauss-5] connected 549 occurrences of 181 variables (average 3.0)
c [gauss-5] limit 462018 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-67] removed 3 variables
c [treelook-6] limit 3696146 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 11044 literals 82%
c [treelook-6] scheduling used 470031 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3696146 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3700628 steps
c [treelook-6] 10506 literals remain 78%
c [treelook-6] 4463 variables remain to probed next time 66%
c [treelook-6] removed 1 variables, found 3967 hbrs
c [unhide-8] limit 462018 with penalty 4 = 4 + 0
c [unhide-8-8] 0 units, 0 failed, 6195 tauts, 0 hbrs, 48977 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 509 transitive binary clauses
c [block-10] scheduling all variables this time
c [block-10] scheduled 6730 variables 100%
c [block-10] limit of 184807349 steps penalty 1 = 1 + 0
c [block-10] fully completed
c [block-10] transition to [ all 0 rem 0 ] state
c [block-10] eliminated 73 blocked clauses
c [block-10] 73 < 1/100 * 38867 = 388 considered unsuccessful
c [cce-8] boosting limit by 10
c [cce-8] limit of 1848073490 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-8-1] eliminated 2 clauses out of 57 (4%) of length 12
c [cce-8-1] eliminated 3 clauses out of 86 (3%) of length 11
c [cce-8-1] eliminated 3 clauses out of 149 (2%) of length 10
c [cce-8-1] eliminated 13 clauses out of 315 (4%) of length 9
c [cce-8-1] eliminated 24 clauses out of 587 (4%) of length 8
c [cce-8-1] eliminated 26 clauses out of 1089 (2%) of length 7
c [cce-8-1] eliminated 41 clauses out of 2040 (2%) of length 6
c [cce-8-1] eliminated 66 clauses out of 3836 (2%) of length 5
c [cce-8-1] eliminated 86 clauses out of 8538 (1%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 265 large clauses in 27875744 steps
c [cce-8-1] allowing another 13937872 steps for small clauses
c [cce-8-1] scheduling 16546 clauses = 7174 binary + 9372 ternary
c [cce-8-1] tried to eliminate 16546 small clauses 100%
c [cce-8-1] eliminated 11 binary clauses 0%
c [cce-8-1] eliminated 147 ternary clauses 2%
c [cce-8-1] eliminated 158 small clauses 1%
c [cce-8-1] eliminated 158 small clauses in 36362864 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 423 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 13660636 steps for small clauses
c [cce-8-2] scheduling 16388 clauses = 7163 binary + 9225 ternary
c [cce-8-2] tried to eliminate 16388 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 423 covered clauses in TOTAL during 2 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 6726 variables 100%
c [elim-14] limit of 739229399 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 93 variables 1% in round 1 in 10494412 steps
c [elim-14-1] backward subsumption/strengthening limit 10494400
c [elim-14-1-1] backward checking 569 touched variables 8%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 1 and strengthened 0 clauses in 727218 steps
c [elim-14-1] rescheduled 3 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 32973 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 93 = 1% variables out of 6726 scheduled
c [bca-11] limit of 10000000 steps and 76868 added (scaled 2)
c [bca-11] 2031 out of 13268 literals actually usable 15%
c [bca-11] added 5 blocked clauses in 118195 steps
c [sweep-15] limit 11088440 penalty 0 = 0 + 0
c [sweep-15-1] 424 pos 46.6% + 485 neg 53.4% = 909 sched 13.7% ret 5724
c [sweep-15-1] 5706226 steps 362 queries 17.77 avg class size
c [sweep-15-1] 4830 decisions 359 SAT calls 47.86 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-69] removed 23 variables
c [sweep-15-1] removed 23 vars (0 failed, 23 eqs, 20 impls)
c [sweep-15-2] 2899 pos 43.9% + 3711 neg 56.1% = 6610 sched 100.0% ret 0
c [sweep-15-2] 5433082 steps 63 queries 255.08 avg class size
c [sweep-15-2] 2707 decisions 63 SAT calls 121.86 avg env size
c [sweep-15-2] 5077 variables remain 77% (1533 retained 23%)
c [decomp-70] removed 1 variables
c [sweep-15-2] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-15] removed 24 vars in TOTAL (2 rounds, 423 queries)
c [sort-queue-19] sorted 6609 enqueued variables after 642860 conflicts
c [score-dist-19] active 0 (0%), one 6609 (100%), zero 0 (0%)
c [score-dist-19] max exp 1, different 1 (50%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 125 variables 1.9% (6609 remain 13%)
c [simplification-19] removed 760 irredundant clauses 2.0% (38128 remain 25%)
c [simplification-19] maximum reduction of 2% = max (2%, 2%)
c [simplification-19] geometric conflict interval increment 48985 = 146957 / 3
c [simplification-19] new conflict interval 195942
c [simplification-19] penalized conflict interval 195942 = 1 * 195942
c [simplification-19] hard conflict limit 936773 (soft 838802 + delta 97971)
c [simplification-19] new conflict limit 838802 (hard 936773)
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 -  156.0    6609    38128    657272   90730  20779 15257   10    47   26  20%    989    6   10    9  121%
c i  158.9    6608    38128    677373  109837  20800 15262    8    37   31  21%    998   -3    8    9   89%
c -  165.0    6608    38128    702910   97141  20818 15265    9    29   26  31%  -1981   -8   12    8  139%
c -  173.5    6608    38127    743162   97732  20843 15268    9    27   26  33%   -602  -10   11    9  133%
c -  181.9    6608    38127    785091   98666  20861 15269    8    31   26  27%    166   -4    9    9  104%
c -  190.5    6608    38127    828942  101962  20878 15269   10    41   27  24%    585    6   11    9  120%
c 
c [simplification-20] limit 838802 conflicts (hard 936773) hit after 848952 conflicts
c [quatres-16] found 17900 quaternary clauses 20% in total
c [quatres-16-1] removed 37 duplicate quaternary clauses
c [quatres-16-1] added 4 double-self-subsuming ternary resolvents
c [quatres-16-2] added 148 single-self-subsuming ternary resolvents
c [quatres-16-2] added 266 quaternary resolvents
c [ternres-16] limit 53155606 with penalty 0 = 0 + 0
c [ternres-16] 1 schedulable variables 0%
c [ternres-16] 6876 ternary resolvents (48 bin, 6828 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-71] removed 2 variables
c [basicprobe-6] limit 265778030 penalty 0 = 0 + 0
c [basicprobe-6-0] 3751 sched 57%, 1 failed, 0 lifted, 792 hbrs
c [decomp-72] removed 2 variables
c [basicprobe-6-1] 3741 sched 57%, 0 failed, 0 lifted, 68 hbrs
c [basicprobe-6-2] 3741 sched 57%, 0 failed, 0 lifted, 19 hbrs
c [basicprobe-6-3] 3741 sched 57%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-6-4] 3741 sched 57%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-6-5] 3741 sched 57%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-6-6] 3741 sched 57%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-6-7] 3741 sched 57%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-6-8] 3741 sched 57%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-8] round limit 8 hit
c [basicprobe-6-8] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-6-8] removed 2 variables, found 902 hbrs
c [bate-5] eliminated 2 asymmetric tautologies during probing
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 518 transitive binary clauses
c [cce-9] limit of 265778030 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-9-1] eliminated 3 clauses out of 76 (4%) of length 13
c [cce-9-1] eliminated 4 clauses out of 55 (7%) of length 12
c [cce-9-1] eliminated 4 clauses out of 84 (5%) of length 11
c [cce-9-1] eliminated 5 clauses out of 154 (3%) of length 10
c [cce-9-1] eliminated 19 clauses out of 325 (6%) of length 9
c [cce-9-1] eliminated 25 clauses out of 569 (4%) of length 8
c [cce-9-1] eliminated 32 clauses out of 1052 (3%) of length 7
c [cce-9-1] eliminated 52 clauses out of 2026 (3%) of length 6
c [cce-9-1] eliminated 112 clauses out of 3785 (3%) of length 5
c [cce-9-1] eliminated 215 clauses out of 8404 (3%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 472 large clauses in 42863418 steps
c [cce-9-1] allowing another 21431709 steps for small clauses
c [cce-9-1] scheduling 12397 clauses = 7042 binary + 5355 ternary
c [cce-9-1] tried to eliminate 12397 small clauses 100%
c [cce-9-1] eliminated 109 binary clauses 2%
c [cce-9-1] eliminated 111 ternary clauses 2%
c [cce-9-1] eliminated 220 small clauses 2%
c [cce-9-1] eliminated 220 small clauses in 43639963 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 692 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 149 (1%) of length 10
c [cce-9-2] eliminated 2 clauses out of 306 (1%) of length 9
c [cce-9-2] eliminated 1 clauses out of 544 (0%) of length 8
c [cce-9-2] eliminated 10 clauses out of 1020 (1%) of length 7
c [cce-9-2] eliminated 29 clauses out of 1974 (1%) of length 6
c [cce-9-2] eliminated 42 clauses out of 3673 (1%) of length 5
c [cce-9-2] eliminated 113 clauses out of 8189 (1%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 198 large clauses in 40085372 steps
c [cce-9-2] allowing another 20042686 steps for small clauses
c [cce-9-2] scheduling 12177 clauses = 6933 binary + 5244 ternary
c [cce-9-2] tried to eliminate 12177 small clauses 100%
c [cce-9-2] eliminated 72 binary clauses 1%
c [cce-9-2] eliminated 76 ternary clauses 1%
c [cce-9-2] eliminated 148 small clauses 1%
c [cce-9-2] eliminated 148 small clauses in 41370373 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 346 covered clauses in round 2
c [cce-9-3] eliminated 1 clauses out of 304 (0%) of length 9
c [cce-9-3] eliminated 5 clauses out of 543 (1%) of length 8
c [cce-9-3] eliminated 6 clauses out of 1010 (1%) of length 7
c [cce-9-3] eliminated 18 clauses out of 1945 (1%) of length 6
c [cce-9-3] eliminated 35 clauses out of 3631 (1%) of length 5
c [cce-9-3] eliminated 50 clauses out of 8076 (1%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 115 large clauses in 39167856 steps
c [cce-9-3] allowing another 19583928 steps for small clauses
c [cce-9-3] scheduling 12029 clauses = 6861 binary + 5168 ternary
c [cce-9-3] tried to eliminate 12029 small clauses 100%
c [cce-9-3] eliminated 68 binary clauses 1%
c [cce-9-3] eliminated 35 ternary clauses 1%
c [cce-9-3] eliminated 103 small clauses 1%
c [cce-9-3] eliminated 103 small clauses in 40493588 steps
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 218 covered clauses in round 3
c [cce-9] eliminated 1256 covered clauses in TOTAL during 3 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 6605 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 290 variables 4% in round 1 in 9836339 steps
c [elim-15-1] backward subsumption/strengthening limit 9836300
c [elim-15-1-1] backward checking 707 touched variables 11%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 10 clauses in 750623 steps
c [elim-15-1] rescheduled 36 variables 1% by backward subsumption
c [elim-15-2] eliminated 3 variables 0% in round 2 in 525282 steps
c [elim-15-2] backward subsumption/strengthening limit 525200
c [elim-15-2-1] backward checking 18 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 11 and strengthened 5 clauses in 466040 steps
c [elim-15-2] rescheduled 16 variables 0% by backward subsumption
c [elim-15-3] eliminated 3 variables 0% in round 3 in 1791374 steps
c [elim-15-3] backward subsumption/strengthening limit 1791300
c [elim-15-3-1] backward checking 17 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 0 and strengthened 0 clauses in 465351 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 296 = 4% variables out of 6605 scheduled
c [bca-12] limit of 10000000 steps and 72688 added (scaled 2)
c [bca-12] 1960 out of 12620 literals actually usable 16%
c [bca-12] added 18 blocked clauses in 119791 steps
c [sweep-16] limit 15946681 penalty 0 = 0 + 0
c [sweep-16-1] 2068 pos 43.0% + 2743 neg 57.0% = 4811 sched 76.3% ret 1498
c [sweep-16-1] 15986754 steps 534 queries 47.61 avg class size
c [sweep-16-1] 11621 decisions 529 SAT calls 59.95 avg env size
c [sweep-16-1] 460 variables remain 7% (5849 retained 93%)
c [decomp-80] removed 39 variables
c [sweep-16-1] removed 39 vars (0 failed, 39 eqs, 35 impls)
c [sweep-16] removed 39 vars in TOTAL (1 rounds, 533 queries)
c [sort-queue-20] sorted 6270 enqueued variables after 848952 conflicts
c [score-dist-20] active 0 (0%), one 6270 (100%), zero 0 (0%)
c [score-dist-20] max exp 1, different 1 (50%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 338 variables 5.1% (6270 remain 12%)
c [simplification-20] removed 2103 irredundant clauses 5.5% (36024 remain 24%)
c [simplification-20] maximum reduction of 6% = max (5%, 6%)
c [simplification-20] large reduction 6% >= 5% limit
c [simplification-20] next conflict interval 8489 = min (848952/100, 195942)
c [simplification-20] penalized conflict interval 8489 = 1 * 8489
c [simplification-20] hard conflict limit 867441 (soft 857441 + delta 10000)
c [simplification-20] new conflict limit 857441 (hard 867441)
c 
c [simplification-21] limit 857441 conflicts (hard 867441) hit after 857442 conflicts
c [quatres-17] found 17185 quaternary clauses 20% in total
c [quatres-17-1] removed 18 duplicate quaternary clauses
c [quatres-17-1] added 3 double-self-subsuming ternary resolvents
c [quatres-17-2] added 86 single-self-subsuming ternary resolvents
c [quatres-17-2] added 126 quaternary resolvents
c [ternres-17] limit 53798146 with penalty 0 = 0 + 0
c [ternres-17] all 6270 free variables schedulable
c [ternres-17] 4308 ternary resolvents (84 bin, 4224 trn)
c [ternres-17] 4 variables remain 0% (6266 retained 100%)
c [card-6] limit 1681192 penalty 4 = 4 + 0
c [card-6] found 292 at-most-one constraints of average size 3.1
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1681192 for elimination
c [card-6] 292 out of 292 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-81] removed 4 variables
c [simpleprobe-7] all 6266 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-82] removed 6 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 6 variables, found 2144 hbrs, 2 units
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 909 transitive binary clauses
c [cce-10] limit of 268990730 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 57 (2%) of length 12
c [cce-10-1] eliminated 2 clauses out of 83 (2%) of length 11
c [cce-10-1] eliminated 2 clauses out of 308 (1%) of length 9
c [cce-10-1] eliminated 20 clauses out of 546 (4%) of length 8
c [cce-10-1] eliminated 40 clauses out of 1018 (4%) of length 7
c [cce-10-1] eliminated 49 clauses out of 1940 (3%) of length 6
c [cce-10-1] eliminated 65 clauses out of 3555 (2%) of length 5
c [cce-10-1] eliminated 70 clauses out of 7848 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 249 large clauses in 23564706 steps
c [cce-10-1] allowing another 11782353 steps for small clauses
c [cce-10-1] scheduling 15273 clauses = 6570 binary + 8703 ternary
c [cce-10-1] tried to eliminate 15273 small clauses 100%
c [cce-10-1] eliminated 7 binary clauses 0%
c [cce-10-1] eliminated 42 ternary clauses 0%
c [cce-10-1] eliminated 49 small clauses 0%
c [cce-10-1] eliminated 49 small clauses in 30687366 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 298 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 11521390 steps for small clauses
c [cce-10-2] scheduling 15224 clauses = 6563 binary + 8661 ternary
c [cce-10-2] tried to eliminate 15224 small clauses 100%
c [cce-10-2] completed small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 298 covered clauses in TOTAL during 2 rounds
c [cce-10] 298 < 1/100 * 35960 = 359 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 6260 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 118 variables 2% in round 1 in 9512991 steps
c [elim-16-1] backward subsumption/strengthening limit 9512900
c [elim-16-1-1] backward checking 409 touched variables 7%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 1 and strengthened 6 clauses in 649968 steps
c [elim-16-1] rescheduled 28 variables 0% by backward subsumption
c [elim-16-2] eliminated 3 variables 0% in round 2 in 74197 steps
c [elim-16-2] backward subsumption/strengthening limit 74100
c [elim-16-2-1] backward checking 14 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 0 and strengthened 0 clauses in 26827 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 121 = 2% variables out of 6260 scheduled
c [bca-13] limit of 10000000 steps and 70931 added (scaled 2)
c [bca-13] 1805 out of 12280 literals actually usable 15%
c [bca-13] added 6 blocked clauses in 127566 steps
c [sweep-17] limit 16139443 penalty 0 = 0 + 0
c [sweep-17-1] 195 pos 44.1% + 247 neg 55.9% = 442 sched 7.2% ret 5697
c [sweep-17-1] 5504284 steps 227 queries 12.81 avg class size
c [sweep-17-1] 3216 decisions 228 SAT calls 50.19 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-83] removed 29 variables
c [sweep-17-1] removed 29 vars (0 failed, 28 eqs, 17 impls)
c [sweep-17-2] 2566 pos 42.0% + 3544 neg 58.0% = 6110 sched 100.0% ret 0
c [sweep-17-2] 10656952 steps 172 queries 106.81 avg class size
c [sweep-17-2] 5182 decisions 171 SAT calls 88.35 avg env size
c [sweep-17-2] 2510 variables remain 41% (3600 retained 59%)
c [decomp-84] removed 7 variables
c [sweep-17-2] removed 7 vars (0 failed, 7 eqs, 6 impls)
c [sweep-17] removed 36 vars in TOTAL (2 rounds, 397 queries)
c [sort-queue-21] sorted 6103 enqueued variables after 857442 conflicts
c [score-dist-21] active 0 (0%), one 6103 (100%), zero 0 (0%)
c [score-dist-21] max exp 1, different 1 (50%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 167 variables 2.7% (6103 remain 12%)
c [simplification-21] removed 906 irredundant clauses 2.5% (35117 remain 23%)
c [simplification-21] maximum reduction of 3% = max (3%, 3%)
c [simplification-21] geometric conflict interval increment 48985 = 195942 / 4
c [simplification-21] new conflict interval 244927
c [simplification-21] penalized conflict interval 244927 = 1 * 244927
c [simplification-21] hard conflict limit 1224832 (soft 1102369 + delta 122463)
c [simplification-21] new conflict limit 1102369 (hard 1224832)
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 -  214.4    6103    35116    875705  101263  28019 14193   11    33   28  33%    809   -2   11    9  118%
c -  222.2    6103    35116    923423  108045  28033 14193    8    39   29  20%    920    5   11    9  128%
c -  231.8    6103    35116    964655  106636  28051 14197   10    36   28  26%    969    1   11    9  125%
c -  241.7    6103    35116   1010781  109559  28061 14198   10    38   29  26%    997    0    7    9   71%
c -  252.4    6103    35116   1057593  112836  28070 14198   10    27   29  38%   1011   -8   10    9  105%
c i  254.4    6102    35116   1077308  128618  28075 14198    8    10   35  85%   1014  -20    7    9   73%
c -  261.1    6102    35116   1105982  115358  28080 14198   11    34   29  32%  -3081    4   13    9  137%
c -  272.2    6102    35116   1152126  117291  28092 14198   11    37   29  29%  -1006    3   10    9  109%
c 
c [simplification-22] limit 1102369 conflicts (hard 1224832) hit after 1196976 conflicts
c [quatres-18] found 17056 quaternary clauses 17% in total
c [quatres-18-1] removed 26 duplicate quaternary clauses
c [quatres-18-1] added 2 double-self-subsuming ternary resolvents
c [quatres-18-2] added 99 single-self-subsuming ternary resolvents
c [quatres-18-2] added 159 quaternary resolvents
c [ternres-18] limit 83082451 with penalty 0 = 0 + 0
c [ternres-18] 4 schedulable variables 0%
c [ternres-18] 2316 ternary resolvents (28 bin, 2288 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-85] removed 2 variables
c [treelook-7] limit 8308245 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 9897 literals 81%
c [treelook-7] scheduling used 561540 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 8308245 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 7483949 steps
c [treelook-7] fully completed tree based probing
c [decomp-86] removed 5 variables
c [treelook-7] removed 8 variables, found 4284 hbrs
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 1006 transitive binary clauses
c [block-11] scheduling all variables this time
c [block-11] scheduled 6093 variables 100%
c [block-11] limit of 200000000 steps penalty 2 = 2 + 0
c [block-11] fully completed
c [block-11] transition to [ all 0 rem 0 ] state
c [block-11] eliminated 60 blocked clauses
c [block-11] 60 < 1/100 * 35014 = 350 considered unsuccessful
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 6082 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 33 variables 1% in round 1 in 9478594 steps
c [elim-17-1] backward subsumption/strengthening limit 9478500
c [elim-17-1-1] backward checking 167 touched variables 3%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 1 and strengthened 5 clauses in 2056739 steps
c [elim-17-1] rescheduled 17 variables 0% by backward subsumption
c [elim-17-2] eliminated 1 variables 0% in round 2 in 1235053 steps
c [elim-17-2] backward subsumption/strengthening limit 1235000
c [elim-17-2-1] backward checking 3 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 0 and strengthened 0 clauses in 448315 steps
c [elim-17] fully completed in 2 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 34 = 1% variables out of 6082 scheduled
c [elim-17] 34 < 1/100 * 6082 = 60 considered unsuccessful
c [bca-14] limit of 10000000 steps and 70252 added (scaled 2)
c [bca-14] 1780 out of 12098 literals actually usable 15%
c [bca-14] added 3 blocked clauses in 158896 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 1086 pos 43.8% + 1395 neg 56.2% = 2481 sched 41.0% ret 3567
c [sweep-18-1] 18909256 steps 555 queries 21.89 avg class size
c [sweep-18-1] 9637 decisions 552 SAT calls 57.32 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-87] removed 16 variables
c [sweep-18-1] removed 16 vars (0 failed, 21 eqs, 23 impls)
c [sweep-18-2] 2609 pos 43.3% + 3423 neg 56.7% = 6032 sched 100.0% ret 0
c [sweep-18-2] 30023162 steps 725 queries 30.10 avg class size
c [sweep-18-2] 14693 decisions 736 SAT calls 69.19 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-88] removed 30 variables
c [sweep-18-2] removed 30 vars (0 failed, 36 eqs, 15 impls)
c [sweep-18-3] 2597 pos 43.3% + 3405 neg 56.7% = 6002 sched 100.0% ret 0
c [sweep-18-3] 29486031 steps 687 queries 26.69 avg class size
c [sweep-18-3] 14406 decisions 688 SAT calls 73.16 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-89] removed 30 variables
c [sweep-18-3] removed 30 vars (0 failed, 35 eqs, 23 impls)
c [sweep-18] removed 76 vars in TOTAL (3 rounds, 1964 queries)
c [sort-queue-22] sorted 5972 enqueued variables after 1196976 conflicts
c [score-dist-22] active 0 (0%), one 5972 (100%), zero 0 (0%)
c [score-dist-22] max exp 1, different 1 (50%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 130 variables 2.1% (5972 remain 11%)
c [simplification-22] removed 333 irredundant clauses 0.9% (34783 remain 23%)
c [simplification-22] maximum reduction of 2% = max (2%, 1%)
c [simplification-22] geometric conflict interval increment 81642 = 244927 / 3
c [simplification-22] new conflict interval 326569
c [simplification-22] penalized conflict interval 326569 = 1 * 326569
c [simplification-22] hard conflict limit 1686829 (soft 1523545 + delta 163284)
c [simplification-22] new conflict limit 1523545 (hard 1686829)
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 -  287.6    5972    34783   1201304  118539  28709 16376    9    36   21  26%     65    1   10    9  109%
c i  291.9    5971    34783   1241207  149305  28765 16386    7     8   30  89%    503  -17    6    9   64%
c -  295.9    4553    34778   1254570  120006  28772 16388   10    34   32  28%  -1523    9   12    9  133%
c -  310.5    4553    34778   1302923  120647  28802 16390   11    35   33  31%   -194    6   12    9  128%
c -  326.1    4553    34778   1353473  122694  28821 16397   11    40   33  29%    461    5   12   10  125%
c -  340.0    4553    34778   1405201  126552  28837 16399   10    34   33  30%    768   -1    8   10   88%
c -  355.4    4553    34778   1457041  130656  28852 16401   11    38   33  28%    908    4   13    9  139%
c -  372.2    4553    34778   1507272  131019  28868 16404   11    38   33  30%    970    4    9   10   96%
c 
c [simplification-23] limit 1523545 conflicts (hard 1686829) hit after 1528652 conflicts
c [quatres-19] found 9406 quaternary clauses 12% in total
c [quatres-19-1] removed 47 duplicate quaternary clauses
c [quatres-19-1] added 2 double-self-subsuming ternary resolvents
c [quatres-19-2] added 75 single-self-subsuming ternary resolvents
c [quatres-19-2] added 494 quaternary resolvents
c [ternres-19] limit 117992639 with penalty 0 = 0 + 0
c [ternres-19] all 4553 free variables schedulable
c [ternres-19] 2738 ternary resolvents (52 bin, 2686 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-90] removed 2248 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 2003 sched 54%, 28 failed, 5 lifted, 2396 hbrs
c [decomp-91] removed 94 variables
c [basicprobe-7-1] 1864 sched 51%, 4 failed, 0 lifted, 447 hbrs
c [decomp-92] removed 10 variables
c [basicprobe-7-2] 1855 sched 51%, 1 failed, 0 lifted, 55 hbrs
c [decomp-93] removed 1 variables
c [basicprobe-7-3] 1854 sched 51%, 1 failed, 0 lifted, 20 hbrs
c [decomp-94] removed 1 variables
c [basicprobe-7-4] 1853 sched 51%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-7-5] 1851 sched 51%, 0 failed, 0 lifted, 19 hbrs
c [basicprobe-7-6] 1851 sched 51%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-7-7] 1851 sched 51%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-7-7] fully completed probing
c [basicprobe-7-7] 39 units = 34 failed (87%) + 5 lifted (13%)
c [basicprobe-7-7] removed 106 variables, found 2961 hbrs
c [bate-6] eliminated 229 asymmetric tautologies during probing
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 1107 transitive binary clauses
c [cce-11] limit of 294981597 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 1 clauses out of 2 (50%) of length 16
c [cce-11-1] eliminated 7 clauses out of 22 (32%) of length 13
c [cce-11-1] eliminated 4 clauses out of 15 (27%) of length 12
c [cce-11-1] eliminated 6 clauses out of 25 (24%) of length 11
c [cce-11-1] eliminated 8 clauses out of 40 (20%) of length 10
c [cce-11-1] eliminated 19 clauses out of 59 (32%) of length 9
c [cce-11-1] eliminated 32 clauses out of 179 (18%) of length 8
c [cce-11-1] eliminated 60 clauses out of 286 (21%) of length 7
c [cce-11-1] eliminated 157 clauses out of 587 (27%) of length 6
c [cce-11-1] eliminated 319 clauses out of 1528 (21%) of length 5
c [cce-11-1] eliminated 564 clauses out of 4578 (12%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 1177 large clauses in 9778238 steps
c [cce-11-1] allowing another 4889119 steps for small clauses
c [cce-11-1] scheduling 7438 clauses = 3957 binary + 3481 ternary
c [cce-11-1] tried to eliminate 7438 small clauses 100%
c [cce-11-1] eliminated 508 binary clauses 13%
c [cce-11-1] eliminated 414 ternary clauses 12%
c [cce-11-1] eliminated 922 small clauses 12%
c [cce-11-1] eliminated 922 small clauses in 10385322 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 2099 covered clauses in round 1
c [cce-11-2] eliminated 1 clauses out of 147 (1%) of length 8
c [cce-11-2] eliminated 10 clauses out of 226 (4%) of length 7
c [cce-11-2] eliminated 6 clauses out of 430 (1%) of length 6
c [cce-11-2] eliminated 12 clauses out of 1209 (1%) of length 5
c [cce-11-2] eliminated 34 clauses out of 4014 (1%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 63 large clauses in 8521212 steps
c [cce-11-2] allowing another 4260606 steps for small clauses
c [cce-11-2] scheduling 6527 clauses = 3449 binary + 3078 ternary
c [cce-11-2] tried to eliminate 6527 small clauses 100%
c [cce-11-2] eliminated 48 binary clauses 1%
c [cce-11-2] eliminated 38 ternary clauses 1%
c [cce-11-2] eliminated 86 small clauses 1%
c [cce-11-2] eliminated 86 small clauses in 8968674 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 149 covered clauses in round 2
c [cce-11-3] eliminated 7 clauses out of 216 (3%) of length 7
c [cce-11-3] eliminated 1 clauses out of 424 (0%) of length 6
c [cce-11-3] eliminated 2 clauses out of 1197 (0%) of length 5
c [cce-11-3] eliminated 3 clauses out of 3980 (0%) of length 4
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] eliminated 13 large clauses in 8457240 steps
c [cce-11-3] allowing another 4228620 steps for small clauses
c [cce-11-3] scheduling 6445 clauses = 3401 binary + 3044 ternary
c [cce-11-3] tried to eliminate 6445 small clauses 100%
c [cce-11-3] eliminated 15 binary clauses 0%
c [cce-11-3] eliminated 13 ternary clauses 0%
c [cce-11-3] eliminated 28 small clauses 0%
c [cce-11-3] eliminated 28 small clauses in 8863776 steps
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 41 covered clauses in round 3
c [cce-11] eliminated 2289 covered clauses in TOTAL during 3 rounds
c [bca-15] limit of 10000000 steps and 35934 added (scaled 2)
c [bca-15] 1042 out of 7238 literals actually usable 14%
c [bca-15] added 4 blocked clauses in 136875 steps
c [sweep-19] limit 35397791 penalty 0 = 0 + 0
c [sweep-19-1] 1627 pos 45.0% + 1991 neg 55.0% = 3618 sched 100.0% ret 0
c [sweep-19-1] 23328166 steps 500 queries 21.07 avg class size
c [sweep-19-1] 9209 decisions 447 SAT calls 77.34 avg env size
c [sweep-19-1] fully completed sweeping round
c [decomp-98] removed 79 variables
c [sweep-19-1] removed 79 vars (0 failed, 89 eqs, 73 impls)
c [sweep-19-2] 1600 pos 45.2% + 1939 neg 54.8% = 3539 sched 100.0% ret 0
c [sweep-19-2] 12421222 steps 205 queries 37.98 avg class size
c [sweep-19-2] 4958 decisions 197 SAT calls 93.06 avg env size
c [sweep-19-2] 697 variables remain 20% (2842 retained 80%)
c [decomp-99] removed 9 variables
c [sweep-19-2] removed 9 vars (0 failed, 12 eqs, 8 impls)
c [sweep-19] removed 88 vars in TOTAL (2 rounds, 703 queries)
c [sort-queue-23] sorted 3530 enqueued variables after 1528652 conflicts
c [score-dist-23] active 0 (0%), one 3530 (100%), zero 0 (0%)
c [score-dist-23] max exp 1, different 1 (50%)
c [score-dist-23] median active exp 0, avg 0.0
c [simplification-23] removed 1023 variables 22.5% (3530 remain 7%)
c [simplification-23] removed 17192 irredundant clauses 49.4% (17586 remain 12%)
c [simplification-23] maximum reduction of 49% = max (22%, 49%)
c [simplification-23] large reduction 49% >= 5% limit
c [simplification-23] next conflict interval 15286 = min (1528652/100, 326569)
c [simplification-23] penalized conflict interval 15286 = 1 * 15286
c [simplification-23] hard conflict limit 1553938 (soft 1543938 + delta 10000)
c [simplification-23] new conflict limit 1543938 (hard 1553938)
c 
c [simplification-24] limit 1543938 conflicts (hard 1553938) hit after 1543938 conflicts
c [quatres-20] found 10388 quaternary clauses 12% in total
c [quatres-20-1] removed 162 duplicate quaternary clauses
c [quatres-20-1] added 4 double-self-subsuming ternary resolvents
c [quatres-20-2] added 213 single-self-subsuming ternary resolvents
c [quatres-20-2] added 169 quaternary resolvents
c [ternres-20] limit 119199791 with penalty 0 = 0 + 0
c [ternres-20] all 3530 free variables schedulable
c [ternres-20] 4511 ternary resolvents (110 bin, 4401 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-100] removed 9 variables
c [simpleprobe-8] all 3521 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-101] removed 14 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 14 variables, found 3850 hbrs, 2 units
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 1236 transitive binary clauses
c [cce-12] limit of 595998955 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 4 clauses out of 204 (2%) of length 7
c [cce-12-1] eliminated 5 clauses out of 429 (1%) of length 6
c [cce-12-1] eliminated 27 clauses out of 1197 (2%) of length 5
c [cce-12-1] eliminated 56 clauses out of 3896 (1%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 92 large clauses in 4029203 steps
c [cce-12-1] allowing another 2014601 steps for small clauses
c [cce-12-1] scheduling 6391 clauses = 3311 binary + 3080 ternary
c [cce-12-1] tried to eliminate 6391 small clauses 100%
c [cce-12-1] eliminated 30 binary clauses 1%
c [cce-12-1] eliminated 39 ternary clauses 1%
c [cce-12-1] eliminated 69 small clauses 1%
c [cce-12-1] eliminated 69 small clauses in 5191970 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 161 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 1965094 steps for small clauses
c [cce-12-2] scheduling 6322 clauses = 3281 binary + 3041 ternary
c [cce-12-2] tried to eliminate 6322 small clauses 100%
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 161 covered clauses in TOTAL during 2 rounds
c [cce-12] 161 < 1/100 * 17478 = 174 considered unsuccessful
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 3507 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 685 variables 20% in round 1 in 2892307 steps
c [elim-18-1] backward subsumption/strengthening limit 2892300
c [elim-18-1-1] backward checking 1119 touched variables 32%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 3 and strengthened 25 clauses in 283899 steps
c [elim-18-1] rescheduled 76 variables 2% by backward subsumption
c [elim-18-2] eliminated 4 variables 0% in round 2 in 244010 steps
c [elim-18-2] backward subsumption/strengthening limit 244000
c [elim-18-2-1] backward checking 34 touched variables 1%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 1 and strengthened 2 clauses in 44940 steps
c [elim-18-2] rescheduled 12 variables 0% by backward subsumption
c [elim-18-3] no variable eliminated in round 3 in 70517 steps
c [elim-18] fully completed in 3 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 689 = 20% variables out of 3507 scheduled
c [bca-16] limit of 10000000 steps and 32566 added (scaled 2)
c [bca-16] 512 out of 5638 literals actually usable 9%
c [bca-16] added 7 blocked clauses in 141513 steps
c [sweep-20] limit 35759937 penalty 0 = 0 + 0
c [sweep-20-1] 275 pos 54.9% + 226 neg 45.1% = 501 sched 17.8% ret 2317
c [sweep-20-1] 4522823 steps 174 queries 12.34 avg class size
c [sweep-20-1] 2714 decisions 167 SAT calls 76.81 avg env size
c [sweep-20-1] fully completed sweeping round
c [decomp-102] removed 6 variables
c [sweep-20-1] removed 6 vars (0 failed, 8 eqs, 9 impls)
c [sweep-20-2] 1246 pos 44.3% + 1566 neg 55.7% = 2812 sched 100.0% ret 0
c [sweep-20-2] 20237124 steps 298 queries 20.78 avg class size
c [sweep-20-2] 7571 decisions 297 SAT calls 102.18 avg env size
c [sweep-20-2] fully completed sweeping round
c [decomp-103] removed 7 variables
c [sweep-20-2] removed 7 vars (0 failed, 7 eqs, 5 impls)
c [sweep-20-3] 1244 pos 44.3% + 1561 neg 55.7% = 2805 sched 100.0% ret 0
c [sweep-20-3] 11009202 steps 75 queries 57.48 avg class size
c [sweep-20-3] 3724 decisions 74 SAT calls 159.73 avg env size
c [sweep-20-3] 1038 variables remain 37% (1767 retained 63%)
c [sweep-20-3] removed 0 vars (0 failed, 1 eqs, 0 impls)
c [sweep-20] removed 13 vars in TOTAL (3 rounds, 544 queries)
c [sort-queue-24] sorted 2805 enqueued variables after 1543938 conflicts
c [score-dist-24] active 0 (0%), one 2805 (100%), zero 0 (0%)
c [score-dist-24] max exp 1, different 1 (50%)
c [score-dist-24] median active exp 0, avg 0.0
c [simplification-24] removed 725 variables 20.5% (2805 remain 5%)
c [simplification-24] removed 1650 irredundant clauses 9.4% (15934 remain 10%)
c [simplification-24] maximum reduction of 21% = max (21%, 9%)
c [simplification-24] large reduction 21% >= 5% limit
c [simplification-24] next conflict interval 15439 = min (1543938/100, 326569)
c [simplification-24] penalized conflict interval 15439 = 1 * 15439
c [simplification-24] hard conflict limit 1569377 (soft 1559377 + delta 10000)
c [simplification-24] new conflict limit 1559377 (hard 1569377)
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 -  394.2    2805    15934   1564280  115629   6680 11857    9    34   26  26%   1001   -2   10   10  106%
c 
c [simplification-25] limit 1559377 conflicts (hard 1569377) hit after 1564840 conflicts
c [quatres-21] found 9445 quaternary clauses 11% in total
c [quatres-21-1] removed 9 duplicate quaternary clauses
c [quatres-21-2] added 49 single-self-subsuming ternary resolvents
c [quatres-21-2] added 124 quaternary resolvents
c [ternres-21] limit 120996677 with penalty 0 = 0 + 0
c [ternres-21] all 2805 free variables schedulable
c [ternres-21] 674 ternary resolvents (29 bin, 645 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-6] limit 1512458 penalty 4 = 4 + 0
c [gauss-6] extracted 1334 xors of average arity 3.1
c [gauss-6] connected 4162 occurrences of 299 variables (average 13.9)
c [gauss-6] limit 1512458 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 3 ternary equations
c [decomp-105] removed 1 variables
c [treelook-8] limit 12099667 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 5608 literals 100%
c [treelook-8] scheduling used 419030 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 12099667 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 3720052 steps
c [treelook-8] fully completed tree based probing
c [treelook-8] removed 1 variables, found 1766 hbrs
c [unhide-9] limit 1250000 with penalty 4 = 4 + 0
c [unhide-9-9] 0 units, 0 failed, 567 tauts, 0 hbrs, 26474 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 772 transitive binary clauses
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 2803 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 17 variables 1% in round 1 in 2694681 steps
c [elim-19-1] backward subsumption/strengthening limit 2694600
c [elim-19-1-1] backward checking 171 touched variables 6%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 1 and strengthened 0 clauses in 58480 steps
c [elim-19-1] rescheduled 3 variables 0% by backward subsumption
c [elim-19-2] eliminated 1 variables 0% in round 2 in 11846 steps
c [elim-19-2] backward subsumption/strengthening limit 11800
c [elim-19-2-1] backward checking 6 touched variables 0%
c [elim-19-2-1] fully completed backward checking in 1 rounds
c [elim-19-2] subsumed 0 and strengthened 0 clauses in 8578 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 18 = 1% variables out of 2803 scheduled
c [elim-19] 18 < 1/100 * 2803 = 28 considered unsuccessful
c [bca-17] limit of 10000000 steps and 32291 added (scaled 2)
c [bca-17] 490 out of 5572 literals actually usable 9%
c [bca-17] added 1 blocked clauses in 116374 steps
c [sweep-21] limit 36299003 penalty 0 = 0 + 0
c [sweep-21-1] 497 pos 48.3% + 532 neg 51.7% = 1029 sched 36.9% ret 1756
c [sweep-21-1] 12459596 steps 250 queries 14.20 avg class size
c [sweep-21-1] 4821 decisions 252 SAT calls 74.61 avg env size
c [sweep-21-1] fully completed sweeping round
c [decomp-107] removed 5 variables
c [sweep-21-1] removed 5 vars (0 failed, 3 eqs, 3 impls)
c [sweep-21-2] 1275 pos 45.9% + 1505 neg 54.1% = 2780 sched 100.0% ret 0
c [sweep-21-2] 16672770 steps 326 queries 21.04 avg class size
c [sweep-21-2] 7132 decisions 327 SAT calls 82.68 avg env size
c [sweep-21-2] fully completed sweeping round
c [decomp-108] removed 6 variables
c [sweep-21-2] removed 6 vars (0 failed, 9 eqs, 6 impls)
c [sweep-21-3] 1272 pos 45.9% + 1502 neg 54.1% = 2774 sched 100.0% ret 0
c [sweep-21-3] 7311187 steps 93 queries 71.08 avg class size
c [sweep-21-3] 3359 decisions 92 SAT calls 103.47 avg env size
c [sweep-21-3] 890 variables remain 32% (1884 retained 68%)
c [sweep-21-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-21] removed 11 vars in TOTAL (3 rounds, 666 queries)
c [sort-queue-25] sorted 2774 enqueued variables after 1564840 conflicts
c [score-dist-25] active 0 (0%), one 2774 (100%), zero 0 (0%)
c [score-dist-25] max exp 1, different 1 (50%)
c [score-dist-25] median active exp 0, avg 0.0
c [simplification-25] removed 31 variables 1.1% (2774 remain 5%)
c [simplification-25] removed 111 irredundant clauses 0.7% (15823 remain 10%)
c [simplification-25] maximum reduction of 1% = max (1%, 1%)
c [simplification-25] geometric conflict interval increment 163284 = 326569 / 2
c [simplification-25] new conflict interval 489853
c [simplification-25] penalized conflict interval 489853 = 1 * 489853
c [simplification-25] hard conflict limit 2299619 (soft 2054693 + delta 244926)
c [simplification-25] new conflict limit 2054693 (hard 2299619)
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 -  407.4    2774    15823   1614353  118109   6989 11744   10    40   24  25%   1013    3   10   10  102%
c -  420.1    2774    15823   1663731  117416   7022 11746   11    35   24  32%   1019   -0   13   10  129%
c -  437.0    2774    15823   1717514  120665   7040 11746   11    32   24  35%   1022   -0   12   10  121%
c -  451.0    2774    15823   1771154  122859   7051 11747   10    31   28  31%   1023   -7    8   10   80%
c -  465.4    2774    15823   1824411  123281   7064 11747   10    39   28  25%   1024    2    9   10   88%
c -  481.8    2774    15823   1880974  127504   7072 11750    9    37   28  25%   1024    2    9   10   88%
c -  495.2    2774    15823   1934451  128371   7084 11754   10    31   28  33%   1024   -3   10   10   99%
c -  506.5    2774    15823   1990848  132885   7096 11755    9    19   29  51%   1024  -13   11   10  114%
c -  520.3    2774    15823   2044263  132325   7126 11758   10    30   28  33%   1024   -3   10   10  102%
c 
c [simplification-26] limit 2054693 conflicts (hard 2299619) hit after 2054695 conflicts
c [quatres-22] found 9966 quaternary clauses 10% in total
c [quatres-22-1] removed 23 duplicate quaternary clauses
c [quatres-22-2] added 60 single-self-subsuming ternary resolvents
c [quatres-22-2] added 110 quaternary resolvents
c [ternres-22] limit 168807016 with penalty 0 = 0 + 0
c [ternres-22] all 2774 free variables schedulable
c [ternres-22] 543 ternary resolvents (29 bin, 514 trn)
c [ternres-22] fully completed ternary resolution
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 1495 sched 54%, 1 failed, 0 lifted, 183 hbrs
c [decomp-111] removed 1 variables
c [basicprobe-8-1] 1479 sched 53%, 0 failed, 0 lifted, 44 hbrs
c [basicprobe-8-2] 1478 sched 53%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-8-3] 1477 sched 53%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-8-4] 1477 sched 53%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-8-5] 1477 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-8-5] fully completed probing
c [basicprobe-8-5] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-8-5] removed 1 variables, found 232 hbrs
c [bate-7] eliminated 18 asymmetric tautologies during probing
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 617 transitive binary clauses
c [block-12] scheduling all variables this time
c [block-12] scheduled 2773 variables 100%
c [block-12] limit of 100000000 steps penalty 3 = 3 + 0
c [block-12] fully completed
c [block-12] transition to [ all 0 rem 0 ] state
c [block-12] eliminated 22 blocked clauses
c [block-12] 22 < 1/100 * 15787 = 157 considered unsuccessful
c [cce-13] boosting limit by 10
c [cce-13] limit of 4220175400 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 1 clauses out of 3 (33%) of length 14
c [cce-13-1] eliminated 5 clauses out of 12 (42%) of length 11
c [cce-13-1] eliminated 9 clauses out of 36 (25%) of length 10
c [cce-13-1] eliminated 11 clauses out of 82 (13%) of length 9
c [cce-13-1] eliminated 15 clauses out of 208 (7%) of length 8
c [cce-13-1] eliminated 11 clauses out of 198 (6%) of length 7
c [cce-13-1] eliminated 27 clauses out of 491 (5%) of length 6
c [cce-13-1] eliminated 56 clauses out of 1261 (4%) of length 5
c [cce-13-1] eliminated 107 clauses out of 3901 (3%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 242 large clauses in 7595816 steps
c [cce-13-1] allowing another 3797908 steps for small clauses
c [cce-13-1] scheduling 5301 clauses = 2647 binary + 2654 ternary
c [cce-13-1] tried to eliminate 5301 small clauses 100%
c [cce-13-1] eliminated 65 binary clauses 2%
c [cce-13-1] eliminated 57 ternary clauses 2%
c [cce-13-1] eliminated 122 small clauses 2%
c [cce-13-1] eliminated 122 small clauses in 7143039 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 364 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 71 (1%) of length 9
c [cce-13-2] eliminated 1 clauses out of 187 (1%) of length 7
c [cce-13-2] eliminated 1 clauses out of 464 (0%) of length 6
c [cce-13-2] eliminated 5 clauses out of 3794 (0%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 8 large clauses in 7289420 steps
c [cce-13-2] allowing another 3644710 steps for small clauses
c [cce-13-2] scheduling 5179 clauses = 2582 binary + 2597 ternary
c [cce-13-2] tried to eliminate 5179 small clauses 100%
c [cce-13-2] eliminated 5 binary clauses 0%
c [cce-13-2] eliminated 8 ternary clauses 0%
c [cce-13-2] eliminated 13 small clauses 0%
c [cce-13-2] eliminated 13 small clauses in 6831295 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 21 covered clauses in round 2
c [cce-13-3] eliminated 8 clauses out of 193 (4%) of length 8
c [cce-13-3] eliminated 2 clauses out of 463 (0%) of length 6
c [cce-13-3] eliminated 1 clauses out of 1205 (0%) of length 5
c [cce-13-3] eliminated 1 clauses out of 3789 (0%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 12 large clauses in 7233036 steps
c [cce-13-3] allowing another 3616518 steps for small clauses
c [cce-13-3] scheduling 5166 clauses = 2577 binary + 2589 ternary
c [cce-13-3] tried to eliminate 5166 small clauses 100%
c [cce-13-3] eliminated 1 binary clauses 0%
c [cce-13-3] eliminated 2 ternary clauses 0%
c [cce-13-3] eliminated 3 small clauses 0%
c [cce-13-3] eliminated 3 small clauses in 6798213 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 15 covered clauses in round 3
c [cce-13] eliminated 400 covered clauses in TOTAL during 3 rounds
c [bca-18] limit of 10000000 steps and 31364 added (scaled 2)
c [bca-18] 435 out of 5548 literals actually usable 8%
c [bca-18] added 1 blocked clauses in 143215 steps
c [sweep-22] limit 50642104 penalty 0 = 0 + 0
c [sweep-22-1] 464 pos 52.1% + 426 neg 47.9% = 890 sched 32.1% ret 1883
c [sweep-22-1] 6243345 steps 250 queries 13.78 avg class size
c [sweep-22-1] 3306 decisions 250 SAT calls 75.27 avg env size
c [sweep-22-1] fully completed sweeping round
c [decomp-116] removed 8 variables
c [sweep-22-1] removed 8 vars (0 failed, 12 eqs, 4 impls)
c [sweep-22-2] 1261 pos 45.6% + 1504 neg 54.4% = 2765 sched 100.0% ret 0
c [sweep-22-2] 20422546 steps 315 queries 22.77 avg class size
c [sweep-22-2] 6951 decisions 315 SAT calls 83.98 avg env size
c [sweep-22-2] fully completed sweeping round
c [decomp-117] removed 5 variables
c [sweep-22-2] removed 5 vars (0 failed, 8 eqs, 1 impls)
c [sweep-22-3] 1260 pos 45.7% + 1500 neg 54.3% = 2760 sched 100.0% ret 0
c [sweep-22-3] 20934627 steps 336 queries 18.57 avg class size
c [sweep-22-3] 7706 decisions 334 SAT calls 93.42 avg env size
c [sweep-22-3] fully completed sweeping round
c [decomp-118] removed 2 variables
c [sweep-22-3] removed 2 vars (0 failed, 6 eqs, 3 impls)
c [sweep-22] removed 15 vars in TOTAL (3 rounds, 898 queries)
c [sort-queue-26] sorted 2758 enqueued variables after 2054695 conflicts
c [score-dist-26] active 0 (0%), one 2758 (100%), zero 0 (0%)
c [score-dist-26] max exp 1, different 1 (50%)
c [score-dist-26] median active exp 0, avg 0.0
c [simplification-26] removed 16 variables 0.6% (2758 remain 5%)
c [simplification-26] removed 464 irredundant clauses 2.9% (15359 remain 10%)
c [simplification-26] maximum reduction of 3% = max (1%, 3%)
c [simplification-26] geometric conflict interval increment 122463 = 489853 / 4
c [simplification-26] new conflict interval 612316
c [simplification-26] penalized conflict interval 612316 = 1 * 612316
c [simplification-26] hard conflict limit 2973169 (soft 2667011 + delta 306158)
c [simplification-26] new conflict limit 2667011 (hard 2973169)
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 -  538.3    2758    15359   2100037  135755   7762 11450    9    39   27  23%   1024    3    7   10   74%
c -  554.0    2758    15359   2154984  135670   7784 11455   11    30   28  35%   1024   -2   12   10  116%
c -  568.4    2758    15359   2211577  136529   7817 11462   10    17   28  56%   1024  -13    9   10   91%
c i  574.5    2757    15359   2237020  160116   7824 11465   11    33   36  33%   1024    7   12   10  120%
c -  587.7    2757    15359   2271230  136543   7846 11476   11    32   28  35%  -8354    6    9   10   92%
c -  604.1    2757    15359   2332749  141201   7865 11480   11    31   28  37%  -2644    5   13   10  131%
c -  622.7    2757    15359   2391560  142091   7878 11485   11    31   28  35%   -471    4   10   10  102%
c -  636.0    2757    15359   2451286  145051   7886 11489    8    20   32  40%    423  -10    8   10   79%
c -  655.9    2757    15358   2510825  144508   7908 11496   10    22   32  46%    782   -6    8   10   77%
c -  677.1    2757    15358   2572381  146130   7933 11503   11    30   32  38%    929    5   13   10  127%
c -  694.3    2757    15358   2634271  148129   7945 11503   11    30   32  36%    987    3   13   10  123%
c 
c [simplification-27] limit 2667011 conflicts (hard 2973169) hit after 2672630 conflicts
c [quatres-23] found 10353 quaternary clauses 9% in total
c [quatres-23-1] removed 8 duplicate quaternary clauses
c [quatres-23-1] added 1 double-self-subsuming ternary resolvents
c [quatres-23-2] added 56 single-self-subsuming ternary resolvents
c [quatres-23-2] added 79 quaternary resolvents
c [ternres-23] limit 200000000 with penalty 0 = 0 + 0
c [ternres-23] all 2757 free variables schedulable
c [ternres-23] 653 ternary resolvents (30 bin, 623 trn)
c [ternres-23] fully completed ternary resolution
c [decomp-119] removed 13 variables
c [simpleprobe-9] all 2745 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-120] removed 26 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 26 variables, found 1948 hbrs, 6 units
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 852 transitive binary clauses
c [cce-14] limit of 1190886386 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 4 clauses out of 186 (2%) of length 8
c [cce-14-1] eliminated 1 clauses out of 186 (1%) of length 7
c [cce-14-1] eliminated 4 clauses out of 447 (1%) of length 6
c [cce-14-1] eliminated 9 clauses out of 1196 (1%) of length 5
c [cce-14-1] eliminated 20 clauses out of 3770 (1%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 38 large clauses in 3883355 steps
c [cce-14-1] allowing another 1941677 steps for small clauses
c [cce-14-1] scheduling 6728 clauses = 2514 binary + 4214 ternary
c [cce-14-1] tried to eliminate 6728 small clauses 100%
c [cce-14-1] eliminated 9 binary clauses 0%
c [cce-14-1] eliminated 75 ternary clauses 2%
c [cce-14-1] eliminated 84 small clauses 1%
c [cce-14-1] eliminated 84 small clauses in 4859331 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 122 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 1884031 steps for small clauses
c [cce-14-2] scheduling 6644 clauses = 2505 binary + 4139 ternary
c [cce-14-2] tried to eliminate 6644 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 122 covered clauses in TOTAL during 2 rounds
c [cce-14] 122 < 1/100 * 15207 = 152 considered unsuccessful
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 2719 variables 100%
c [elim-20] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 108 variables 4% in round 1 in 2656468 steps
c [elim-20-1] backward subsumption/strengthening limit 2656400
c [elim-20-1-1] backward checking 537 touched variables 20%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 0 and strengthened 23 clauses in 170976 steps
c [elim-20-1] rescheduled 64 variables 2% by backward subsumption
c [elim-20-2] eliminated 5 variables 0% in round 2 in 159461 steps
c [elim-20-2] backward subsumption/strengthening limit 159400
c [elim-20-2-1] backward checking 34 touched variables 1%
c [elim-20-2-1] fully completed backward checking in 1 rounds
c [elim-20-2] subsumed 0 and strengthened 3 clauses in 20669 steps
c [elim-20-2] rescheduled 6 variables 0% by backward subsumption
c [elim-20-3] no variable eliminated in round 3 in 11220 steps
c [elim-20] fully completed in 3 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 113 = 4% variables out of 2719 scheduled
c [bca-19] limit of 10000000 steps and 30122 added (scaled 2)
c [bca-19] 395 out of 5214 literals actually usable 8%
c [bca-19] added 1 blocked clauses in 176056 steps
c [sweep-23] limit 71453183 penalty 0 = 0 + 0
c [sweep-23-1] 1154 pos 44.3% + 1452 neg 55.7% = 2606 sched 100.0% ret 0
c [sweep-23-1] 39514612 steps 342 queries 17.83 avg class size
c [sweep-23-1] 9416 decisions 336 SAT calls 94.41 avg env size
c [sweep-23-1] fully completed sweeping round
c [decomp-121] removed 49 variables
c [sweep-23-1] removed 49 vars (0 failed, 53 eqs, 39 impls)
c [sweep-23-2] 1127 pos 44.1% + 1430 neg 55.9% = 2557 sched 100.0% ret 0
c [sweep-23-2] 32015492 steps 228 queries 23.48 avg class size
c [sweep-23-2] 7300 decisions 230 SAT calls 113.27 avg env size
c [sweep-23-2] 169 variables remain 7% (2388 retained 93%)
c [decomp-122] removed 11 variables
c [sweep-23-2] removed 11 vars (0 failed, 15 eqs, 7 impls)
c [sweep-23] removed 60 vars in TOTAL (2 rounds, 568 queries)
c [sort-queue-27] sorted 2546 enqueued variables after 2672630 conflicts
c [score-dist-27] active 0 (0%), one 2546 (100%), zero 0 (0%)
c [score-dist-27] max exp 1, different 1 (50%)
c [score-dist-27] median active exp 0, avg 0.0
c [simplification-27] removed 211 variables 7.7% (2546 remain 5%)
c [simplification-27] removed 665 irredundant clauses 4.3% (14693 remain 10%)
c [simplification-27] maximum reduction of 8% = max (8%, 4%)
c [simplification-27] large reduction 8% >= 5% limit
c [simplification-27] next conflict interval 26726 = min (2672630/100, 612316)
c [simplification-27] penalized conflict interval 26726 = 1 * 26726
c [simplification-27] hard conflict limit 2712719 (soft 2699356 + delta 13363)
c [simplification-27] new conflict limit 2699356 (hard 2712719)
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 -  719.3    2546    14689   2698481  144393   6970 11345   12    27   30  44%   1010    1   11   10  110%
c 
c [simplification-28] limit 2699356 conflicts (hard 2712719) hit after 2699356 conflicts
c [quatres-24] found 10005 quaternary clauses 10% in total
c [quatres-24-1] removed 37 duplicate quaternary clauses
c [quatres-24-1] added 1 double-self-subsuming ternary resolvents
c [quatres-24-2] added 62 single-self-subsuming ternary resolvents
c [quatres-24-2] added 94 quaternary resolvents
c [ternres-24] limit 200000000 with penalty 0 = 0 + 0
c [ternres-24] all 2546 free variables schedulable
c [ternres-24] 539 ternary resolvents (34 bin, 505 trn)
c [ternres-24] fully completed ternary resolution
c [card-7] limit 7555180 penalty 4 = 4 + 0
c [card-7] found 473 at-most-one constraints of average size 3.3
c [card-7] found 95 at-most-two constraints of average size 4.0
c [card-7] using previous limit 7555180 for elimination
c [card-7] 565 out of 568 constraints (99%) meet size limits
c [card-7] no units found
c [card-7] no at-most-one constraints generated
c [gauss-7] limit 6044144 penalty 3 = 3 + 0
c [gauss-7] extracted 1345 xors of average arity 3.1
c [gauss-7] connected 4187 occurrences of 294 variables (average 14.2)
c [gauss-7] limit 6044144 penalty 3 = 3 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-123] removed 1 variables
c [treelook-9] limit 24176576 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 5090 literals 100%
c [treelook-9] scheduling used 497939 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 24176576 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 2911892 steps
c [treelook-9] fully completed tree based probing
c [decomp-124] removed 1 variables
c [treelook-9] removed 3 variables, found 819 hbrs
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 624 transitive binary clauses
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 2542 variables 100%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 46 variables 2% in round 1 in 2569082 steps
c [elim-21-1] backward subsumption/strengthening limit 2569000
c [elim-21-1-1] backward checking 219 touched variables 9%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 0 and strengthened 3 clauses in 71958 steps
c [elim-21-1] rescheduled 12 variables 0% by backward subsumption
c [elim-21-2] eliminated 1 variables 0% in round 2 in 6345 steps
c [elim-21-2] backward subsumption/strengthening limit 6300
c [elim-21-2-1] backward checking 7 touched variables 0%
c [elim-21-2-1] incomplete backward checking 0 remain 0%
c [elim-21-2] subsumed 0 and strengthened 0 clauses in 6301 steps
c [elim-21-2] fully rescheduled 2495 variables 98%
c [elim-21-3] eliminated 32 variables 1% in round 3 in 2520897 steps
c [elim-21-3] backward subsumption/strengthening limit 2520800
c [elim-21-3-1] backward checking 80 touched variables 3%
c [elim-21-3-1] fully completed backward checking in 1 rounds
c [elim-21-3] subsumed 3 and strengthened 1 clauses in 26564 steps
c [elim-21] incomplete 9 not tried 0% in round 3
c [elim-21] transition to [ all 1 rem 1 ] state
c [elim-21] eliminated 79 = 3% variables out of 2542 scheduled
c [bca-20] limit of 10000000 steps and 28881 added (scaled 2)
c [bca-20] 358 out of 4928 literals actually usable 7%
c [bca-20] added 0 blocked clauses in 144538 steps
c [sweep-24] limit 72529729 penalty 0 = 0 + 0
c [sweep-24-1] 100 pos 61.0% + 64 neg 39.0% = 164 sched 6.7% ret 2299
c [sweep-24-1] 7766429 steps 86 queries 7.69 avg class size
c [sweep-24-1] 2045 decisions 90 SAT calls 93.08 avg env size
c [sweep-24-1] fully completed sweeping round
c [decomp-125] removed 7 variables
c [sweep-24-1] removed 7 vars (0 failed, 6 eqs, 1 impls)
c [sweep-24-2] 1129 pos 46.0% + 1327 neg 54.0% = 2456 sched 100.0% ret 0
c [sweep-24-2] 22480915 steps 300 queries 17.47 avg class size
c [sweep-24-2] 6742 decisions 298 SAT calls 90.79 avg env size
c [sweep-24-2] fully completed sweeping round
c [decomp-126] removed 10 variables
c [sweep-24-2] removed 10 vars (0 failed, 16 eqs, 8 impls)
c [sweep-24-3] 1125 pos 46.0% + 1321 neg 54.0% = 2446 sched 100.0% ret 0
c [sweep-24-3] 31461543 steps 301 queries 20.85 avg class size
c [sweep-24-3] 7790 decisions 301 SAT calls 99.89 avg env size
c [sweep-24-3] fully completed sweeping round
c [decomp-127] removed 15 variables
c [sweep-24-3] removed 15 vars (0 failed, 19 eqs, 3 impls)
c [sweep-24] removed 32 vars in TOTAL (3 rounds, 684 queries)
c [sort-queue-28] sorted 2431 enqueued variables after 2699356 conflicts
c [score-dist-28] active 0 (0%), one 2431 (100%), zero 0 (0%)
c [score-dist-28] max exp 1, different 1 (50%)
c [score-dist-28] median active exp 0, avg 0.0
c [simplification-28] removed 115 variables 4.5% (2431 remain 5%)
c [simplification-28] removed 587 irredundant clauses 4.0% (14102 remain 9%)
c [simplification-28] maximum reduction of 5% = max (5%, 4%)
c [simplification-28] large reduction 5% >= 5% limit
c [simplification-28] next conflict interval 26993 = min (2699356/100, 612316)
c [simplification-28] penalized conflict interval 26993 = 1 * 26993
c [simplification-28] hard conflict limit 2739845 (soft 2726349 + delta 13496)
c [simplification-28] new conflict limit 2726349 (hard 2739845)
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  728.4    2430    14102   2734195  177218   7078 11161    8    10   37  76%   1016  -12    9   10   90%
c 
c [simplification-29] limit 2726349 conflicts (hard 2739845) hit after 2739845 conflicts
c [quatres-25] found 9817 quaternary clauses 9% in total
c [quatres-25-1] removed 21 duplicate quaternary clauses
c [quatres-25-2] added 39 single-self-subsuming ternary resolvents
c [quatres-25-2] added 62 quaternary resolvents
c [ternres-25] limit 200000000 with penalty 0 = 0 + 0
c [ternres-25] all 2430 free variables schedulable
c [ternres-25] 274 ternary resolvents (28 bin, 246 trn)
c [ternres-25] fully completed ternary resolution
c [decomp-128] removed 1 variables
c [basicprobe-9] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-9-0] 1271 sched 52%, 1 failed, 0 lifted, 67 hbrs
c [decomp-129] removed 1 variables
c [basicprobe-9-1] 1270 sched 52%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-9-2] 1269 sched 52%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-9-3] 1269 sched 52%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-9-3] fully completed probing
c [basicprobe-9-3] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-9-3] removed 1 variables, found 74 hbrs
c [bate-8] eliminated 3 asymmetric tautologies during probing
c [transred-25] limit 2000000 with penalty 0 = 0 + 0
c [transred-25] removed 493 transitive binary clauses
c [cce-15] limit of 613265874 steps penalty 1 = 1 + 0
c [cce-15-1] eliminated 1 clauses out of 9 (11%) of length 13
c [cce-15-1] eliminated 1 clauses out of 15 (7%) of length 12
c [cce-15-1] eliminated 1 clauses out of 21 (5%) of length 10
c [cce-15-1] eliminated 9 clauses out of 46 (20%) of length 9
c [cce-15-1] eliminated 20 clauses out of 139 (14%) of length 8
c [cce-15-1] eliminated 12 clauses out of 210 (6%) of length 7
c [cce-15-1] eliminated 44 clauses out of 437 (10%) of length 6
c [cce-15-1] eliminated 80 clauses out of 1152 (7%) of length 5
c [cce-15-1] eliminated 230 clauses out of 3495 (7%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 398 large clauses in 4404341 steps
c [cce-15-1] allowing another 2202170 steps for small clauses
c [cce-15-1] scheduling 4730 clauses = 2295 binary + 2435 ternary
c [cce-15-1] tried to eliminate 4730 small clauses 100%
c [cce-15-1] eliminated 122 binary clauses 5%
c [cce-15-1] eliminated 134 ternary clauses 6%
c [cce-15-1] eliminated 256 small clauses 5%
c [cce-15-1] eliminated 256 small clauses in 4667144 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 654 covered clauses in round 1
c [cce-15-2] eliminated 3 clauses out of 3 (100%) of length 15
c [cce-15-2] eliminated 2 clauses out of 11 (18%) of length 11
c [cce-15-2] eliminated 1 clauses out of 119 (1%) of length 8
c [cce-15-2] eliminated 8 clauses out of 198 (4%) of length 7
c [cce-15-2] eliminated 3 clauses out of 393 (1%) of length 6
c [cce-15-2] eliminated 15 clauses out of 1072 (1%) of length 5
c [cce-15-2] eliminated 23 clauses out of 3265 (1%) of length 4
c [cce-15-2] completed large round (ACCE)
c [cce-15-2] eliminated 55 large clauses in 3954918 steps
c [cce-15-2] allowing another 1977459 steps for small clauses
c [cce-15-2] scheduling 4474 clauses = 2173 binary + 2301 ternary
c [cce-15-2] tried to eliminate 4474 small clauses 100%
c [cce-15-2] eliminated 26 binary clauses 1%
c [cce-15-2] eliminated 13 ternary clauses 1%
c [cce-15-2] eliminated 39 small clauses 1%
c [cce-15-2] eliminated 39 small clauses in 4292413 steps
c [cce-15-2] completed small round (ACCE)
c [cce-15-2] eliminated 94 covered clauses in round 2
c [cce-15-3] eliminated 2 clauses out of 3242 (0%) of length 4
c [cce-15-3] completed large round (ACCE)
c [cce-15-3] eliminated 2 large clauses in 3907529 steps
c [cce-15-3] allowing another 1953764 steps for small clauses
c [cce-15-3] scheduling 4435 clauses = 2147 binary + 2288 ternary
c [cce-15-3] tried to eliminate 4435 small clauses 100%
c [cce-15-3] eliminated 2 binary clauses 0%
c [cce-15-3] eliminated 2 small clauses 0%
c [cce-15-3] eliminated 2 small clauses in 4251550 steps
c [cce-15-3] completed small round (ACCE)
c [cce-15-3] eliminated 4 covered clauses in round 3
c [cce-15] eliminated 752 covered clauses in TOTAL during 3 rounds
c [elim-22] no untried remaining variables left
c [elim-22] scheduled 2429 variables 100%
c [elim-22] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-22] rescheduling of touched variables disabled
c [elim-22-1] eliminated 153 variables 6% in round 1 in 2313704 steps
c [elim-22-1] backward subsumption/strengthening limit 2313700
c [elim-22-1-1] backward checking 320 touched variables 13%
c [elim-22-1-1] fully completed backward checking in 1 rounds
c [elim-22-1] subsumed 1 and strengthened 9 clauses in 92630 steps
c [elim-22-1] rescheduled 36 variables 1% by backward subsumption
c [elim-22-2] eliminated 2 variables 0% in round 2 in 101994 steps
c [elim-22-2] backward subsumption/strengthening limit 101900
c [elim-22-2-1] backward checking 19 touched variables 1%
c [elim-22-2-1] fully completed backward checking in 1 rounds
c [elim-22-2] subsumed 0 and strengthened 0 clauses in 12170 steps
c [elim-22] fully completed in 2 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 155 = 6% variables out of 2429 scheduled
c [sweep-25] boosting sweeping limit by 10
c [sweep-25] limit 735919040 penalty 0 = 0 + 0
c [sweep-25-1] 1040 pos 45.7% + 1234 neg 54.3% = 2274 sched 100.0% ret 0
c [sweep-25-1] 32757533 steps 276 queries 23.43 avg class size
c [sweep-25-1] 7762 decisions 278 SAT calls 98.03 avg env size
c [sweep-25-1] fully completed sweeping round
c [decomp-132] removed 6 variables
c [sweep-25-1] removed 6 vars (0 failed, 11 eqs, 2 impls)
c [sweep-25-2] 1039 pos 45.8% + 1229 neg 54.2% = 2268 sched 100.0% ret 0
c [sweep-25-2] 51146724 steps 283 queries 22.18 avg class size
c [sweep-25-2] 10363 decisions 288 SAT calls 108.77 avg env size
c [sweep-25-2] fully completed sweeping round
c [decomp-133] removed 9 variables
c [sweep-25-2] removed 9 vars (0 failed, 15 eqs, 3 impls)
c [sweep-25-3] 1036 pos 45.9% + 1223 neg 54.1% = 2259 sched 100.0% ret 0
c [sweep-25-3] 34095101 steps 254 queries 23.19 avg class size
c [sweep-25-3] 7099 decisions 253 SAT calls 105.20 avg env size
c [sweep-25-3] fully completed sweeping round
c [decomp-134] removed 9 variables
c [sweep-25-3] removed 9 vars (0 failed, 14 eqs, 4 impls)
c [sweep-25] removed 24 vars in TOTAL (3 rounds, 810 queries)
c [sort-queue-29] sorted 2250 enqueued variables after 2739845 conflicts
c [score-dist-29] active 0 (0%), one 2250 (100%), zero 0 (0%)
c [score-dist-29] max exp 1, different 1 (50%)
c [score-dist-29] median active exp 0, avg 0.0
c [simplification-29] removed 180 variables 7.4% (2250 remain 4%)
c [simplification-29] removed 1131 irredundant clauses 8.0% (12971 remain 9%)
c [simplification-29] maximum reduction of 8% = max (7%, 8%)
c [simplification-29] large reduction 8% >= 5% limit
c [simplification-29] next conflict interval 27398 = min (2739845/100, 612316)
c [simplification-29] penalized conflict interval 27398 = 1 * 27398
c [simplification-29] hard conflict limit 2780942 (soft 2767243 + delta 13699)
c [simplification-29] new conflict limit 2767243 (hard 2780942)
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  736.2    2249    12971   2742555  173442   6836 10243    9    21   33  41%  -5927   -1   11   10  112%
c -  746.9    2249    12971   2770740  141479   6870 10256   11    19   29  56%  -3585   -3    8   10   83%
c i  747.6    2248    12971   2773944  144575   6872 10260   11    22   36  47%  -3365    1   11   10  106%
c i  748.9    2247    12971   2780838  150958   6879 10263   11    27   37  40%  -3375    5   12   10  121%
c 
c [simplification-30] limit 2767243 conflicts (hard 2780942) hit after 2780943 conflicts
c [quatres-26] found 9336 quaternary clauses 9% in total
c [quatres-26-1] removed 11 duplicate quaternary clauses
c [quatres-26-2] added 33 single-self-subsuming ternary resolvents
c [quatres-26-2] added 74 quaternary resolvents
c [ternres-26] limit 200000000 with penalty 0 = 0 + 0
c [ternres-26] all 2247 free variables schedulable
c [ternres-26] 276 ternary resolvents (26 bin, 250 trn)
c [ternres-26] fully completed ternary resolution
c [decomp-135] removed 8 variables
c [simpleprobe-10] all 2242 free variables schedulable
c [simpleprobe-10] limit 200000000 penalty 0 = 0 + 0
c [decomp-136] removed 6 variables
c [simpleprobe-10] fully completed simple probing
c [simpleprobe-10] removed 6 variables, found 1314 hbrs, 0 units
c [transred-26] limit 2000000 with penalty 0 = 0 + 0
c [transred-26] removed 660 transitive binary clauses
c [cce-16] limit of 1249132226 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 1 clauses out of 1 (100%) of length 15
c [cce-16-1] eliminated 1 clauses out of 5 (20%) of length 13
c [cce-16-1] eliminated 1 clauses out of 44 (2%) of length 9
c [cce-16-1] eliminated 2 clauses out of 124 (2%) of length 8
c [cce-16-1] eliminated 5 clauses out of 184 (3%) of length 7
c [cce-16-1] eliminated 4 clauses out of 387 (1%) of length 6
c [cce-16-1] eliminated 25 clauses out of 1057 (2%) of length 5
c [cce-16-1] eliminated 57 clauses out of 3207 (2%) of length 4
c [cce-16-1] completed large round (ATE)
c [cce-16-1] eliminated 96 large clauses in 2944166 steps
c [cce-16-1] allowing another 1472083 steps for small clauses
c [cce-16-1] scheduling 5606 clauses = 2039 binary + 3567 ternary
c [cce-16-1] tried to eliminate 5606 small clauses 100%
c [cce-16-1] eliminated 12 binary clauses 1%
c [cce-16-1] eliminated 107 ternary clauses 3%
c [cce-16-1] eliminated 119 small clauses 2%
c [cce-16-1] eliminated 119 small clauses in 3520083 steps
c [cce-16-1] completed small round (ATE)
c [cce-16-1] eliminated 215 covered clauses in round 1
c [cce-16-2] completed large round (ATE)
c [cce-16-2] allowing another 1432209 steps for small clauses
c [cce-16-2] scheduling 5487 clauses = 2027 binary + 3460 ternary
c [cce-16-2] tried to eliminate 5487 small clauses 100%
c [cce-16-2] completed small round (ATE)
c [cce-16-2] eliminated 0 covered clauses in round 2
c [cce-16] eliminated 215 covered clauses in TOTAL during 2 rounds
c [elim-23] scheduling all variables this time
c [elim-23] scheduled 2236 variables 100%
c [elim-23] almost no limit of 100000000000 steps
c [elim-23] rescheduling of touched variables disabled
c [elim-23-1] eliminated 44 variables 2% in round 1 in 2282319 steps
c [elim-23-1] backward subsumption/strengthening limit 2282300
c [elim-23-1-1] backward checking 279 touched variables 12%
c [elim-23-1-1] fully completed backward checking in 1 rounds
c [elim-23-1] subsumed 0 and strengthened 0 clauses in 102710 steps
c [elim-23] fully completed in 1 rounds
c [elim-23] transition to [ all 0 rem 0 ] state
c [elim-23] eliminated 44 = 2% variables out of 2236 scheduled
c [bca-21] limit of 10000000 steps and 25607 added (scaled 2)
c [bca-21] 308 out of 4386 literals actually usable 7%
c [bca-21] added 3 blocked clauses in 139419 steps
c [sweep-26] limit 74947933 penalty 0 = 0 + 0
c [sweep-26-1] 919 pos 41.9% + 1273 neg 58.1% = 2192 sched 100.0% ret 0
c [sweep-26-1] 25766070 steps 278 queries 24.09 avg class size
c [sweep-26-1] 7150 decisions 273 SAT calls 104.75 avg env size
c [sweep-26-1] fully completed sweeping round
c [decomp-137] removed 19 variables
c [sweep-26-1] removed 19 vars (0 failed, 20 eqs, 12 impls)
c [sweep-26-2] 914 pos 42.1% + 1259 neg 57.9% = 2173 sched 100.0% ret 0
c [sweep-26-2] 26523038 steps 272 queries 21.28 avg class size
c [sweep-26-2] 6325 decisions 270 SAT calls 87.17 avg env size
c [sweep-26-2] fully completed sweeping round
c [decomp-138] removed 4 variables
c [sweep-26-2] removed 4 vars (0 failed, 6 eqs, 6 impls)
c [sweep-26-3] 913 pos 42.1% + 1256 neg 57.9% = 2169 sched 100.0% ret 0
c [sweep-26-3] 23839894 steps 167 queries 31.89 avg class size
c [sweep-26-3] 6135 decisions 172 SAT calls 108.35 avg env size
c [sweep-26-3] 298 variables remain 14% (1871 retained 86%)
c [decomp-139] removed 4 variables
c [sweep-26-3] removed 4 vars (0 failed, 5 eqs, 3 impls)
c [sweep-26] removed 27 vars in TOTAL (3 rounds, 714 queries)
c [sort-queue-30] sorted 2165 enqueued variables after 2780943 conflicts
c [score-dist-30] active 0 (0%), one 2165 (100%), zero 0 (0%)
c [score-dist-30] max exp 1, different 1 (50%)
c [score-dist-30] median active exp 0, avg 0.0
c [simplification-30] removed 82 variables 3.6% (2165 remain 4%)
c [simplification-30] removed 497 irredundant clauses 3.8% (12474 remain 8%)
c [simplification-30] maximum reduction of 4% = max (4%, 4%)
c [simplification-30] geometric conflict interval increment 122463 = 612316 / 5
c [simplification-30] new conflict interval 734779
c [simplification-30] penalized conflict interval 734779 = 1 * 734779
c [simplification-30] hard conflict limit 3883111 (soft 3515722 + delta 367389)
c [simplification-30] new conflict limit 3515722 (hard 3883111)
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.7    2164    12474   2781276  141669   6567 10575   11    27   26  41%  -3383    5   12   10  117%
c i  760.2    2163    12474   2819991  178196   6587 10580   10    20   37  49%  -1461   -3   12   10  120%
c -  764.6    2163    12474   2839054  140179   6589 10581    9    25   27  38%  -1293    2   10   10  103%
c i  767.8    2162    12474   2859589  158621   6633 10595    7    11   34  64%   -670  -11    5    9   49%
c i  773.3    2160    12474   2885560  182609   6648 10599   10    19   40  51%   -538   -2    8    9   87%
c -  779.4    2160    12474   2904250  143033   6662 10601    8    14   27  56%   -461   -7    8    9   86%
c i  785.8    2159    12474   2924800  161848   6677 10612   12    22   35  53%    -61    2   12   10  124%
c -  796.8    2159    12474   2969876  140431   6688 10613    9    11   27  81%    165   -8    9   10   91%
c i  800.0    2158    12474   2993967  156087   6759 10625    7     8   34  84%    430   -8    5    9   59%
c i  801.9    2139    12474   3006431  165627   6828 10642    7     9   34  76%   -375   -6    4    9   48%
c i  803.2    2134    12474   3013934  171080   6875 10654    7     9   38  79%   -400   -6    6    9   65%
c i  803.3    2123    12474   3014851  171691   6904 10665    6     8   38  79%   -449   -6    4    9   51%
c i  803.8    2102    12474   3017905  173757   6929 10675    6     8   38  78%   -439   -6    5    9   56%
c i  803.9    2086    12474   3018930  174386   6947 10682    6     8   38  80%   -449   -6    5    8   61%
c i  804.1    2082    12474   3019748  174992   6972 10688    6     8   38  79%   -449   -6    5    8   57%
c i  804.1    2081    12474   3019985  175131   6987 10693    6     8   38  79%   -450   -6    5    8   54%
c i  804.1    2075    12474   3020106  175209   6991 10694    6     7   38  79%   -450   -6    5    8   55%
c i  804.1    2073    12474   3020110  175209   6991 10696    6     7   38  79%   -450   -6    5    8   54%
c i  804.1    2070    12474   3020157  175222   7002 10701    6     7   38  80%   -450   -6    4    8   50%
c i  804.1    1691    12474   3020185  175247   7002 10702    6     7   38  80%   -450   -6    4    8   48%
c i  804.1    1632    12474   3020201  175243   7005 10703    6     7   38  80%   -450   -6    4    8   47%
c i  804.1    1614    12474   3020209  175248   7005 10704    6     7   38  80%   -450   -6    4    8   46%
c i  804.1    1555    12474   3020211  175248   7005 10705    6     7   38  80%   -450   -6    4    8   46%
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  804.1    1554    12474   3020213  175248   7005 10706    6     7   38  80%   -450   -7    4    8   46%
c i  804.1    1545    12474   3020215  175249   7005 10706    6     7   38  80%   -450   -7    4    8   45%
c i  804.1    1493    12474   3020216  175249   7005 10706    6     7   38  80%   -450   -7    4    8   45%
c 0  804.1    1468    12474   3020216  175249   7005 10706    6     7   38  80%   -450   -7    4    8   45%
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 
s UNSATISFIABLE
c
c bate: 385 basic ate = 204 trn 53% + 181 lrg 47% in 8 updates
c bcas: 21 count, 273 added (551 skipped), 2282506 steps
c bkwd: tried 163388 clauses, 326499 lits, 2.00 lits/clause
c bkwd: checked 37200717 occs, 227.68 occs/clause, 113.94 occs/lit
c bkwd: subsumed 2 binary, 26 ternary, 41 large
c bkwd: strengthened 1 binary, 7 ternary (100% self), 372 large (0% self)
c blkd: 12 bces, 9239 removed, 3329802 resolutions, 8647968 steps
c blkd: 5477 blocking literals 5%, 751 pure
c bump: 3067529 bumped seen, 184056772 lits 60.0 on average
c card: 7 count, 0 units, 84 am1, 36157889 steps
c card: 40 rescheduled, 337 eliminated, 15145 resolved, 5844 subsumed
c card: 1481 at-most-one constraints found, average size 3.10
c card: 1481 at-most-one constraints used 100%, average size 3.10
c card: 99 at-most-two constraints found, average size 4.03
c card: 96 at-most-two constraints used 97%, average size 4.03
c cces: 16 cces, 15780 eliminated, 12051 ate 76%, 3729 abce 24%
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: 511854 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 189 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 139 decompositions, 4600 equivalent 9%
c deco: 9 decision-only clauses 0%, 66% reduction
c decs: 11000291 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 23 elims, 43301 eliminated 83%, 691 pure 2%
c elms: 66 rounds, 2.9 rounds/bve
c elms: 39861 small 92%, 1998 large 5%
c elms: 82962 tried small, 39861 succeeded 48%, 43101 failed 52%
c elms: 5244 subsumed, 5770 strengthened, 1536 blocked
c elms: 5535906 copies, 7468713 resolutions, 2763977 ipos
c elms: 2807544 subchks, 1861382 strchks
c gaus: 7 extractions, 11112 extracted, 3.0 size, 4 max
c gaus: exported 0 units, 0 binary and 3 ternary equations
c gaus: 0 gc, 13568958 steps, 6784479 extr 50%, 591597 elim 4%
c glue: 9.2 orig avg, 9.2 real avg, 2.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 84532 = 22680 simple 27% + 51986 trn 61% + 9866 lrg 12%, 1628 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3067529 clauses, 26.6 length
c lrnd: 81475002 lits = 117074057 orig - 35599055 removed 30%
c lrnd: 589831 uips 19%, 2247575 flips 73%
c mins: 3040818 mins 99%, 1088 bin 0%, 25614 size 1%
c mins: 135073294 poisoned searches, 20760346 hits, 15% hit rate
c mins: 228191360 used twice searches, 10881488 hits, 5% hit rate
c move: moved 10964, 3638 bin 33%, 7326 trn 67%
c otfs: 13187 driving 30%, 30061 restarting 70%
c otfs: str 43248, 42678 red 99%, 570 irr 1%
c otfs: str 43248, 0 bin 0%, 1170 trn 3%, 42078 lrg 97%
c otfs: sub 862, 777 red 90%, 85 irr 10%
c otfs: sub 862, 0 bin 0%, 119 trn 14%, 743 lrg 86%
c phas: 1 computed, 13304 set, 3169 pos (24%), 10135 neg (76%)
c prbs: 9 basic, 351628 probed, 136 failed, 13 lifted
c prbs: 10 simple, 218662 probed, 173 failed, 2417 eqs
c prbs: 9 treelook, 21779 probed, 15 failed, 0 lifted
c prom: 1025625 locked 15% out of 6978646 tried
c prps: 548769522 props, 46 props/dec
c prps: 93% srch, 7% simp, 0% lkhd
c quat: 26 count, 8777 quat, 2999 self1, 125 self2, 1345 dup
c queu: 30 sorted, 11000291 next (153 steps 0.00)
c queu: 184349393 enq (0 steps 0.00), 184056772 deq 100%
c redc: 97619 clauses 13%, 753321 tried 25%, 30 sat 0%
c redc: 136903 lits 1%, 11836219 tried 10%, 30 sat 0%
c redc: 1634 times jump level reduced, 4.3 levels on average
c reds: 57 count, 52986.2 conflicts per reduce
c reds: 0 memlim 0%, 57 arith 100%
c reds: 2223129 collected 87%, 334347 retired 13%
c rmbd: 3542 removed, 3183 red 90%
c rsts: 82606 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 30 count, 28 confs 93%, 0 vars 0%
c simp: 1 its 3%, 1 bin 3%, 0 trns 0%
c subl: 3067529 count (1248225 tried 0.4), 182061 sub out of 3055998 (6.0%)
c swps: 26 count, 48 rounds, 14316 queries (298.2/round)
c swps: 13890 sat calls, 1168 unsat (4.4% success rate)
c swps: 303266 decisions 21.8, 60500 conflicts 4.4
c swps; 54.3 avg class size, 72.6 avg environment size
c swps: 0 failed, 1286 impls, 1591 equivs
c swp0: 4753 type 0 queries, 1152 unsat (24.2%), 4438 sat (93.4%)
c swp1: 9563 type 1 queries, 4239 unsat (44.3%), 8287 sat (86.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: 28136354 calls to obtain time
c tops: 3057 fixed 6%, 71 its, 42538.25 confs/it
c trds: 26 transitive reductions, 20249 removed, 16 failed
c trds: 292713 nodes, 319552 edges, 37487566 steps
c trim: 1205125 words, 4.6 MB
c trnr: 26 count, 1648 bin, 58240 trn, 570647444 steps
c unhd: 9 count, 9 rounds, 10367920 steps
c unhd: 190 non-trivial sccs of average size 2.0
c unhd: 1 units, 1 bin, 0 trn, 0 lrg
c unhd: 2 failed, 2 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 14420 tauts, 315 bin 2%, 4375 trn 30%, 2606 lrg 18%
c unhd: 14420 tauts, 7124 stamp 49%, 14216 red 99%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 156943 str, 1 bin 0%, 695 trn 0%, 156247 lrg 100%, 154265 red 98%
c vars: 1478 remaining 3% and 50958 removed 97% out of 52436
c vars: 3057 fixed 6%, 43301 eliminated 83%, 4600 equivalent 9%
c vsts: 28662617903 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 54.2 search visits per propagation, 9146.2 per conflict
c wchs: 11400904471 pushed, 16760274 enlarged, 365 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3064775       2223129        334347     116260376      32236290       1922178
c 
c  0 0        327711  11    132048   6         0   0  83775261  72< 18237245  57    840347  44     4.7
c  1 5        261398   9    186653   8     36875  11  13553442  12   4441656  14<   268614  14<    1.1
c  2 6        967149  32<   756050  34<    94296  28  13922514  12   6180685  19    482698  25     3.5
c  3 9       1070909  35    839105  38    111560  33<  4128035   4   2729826   8    264473  14     4.9
c  4 14       371505  12    268735  12     70425  21    792454   1    589097   2     61927   3     2.0
c  5 21        56774   2     35305   2     17655   5     77179   0     51158   0      3763   0     0.4
c  6 30         7845   0      4416   0      2951   1      9704   0      5622   0       311   0     0.1
c  7 41         1207   0       666   0       483   0      1459   0       807   0        37   0     0.0
c  8 54          223   0       125   0        86   0       264   0       150   0         5   0     0.0
c  9 69           33   0        16   0        12   0        36   0        20   0         3   0     0.0
c 10 86           21   0        10   0         4   0        28   0        24   0         0   0     0.0
c 
c avg                  2.4           2.5           2.8           0.5           0.9           1.2
c std                  1.2           1.1           1.1           0.9           1.1           1.2
c 
c   29.562   4% sweep
c   24.395   3% cce
c   16.069   2% probe
c    8.874   1% elim
c    7.826   1% ternres
c    7.667   1% bump
c    7.438   1% decide
c 
c    9.482 < 1% rest (below)
c 
c    2.953   0% quatres
c    2.532   0% transred
c    1.084   0% unhide
c    1.068   0% block
c    1.061   0% bca
c    0.511   0% gauss
c    0.272   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.552   0% preprocessing     2%
c   98.327  12% inprocessing     98%
c ==================================
c   99.879  12% simplifying
c  704.263  88% search
c ==================================
c  804.142 100% all
c 
c       3020216 conflicts,        3755.8 confs/sec
c          6281 ternaries,         480.8 confs/ternary
c          1092 binaries,         2765.8 confs/binary
c            71 iterations,      42538.3 confs/iteration
c 
c            57 reductions,          0.1 redus/sec,  52986.2 confs/reduction
c         82606 restarts,          102.7 rests/sec,     36.6 confs/restart
c      11000291 decisions,       13679.5 decis/sec,      3.6 decis/conflict
c     548769522 propagations,   682428.8 props/sec,     49.9 props/decision
c 
c 804.1 seconds, 59.2 MB
c launch: done
