c launch: /data/cnf/sc2014/app/11pipe_k.cnf.bz2
c host: atom24
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/11pipe_k.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/11pipe_k.cnf.bz2
c no embedded options
c found 'p cnf 89315 5584003' header
c read 89315 variables, 5584003 clauses, 16593705 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=6
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 89314 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] AVG (--score=6)
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   89314  5584002         0       0      0     0    0     0  158   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1396000 based on 5584002 irredundant clauses
c [card-1] found 1 at-most-one constraints of average size 4.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1396000 for elimination
c [card-1] 1 out of 1 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 13 variables
c [simpleprobe-1] all 89302 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 11166260 based on 5583130 irredundant clauses
c [simpleprobe-1] 82260 variables remain 92% (7042 retained 8%)
c [simpleprobe-1] removed 0 variables, found 5233 hbrs, 0 units
c [unhide-1] limit 348945 based on 5583130 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 89302 variables 100%
c [elim-1] limit of 5583130 steps based on 5583130 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 89254 not tried 100% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 48 = 0% variables out of 89302 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 5581640 negative 100.0% of 5583034 except 1394 0.0%
c [phase-count-1] 382045 positive 6.8% of 5583034 except 5200989 93.2%
c [phase-count-1] less non-negative clauses 1394 than limit 558300 (10.0%)
c [phase-count-1] non-pos/non-neg = 5200989/1394 = 3730.98 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 89254 negative 100%
c [sort-queue-1] sorted 89254 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 89254 (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 48 variables 0.1% (89254 remain 100%)
c [simplification-1] removed 968 irredundant clauses 0.0% (5583034 remain 100%)
c [simplification-1] maximum reduction of 0% = max (0%, 0%)
c [simplification-1] full geometric conflict interval increment 20000
c [simplification-1] new conflict interval 20000
c [simplification-1] penalized conflict interval 20000 = 1 * 20000
c [simplification-1] hard conflict limit 30000 (soft 20000 + delta 10000)
c [simplification-1] new conflict limit 20000 (hard 30000)
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [treelook-1] limit 1395758 based on 5583034 irredundant clauses
c [treelook-1] scheduled 88037 literals 49%
c [treelook-1] scheduling used 1396194 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1395758 based on 5583034 irredundant clauses
c [treelook-1] used 10735160 steps
c [treelook-1] 88034 literals remain 49%
c [treelook-1] 80288 variables remain to probed next time 90%
c [treelook-1] removed 0 variables, found 69 hbrs
c [basicprobe-1] limit 44664272 based on 5583034 irredundant clauses
c [basicprobe-1-0] 80711 probes remain 91% after last round
c [basicprobe-1-0] 264 units = 264 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 282 variables, found 11574 hbrs
c [elim-2] 88972 variables 100% will be scheduled this time
c [elim-2] scheduled 88972 variables 100%
c [elim-2] limit of 5547540 steps based on 5547540 irredundant clauses
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 88489 not tried 99% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 483 = 1% variables out of 88972 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 71241 enqueued variables after 2635 conflicts
c [score-dist-2] active 17248 (19%), one 0 (0%), zero 71241 (81%)
c [score-dist-2] max exp 513, different 11 (2%)
c [score-dist-2] median active exp 512, avg 511.4
c [simplification-2] removed 765 variables 0.9% (88489 remain 99%)
c [simplification-2] removed 36459 irredundant clauses 0.7% (5546575 remain 99%)
c [simplification-2] maximum reduction of 1% = max (1%, 1%)
c [simplification-2] forced so keeping old conflict interval 20000
c [simplification-2] conflict limit remains at 20000 (hard 30000)
c [simplification-2] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   40.2   88488  5546575     16659   13766    446 17606   53   301  165  18%    217  248   67   12  570%
c 
c [simplification-3] limit 20000 conflicts (hard 30000) hit after 20005 conflicts
c [card-2] limit 1386643 based on 5546575 irredundant clauses
c [card-2] found 1 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1386643 for elimination
c [card-2] 1 out of 1 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 1 variables
c [simpleprobe-2] 81508 schedulable variables 92%
c [simpleprobe-2] limit 11093084 based on 5546542 irredundant clauses
c [simpleprobe-2] 70729 variables remain 80% (17759 retained 20%)
c [simpleprobe-2] removed 0 variables, found 5636 hbrs, 0 units
c [unhide-2] limit 346658 based on 5546542 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 13 tauts, 0 hbrs, 8880 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 88488 variables 100%
c [elim-3] limit of 11292235 steps penalty 3 = 0 + 3
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 86357 not tried 98% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2131 = 2% variables out of 88488 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 49694 enqueued variables after 20005 conflicts
c [score-dist-3] active 36663 (42%), one 0 (0%), zero 49694 (58%)
c [score-dist-3] max exp 516, different 13 (3%)
c [score-dist-3] median active exp 515, avg 514.3
c [simplification-3] removed 2131 variables 2.4% (86357 remain 97%)
c [simplification-3] removed 4003 irredundant clauses 0.1% (5542572 remain 99%)
c [simplification-3] maximum reduction of 2% = max (2%, 0%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 26666
c [simplification-3] penalized conflict interval 26666 = 1 * 26666
c [simplification-3] hard conflict limit 60004 (soft 46671 + delta 13333)
c [simplification-3] new conflict limit 46671 (hard 60004)
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.5   86356  5542572     26734   21917    496 21838   59   298  170  20%    105  215   74   18  411%
c 
c [simplification-4] limit 46671 conflicts (hard 60004) hit after 46671 conflicts
c [decomp-7] removed 1 variables
c [elim-4] 86356 variables 100% will be scheduled this time
c [elim-4] scheduled 86356 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 530226657 steps penalty 3 = 0 + 3
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 24791 not tried 29% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 7357 = 9% variables out of 86356 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 36465 enqueued variables after 46671 conflicts
c [score-dist-4] active 42534 (54%), one 0 (0%), zero 36465 (46%)
c [score-dist-4] max exp 517, different 12 (2%)
c [score-dist-4] median active exp 517, avg 516.1
c [simplification-4] removed 7357 variables 8.5% (78999 remain 88%)
c [simplification-4] removed 14857 irredundant clauses 0.3% (5527715 remain 99%)
c [simplification-4] maximum reduction of 9% = max (9%, 0%)
c [simplification-4] large reduction 9% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 58671 (soft 48671 + delta 10000)
c [simplification-4] new conflict limit 48671 (hard 58671)
c 
c [simplification-5] limit 48671 conflicts (hard 58671) hit after 48671 conflicts
c [quatres-1] found 7885 quaternary clauses 6% in total
c [quatres-1-2] added 293 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 22110860 based on 5527715 irredundant clauses
c [ternres-1] all 78999 free variables schedulable
c [ternres-1] 5203 ternary resolvents (0 bin, 5203 trn)
c [ternres-1] 453 variables remain 1% (78546 retained 99%)
c [gauss-1] limit 2763857 based on 5527715 irredundant clauses
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-2] limit 1381928 based on 5527715 irredundant clauses
c [treelook-2] scheduled 80519 literals 51%
c [treelook-2] scheduling used 1381948 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1381928 based on 5527715 irredundant clauses
c [treelook-2] used 5822434 steps
c [treelook-2] 80517 literals remain 51%
c [treelook-2] 73756 variables remain to probed next time 93%
c [treelook-2] removed 0 variables, found 190 hbrs
c [transred-1] limit 5527715 based on 5527715 irredundant clauses
c [transred-1] removed 2 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 78999 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 136267348 steps penalty 3 = 0 + 3
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 148231 blocked clauses
c [cce-1] limit of 6813367 steps penalty 3 = 0 + 3
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 295
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 2 large clauses in 6815771 steps
c [cce-1-1] allowing another 3407885 steps for small clauses
c [cce-1-1] scheduling 5228134 clauses = 5226869 binary + 1265 ternary
c [cce-1-1] tried to eliminate 5 small clauses 0%
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2 covered clauses in round 1
c [cce-1] eliminated 2 covered clauses in TOTAL during 1 rounds
c [cce-1] 2 < 1/100 * 5379482 = 53794 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 78991 variables 100%
c [elim-5] limit of 27253469 steps penalty 3 = 0 + 3
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 76472 not tried 97% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2519 = 3% variables out of 78991 scheduled
c [bca-1] limit of 10000000 steps and 10754422 added (scaled 2)
c [bca-1] 125783 out of 152946 literals actually usable 82%
c [bca-1] added 22920 blocked clauses in 480571 steps
c [sweep-1] limit 10753922 based on 5376961 irredundant clauses
c [sweep-1-1] 765 pos 1.0% + 75707 neg 99.0% = 76472 sched 100.0% ret 0
c [sweep-1-1] 10833363 steps 112 queries 3368.35 avg class size
c [sweep-1-1] 3456 decisions 96 SAT calls 416.49 avg env size
c [sweep-1-1] 64328 variables remain 84% (12144 retained 16%)
c [decomp-10] removed 18 variables
c [sweep-1-1] removed 18 vars (0 failed, 18 eqs, 37 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 18 vars in TOTAL (1 rounds, 111 queries)
c [sort-queue-5] sorted 34295 enqueued variables after 48671 conflicts
c [score-dist-5] active 42159 (55%), one 0 (0%), zero 34295 (45%)
c [score-dist-5] max exp 517, different 12 (2%)
c [score-dist-5] median active exp 517, avg 516.1
c [simplification-5] removed 2545 variables 3.2% (76454 remain 86%)
c [simplification-5] removed 150754 irredundant clauses 2.7% (5376961 remain 96%)
c [simplification-5] maximum reduction of 3% = max (3%, 3%)
c [simplification-5] geometric conflict interval increment 6666 = 26666 / 4
c [simplification-5] new conflict interval 33332
c [simplification-5] penalized conflict interval 33332 = 1 * 33332
c [simplification-5] hard conflict limit 98669 (soft 82003 + delta 16666)
c [simplification-5] new conflict limit 82003 (hard 98669)
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 -  148.1   76454  5376961     79818   18135   7631 56636   38   208  166  18%    544   41   36   32  110%
c 
c [simplification-6] limit 82003 conflicts (hard 98669) hit after 82003 conflicts
c [quatres-2] found 7957 quaternary clauses 6% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [quatres-2-2] added 298 quaternary resolvents
c [ternres-2] limit 21507844 based on 5376961 irredundant clauses
c [ternres-2] 452 schedulable variables 1%
c [ternres-2] 3788 ternary resolvents (1 bin, 3787 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 1344240 based on 5376961 irredundant clauses
c [card-3] found 1 at-most-one constraints of average size 4.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1344240 for elimination
c [card-3] 1 out of 1 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 43015688 based on 5376961 irredundant clauses
c [basicprobe-2-0] 71409 probes remain 94% after last round
c [basicprobe-2-0] 252 units = 252 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 252 variables, found 1885 hbrs
c [unhide-3] limit 336060 based on 5376961 irredundant clauses
c [unhide-3-3] 0 units, 1 failed, 7286 tauts, 0 hbrs, 4663 literals
c [transred-2] limit 5335772 based on 5335772 irredundant clauses
c [transred-2] removed 0 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 76201 variables 100%
c [block-2] limit of 19986657 steps penalty 3 = 0 + 3
c [block-2] incomplete 14376 not tried 19%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 99 blocked clauses
c [block-2] 99 < 1/100 * 5335772 = 53357 considered unsuccessful
c [elim-6] 24473 variables 32% will be scheduled this time
c [elim-6] scheduled 24473 variables 32%
c [elim-6] limit of 39973314 steps penalty 3 = 0 + 3
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 24312 not tried 32% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 38 = 0% variables out of 24473 scheduled
c [elim-6] 38 < 1/100 * 24473 = 244 considered unsuccessful
c [bca-2] limit of 10000000 steps and 10683038 added (scaled 2)
c [bca-2] 125826 out of 152328 literals actually usable 83%
c [bca-2] added 743 blocked clauses in 497092 steps
c [sweep-2] limit 10671078 based on 5335539 irredundant clauses
c [sweep-2-1] 725 pos 1.1% + 63315 neg 98.9% = 64040 sched 84.1% ret 12123
c [sweep-2-1] 10721831 steps 135 queries 1804.66 avg class size
c [sweep-2-1] 3205 decisions 106 SAT calls 618.05 avg env size
c [sweep-2-1] 55543 variables remain 73% (20620 retained 27%)
c [decomp-12] removed 28 variables
c [sweep-2-1] removed 28 vars (0 failed, 28 eqs, 61 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 28 vars in TOTAL (1 rounds, 134 queries)
c [sort-queue-6] sorted 30592 enqueued variables after 82003 conflicts
c [score-dist-6] active 45543 (60%), one 0 (0%), zero 30592 (40%)
c [score-dist-6] max exp 518, different 13 (3%)
c [score-dist-6] median active exp 517, avg 516.9
c [simplification-6] removed 319 variables 0.4% (76135 remain 85%)
c [simplification-6] removed 41422 irredundant clauses 0.8% (5335539 remain 96%)
c [simplification-6] maximum reduction of 1% = max (0%, 1%)
c [simplification-6] geometric conflict interval increment 16666 = 33332 / 2
c [simplification-6] new conflict interval 49998
c [simplification-6] penalized conflict interval 49998 = 1 * 49998
c [simplification-6] hard conflict limit 157000 (soft 132001 + delta 24999)
c [simplification-6] new conflict limit 132001 (hard 157000)
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 -  189.3   76135  5335476    123050   24081  11859 54169   63   276  166  23%    776   29   30   46   65%
c 
c [simplification-7] limit 132001 conflicts (hard 157000) hit after 132565 conflicts
c [quatres-3] found 8304 quaternary clauses 6% in total
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 255 quaternary resolvents
c [ternres-3] limit 21341904 based on 5335476 irredundant clauses
c [ternres-3] all 76135 free variables schedulable
c [ternres-3] 330 ternary resolvents (1 bin, 329 trn)
c [ternres-3] 14024 variables remain 18% (62111 retained 82%)
c [gauss-2] limit 2667738 based on 5335476 irredundant clauses
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [cce-2] limit of 7603114 steps penalty 4 = 1 + 3
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 3801564 steps for small clauses
c [cce-2-1] scheduling 5185119 clauses = 5183617 binary + 1502 ternary
c [cce-2-1] tried to eliminate 1 small clauses 0%
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 0 covered clauses in round 1
c [cce-2] eliminated 0 covered clauses in TOTAL during 1 rounds
c [bca-3] limit of 10000000 steps and 10683283 added (scaled 2)
c [bca-3] 107401 out of 152272 literals actually usable 71%
c [bca-3] added 0 blocked clauses in 383272 steps
c [sweep-3] limit 10670952 based on 5335476 irredundant clauses
c [sweep-3-1] 723 pos 1.3% + 54813 neg 98.7% = 55536 sched 72.9% ret 20599
c [sweep-3-1] 11240425 steps 127 queries 2910.96 avg class size
c [sweep-3-1] 3437 decisions 93 SAT calls 482.44 avg env size
c [sweep-3-1] 49592 variables remain 65% (26543 retained 35%)
c [decomp-14] removed 34 variables
c [sweep-3-1] removed 34 vars (0 failed, 34 eqs, 74 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 34 vars in TOTAL (1 rounds, 126 queries)
c [sort-queue-7] sorted 20909 enqueued variables after 132565 conflicts
c [score-dist-7] active 55192 (73%), one 0 (0%), zero 20909 (27%)
c [score-dist-7] max exp 518, different 12 (2%)
c [score-dist-7] median active exp 518, avg 517.8
c [simplification-7] removed 34 variables 0.0% (76101 remain 85%)
c [simplification-7] removed 0 irredundant clauses 0.0% (5335476 remain 96%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 49998
c [simplification-7] new conflict interval 99996
c [simplification-7] penalized conflict interval 99996 = 1 * 99996
c [simplification-7] hard conflict limit 282559 (soft 232561 + delta 49998)
c [simplification-7] new conflict limit 232561 (hard 282559)
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 -  208.5   76101  5335476    162644   27274  12417 55014   45   255  168  17%    888   19   62   45  137%
c -  221.6   76101  5335422    201073   27970  12748 55288   34   223  169  15%    949   -7   27   43   62%
c i  230.9   76100  5335405    233229   54560  13009 55339   12    25  182  48%    978 -170    8   36   22%
c -  235.2   76100  5335375    240787   29702  13108 55467   39   237  168  17%  -1936   47   45   37  121%
c -  256.9   76100  5335341    280395   29496  13437 55786   46   213  169  22%   -594  -35   58   48  121%
c 
c [simplification-8] limit 232561 conflicts (hard 282559) hit after 282562 conflicts
c [quatres-4] found 8777 quaternary clauses 7% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [quatres-4-2] added 233 quaternary resolvents
c [ternres-4] limit 21341364 based on 5335341 irredundant clauses
c [ternres-4] 14019 schedulable variables 18%
c [ternres-4] 20 ternary resolvents (0 bin, 20 trn)
c [ternres-4] 4 variables remain 0% (76096 retained 100%)
c [decomp-15] removed 1 variables
c [unhide-4] limit 332169 based on 5314714 irredundant clauses
c [unhide-4-4] 0 units, 1 failed, 441 tauts, 0 hbrs, 16942 literals
c [transred-3] limit 5306238 based on 5306238 irredundant clauses
c [transred-3] removed 3 transitive binary clauses
c [block-3] 14339 variables 19% will be scheduled this time
c [block-3] scheduled 14339 variables 19%
c [block-3] limit of 25911861 steps penalty 4 = 1 + 3
c [block-3] incomplete 194 not tried 0%
c [block-3] transition to [ all 0 rem 1 ] state
c [block-3] eliminated 24 blocked clauses
c [block-3] 24 < 1/100 * 5306236 = 53062 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 76099 variables 100%
c [elim-7] limit of 50000000 steps penalty 4 = 1 + 3
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 64898 not tried 85% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 380 = 0% variables out of 76099 scheduled
c [elim-7] 380 < 1/100 * 76099 = 760 considered unsuccessful
c [sweep-4] limit 10611496 based on 5305748 irredundant clauses
c [sweep-4-1] 642 pos 1.3% + 48747 neg 98.7% = 49389 sched 65.2% ret 26330
c [sweep-4-1] 10620971 steps 133 queries 2168.05 avg class size
c [sweep-4-1] 3196 decisions 98 SAT calls 176.07 avg env size
c [sweep-4-1] 43572 variables remain 58% (32147 retained 42%)
c [decomp-16] removed 34 variables
c [sweep-4-1] removed 34 vars (0 failed, 35 eqs, 75 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 34 vars in TOTAL (1 rounds, 132 queries)
c [sort-queue-8] sorted 15200 enqueued variables after 282562 conflicts
c [score-dist-8] active 60485 (80%), one 0 (0%), zero 15200 (20%)
c [score-dist-8] max exp 520, different 13 (2%)
c [score-dist-8] median active exp 519, avg 519.0
c [simplification-8] removed 415 variables 0.5% (75685 remain 85%)
c [simplification-8] removed 29593 irredundant clauses 0.6% (5305748 remain 95%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 49998 = 99996 / 2
c [simplification-8] new conflict interval 149994
c [simplification-8] penalized conflict interval 149994 = 1 * 149994
c [simplification-8] hard conflict limit 507553 (soft 432556 + delta 74997)
c [simplification-8] new conflict limit 432556 (hard 507553)
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 -  291.4   75685  5305721    326604   31306  11215 50415   36   160  167  23%    224  -69   26   44   59%
c i  303.0   75684  5305698    357219   55983  11456 50556   21   102  179  21%    523 -117    7   40   17%
c -  308.8   75684  5305698    371632   34320  11524 50668   25   153  170  16%   -958  -57   22   38   57%
c i  311.3   75683  5305698    380003   40743  11539 50677   16    95  176  17%   -720 -106   10   36   27%
c i  315.9   75682  5305676    390480   49063  11656 50768   29   132  177  22%   -771  -67    9   36   25%
c -  323.0   75682  5305676    413354   35825  11700 50854   29    72  170  41%   -359 -115   36   35  103%
c i  324.2   75681  5305673    416094   38074  11710 50867   31   155  176  20%   -303  -28   59   35  167%
c i  324.2   75680  5305673    416172   38107  11712 50891   32   153  176  21%   -330  -30   56   35  158%
c i  324.2   75679  5305669    416215   38145  11712 50891   32   153  176  21%   -345  -30   57   35  161%
c i  324.3   75678  5305669    416298   38198  11722 50891   32   152  176  21%   -371  -31   57   35  162%
c i  328.1   75677  5305661    427327   47011  11807 50930   20   111  177  18%   -439  -69    7   34   21%
c i  328.1   75676  5305661    427328   47011  11807 50930   20   111  177  18%   -439  -69    7   34   21%
c i  334.1   75675  5305650    434985   53986  11872 51000   49   434  182  11%   -433  236   36   36   99%
c -  349.1   75675  5305645    456476   34468  11970 51073   57   125  170  45%   -113 -108   44   46   95%
c 
c [simplification-9] limit 432566 conflicts (hard 507553) hit after 507553 conflicts
c [quatres-5] found 8775 quaternary clauses 8% in total
c [quatres-5-2] added 5 single-self-subsuming ternary resolvents
c [quatres-5-2] added 220 quaternary resolvents
c [ternres-5] limit 21222580 based on 5305645 irredundant clauses
c [ternres-5] 4 schedulable variables 0%
c [ternres-5] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-17] removed 10 variables
c [simpleprobe-3] 60555 schedulable variables 80%
c [simpleprobe-3] limit 10477308 based on 5238654 irredundant clauses
c [simpleprobe-3] 53883 variables remain 71% (21792 retained 29%)
c [simpleprobe-3] removed 0 variables, found 2144 hbrs, 0 units
c [unhide-5] limit 773192 with penalty 4 = 0 + 4
c [unhide-5-5] 0 units, 1 failed, 7220 tauts, 0 hbrs, 7488 literals
c [transred-4] limit 5227490 based on 5227490 irredundant clauses
c [transred-4] removed 0 transitive binary clauses
c [bca-4] limit of 10000000 steps and 10467125 added (scaled 2)
c [bca-4] 98283 out of 151350 literals actually usable 65%
c [bca-4] added 269 blocked clauses in 376628 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 23195772 penalty 3 = 0 + 3
c [sweep-5-1] 910 pos 2.1% + 42647 neg 97.9% = 43557 sched 57.6% ret 32117
c [sweep-5-1] 23304644 steps 377 queries 2079.17 avg class size
c [sweep-5-1] 8046 decisions 220 SAT calls 237.24 avg env size
c [sweep-5-1] 34121 variables remain 45% (41538 retained 55%)
c [decomp-19] removed 172 variables
c [sweep-5-1] removed 172 vars (0 failed, 159 eqs, 337 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 172 vars in TOTAL (1 rounds, 376 queries)
c [sort-queue-9] sorted 13108 enqueued variables after 507553 conflicts
c [score-dist-9] active 62394 (83%), one 0 (0%), zero 13108 (17%)
c [score-dist-9] max exp 520, different 12 (2%)
c [score-dist-9] median active exp 520, avg 519.8
c [simplification-9] removed 173 variables 0.2% (75502 remain 85%)
c [simplification-9] removed 79308 irredundant clauses 1.5% (5226337 remain 94%)
c [simplification-9] maximum reduction of 1% = max (0%, 1%)
c [simplification-9] geometric conflict interval increment 74997 = 149994 / 2
c [simplification-9] new conflict interval 224991
c [simplification-9] penalized conflict interval 224991 = 1 * 224991
c [simplification-9] hard conflict limit 845039 (soft 732544 + delta 112495)
c [simplification-9] new conflict limit 732544 (hard 845039)
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 -  383.5   75502  5226337    517851   35060  10299 53541   30    61  168  49%    578  -75   30   40   75%
c -  396.3   75502  5226337    565083   36139  10333 53551   19    87  171  22%    807  -16   18   31   57%
c i  405.0   75501  5226337    598866   61239  10362 53558   12    71  181  17%    894  -25    9   25   35%
c -  416.1   75499  5226336    611806   35500  10505 53670   68   311  171  22%  -1217  179   51   34  153%
c -  436.0   75499  5226295    660570   37122  10665 53827   15    58  172  25%    -41  -67   13   29   45%
c i  438.7   75498  5226295    668051   43133  10683 53847   14    48  178  29%     74  -71   10   27   37%
c i  439.8   75496  5226276    669090   43990  10703 53927   23   187  179  12%   -594   68   62   28  222%
c i  450.1   75495  5226255    682095   54885  10807 54123   56   301  183  19%   -643  151   38   33  116%
c i  455.1   75494  5226255    692011   62965  10866 54153   36   148  187  25%   -586  -12   27   34   79%
c i  457.1   75493  5226255    696831   66815  10894 54162   29   136  189  22%   -617  -23   23   34   68%
c -  460.9   75493  5226255    709171   37643  10906 54163   17    49  172  36%   -400  -97   18   31   57%
c i  466.5   75492  5226255    726215   50780  10917 54168   14    42  181  32%    -74  -82   11   27   42%
c i  467.3   75483  5226255    727627   51942  10935 54233   18   151  182  12%   -389   27   31   27  112%
c i  467.4   75482  5226255    727661   51974  10935 54234   19   153  182  12%   -393   29   33   27  119%
c i  467.4   75481  5226255    727665   51976  10936 54234   19   153  182  12%   -394   29   33   27  119%
c i  472.2   75480  5226255    738877   60920  11058 54384   30   226  182  13%   -285   95   31   28  111%
c i  472.3   75479  5226255    738938   60979  11058 54384   30   228  182  13%   -294   96   32   28  115%
c i  472.7   75478  5226255    739958   61857  11059 54387   30   233  183  13%   -377  100   32   28  115%
c i  472.7   75477  5226255    739959   61857  11059 54387   30   233  183  13%   -377  100   32   28  115%
c i  472.7   75476  5226255    739960   61857  11059 54387   30   233  183  13%   -377  100   32   28  114%
c i  472.7   75475  5226255    739961   61857  11059 54387   30   233  183  13%   -377  100   32   28  114%
c i  472.7   75474  5226255    739962   61857  11059 54387   30   233  183  13%   -377  100   31   28  113%
c i  472.9   75473  5226255    740178   62052  11070 54388   30   238  183  13%   -387  105   33   28  119%
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  472.9   75472  5226255    740181   62054  11070 54388   30   238  183  13%   -387  105   33   28  118%
c i  472.9   75471  5226255    740184   62055  11070 54388   30   238  183  13%   -388  104   33   28  118%
c i  472.9   75470  5226255    740214   62074  11074 54388   30   236  183  13%   -389  103   33   28  118%
c i  472.9   75469  5226255    740224   62080  11074 54389   30   236  183  13%   -389  103   32   28  115%
c i  473.0   75468  5226255    740352   62192  11079 54391   30   239  184  13%   -394  106   34   28  122%
c i  473.1   75467  5226255    740412   62242  11082 54391   31   239  185  13%   -396  105   44   28  159%
c i  473.1   75466  5226255    740414   62243  11082 54391   31   239  185  13%   -396  105   45   28  160%
c i  473.1   75465  5226255    740428   62256  11082 54391   31   238  185  13%   -396  105   49   28  175%
c i  474.4   75464  5226255    742569   64037  11089 54406   31   243  185  13%   -398  106   33   28  116%
c i  474.5   75453  5226255    742625   64084  11093 54408   31   244  185  13%   -399  106   34   28  123%
c i  474.5   75452  5226255    742644   64090  11097 54411   31   243  185  13%   -399  105   34   28  121%
c i  474.7   75451  5226241    742890   64296  11100 54423   32   251  185  13%   -402  114   45   28  161%
c i  474.7   75450  5226241    742912   64310  11101 54425   32   250  185  13%   -402  113   48   28  170%
c i  474.7   75449  5226241    742930   64325  11101 54425   32   250  185  13%   -403  112   48   28  170%
c i  474.7   75448  5226241    742931   64325  11101 54425   32   250  185  13%   -403  112   47   28  169%
c i  474.7   75447  5226241    742935   64327  11102 54425   32   249  185  13%   -403  112   48   28  172%
c i  474.7   75446  5226240    742960   64343  11105 54427   32   249  185  13%   -403  111   49   28  175%
c i  474.7   75445  5226239    742974   64351  11105 54427   32   248  185  13%   -403  110   50   28  177%
c i  474.7   75444  5226239    742975   64351  11105 54427   32   248  185  13%   -403  110   49   28  176%
c i  474.7   75443  5226239    742979   64354  11105 54427   32   248  185  13%   -403  110   50   28  177%
c i  474.7   75441  5226239    742996   64367  11105 54427   33   247  185  13%   -403  109   50   28  178%
c i  474.7   75440  5226239    742997   64367  11105 54427   33   247  185  13%   -403  109   50   28  178%
c i  474.7   75439  5226239    743001   64370  11105 54427   33   247  185  13%   -403  109   50   28  178%
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  474.8   75438  5226238    743020   64382  11106 54429   33   246  185  13%   -403  108   50   28  178%
c i  474.8   75437  5226238    743041   64392  11106 54429   33   245  185  13%   -404  107   50   28  179%
c i  474.8   75436  5226238    743043   64393  11106 54429   33   245  185  13%   -404  107   50   28  179%
c i  474.8   75435  5226238    743045   64393  11107 54429   33   245  185  13%   -404  107   50   28  178%
c i  474.8   75434  5226238    743068   64406  11111 54429   33   244  185  13%   -404  106   48   28  170%
c i  474.8   75433  5226238    743070   64406  11112 54429   33   244  185  13%   -404  106   47   28  168%
c i  474.8   75432  5226238    743072   64406  11113 54429   33   244  185  13%   -404  106   47   28  167%
c i  474.8   75431  5226233    743098   64427  11114 54429   33   242  185  13%   -404  105   45   28  161%
c i  474.9   75430  5226232    743182   64500  11122 54429   33   244  185  13%   -405  106   41   28  147%
c i  474.9   75429  5226232    743184   64500  11123 54429   33   244  185  13%   -405  106   41   28  146%
c i  476.0   75428  5226232    746065   66850  11164 54469   28   207  187  14%   -370   66   32   28  114%
c i  477.2   75427  5226232    749088   69539  11182 54474   27   189  189  14%   -350   45   34   28  124%
c i  480.6   75426  5226228    756713   76311  11249 54531   24   166  195  14%   -244   13   20   28   72%
c -  482.0   75426  5226228    758732   40078  11258 54537   26   309  175   8%   -306  154   26   28   93%
c i  483.3   75425  5226228    761562   42595  11267 54565   26   275  191  10%   -265  113   33   28  119%
c i  483.3   75424  5226228    761571   42599  11267 54565   26   275  191  10%   -266  113   32   28  116%
c i  483.5   75423  5226228    761864   42867  11268 54565   27   277  191  10%   -279  115   36   28  129%
c i  483.8   75422  5226228    762243   43193  11273 54571   27   267  191  10%   -291  104   36   28  129%
c i  483.8   75421  5226228    762281   43217  11277 54574   27   266  191  10%   -292  103   36   28  130%
c i  483.9   75420  5226228    762344   43271  11279 54574   27   264  191  10%   -293  101   32   28  115%
c i  483.9   75419  5226228    762346   43271  11280 54574   27   264  191  10%   -293  101   32   28  114%
c i  483.9   75418  5226228    762350   43271  11283 54574   27   264  191  10%   -293  100   31   28  113%
c i  484.2   75417  5226228    762848   43686  11295 54579   28   258  191  11%   -301   94   31   28  113%
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  484.8   75416  5226228    764436   45077  11307 54585   26   221  193  12%   -297   55   33   28  118%
c i  484.8   75415  5226228    764437   45077  11307 54585   26   221  193  12%   -297   55   33   28  118%
c i  484.8   75414  5226228    764438   45077  11307 54585   26   221  193  12%   -297   55   32   28  117%
c i  484.8   75413  5226228    764439   45077  11307 54585   26   221  193  12%   -297   55   32   28  117%
c i  484.8   75412  5226228    764441   45077  11308 54585   26   221  193  12%   -297   55   32   28  116%
c i  485.2   75411  5226228    765078   45646  11311 54591   27   220  196  12%   -299   54   36   28  129%
c i  485.2   75410  5226228    765079   45646  11311 54591   27   220  196  12%   -299   54   35   28  129%
c i  485.2   75409  5226228    765080   45646  11311 54591   27   220  196  12%   -299   54   35   28  128%
c i  485.2   75408  5226228    765081   45646  11311 54591   27   220  196  12%   -299   54   35   28  128%
c i  485.2   75407  5226228    765084   45648  11311 54591   27   220  196  12%   -299   54   35   28  128%
c i  485.4   75406  5226228    765276   45804  11315 54591   27   215  196  13%   -300   48   30   28  110%
c i  488.9   75405  5226228    774676   53991  11355 54596   19    69  198  27%   -145  -92   14   26   54%
c i  489.0   75404  5226228    774994   54282  11355 54597   20   112  198  18%   -179  -48   31   26  117%
c i  489.0   75403  5226228    774995   54282  11355 54597   20   112  198  18%   -179  -48   31   26  117%
c i  489.2   75402  5226228    775099   54363  11365 54599   21   117  198  18%   -188  -43   36   27  135%
c i  489.3   75401  5226228    775185   54437  11367 54603   21   119  198  17%   -195  -41   35   27  133%
c i  489.3   75400  5226228    775205   54447  11371 54604   21   119  198  18%   -196  -41   37   27  140%
c i  489.3   75399  5226228    775207   54447  11372 54604   21   119  198  18%   -196  -41   37   27  139%
c i  489.3   75398  5226225    775234   54462  11376 54605   21   119  198  18%   -198  -41   36   27  137%
c i  489.3   75397  5226225    775236   54462  11377 54605   21   119  198  18%   -198  -41   36   27  136%
c i  489.3   75396  5226225    775238   54462  11378 54605   21   119  198  18%   -198  -41   36   27  135%
c i  489.4   75395  5226225    775262   54480  11380 54605   21   118  198  18%   -200  -42   37   27  138%
c i  489.4   75394  5226225    775272   54488  11380 54605   21   118  198  18%   -201  -42   38   27  142%
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  489.4   75393  5226224    775338   54525  11388 54605   21   119  198  18%   -205  -41   34   27  127%
c i  489.4   75392  5226224    775340   54525  11389 54605   21   119  198  18%   -205  -41   33   27  126%
c i  489.4   75391  5226224    775342   54525  11390 54605   21   119  198  18%   -205  -41   33   27  125%
c i  489.4   75390  5226224    775344   54525  11391 54605   21   119  198  18%   -206  -41   33   27  124%
c i  489.5   75389  5226224    775377   54549  11393 54606   21   118  198  18%   -208  -41   32   27  122%
c i  489.5   75388  5226224    775378   54549  11393 54606   21   118  198  18%   -208  -42   32   27  121%
c i  489.5   75387  5226224    775423   54571  11394 54606   22   119  198  19%   -210  -41   45   27  170%
c i  489.6   75386  5226223    775503   54622  11406 54607   22   117  198  19%   -215  -42   37   27  139%
c i  491.0   75385  5226223    778309   57037  11448 54662   24   188  198  13%   -231   28   31   27  115%
c i  491.3   75384  5226223    778528   57207  11464 54665   27   192  198  14%   -236   32   56   27  209%
c i  494.9   75383  5226223    789141   66144  11504 54722   24   148  199  16%    -85   -9   30   26  114%
c i  494.9   75382  5226223    789143   66145  11504 54722   24   148  199  16%    -85   -9   30   26  114%
c i  494.9   75381  5226223    789166   66162  11504 54722   24   147  199  17%    -88  -10   33   26  123%
c i  496.4   75380  5226223    793237   69717  11519 54730   25   118  199  21%   -173  -37   36   26  137%
c i  496.4   75379  5226223    793239   69717  11519 54730   25   118  199  21%   -173  -37   36   26  136%
c i  496.4   75378  5226223    793313   69785  11521 54730   25   117  199  21%   -176  -37   33   26  127%
c i  496.4   75377  5226223    793314   69785  11521 54730   25   117  199  21%   -177  -37   33   26  126%
c i  496.4   75376  5226223    793315   69785  11521 54730   25   117  199  21%   -177  -37   33   26  126%
c i  496.5   75375  5226223    793352   69818  11521 54731   25   118  199  21%   -178  -37   33   26  124%
c i  496.5   75374  5226223    793354   69819  11521 54731   25   118  199  21%   -178  -37   33   26  124%
c i  496.5   75373  5226223    793356   69820  11521 54731   25   117  199  21%   -178  -37   33   26  125%
c i  496.5   75372  5226223    793358   69821  11521 54731   25   117  199  21%   -178  -37   33   26  125%
c i  496.5   75371  5226223    793360   69822  11521 54731   25   117  199  21%   -178  -37   33   26  125%
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  496.5   75370  5226223    793392   69847  11522 54731   25   118  199  21%   -180  -37   33   26  127%
c i  496.5   75369  5226223    793393   69847  11522 54731   25   118  199  21%   -180  -37   33   26  126%
c i  496.5   75368  5226223    793394   69847  11522 54731   25   117  199  21%   -180  -37   33   26  126%
c i  500.0   75367  5226222    802693   77893  11544 54749   23    98  201  24%    -73  -49   29   26  115%
c i  500.3   75366  5226222    802921   78079  11554 54762   24   106  202  23%    -98  -41   34   26  131%
c i  500.4   75365  5226222    803053   78175  11558 54765   24   107  202  23%   -110  -40   31   26  122%
c -  501.0   75365  5226222    804485   41420  11568 54766   25   110  172  23%   -166  -36   24   26   92%
c i  502.5   75364  5226222    808009   44341  11591 54783   23   157  179  15%   -128   12   31   25  121%
c i  502.5   75363  5226222    808019   44350  11591 54783   23   156  179  15%   -129   12   32   25  126%
c 
c [simplification-10] limit 732857 conflicts (hard 845039) hit after 845040 conflicts
c [quatres-6] found 8943 quaternary clauses 9% in total
c [quatres-6-2] added 42 single-self-subsuming ternary resolvents
c [quatres-6-2] added 371 quaternary resolvents
c [card-4] limit 1306555 based on 5226222 irredundant clauses
c [card-4] found 1 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1306555 for elimination
c [card-4] 1 out of 1 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 2613111 based on 5226222 irredundant clauses
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-6] limit 1129410 with penalty 4 = 0 + 4
c [unhide-6-6] 81 units, 11 failed, 289 tauts, 0 hbrs, 58163 literals
c [cce-3] limit of 14117633 steps penalty 5 = 2 + 3
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 287
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 286
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 285
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 284
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 283
c [cce-3-1] eliminated 9 clauses out of 9 (100%) of length 282
c [cce-3-1] eliminated 5 clauses out of 5 (100%) of length 281
c [cce-3-1] eliminated 7 clauses out of 9 (78%) of length 280
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 39 large clauses in 14117701 steps
c [cce-3-1] allowing another 7058850 steps for small clauses
c [cce-3-1] scheduling 4998480 clauses = 4986963 binary + 11517 ternary
c [cce-3-1] tried to eliminate 4 small clauses 0%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 1 small clauses 0%
c [cce-3-1] eliminated 10850 small clauses in 14140779 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 10889 covered clauses in round 1
c [cce-3] eliminated 10889 covered clauses in TOTAL during 1 rounds
c [cce-3] 10889 < 1/100 * 5133130 = 51331 considered unsuccessful
c [bca-5] limit of 10000000 steps and 10256948 added (scaled 2)
c [bca-5] 100385 out of 150550 literals actually usable 67%
c [bca-5] added 2589 blocked clauses in 405605 steps
c [sweep-6] limit 10244482 based on 5122241 irredundant clauses
c [sweep-6-1] 656 pos 1.9% + 33273 neg 98.1% = 33929 sched 45.1% ret 41345
c [sweep-6-1] 11039961 steps 257 queries 3237.73 avg class size
c [sweep-6-1] 4526 decisions 105 SAT calls 179.44 avg env size
c [sweep-6-1] 30893 variables remain 41% (43870 retained 59%)
c [decomp-21] removed 881 variables
c [sweep-6-1] removed 881 vars (0 failed, 155 eqs, 306 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 881 vars in TOTAL (1 rounds, 256 queries)
c [sort-queue-10] sorted 11353 enqueued variables after 845040 conflicts
c [score-dist-10] active 63040 (85%), one 0 (0%), zero 11353 (15%)
c [score-dist-10] max exp 521, different 11 (2%)
c [score-dist-10] median active exp 521, avg 520.6
c [simplification-10] removed 970 variables 1.3% (74393 remain 83%)
c [simplification-10] removed 190918 irredundant clauses 3.7% (5035304 remain 90%)
c [simplification-10] maximum reduction of 4% = max (1%, 4%)
c [simplification-10] geometric conflict interval increment 44998 = 224991 / 5
c [simplification-10] new conflict interval 269989
c [simplification-10] penalized conflict interval 269989 = 1 * 269989
c [simplification-10] hard conflict limit 1250023 (soft 1115029 + delta 134994)
c [simplification-10] new conflict limit 1115029 (hard 1250023)
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 -  528.1   74393  5035304    857168   36956   8498 57033   17    52  163  33%    442  -44   17   21   81%
c i  534.6   74392  5035304    877779   54850   8507 57045   13    52  171  25%    599  -28   23   19  120%
c i  534.6   74391  5035304    877780   54850   8507 57045   13    52  171  25%    598  -28   23   19  119%
c i  534.6   74390  5035304    877781   54850   8507 57045   13    52  171  25%    597  -28   23   19  119%
c i  534.6   74389  5035304    877817   54879   8507 57045   14    53  171  26%    560  -27   33   19  169%
c i  543.8   74388  5035304    899216   72633   8578 57074   11    34  179  32%    -81  -35    7   17   42%
c i  544.1   74387  5035304    899338   72718   8580 57074   11    43  179  25%   -117  -25   10   17   60%
c -  545.9   74387  5035304    903826   38647   8590 57075   14    36  164  39%   -321  -31   16   17   93%
c i  551.6   74386  5035301    921537   53079   8658 57091   10    16  170  65%     -5  -42    6   16   36%
c i  551.6   74384  5035301    921541   53081   8658 57091   10    16  170  64%     -6  -42    6   16   38%
c i  551.6   74383  5035301    921543   53081   8658 57092   10    16  170  64%     -7  -42    6   16   38%
c i  551.6   74382  5035301    921544   53081   8658 57092   10    16  170  64%     -7  -42    6   16   37%
c i  551.6   74381  5035301    921545   53081   8658 57092   10    16  170  64%     -8  -42    6   16   37%
c i  551.6   74380  5035301    921546   53081   8658 57092   10    16  170  64%     -8  -42    6   16   37%
c i  551.8   74379  5035301    921642   53112   8679 57092   10    17  170  61%    -37  -41   12   16   78%
c i  559.1   74378  5035301    943862   72563   8738 57097   15    22  176  67%     40  -25   19   15  124%
c i  559.1   74377  5035301    943864   72564   8738 57097   15    22  176  67%     40  -25   19   15  123%
c i  559.1   74376  5035301    943866   72565   8738 57097   15    22  176  67%     39  -25   19   15  123%
c -  562.4   74376  5035301    950356   38953   8760 57099   18    29  163  61%   -186  -17   19   16  118%
c i  566.3   74375  5035301    965202   51802   8783 57105   15    22  170  70%     59  -19   18   16  113%
c i  566.3   74374  5035301    965203   51802   8783 57105   15    22  170  70%     59  -19   17   16  112%
c i  566.3   74373  5035301    965204   51802   8783 57105   15    22  170  70%     58  -19   17   16  112%
c i  566.3   74372  5035301    965205   51802   8783 57105   15    22  170  70%     58  -19   17   16  111%
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  566.3   74371  5035301    965208   51803   8783 57105   15    22  170  68%     57  -19   17   16  111%
c -  577.9   74371  5035301    996968   40344   8840 57109   13    17  163  73%    221  -16   11   15   78%
c i  580.8   74370  5035301   1003308   45348   8865 57112   11    14  168  73%    295  -17    8   14   58%
c i  590.7   74359  5035297   1020313   59693   8939 57121   15    20  194  76%     -5  -10   18   15  121%
c i  590.7   74358  5035297   1020314   59693   8939 57121   15    20  194  76%     -5  -10   18   15  120%
c i  590.7   74357  5035297   1020315   59693   8939 57121   15    20  194  76%     -5  -10   18   15  120%
c i  590.7   74356  5035297   1020316   59693   8939 57121   15    20  194  76%     -6  -10   17   15  119%
c i  590.7   74355  5035297   1020319   59693   8940 57122   15    20  194  76%     -6  -10   17   15  118%
c i  590.7   74354  5035297   1020320   59693   8940 57122   15    20  194  76%     -7  -10   17   15  118%
c i  594.7   74353  5035297   1032239   69149   8977 57130   11    15  197  73%    -59  -13    8   14   57%
c i  594.7   74349  5035297   1032246   69155   8977 57130   11    15  197  72%    -60  -13    8   14   58%
c i  594.7   74348  5035297   1032247   69155   8977 57130   11    15  197  72%    -60  -13    8   14   58%
c i  594.7   74347  5035297   1032248   69155   8977 57130   11    15  197  72%    -60  -13    8   14   57%
c i  594.7   74346  5035297   1032249   69155   8977 57130   11    15  197  72%    -60  -13    8   14   57%
c -  601.4   74346  5035297   1046226   40988   8998 57135   13    19  169  68%     -4   -7   13   14   96%
c i  603.6   74345  5035297   1048595   42878   9006 57136   11    17  181  69%     33   -9    7   14   52%
c i  603.6   74343  5035297   1048601   42883   9006 57136   12    20  181  58%     31   -6   10   14   71%
c 
c [simplification-11] limit of 140 iterations hit after 165 iterations
c [quatres-7] found 7612 quaternary clauses 9% in total
c [quatres-7-1] removed 3 duplicate quaternary clauses
c [quatres-7-2] added 586 single-self-subsuming ternary resolvents
c [quatres-7-2] added 263 quaternary resolvents
c [ternres-6] limit 20141180 based on 5035295 irredundant clauses
c [ternres-6] all 74343 free variables schedulable
c [ternres-6] 659 ternary resolvents (3 bin, 656 trn)
c [ternres-6] 219 variables remain 0% (74124 retained 100%)
c [decomp-22] removed 53 variables
c [unhide-7] limit 1250000 with penalty 4 = 0 + 4
c [unhide-7-7] 2 units, 1 failed, 12377 tauts, 0 hbrs, 7153 literals
c [transred-5] limit 4868782 based on 4868782 irredundant clauses
c [transred-5] removed 5 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 74337 variables 100%
c [block-4] limit of 50000000 steps penalty 4 = 2 + 2
c [block-4] incomplete 20026 not tried 27%
c [block-4] transition to [ all 1 rem 1 ] state
c [block-4] eliminated 75901 blocked clauses
c [elim-8] 23562 variables 32% will be scheduled this time
c [elim-8] scheduled 23562 variables 32%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1000000000 steps penalty 4 = 2 + 2
c [elim-8] rescheduling of touched variables disabled
c [elim-8] incomplete 16680 not tried 23% in round 1
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 1631 = 7% variables out of 23562 scheduled
c [bca-6] limit of 10000000 steps and 9470300 added (scaled 2)
c [bca-6] 121886 out of 142808 literals actually usable 85%
c [bca-6] added 15709 blocked clauses in 508995 steps
c [sweep-7] limit 9456540 based on 4728270 irredundant clauses
c [sweep-7-1] 742 pos 2.5% + 28536 neg 97.5% = 29278 sched 41.0% ret 42125
c [sweep-7-1] 9463085 steps 324 queries 2979.69 avg class size
c [sweep-7-1] 5547 decisions 141 SAT calls 173.13 avg env size
c [sweep-7-1] 26325 variables remain 37% (44874 retained 63%)
c [decomp-23] removed 392 variables
c [sweep-7-1] removed 392 vars (0 failed, 189 eqs, 374 impls)
c [sweep-7] removed 392 vars in TOTAL (1 rounds, 323 queries)
c [sort-queue-11] sorted 9631 enqueued variables after 1048640 conflicts
c [score-dist-11] active 61380 (86%), one 0 (0%), zero 9631 (14%)
c [score-dist-11] max exp 521, different 10 (2%)
c [score-dist-11] median active exp 521, avg 520.6
c [simplification-11] removed 3332 variables 4.5% (71011 remain 80%)
c [simplification-11] removed 318415 irredundant clauses 6.3% (4716882 remain 84%)
c [simplification-11] maximum reduction of 6% = max (4%, 6%)
c [simplification-11] forced so keeping old conflict interval 269989
c [simplification-11] conflict limit remains at 1115204 (hard 1250023)
c [simplification-11] 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  651.0   71010  4716882   1048790   15903   7332 81237   12    37  165  34%     -9   11   19   14  141%
c i  651.5   71009  4716882   1049332   16329   7362 81240   15    53  166  29%    -88   27   35   14  248%
c i  653.0   71008  4716882   1051520   18034   7503 81252   18    72  166  25%   -167   45   22   14  156%
c i  653.0   71007  4716882   1051521   18034   7503 81252   18    72  166  25%   -167   45   22   14  155%
c i  653.0   71006  4716882   1051522   18034   7503 81252   18    72  166  25%   -167   45   22   14  155%
c i  657.0   71005  4716882   1057446   22749   7800 81316   32   120  167  26%   -111   87   26   16  160%
c i  657.0   71004  4716882   1057449   22751   7800 81316   32   120  167  26%   -111   87   25   16  158%
c i  657.0   71003  4716882   1057451   22751   7800 81316   32   120  167  26%   -111   87   25   16  158%
c i  657.0   71002  4716882   1057452   22751   7800 81316   32   120  167  26%   -111   87   25   16  157%
c i  660.9   71001  4716882   1066068   29483   7975 81361   18    78  170  23%    -53   38   20   16  125%
c i  661.0   71000  4716882   1066250   29630   7984 81363   18    79  170  23%    -72   39   21   16  128%
c i  661.1   70999  4716882   1066266   29638   7985 81363   18    79  170  23%    -74   40   20   16  126%
c i  661.3   70998  4716882   1066551   29860   8015 81364   19    82  170  23%    -97   42   23   16  140%
c i  661.3   70997  4716882   1066682   29957   8035 81364   19    82  170  23%   -105   42   22   16  133%
c i  661.8   70996  4716882   1067482   30515   8097 81381   19    83  170  23%   -136   43   20   16  126%
c i  663.6   70995  4716882   1070417   32719   8277 81428   20    97  171  21%   -131   54   13   16   79%
c i  663.6   70993  4716882   1070430   32726   8277 81430   20    97  171  21%   -131   54   13   16   79%
c 
c [simplification-12] limit of 6902 ternary hit after 7202 ternaries
c [quatres-8] found 9196 quaternary clauses 4% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 998 single-self-subsuming ternary resolvents
c [quatres-8-2] added 305 quaternary resolvents
c [ternres-7] limit 28310244 with penalty 2 = 0 + 2
c [ternres-7] 217 schedulable variables 0%
c [ternres-7] 842 ternary resolvents (4 bin, 838 trn)
c [ternres-7] 2 variables remain 0% (70991 retained 100%)
c [decomp-24] removed 27 variables
c [treelook-3] limit 1178913 based on 4715654 irredundant clauses
c [treelook-3] scheduled 71334 literals 50%
c [treelook-3] scheduling used 1180267 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1178913 based on 4715654 irredundant clauses
c [treelook-3] used 1572431 steps
c [treelook-3] 71329 literals remain 50%
c [treelook-3] 65528 variables remain to probed next time 92%
c [treelook-3] removed 0 variables, found 41 hbrs
c [unhide-8] limit 1250000 with penalty 4 = 0 + 4
c [unhide-8-8] 51 units, 20 failed, 1201 tauts, 0 hbrs, 128549 literals
c [transred-6] limit 4697674 based on 4697674 irredundant clauses
c [transred-6] removed 0 transitive binary clauses
c [bca-7] limit of 10000000 steps and 9403899 added (scaled 2)
c [bca-7] 109227 out of 141836 literals actually usable 77%
c [bca-7] added 437 blocked clauses in 444709 steps
c [sweep-8] limit 9382284 based on 4691142 irredundant clauses
c [sweep-8-1] 627 pos 2.4% + 25607 neg 97.6% = 26234 sched 37.0% ret 44683
c [sweep-8-1] 9395829 steps 275 queries 3198.75 avg class size
c [sweep-8-1] 4943 decisions 120 SAT calls 180.78 avg env size
c [sweep-8-1] 24733 variables remain 35% (46005 retained 65%)
c [decomp-26] removed 348 variables
c [sweep-8-1] removed 348 vars (0 failed, 165 eqs, 317 impls)
c [sweep-8] removed 348 vars in TOTAL (1 rounds, 274 queries)
c [sort-queue-12] sorted 9545 enqueued variables after 1081044 conflicts
c [score-dist-12] active 61024 (86%), one 0 (0%), zero 9545 (14%)
c [score-dist-12] max exp 521, different 10 (2%)
c [score-dist-12] median active exp 521, avg 520.6
c [simplification-12] removed 424 variables 0.6% (70569 remain 79%)
c [simplification-12] removed 41850 irredundant clauses 0.9% (4675032 remain 84%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] forced so keeping old conflict interval 269989
c [simplification-12] conflict limit remains at 1115242 (hard 1250023)
c [simplification-12] new ternary interval 10000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  679.5   70568  4675032   1086811   45873   8970 81100   12    32  172  37%     86  -17    7   16   43%
c i  679.6   70523  4675032   1087114   46042   9063 81100   12    37  172  32%     25  -11    8   16   54%
c i  680.6   70522  4675032   1089361   47853   9158 81120   12    54  173  22%   -111    6   11   16   71%
c i  685.3   70509  4675032   1098902   55272   9518 81145   12    55  173  22%     -7    5    6   15   40%
c i  688.3   70498  4675032   1107399   61953   9653 81155   12    68  173  18%    -14   13    6   15   38%
c i  688.9   70426  4675032   1109166   63456   9685 81157   11    52  173  20%    -94   -3    7   15   49%
c i  688.9   70110  4675032   1109167   63456   9685 81157   11    52  173  20%    -94   -3    7   15   49%
c i  690.0   70102  4675032   1111873   65598   9766 81164   11    50  173  22%    -95   -4   17   15  114%
c i  691.2   70101  4675032   1113978   67002  10002 81180   12    62  175  20%    -99    8    9   15   61%
c i  691.2   70085  4675032   1113979   67002  10002 81180   12    62  175  20%    -99    8    9   15   61%
c i  691.2   43981  4675032   1113999   67016  10003 81181   12    62  175  19%    -99    8    9   15   59%
c i  691.2   43978  4675032   1114005   67013  10003 81185   12    62  175  19%   -100    8    9   15   58%
c i  691.3   43977  4675032   1114257   67216  10010 81195   12    59  175  20%   -104    5    6   15   41%
c i  691.3   43966  4675032   1114403   67296  10015 81200   11    58  175  20%   -106    3    6   15   38%
c 0  691.3   37962  4675032   1114403   67296  10015 81200   11    58  175  20%   -106    3    6   15   38%
c 
s UNSATISFIABLE
c
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 7 count, 42667 added (17177 skipped), 3096872 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 4 bces, 224255 removed, 63384849 resolutions, 202092281 steps
c blkd: 6725 blocking literals 4%, 1311 pure
c bump: 1072047 bumped seen, 287787489 lits 268.4 on average
c card: 4 count, 0 units, 0 am1, 39543135 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 454 subsumed
c card: 4 at-most-one constraints found, average size 3.50
c card: 4 at-most-one constraints used 100%, average size 3.50
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 3 cces, 42 eliminated, 42 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 22177708 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 62 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 26 decompositions, 1009 equivalent 1%
c deco: 10547 decision-only clauses 1%, 62% reduction
c decs: 17140672 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 15898 eliminated 18%, 12 pure 0%
c elms: 8 rounds, 1.0 rounds/bve
c elms: 5877 small 37%, 8698 large 55%
c elms: 5895 tried small, 5877 succeeded 100%, 18 failed 0%
c elms: 2059 subsumed, 272168 strengthened, 0 blocked
c elms: 4225684 copies, 11371285 resolutions, 115989 ipos
c elms: 25638970 subchks, 6551439 strchks
c gaus: 3 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 16102686 steps, 8051343 extr 50%, 0 elim 0%
c glue: 31.4 orig avg, 31.4 real avg, 4.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 46781 = 13013 simple 28% + 33539 trn 72% + 229 lrg 0%, 1038 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1072047 clauses, 72.2 length
c lrnd: 77355047 lits = 252593943 orig - 175238896 removed 69%
c lrnd: 369132 uips 34%, 515730 flips 48%
c mins: 1043580 mins 98%, 6863 bin 1%, 7426 size 1%
c mins: 347172390 poisoned searches, 13305796 hits, 4% hit rate
c mins: 567838217 used twice searches, 21103726 hits, 4% hit rate
c move: moved 218675, 216932 bin 99%, 1743 trn 1%
c otfs: 42870 driving 16%, 227394 restarting 84%
c otfs: str 270264, 244301 red 90%, 25963 irr 10%
c otfs: str 270264, 0 bin 0%, 1051 trn 0%, 269213 lrg 100%
c otfs: sub 2088, 1654 red 79%, 434 irr 21%
c otfs: sub 2088, 0 bin 0%, 10 trn 0%, 2078 lrg 100%
c phas: 1 computed, 89254 set, 0 pos (0%), 89254 neg (100%)
c prbs: 2 basic, 5331 probed, 516 failed, 0 lifted
c prbs: 3 simple, 148793 probed, 0 failed, 0 eqs
c prbs: 3 treelook, 10 probed, 0 failed, 0 lifted
c prom: 126549 locked 2% out of 6391963 tried
c prps: 2420229049 props, 140 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 8 count, 2238 quat, 1633 self1, 1 self2, 14 dup
c queu: 12 sorted, 17140672 next (17889 steps 0.00)
c queu: 288268091 enq (3410434830 steps 11.83), 287787489 deq 100%
c redc: 6501 clauses 12%, 55550 tried 5%, 70 sat 0%
c redc: 26498 lits 5%, 572505 tried 0%, 70 sat 0%
c redc: 1728 times jump level reduced, 38.6 levels on average
c reds: 22 count, 50654.7 conflicts per reduce
c reds: 0 memlim 0%, 22 arith 100%
c reds: 665579 collected 86%, 105858 retired 14%
c rmbd: 63920 removed, 2861 red 4%
c rsts: 15868 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 12 count, 9 confs 75%, 0 vars 0%
c simp: 1 its 8%, 1 bin 8%, 1 trns 8%
c subl: 1072047 count (1349490 tried 1.3), 155584 sub out of 1055994 (14.7%)
c swps: 8 count, 8 rounds, 1732 queries (216.5/round)
c swps: 979 sat calls, 38 unsat (0.5% success rate)
c swps: 36356 decisions 37.1, 514 conflicts 0.5
c swps; 2736.7 avg class size, 290.9 avg environment size
c swps: 0 failed, 1581 impls, 783 equivs
c swp0: 575 type 0 queries, 633 unsat (110.1%), 265 sat (46.1%)
c swp1: 1157 type 1 queries, 1036 unsat (89.5%), 684 sat (59.1%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 36425849 calls to obtain time
c tops: 34446 fixed 39%, 196 its, 5685.73 confs/it
c trds: 6 transitive reductions, 10 removed, 0 failed
c trds: 1132 nodes, 22533 edges, 31000934 steps
c trim: 1729781 words, 6.6 MB
c trnr: 7 count, 9 bin, 10833 trn, 130678481 steps
c unhd: 8 count, 8 rounds, 42589137 steps
c unhd: 4 non-trivial sccs of average size 2.0
c unhd: 134 units, 134 bin, 0 trn, 0 lrg
c unhd: 35 failed, 29 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 28827 tauts, 4 bin 0%, 481 trn 2%, 255 lrg 1%
c unhd: 28827 tauts, 28087 stamp 97%, 2032 red 7%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 231838 str, 134 bin 0%, 2716 trn 1%, 228988 lrg 99%, 138205 red 60%
c vars: 37962 remaining 43% and 51353 removed 57% out of 89315
c vars: 34446 fixed 39%, 15898 eliminated 18%, 1009 equivalent 1%
c vsts: 11828160882 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 4.9 search visits per propagation, 10502.4 per conflict
c wchs: 1375878969 pushed, 83471834 enlarged, 100 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1058232        665579        105858      38503167      16134321        859449
c 
c  0 0         33041   3      5850   1         0   0  17852143  46   4866289  30     69047   8     2.0
c  1 5         16419   2      5072   1      1895   2   1634562   4    868384   5     33753   4     0.6
c  2 6         70088   7     29393   4      7005   7   3231349   8<  1770277  11    106062  12     3.0
c  3 9        175349  17    110697  17     13943  13   4823714  13   1996965  12<   148062  17    10.9
c  4 14       234988  22    166448  25     18766  18   3907978  10   1962211  12    148616  17<   14.1
c  5 21       160928  15<   111437  17<    14720  14   2468635   6   1577188  10    119949  14     5.0
c  6 30       126688  12     85292  13     12374  12<  1704941   4   1194581   7     99971  12     8.3
c  7 41        84240   8     55862   8     10527  10   1182156   3    821099   5     67378   8     3.8
c  8 54        55111   5     36386   5      7784   7    801025   2    551636   3     31666   4     2.9
c  9 69        40473   4     25983   4      6795   6    418213   1    243693   2     16407   2     2.6
c 10 86        37085   4     22348   3      6873   6    290750   1    172524   1     11842   1     3.6
c 11 126       18644   2      9851   1      3546   3    180284   0    101485   1      3889   0     4.6
c 12 230        4993   0       938   0      1547   1      7200   0      7893   0      2795   0     1.7
c 13 534         185   0        22   0        83   0       217   0        96   0        12   0     0.1
c 
c avg                  4.9           5.1           5.7           2.2           3.0           4.1
c std                  2.4           2.2           2.6           2.6           2.7           2.4
c 
c   85.255  12% bump
c   61.986   9% elim
c   50.718   7% probe
c   37.643   5% block
c   19.844   3% sweep
c   12.008   2% unhide
c   11.991   2% decide
c    5.795   1% bca
c    4.119   1% quatres
c 
c    7.018 < 1% rest (below)
c 
c    3.378   0% cce
c    2.367   0% gauss
c    0.544   0% transred
c    0.544   0% ternres
c    0.185   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   14.797   2% preprocessing     7%
c  205.429  30% inprocessing     93%
c ==================================
c  220.226  32% simplifying
c  471.093  68% search
c ==================================
c  691.319 100% all
c 
c       1114403 conflicts,        1612.0 confs/sec
c          8276 ternaries,         134.7 confs/ternary
c          7302 binaries,          152.6 confs/binary
c           196 iterations,       5685.7 confs/iteration
c 
c            22 reductions,          0.0 redus/sec,  50654.7 confs/reduction
c         15868 restarts,           23.0 rests/sec,     70.2 confs/restart
c      17140672 decisions,       24794.2 decis/sec,     15.4 decis/conflict
c    2420229049 propagations,  3500888.1 props/sec,    141.2 props/decision
c 
c 691.3 seconds, 443.1 MB
c launch: done
