c launch: /data/cnf/sc2014/app/minandmaxor128.cnf.bz2
c host: atom30
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/minandmaxor128.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/minandmaxor128.cnf.bz2
c no embedded options
c found 'p cnf 249327 746444' header
c read 249327 variables, 746444 clauses, 1741700 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=5
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 249325 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] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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  249325   746442         0       0      0     0    0     0   39   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] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 10 variables
c [simpleprobe-1] all 249317 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 2 variables
c [simpleprobe-1] 48777 variables remain 20% (200538 retained 80%)
c [simpleprobe-1] removed 2 variables, found 0 hbrs, 1 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 2 units, 13 failed, 26 tauts, 0 hbrs, 3 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 249305 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 75394 not tried 30% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 173728 = 70% variables out of 249305 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 339408 negative 89.2% of 380700 except 41292 10.8%
c [phase-count-1] 306793 positive 80.6% of 380700 except 73907 19.4%
c [phase-1] phase bias: 23989 positive 32%, 51588 negative 68%
c [sort-queue-1] sorted 75577 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 75577 (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 173740 variables 69.7% (75577 remain 30%)
c [simplification-1] removed 365742 irredundant clauses 49.0% (380700 remain 51%)
c [simplification-1] maximum reduction of 70% = max (70%, 49%)
c [simplification-1] large reduction 70% >= 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 1020 conflicts
c [simpleprobe-2] 14706 schedulable variables 19%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 15768 variables remain 21% (59809 retained 79%)
c [simpleprobe-2] removed 0 variables, found 699 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 38417 literals 25%
c [treelook-1] scheduling used 300008 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 443829 steps
c [treelook-1] 38396 literals remain 25%
c [treelook-1] 35349 variables remain to probed next time 47%
c [treelook-1] removed 0 variables, found 6678 hbrs
c [basicprobe-1] limit 3045600 based on 380700 irredundant clauses
c [basicprobe-1-0] 34267 probes remain 45% after last round
c [basicprobe-1-0] removed 0 variables, found 50636 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 1 failed, 2196 tauts, 0 hbrs, 1213 literals
c [elim-2] 75393 variables 100% will be scheduled this time
c [elim-2] scheduled 75393 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 15409 not tried 20% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 13376 = 18% variables out of 75393 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 322107 negative 87.0% of 370298 except 48191 13.0%
c [phase-count-2] 299270 positive 80.8% of 370298 except 71028 19.2%
c [phase-2] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-2] sorted 38361 enqueued variables after 1020 conflicts
c [score-dist-2] active 23839 (38%), one 0 (0%), zero 38361 (62%)
c [score-dist-2] max exp 705, different 186 (26%)
c [score-dist-2] median active exp 655, avg 626.8
c [simplification-2] removed 13377 variables 17.7% (62200 remain 25%)
c [simplification-2] removed 10402 irredundant clauses 2.7% (370298 remain 50%)
c [simplification-2] maximum reduction of 18% = max (18%, 3%)
c [simplification-2] large reduction 18% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13020 (soft 3020 + delta 10000)
c [simplification-2] new conflict limit 3020 (hard 13020)
c 
c [simplification-3] limit of 129 binary hit after 129 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 12 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 12 out of 12 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [unhide-3] limit 121962 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 173 tauts, 0 hbrs, 2650 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 62200 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 6953 not tried 11% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 902 = 1% variables out of 62200 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 320675 negative 87.0% of 368672 except 47997 13.0%
c [phase-count-3] 298077 positive 80.9% of 368672 except 70595 19.1%
c [phase-3] phase bias: 1 positive 50%, 1 negative 50%
c [sort-queue-3] sorted 36557 enqueued variables after 1853 conflicts
c [score-dist-3] active 24741 (40%), one 0 (0%), zero 36557 (60%)
c [score-dist-3] max exp 916, different 303 (33%)
c [score-dist-3] median active exp 877, avg 828.4
c [simplification-3] removed 902 variables 1.5% (61298 remain 25%)
c [simplification-3] removed 1626 irredundant clauses 0.4% (368672 remain 49%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3020 (hard 13020)
c [simplification-3] new binary interval 1000
c 
c [simplification-4] limit 3020 conflicts (hard 13020) hit after 3021 conflicts
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 13671 literals 11%
c [treelook-2] scheduling used 150141 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 660149 steps
c [treelook-2] 13646 literals remain 11%
c [treelook-2] 11853 variables remain to probed next time 19%
c [treelook-2] removed 0 variables, found 2 hbrs
c [elim-4] 6740 variables 11% will be scheduled this time
c [elim-4] scheduled 6740 variables 11%
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 1483 variables 2% in round 1 in 99682763 steps
c [elim-4-1] backward subsumption/strengthening limit 99682700
c [elim-4-1-1] backward checking 3199 touched variables 5%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1007 and strengthened 455 clauses in 20209575 steps
c [elim-4-1] rescheduled 1064 variables 2% by backward subsumption
c [elim-4-2] eliminated 4 variables 0% in round 2 in 2943207 steps
c [elim-4-2] backward subsumption/strengthening limit 2943200
c [elim-4-2-1] backward checking 57 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 9 clauses in 1058497 steps
c [elim-4-2] rescheduled 18 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 813944 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 1487 = 22% variables out of 6740 scheduled
c [phase-count-4] 317362 negative 86.9% of 365050 except 47688 13.1%
c [phase-count-4] 295262 positive 80.9% of 365050 except 69788 19.1%
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-4] sorted 32979 enqueued variables after 3021 conflicts
c [score-dist-4] active 26832 (45%), one 0 (0%), zero 32979 (55%)
c [score-dist-4] max exp 678, different 499 (73%)
c [score-dist-4] median active exp 515, avg 491.3
c [simplification-4] removed 1487 variables 2.4% (59811 remain 24%)
c [simplification-4] removed 3622 irredundant clauses 1.0% (365050 remain 49%)
c [simplification-4] maximum reduction of 2% = max (2%, 1%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 6666
c [simplification-4] penalized conflict interval 6666 = 1 * 6666
c [simplification-4] hard conflict limit 19687 (soft 9687 + delta 10000)
c [simplification-4] new conflict limit 9687 (hard 19687)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   18.4   59810   365050      4256    2100    449 37456   10    68   43  15%     49   65   12    1 1290%
c i   21.0   59809   365050      6526    3722    625 37701   15    95   44  15%     24   90   16    2  993%
c i   21.6   59806   365050      7163    4177    653 37726   17    98   44  17%     14   93   34    2 1804%
c i   21.9   59803   365050      7351    4317    658 37760   20   103   44  20%     12   97   60    2 2843%
c 
c [simplification-5] limit 9687 conflicts (hard 19687) hit after 9689 conflicts
c [quatres-1] found 55406 quaternary clauses 52% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 59 single-self-subsuming ternary resolvents
c [quatres-1-2] added 3361 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 59803 free variables schedulable
c [ternres-1] 79349 ternary resolvents (0 bin, 79349 trn)
c [ternres-1] 9840 variables remain 16% (49963 retained 84%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 13814 xors of average arity 3.0
c [gauss-1] connected 41336 occurrences of 15168 variables (average 2.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [decomp-9] removed 174 variables
c [gauss-1] exported 0 unary, 3 binary and 3 ternary equations
c [unhide-4] limit 288137 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 0 failed, 677 tauts, 0 hbrs, 12622 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 47 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 59629 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 961 blocked clauses
c [block-1] 961 < 1/100 * 363898 = 3638 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 6 (17%) of length 129
c [cce-1-1] eliminated 1 clauses out of 22 (5%) of length 69
c [cce-1-1] eliminated 1 clauses out of 16 (6%) of length 68
c [cce-1-1] eliminated 1 clauses out of 20 (5%) of length 67
c [cce-1-1] eliminated 1 clauses out of 20 (5%) of length 66
c [cce-1-1] eliminated 1 clauses out of 23 (4%) of length 65
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 6 large clauses in 30000004 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 237560 clauses = 72563 binary + 164997 ternary
c [cce-1-1] tried to eliminate 365 small clauses 0%
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 6 covered clauses in round 1
c [cce-1] eliminated 6 covered clauses in TOTAL during 1 rounds
c [cce-1] 6 < 1/100 * 362937 = 3629 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 59629 variables 100%
c [elim-5] limit of 57627560 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 443 not tried 1% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 332 = 1% variables out of 59629 scheduled
c [elim-5] 332 < 1/100 * 59629 = 596 considered unsuccessful
c [bca-1] limit of 10000000 steps and 725874 added (scaled 2)
c [bca-1] 95013 out of 118596 literals actually usable 80%
c [bca-1] added 6601 blocked clauses in 257069 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 29161 pos 49.2% + 30136 neg 50.8% = 59297 sched 100.0% ret 0
c [sweep-1-1] 1129769 steps 12 queries 19052.50 avg class size
c [sweep-1-1] 179 decisions 10 SAT calls 1563.50 avg env size
c [sweep-1-1] 59276 variables remain 100% (21 retained 0%)
c [decomp-11] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-5] 315199 negative 86.9% of 362685 except 47486 13.1%
c [phase-count-5] 293772 positive 81.0% of 362685 except 68913 19.0%
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-5] sorted 35326 enqueued variables after 9689 conflicts
c [score-dist-5] active 23970 (40%), one 11346 (19%), zero 23980 (40%)
c [score-dist-5] max exp 752, different 530 (70%)
c [score-dist-5] median active exp 704, avg 615.8
c [simplification-5] removed 507 variables 0.8% (59296 remain 24%)
c [simplification-5] removed 2365 irredundant clauses 0.6% (362685 remain 49%)
c [simplification-5] maximum reduction of 1% = max (1%, 1%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 16666
c [simplification-5] penalized conflict interval 16666 = 1 * 16666
c [simplification-5] hard conflict limit 36355 (soft 26355 + delta 10000)
c [simplification-5] new conflict limit 26355 (hard 36355)
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   32.3   59295   362685     11017    9362  80226 60594   28   117   51  24%     39  106   21    4  552%
c i   32.3   59294   362685     11027    9362  80230 60594   28   117   51  24%     38  106   20    4  534%
c i   34.5   59293   362685     12650   10366  80352 60718   33   128   51  26%     17  115   43    5  913%
c i   36.7   59292   362685     14433   11250  80475 60932   31   126   51  25%     14  110   30    5  575%
c i   38.3   59291   362685     15656   12226  80541 60999   33   142   51  23%      9  124   39    6  688%
c 
c [simplification-6] limit of 1923 binary hit after 1923 binaries
c [quatres-2] found 59295 quaternary clauses 52% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 12 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1217 quaternary resolvents
c [ternres-2] limit 8466692 with penalty 0 = 0 + 0
c [ternres-2] 9826 schedulable variables 17%
c [ternres-2] 31514 ternary resolvents (1 bin, 31513 trn)
c [ternres-2] 1434 variables remain 2% (57857 retained 98%)
c [card-3] limit 1058336 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1058336 for elimination
c [card-3] 3 out of 3 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 10975 xors of average arity 3.0
c [gauss-2] connected 32807 occurrences of 13495 variables (average 2.4)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-12] removed 215 variables
c [gauss-2] exported 0 unary, 2 binary and 0 ternary equations
c [basicprobe-2] limit 21166732 penalty 1 = 1 + 0
c [basicprobe-2-0] 28903 probes remain 49% after last round
c [basicprobe-2-0] removed 0 variables, found 144332 hbrs
c [bate-1] eliminated 14 asymmetric tautologies during probing
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 226 transitive binary clauses
c [bca-2] limit of 10000000 steps and 726908 added (scaled 2)
c [bca-2] 80095 out of 118154 literals actually usable 68%
c [bca-2] added 37 blocked clauses in 218243 steps
c [sweep-2] limit 2540007 penalty 0 = 0 + 0
c [sweep-2-1] 26726 pos 45.3% + 32330 neg 54.7% = 59056 sched 100.0% ret 20
c [sweep-2-1] 2669739 steps 25 queries 9575.56 avg class size
c [sweep-2-1] 762 decisions 23 SAT calls 589.87 avg env size
c [sweep-2-1] 58853 variables remain 100% (223 retained 0%)
c [decomp-14] removed 3 variables
c [sweep-2-1] removed 3 vars (0 failed, 1 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 3 vars in TOTAL (1 rounds, 24 queries)
c [sort-queue-6] sorted 28101 enqueued variables after 22534 conflicts
c [score-dist-6] active 30972 (52%), one 17767 (30%), zero 10334 (17%)
c [score-dist-6] max exp 703, different 621 (88%)
c [score-dist-6] median active exp 545, avg 497.7
c [simplification-6] removed 218 variables 0.4% (59073 remain 24%)
c [simplification-6] removed 1137 irredundant clauses 0.3% (361548 remain 48%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] forced so keeping old conflict interval 16666
c [simplification-6] conflict limit remains at 26356 (hard 36355)
c [simplification-6] new binary interval 10000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   53.0   59072   361548     23985   19313 110727 220580   51   179   62  29%    104  145   61   11  575%
c 
c [simplification-7] limit 26356 conflicts (hard 36355) hit after 26356 conflicts
c [quatres-3] found 60597 quaternary clauses 53% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [quatres-3-2] added 38 quaternary resolvents
c [ternres-3] limit 10392708 with penalty 0 = 0 + 0
c [ternres-3] 1412 schedulable variables 2%
c [ternres-3] 10308 ternary resolvents (29 bin, 10279 trn)
c [ternres-3] 6 variables remain 0% (59066 retained 100%)
c [gauss-3] limit 2078541 penalty 0 = 0 + 0
c [gauss-3] extracted 7327 xors of average arity 3.0
c [gauss-3] connected 21971 occurrences of 4078 variables (average 5.4)
c [gauss-3] limit 2078541 penalty 0 = 0 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 28 variables
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 189 transitive binary clauses
c [transred-3] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 59043 variables 100%
c [block-2] limit of 51963540 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 82 blocked clauses
c [block-2] 82 < 1/100 * 361353 = 3613 considered unsuccessful
c [cce-2] limit of 25981770 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 127
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 125
c [cce-2-1] eliminated 2 clauses out of 8 (25%) of length 124
c [cce-2-1] eliminated 1 clauses out of 5 (20%) of length 123
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 122
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 120
c [cce-2-1] eliminated 2 clauses out of 10 (20%) of length 119
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 117
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 116
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 115
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 114
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 113
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 112
c [cce-2-1] eliminated 2 clauses out of 8 (25%) of length 111
c [cce-2-1] eliminated 2 clauses out of 8 (25%) of length 109
c [cce-2-1] eliminated 2 clauses out of 7 (29%) of length 107
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 105
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 104
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 103
c [cce-2-1] eliminated 1 clauses out of 9 (11%) of length 102
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 101
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 100
c [cce-2-1] eliminated 2 clauses out of 8 (25%) of length 99
c [cce-2-1] eliminated 2 clauses out of 7 (29%) of length 97
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 96
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 95
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 94
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 93
c [cce-2-1] eliminated 2 clauses out of 8 (25%) of length 91
c [cce-2-1] eliminated 2 clauses out of 8 (25%) of length 89
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 88
c [cce-2-1] eliminated 2 clauses out of 8 (25%) of length 86
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 85
c [cce-2-1] eliminated 2 clauses out of 7 (29%) of length 83
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 82
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 81
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 80
c [cce-2-1] eliminated 2 clauses out of 9 (22%) of length 78
c [cce-2-1] eliminated 1 clauses out of 10 (10%) of length 77
c [cce-2-1] eliminated 1 clauses out of 9 (11%) of length 76
c [cce-2-1] eliminated 1 clauses out of 10 (10%) of length 75
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 74
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 73
c [cce-2-1] eliminated 1 clauses out of 11 (9%) of length 72
c [cce-2-1] eliminated 1 clauses out of 10 (10%) of length 71
c [cce-2-1] eliminated 1 clauses out of 12 (8%) of length 70
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 59 large clauses in 25983251 steps
c [cce-2-1] allowing another 12991625 steps for small clauses
c [cce-2-1] scheduling 90847 clauses = 72075 binary + 18772 ternary
c [cce-2-1] tried to eliminate 623 small clauses 1%
c [cce-2-1] eliminated 30 ternary clauses 0%
c [cce-2-1] eliminated 30 small clauses 0%
c [cce-2-1] eliminated 30 small clauses in 25981821 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 89 covered clauses in round 1
c [cce-2] eliminated 89 covered clauses in TOTAL during 1 rounds
c [cce-2] 89 < 1/100 * 361129 = 3611 considered unsuccessful
c [elim-6] 441 variables 1% will be scheduled this time
c [elim-6] scheduled 441 variables 1%
c [elim-6] limit of 103927081 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 46291816 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 441 scheduled
c [bca-3] limit of 10000000 steps and 725897 added (scaled 2)
c [bca-3] 78060 out of 118088 literals actually usable 66%
c [bca-3] added 0 blocked clauses in 216011 steps
c [sweep-3] limit 3117812 penalty 0 = 0 + 0
c [sweep-3-1] 26876 pos 45.7% + 31946 neg 54.3% = 58822 sched 99.6% ret 221
c [sweep-3-1] 3407814 steps 30 queries 8610.43 avg class size
c [sweep-3-1] 521 decisions 28 SAT calls 313.07 avg env size
c [sweep-3-1] 58601 variables remain 99% (442 retained 1%)
c [decomp-16] removed 7 variables
c [sweep-3-1] removed 7 vars (0 failed, 3 eqs, 2 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 7 vars in TOTAL (1 rounds, 29 queries)
c [sort-queue-7] sorted 32889 enqueued variables after 26356 conflicts
c [score-dist-7] active 26147 (44%), one 23105 (39%), zero 9784 (17%)
c [score-dist-7] max exp 594, different 503 (85%)
c [score-dist-7] median active exp 546, avg 460.5
c [simplification-7] removed 36 variables 0.1% (59036 remain 24%)
c [simplification-7] removed 523 irredundant clauses 0.1% (361025 remain 48%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20000
c [simplification-7] new conflict interval 36666
c [simplification-7] penalized conflict interval 36666 = 1 * 36666
c [simplification-7] hard conflict limit 81355 (soft 63022 + delta 18333)
c [simplification-7] new conflict limit 63022 (hard 81355)
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   61.9   59035   361025     26897   21616 120836 229579   59   195   65  30%     25  156   75   13  585%
c i   65.7   59034   361025     29651   23570 120939 229636   56   170   65  33%     18  125   46   14  319%
c i   69.6   59033   361025     32024   25250 121030 229681   63   192   65  33%     13  143   63   16  390%
c i   72.7   59032   361025     34103   26896 121099 229710   64   203   65  32%      9  151   58   18  329%
c i   91.5   59031   361025     46694   36910 121529 229981   68   210   72  32%    155  133   47   25  186%
c i   94.6   59024   361025     48965   38692 121608 230021   63   200   73  31%     13  120   42   26  158%
c 
c [simplification-8] limit of 2620 ternary hit after 2620 ternaries
c [quatres-4] found 61375 quaternary clauses 51% in total
c [quatres-4-2] added 24 single-self-subsuming ternary resolvents
c [quatres-4-2] added 18 quaternary resolvents
c [ternres-4] limit 24354203 with penalty 0 = 0 + 0
c [ternres-4] 6 schedulable variables 0%
c [ternres-4] 43820 ternary resolvents (12 bin, 43808 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 306 variables
c [simpleprobe-3] 12164 schedulable variables 21%
c [simpleprobe-3] limit 48708406 penalty 1 = 1 + 0
c [decomp-18] removed 14 variables
c [simpleprobe-3] 11312 variables remain 19% (47404 retained 81%)
c [simpleprobe-3] removed 14 variables, found 15187 hbrs, 1 units
c [unhide-5] limit 608855 with penalty 3 = 2 + 1
c [unhide-5-5] 0 units, 0 failed, 4100 tauts, 0 hbrs, 140160 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 216 transitive binary clauses
c [sweep-4] limit 7306260 penalty 0 = 0 + 0
c [sweep-4-1] 22483 pos 38.6% + 35797 neg 61.4% = 58280 sched 99.3% ret 436
c [sweep-4-1] 8256234 steps 60 queries 6133.57 avg class size
c [sweep-4-1] 2257 decisions 56 SAT calls 256.27 avg env size
c [sweep-4-1] 57052 variables remain 97% (1664 retained 3%)
c [decomp-19] removed 10 variables
c [sweep-4-1] removed 10 vars (0 failed, 3 eqs, 6 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 10 vars in TOTAL (1 rounds, 59 queries)
c [sort-queue-8] sorted 38476 enqueued variables after 61581 conflicts
c [score-dist-8] active 20230 (34%), one 32489 (55%), zero 5987 (10%)
c [score-dist-8] max exp 664, different 373 (56%)
c [score-dist-8] median active exp 589, avg 574.9
c [simplification-8] removed 318 variables 0.5% (58706 remain 24%)
c [simplification-8] removed 2185 irredundant clauses 0.6% (358840 remain 48%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] forced so keeping old conflict interval 36666
c [simplification-8] conflict limit remains at 63022 (hard 81355)
c [simplification-8] new ternary interval 10000
c 
c [simplification-9] limit 63022 conflicts (hard 81355) hit after 63022 conflicts
c [quatres-5] found 61336 quaternary clauses 51% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 6 single-self-subsuming ternary resolvents
c [quatres-5-2] added 16 quaternary resolvents
c [ternres-5] limit 24658064 with penalty 0 = 0 + 0
c [ternres-5] all 58706 free variables schedulable
c [ternres-5] 8090 ternary resolvents (5 bin, 8085 trn)
c [ternres-5] 35658 variables remain 61% (23048 retained 39%)
c [gauss-4] limit 2465806 penalty 1 = 1 + 0
c [gauss-4] extracted 4822 xors of average arity 3.0
c [gauss-4] connected 14464 occurrences of 6703 variables (average 2.2)
c [gauss-4] limit 2465806 penalty 1 = 1 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 1 variables
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 199 transitive binary clauses
c [bca-4] limit of 10000000 steps and 721487 added (scaled 2)
c [bca-4] 63348 out of 117412 literals actually usable 54%
c [bca-4] added 2 blocked clauses in 200079 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 73974190 penalty 0 = 0 + 0
c [sweep-5-1] 20728 pos 36.3% + 36317 neg 63.7% = 57045 sched 97.2% ret 1660
c [sweep-5-1] 76328825 steps 405 queries 807.13 avg class size
c [sweep-5-1] 8627 decisions 355 SAT calls 109.79 avg env size
c [sweep-5-1] 45616 variables remain 78% (13089 retained 22%)
c [decomp-21] removed 86 variables
c [sweep-5-1] removed 86 vars (0 failed, 64 eqs, 109 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 86 vars in TOTAL (1 rounds, 404 queries)
c [sort-queue-9] sorted 29470 enqueued variables after 63022 conflicts
c [score-dist-9] active 29149 (50%), one 24163 (41%), zero 5307 (9%)
c [score-dist-9] max exp 626, different 502 (80%)
c [score-dist-9] median active exp 533, avg 447.3
c [simplification-9] removed 87 variables 0.1% (58619 remain 24%)
c [simplification-9] removed 174 irredundant clauses 0.0% (358666 remain 48%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 36666
c [simplification-9] new conflict interval 73332
c [simplification-9] penalized conflict interval 73332 = 1 * 73332
c [simplification-9] hard conflict limit 173020 (soft 136354 + delta 36666)
c [simplification-9] new conflict limit 136354 (hard 173020)
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  124.0   58618   358666     66491   53701 163339 464459   28   111   93  26%    206   10   46   27  173%
c i  135.2   58617   358666     78066   63927 163531 464552   63   196   93  32%    105   89   63   30  208%
c -  138.5   58617   358666     80067   26904 163580 464614   70   197   67  36%    -19   87   37   32  115%
c i  139.2   58616   358666     82329   28937 163610 464647   48   131   70  36%     -6   20   13   31   40%
c i  140.9   58615   358666     85589   31918 163686 464670   39   119   70  33%    -20    8   48   31  153%
c i  145.3   58614   358666     88880   34464 163782 464710   46   151   72  30%    -19   38   53   32  165%
c i  145.3   58613   358666     88881   34464 163782 464710   46   151   72  30%    -19   38   53   32  164%
c i  159.8   58607   358666    102803   46721 164072 464809   57   194   79  30%    137   66   79   37  210%
c i  166.4   58606   358666    111733   54929 164233 464855   41   226   84  18%     57   83   59   38  155%
c -  180.3   58606   358666    134077   40303 164568 465022   23   148   69  16%    235   -6   10   35   29%
c i  194.9   58605   358666    153560   58203 164794 465096   26   130   81  20%    438  -11   38   30  124%
c i  195.5   58604   358666    153848   58304 164800 465099   28   127   81  22%    281  -14   48   31  157%
c 
c [simplification-10] limit 136364 conflicts (hard 173020) hit after 154643 conflicts
c [quatres-6] found 62922 quaternary clauses 48% in total
c [quatres-6-2] added 25 single-self-subsuming ternary resolvents
c [quatres-6-2] added 61 quaternary resolvents
c [ternres-6] limit 51886809 with penalty 0 = 0 + 0
c [ternres-6] 35602 schedulable variables 61%
c [ternres-6] 23375 ternary resolvents (92 bin, 23283 trn)
c [ternres-6] 2667 variables remain 5% (55937 retained 95%)
c [card-4] limit 3242925 penalty 3 = 3 + 0
c [card-4] found 24 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 3242925 for elimination
c [card-4] 24 out of 24 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-22] removed 459 variables
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 227 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 58160 variables 100%
c [block-3] limit of 129717024 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 500 blocked clauses
c [block-3] 500 < 1/100 * 356189 = 3561 considered unsuccessful
c [cce-3] limit of 64858512 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 3 clauses out of 5 (60%) of length 129
c [cce-3-1] eliminated 1 clauses out of 18 (6%) of length 68
c [cce-3-1] eliminated 1 clauses out of 24 (4%) of length 67
c [cce-3-1] eliminated 2 clauses out of 20 (10%) of length 66
c [cce-3-1] eliminated 1 clauses out of 22 (5%) of length 65
c [cce-3-1] eliminated 2 clauses out of 32 (6%) of length 64
c [cce-3-1] eliminated 1 clauses out of 29 (3%) of length 63
c [cce-3-1] eliminated 2 clauses out of 45 (4%) of length 62
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 13 large clauses in 64859366 steps
c [cce-3-1] allowing another 32429683 steps for small clauses
c [cce-3-1] scheduling 228463 clauses = 70786 binary + 157677 ternary
c [cce-3-1] tried to eliminate 1186 small clauses 1%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 20 ternary clauses 0%
c [cce-3-1] eliminated 21 small clauses 0%
c [cce-3-1] eliminated 21 small clauses in 64858514 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 34 covered clauses in round 1
c [cce-3] eliminated 34 covered clauses in TOTAL during 1 rounds
c [cce-3] 34 < 1/100 * 355689 = 3556 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 58160 variables 100%
c [elim-7] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 244 variables 0% in round 1 in 131320287 steps
c [elim-7-1] backward subsumption/strengthening limit 68679713
c [elim-7-1-1] backward checking 1760 touched variables 3%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 240 clauses in 22196865 steps
c [elim-7-1] rescheduled 487 variables 1% by backward subsumption
c [elim-7-2] eliminated 1 variables 0% in round 2 in 23793284 steps
c [elim-7-2] backward subsumption/strengthening limit 22689564
c [elim-7-2-1] backward checking 20 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 159551 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 245 = 0% variables out of 58160 scheduled
c [elim-7] 245 < 1/100 * 58160 = 581 considered unsuccessful
c [bca-5] limit of 10000000 steps and 714052 added (scaled 2)
c [bca-5] 66435 out of 115832 literals actually usable 57%
c [bca-5] added 46 blocked clauses in 217713 steps
c [sweep-6] limit 15566042 penalty 0 = 0 + 0
c [sweep-6-1] 19434 pos 43.2% + 25595 neg 56.8% = 45029 sched 77.8% ret 12886
c [sweep-6-1] 15597368 steps 64 queries 5016.19 avg class size
c [sweep-6-1] 942 decisions 57 SAT calls 103.95 avg env size
c [sweep-6-1] 44459 variables remain 77% (13456 retained 23%)
c [decomp-23] removed 17 variables
c [sweep-6-1] removed 17 vars (0 failed, 10 eqs, 14 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 17 vars in TOTAL (1 rounds, 63 queries)
c [sort-queue-10] sorted 30851 enqueued variables after 154643 conflicts
c [score-dist-10] active 27047 (47%), one 27529 (48%), zero 3322 (6%)
c [score-dist-10] max exp 598, different 451 (75%)
c [score-dist-10] median active exp 496, avg 448.0
c [simplification-10] removed 706 variables 1.2% (57898 remain 23%)
c [simplification-10] removed 3584 irredundant clauses 1.0% (355082 remain 48%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 36666 = 73332 / 2
c [simplification-10] new conflict interval 109998
c [simplification-10] penalized conflict interval 109998 = 1 * 109998
c [simplification-10] hard conflict limit 319640 (soft 264641 + delta 54999)
c [simplification-10] new conflict limit 264641 (hard 319640)
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  232.7   57897   355082    176998   77098 178506 442313   50   174   89  29%    147   31   61   32  191%
c i  232.9   57896   355082    177136   77215 178508 442314   52   174   89  30%    103   32   87   32  275%
c -  238.3   57895   355082    183280   48746 178665 442349   38   158   69  24%   -108   13   26   32   80%
c i  240.5   57894   355082    186547   51738 178705 442367   42   197   74  21%    -54   51   89   33  271%
c -  265.3   57894   355082    230025   57370 179335 442552   27   119   70  23%    392  -38   17   31   54%
c i  275.4   57893   355082    242549   68710 179559 442636   60   209   80  29%    502   53   57   33  174%
c i  275.4   57892   355082    242560   68719 179560 442636   60   209   80  29%    493   53   59   33  179%
c i  277.7   57887   355082    244474   70368 179601 442650   56   193   80  29%   -211   36   47   33  142%
c i  289.8   57885   355082    264407   88769 179781 442714   52   209   90  25%     -9   43   48   33  145%
c i  289.9   57884   355082    264438   88781 179782 442714   52   208   90  25%    -18   42   50   33  151%
c i  290.0   57883   355082    264469   88795 179781 442715   52   207   90  25%    -27   41   51   33  155%
c i  290.7   57882   355082    264862   88955 179795 442721   50   194   90  26%   -114   27   33   33  100%
c -  298.2   57882   355082    276889   64617 179965 442783   25   101   70  25%    -98  -62   21   32   65%
c 
c [simplification-11] limit 264641 conflicts (hard 319640) hit after 283564 conflicts
c [quatres-7] found 65586 quaternary clauses 44% in total
c [quatres-7-1] removed 2 duplicate quaternary clauses
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 37 single-self-subsuming ternary resolvents
c [quatres-7-2] added 173 quaternary resolvents
c [ternres-7] limit 82914971 with penalty 0 = 0 + 0
c [ternres-7] 2610 schedulable variables 5%
c [ternres-7] 11789 ternary resolvents (376 bin, 11413 trn)
c [ternres-7] 3 variables remain 0% (57879 retained 100%)
c [decomp-24] removed 584 variables
c [treelook-3] limit 2072874 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 70119 literals 61%
c [treelook-3] scheduling used 2095109 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 2072874 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 2664085 steps
c [treelook-3] 70006 literals remain 61%
c [treelook-3] 10768 variables remain to probed next time 19%
c [treelook-3] removed 1 variables, found 5995 hbrs
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 221 transitive binary clauses
c [bca-6] limit of 10000000 steps and 707303 added (scaled 2)
c [bca-6] 57097 out of 114628 literals actually usable 50%
c [bca-6] added 100 blocked clauses in 209731 steps
c [sweep-7] limit 24874491 penalty 0 = 0 + 0
c [sweep-7-1] 17732 pos 40.4% + 26210 neg 59.6% = 43942 sched 76.7% ret 13371
c [sweep-7-1] 25122563 steps 95 queries 1580.03 avg class size
c [sweep-7-1] 2804 decisions 89 SAT calls 100.71 avg env size
c [sweep-7-1] 41995 variables remain 73% (15318 retained 27%)
c [decomp-26] removed 10 variables
c [sweep-7-1] removed 10 vars (0 failed, 5 eqs, 10 impls)
c [sweep-7] 10 < 1/1000 * 57313 = 57 considered unsuccessful
c [sweep-7] removed 10 vars in TOTAL (1 rounds, 94 queries)
c [sort-queue-11] sorted 40186 enqueued variables after 283564 conflicts
c [score-dist-11] active 17117 (30%), one 38490 (67%), zero 1696 (3%)
c [score-dist-11] max exp 931, different 659 (71%)
c [score-dist-11] median active exp 672, avg 500.3
c [simplification-11] removed 579 variables 1.0% (57303 remain 23%)
c [simplification-11] removed 3372 irredundant clauses 0.9% (351710 remain 47%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 54999 = 109998 / 2
c [simplification-11] new conflict interval 164997
c [simplification-11] penalized conflict interval 164997 = 1 * 164997
c [simplification-11] hard conflict limit 531059 (soft 448561 + delta 82498)
c [simplification-11] new conflict limit 448561 (hard 531059)
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  324.5   57302   351710    287611   73852 168549 474817   40   171   79  23%     72   12   43   33  130%
c i  332.5   57301   351710    302295   87284 168766 474860   42   144   84  29%    -26  -12   73   32  225%
c i  342.6   57300   351710    317209  100990 168916 474953   34   184   91  18%      2   33   87   31  277%
c -  347.7   57300   351710    324899   71842 169053 475001   21   141   71  15%    -95  -12    8   31   26%
c -  380.4   57300   351710    374229   79342 169746 475325   28   156   72  18%    497   -7   37   32  115%
c i  393.5   57299   351710    394631   98324 169995 475412   31   113   85  28%    638  -58   48   31  154%
c i  393.6   57297   351710    394699   98350 169997 475414   32   113   85  28%    560  -58   55   31  175%
c i  411.6   57296   351710    419052  120532 170365 475540   35   151  100  23%    -89  -16   68   33  205%
c -  412.7   57296   351710    419756   83923 170386 475558   43   167   71  26%   -266    0   97   34  287%
c i  413.8   57295   351710    420589   84698 170398 475560   49   180   77  27%   -355   14   76   34  221%
c i  419.5   57294   351710    427736   91248 170502 475591   53   184   79  29%   -312   17   58   35  163%
c i  420.7   57293   351710    428658   92052 170522 475601   53   186   80  28%   -359   19   37   36  104%
c 
c [simplification-12] limit 448561 conflicts (hard 531059) hit after 455092 conflicts
c [quatres-8] found 68753 quaternary clauses 40% in total
c [quatres-8-1] added 3 double-self-subsuming ternary resolvents
c [quatres-8-2] added 55 single-self-subsuming ternary resolvents
c [quatres-8-2] added 213 quaternary resolvents
c [ternres-8] limit 125481997 with penalty 0 = 0 + 0
c [ternres-8] 2 schedulable variables 0%
c [ternres-8] 1381 ternary resolvents (54 bin, 1327 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-5] limit 6274099 penalty 2 = 2 + 0
c [gauss-5] extracted 10151 xors of average arity 3.0
c [gauss-5] connected 30132 occurrences of 12332 variables (average 2.4)
c [gauss-5] limit 6274099 penalty 2 = 2 + 0
c [decomp-27] removed 712 variables
c [gauss-5] exported 0 unary, 10 binary and 8 ternary equations
c [unhide-6] limit 1250000 with penalty 4 = 3 + 1
c [unhide-6-6] 0 units, 0 failed, 43273 tauts, 0 hbrs, 133941 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 265 transitive binary clauses
c [bca-7] limit of 10000000 steps and 702123 added (scaled 2)
c [bca-7] 43317 out of 113164 literals actually usable 38%
c [bca-7] added 6 blocked clauses in 223008 steps
c [sort-queue-12] sorted 27400 enqueued variables after 455092 conflicts
c [score-dist-12] active 29181 (52%), one 26697 (47%), zero 703 (1%)
c [score-dist-12] max exp 812, different 755 (93%)
c [score-dist-12] median active exp 581, avg 516.8
c [simplification-12] removed 712 variables 1.2% (56581 remain 23%)
c [simplification-12] removed 2595 irredundant clauses 0.7% (349115 remain 47%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 82498 = 164997 / 2
c [simplification-12] new conflict interval 247495
c [simplification-12] penalized conflict interval 247495 = 1 * 247495
c [simplification-12] hard conflict limit 826334 (soft 702587 + delta 123747)
c [simplification-12] new conflict limit 702587 (hard 826334)
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  447.7   56580   349115    459688  119634 158831 397730   56   178   97  32%    125   14   30   36   83%
c -  453.2   56580   349115    470448   90531 159017 397774   24   105   71  23%   -157  -52   40   34  119%
c i  457.7   56579   349115    480394   99671 159156 397804   21   211   78  10%      9   57   38   31  122%
c i  458.8   56578   349115    481521  100435 159206 397824   22   183   78  12%   -187   28   26   31   83%
c -  489.8   56578   349115    521283   97610 159703 398005   17   135   71  12%    294  -23   11   32   34%
c i  502.5   56577   349115    532820  107982 159913 398082   54   182   82  30%    412   23   51   35  146%
c i  511.0   56576   349115    544197  118442 160041 398141   41   159   87  26%   -175    4   33   36   91%
c i  521.0   56575   349115    559339  132288 160244 398182   42   155   96  27%    -71    6  101   35  288%
c i  525.1   56574   349115    562926  135562 160280 398194   59   183  100  32%   -233   33   75   37  203%
c -  528.8   56573   349115    572467  105439 160396 398221   24    97   72  24%   -118  -50   31   34   91%
c i  541.5   56572   349115    595908  126936 160771 398327   32   221   89  14%    225   59   46   31  145%
c -  565.7   56572   349115    623421  112028 161168 398511   28   149   72  19%    155  -17   13   35   36%
c i  582.8   56571   349115    649039  135866 161426 398577   29   145   91  20%    436   -3   40   32  126%
c -  595.8   56571   349115    675194  120912 161655 398638   22   232   73   9%     64   83   35   30  118%
c i  601.0   56570   349115    683837  128621 161776 398671   22   110   82  20%    182  -41   19   29   65%
c 
c [simplification-13] limit 702587 conflicts (hard 826334) hit after 709071 conflicts
c [quatres-9] found 73067 quaternary clauses 36% in total
c [quatres-9-1] removed 6 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 65 single-self-subsuming ternary resolvents
c [quatres-9-2] added 271 quaternary resolvents
c [ternres-9] limit 188774351 with penalty 0 = 0 + 0
c [ternres-9] all 56570 free variables schedulable
c [ternres-9] 17018 ternary resolvents (861 bin, 16157 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-29] removed 1258 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 255 transitive binary clauses
c [bca-8] limit of 10000000 steps and 695130 added (scaled 2)
c [bca-8] 35284 out of 110648 literals actually usable 32%
c [bca-8] added 0 blocked clauses in 237983 steps
c [sweep-8] limit 28316152 penalty 1 = 1 + 0
c [sweep-8-1] 19732 pos 49.1% + 20460 neg 50.9% = 40192 sched 72.6% ret 15131
c [sweep-8-1] 28481041 steps 141 queries 2598.23 avg class size
c [sweep-8-1] 4830 decisions 130 SAT calls 138.22 avg env size
c [sweep-8-1] 36867 variables remain 67% (18456 retained 33%)
c [decomp-30] removed 24 variables
c [sweep-8-1] removed 24 vars (0 failed, 11 eqs, 12 impls)
c [sweep-8] 24 < 1/1000 * 55323 = 55 considered unsuccessful
c [sweep-8] removed 24 vars in TOTAL (1 rounds, 140 queries)
c [sort-queue-13] sorted 26463 enqueued variables after 709071 conflicts
c [score-dist-13] active 28836 (52%), one 25994 (47%), zero 469 (1%)
c [score-dist-13] max exp 653, different 619 (95%)
c [score-dist-13] median active exp 469, avg 422.7
c [simplification-13] removed 1271 variables 2.2% (55299 remain 22%)
c [simplification-13] removed 3541 irredundant clauses 1.0% (345574 remain 46%)
c [simplification-13] maximum reduction of 2% = max (2%, 1%)
c [simplification-13] geometric conflict interval increment 82498 = 247495 / 3
c [simplification-13] new conflict interval 329993
c [simplification-13] penalized conflict interval 329993 = 1 * 329993
c [simplification-13] hard conflict limit 1204060 (soft 1039064 + delta 164996)
c [simplification-13] new conflict limit 1039064 (hard 1204060)
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  645.2   55298   345574    714057  154786 165236 421594   48   136  108  35%    145  -15   85   36  240%
c -  656.5   55298   345574    725770  123515 165390 421654   35   117   75  30%   -112  -36   30   37   80%
c i  664.3   55297   345574    737244  133956 165507 421684   35   193   89  18%     70   41   52   37  141%
c i  664.3   55296   345574    737272  133952 165507 421685   35   192   89  18%     61   40   48   37  131%
c -  695.2   55296   345574    778934  130761 166087 421870   37   154   75  24%    324    2   18   35   51%
c i  714.2   55295   345574    805054  155213 166306 421937   31    95   97  33%    554  -57   19   34   57%
c i  725.9   55294   345574    820442  169386 166442 421972   46   156  103  29%   -198   12   67   34  199%
c -  732.3   55269   345574    832325  139037 166585 421997   16    86   76  19%   -199  -52   13   31   41%
c i  744.4   55268   345574    847492  153046 166775 422042   34   123   91  27%     53  -17   40   33  122%
c i  761.7   55251   345574    868148  172167 166950 422096   42   147  105  29%      3    9   38   36  106%
c -  771.7   55251   345574    883691  143547 167158 422150   31   176   76  18%    -40   38   46   35  132%
c -  819.6   55251   345574    937833  148744 167769 422393   43   119   77  36%    558  -29   44   39  115%
c i  833.5   55250   345574    956299  165654 167938 422463   34   132   93  26%    672  -13   16   37   44%
c i  833.5   55245   345574    956300  165654 167938 422463   34   132   93  26%    671  -13   16   37   44%
c i  864.9   55239   345574    987559  193984 168326 422598   54   159  116  34%    -63    7   79   43  182%
c -  869.4   55239   345574    994332  154823 168404 422605   36   151   77  24%   -403   -1   49   42  117%
c 
c [simplification-14] limit of 65 iterations hit after 65 iterations
c [quatres-10] found 76842 quaternary clauses 33% in total
c [quatres-10-1] removed 4 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 92 single-self-subsuming ternary resolvents
c [quatres-10-2] added 183 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 55239 free variables schedulable
c [ternres-10] 12826 ternary resolvents (702 bin, 12124 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-6] limit 25000000 penalty 1 = 1 + 0
c [gauss-6] extracted 32005 xors of average arity 2.9
c [gauss-6] connected 93975 occurrences of 14462 variables (average 6.5)
c [gauss-6] limit 25000000 penalty 1 = 1 + 0
c [decomp-31] removed 1463 variables
c [gauss-6] exported 0 unary, 69 binary and 54 ternary equations
c [basicprobe-3] limit 100000000 penalty 2 = 2 + 0
c [basicprobe-3-0] 7139 probes remain 13% after last round
c [basicprobe-3-0] 24 units = 24 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 76 variables, found 279556 hbrs
c [bate-2] eliminated 214 asymmetric tautologies during probing
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 479 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 53700 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 4648 blocked clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 1683144736 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 429 (0%) of length 34
c [cce-4-1] eliminated 1 clauses out of 461 (0%) of length 33
c [cce-4-1] eliminated 2 clauses out of 461 (0%) of length 32
c [cce-4-1] eliminated 1 clauses out of 502 (0%) of length 31
c [cce-4-1] eliminated 1 clauses out of 508 (0%) of length 30
c [cce-4-1] eliminated 1 clauses out of 540 (0%) of length 29
c [cce-4-1] eliminated 2 clauses out of 552 (0%) of length 28
c [cce-4-1] eliminated 1 clauses out of 539 (0%) of length 27
c [cce-4-1] eliminated 1 clauses out of 625 (0%) of length 26
c [cce-4-1] eliminated 1 clauses out of 606 (0%) of length 25
c [cce-4-1] eliminated 2 clauses out of 587 (0%) of length 24
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 14 large clauses in 1683144771 steps
c [cce-4-1] allowing another 841572385 steps for small clauses
c [cce-4-1] scheduling 203225 clauses = 61371 binary + 141854 ternary
c [cce-4-1] tried to eliminate 31095 small clauses 15%
c [cce-4-1] eliminated 36 binary clauses 0%
c [cce-4-1] eliminated 1422 ternary clauses 1%
c [cce-4-1] eliminated 1458 small clauses 1%
c [cce-4-1] eliminated 1458 small clauses in 1683144742 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 1472 covered clauses in round 1
c [cce-4] eliminated 1472 covered clauses in TOTAL during 1 rounds
c [cce-4] 1472 < 1/100 * 327950 = 3279 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 53694 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2000000000 steps penalty 3 = 3 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1227 variables 2% in round 1 in 122302341 steps
c [elim-8-1] backward subsumption/strengthening limit 122302300
c [elim-8-1-1] backward checking 4518 touched variables 8%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 49 and strengthened 248 clauses in 10860476 steps
c [elim-8-1] rescheduled 419 variables 1% by backward subsumption
c [elim-8-2] eliminated 2 variables 0% in round 2 in 5728510 steps
c [elim-8-2] backward subsumption/strengthening limit 5728500
c [elim-8-2-1] backward checking 15 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 1 and strengthened 1 clauses in 374325 steps
c [elim-8-2] rescheduled 5 variables 0% by backward subsumption
c [elim-8-3] eliminated 1 variables 0% in round 3 in 382900 steps
c [elim-8-3] backward subsumption/strengthening limit 382900
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 0 and strengthened 0 clauses in 230923 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1230 = 2% variables out of 53694 scheduled
c [sort-queue-14] sorted 29257 enqueued variables after 1018432 conflicts
c [score-dist-14] active 23207 (44%), one 28985 (55%), zero 272 (1%)
c [score-dist-14] max exp 564, different 544 (96%)
c [score-dist-14] median active exp 408, avg 383.5
c [simplification-14] removed 2775 variables 5.0% (52464 remain 21%)
c [simplification-14] removed 20267 irredundant clauses 5.9% (325307 remain 44%)
c [simplification-14] maximum reduction of 6% = max (5%, 6%)
c [simplification-14] forced so keeping old conflict interval 329993
c [simplification-14] conflict limit remains at 1039074 (hard 1204060)
c [simplification-14] new iteration interval 100
c 
c [simplification-15] limit 1039074 conflicts (hard 1204060) hit after 1039074 conflicts
c [quatres-11] found 78982 quaternary clauses 33% in total
c [quatres-11-1] removed 20 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 56 single-self-subsuming ternary resolvents
c [quatres-11-2] added 316 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 52464 free variables schedulable
c [ternres-11] 12745 ternary resolvents (690 bin, 12055 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 8596158 penalty 4 = 4 + 0
c [card-5] found 57 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 8596158 for elimination
c [card-5] 57 out of 57 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-7] limit 50000000 penalty 0 = 0 + 0
c [gauss-7] extracted 59826 xors of average arity 3.0
c [gauss-7] connected 178594 occurrences of 17456 variables (average 10.2)
c [gauss-7] limit 50000000 penalty 0 = 0 + 0
c [decomp-33] removed 244 variables
c [gauss-7] exported 0 unary, 57 binary and 103 ternary equations
c [simpleprobe-4] 10366 schedulable variables 20%
c [simpleprobe-4] limit 200000000 penalty 0 = 0 + 0
c [decomp-35] removed 177 variables
c [simpleprobe-4] 2778 variables remain 5% (49265 retained 95%)
c [simpleprobe-4] removed 177 variables, found 95243 hbrs, 0 units
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 724 transitive binary clauses
c [bca-9] limit of 10000000 steps and 652812 added (scaled 2)
c [bca-9] 26544 out of 104088 literals actually usable 26%
c [bca-9] added 72 blocked clauses in 253164 steps
c [sort-queue-15] sorted 34244 enqueued variables after 1039074 conflicts
c [score-dist-15] active 17799 (34%), one 33982 (65%), zero 262 (1%)
c [score-dist-15] max exp 954, different 781 (82%)
c [score-dist-15] median active exp 516, avg 572.8
c [simplification-15] removed 421 variables 0.8% (52043 remain 21%)
c [simplification-15] removed 849 irredundant clauses 0.3% (324458 remain 43%)
c [simplification-15] maximum reduction of 1% = max (1%, 0%)
c [simplification-15] geometric conflict interval increment 164996 = 329993 / 2
c [simplification-15] new conflict interval 494989
c [simplification-15] penalized conflict interval 494989 = 1 * 494989
c [simplification-15] hard conflict limit 1781557 (soft 1534063 + delta 247494)
c [simplification-15] new conflict limit 1534063 (hard 1781557)
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 -  969.2   52043   324458   1055266  155846 168698 655046   48   238   82  20%    461   85   89   42  211%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 228 basic ate = 118 trn 52% + 110 lrg 48% in 2 updates
c bcas: 9 count, 6864 added (15 skipped), 2033001 steps
c bkwd: tried 273249 clauses, 544804 lits, 1.99 lits/clause
c bkwd: checked 40577113 occs, 148.50 occs/clause, 74.48 occs/lit
c bkwd: subsumed 39 binary, 79 ternary, 939 large
c bkwd: strengthened 0 binary, 42 ternary (100% self), 911 large (0% self)
c blkd: 4 bces, 6191 removed, 10201829 resolutions, 25569713 steps
c blkd: 1900 blocking literals 0%, 6 pure
c bump: 1074621 bumped seen, 188410677 lits 175.3 on average
c card: 5 count, 0 units, 0 am1, 87797115 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 6379 subsumed
c card: 96 at-most-one constraints found, average size 3.00
c card: 96 at-most-one constraints used 100%, average size 3.00
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: 4 cces, 1601 eliminated, 1597 ate 100%, 4 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: 2488144 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 68 gcs, 0 rescored clauses, 565 rescored vars
c dcps: 35 decompositions, 5739 equivalent 2%
c deco: 13455 decision-only clauses 1%, 56% reduction
c decs: 10359626 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 191306 eliminated 77%, 0 pure 0%
c elms: 15 rounds, 1.9 rounds/bve
c elms: 171202 small 89%, 20098 large 11%
c elms: 350043 tried small, 171202 succeeded 49%, 178841 failed 51%
c elms: 2558 subsumed, 3362 strengthened, 186 blocked
c elms: 9053576 copies, 14147598 resolutions, 11239605 ipos
c elms: 8306963 subchks, 5669329 strchks
c gaus: 7 extractions, 138920 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 141 binary and 168 ternary equations
c gaus: 0 gc, 179752234 steps, 89876117 extr 50%, 89986662 elim 50%
c glue: 35.3 orig avg, 35.3 real avg, 4.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 947229 = 111129 simple 12% + 833881 trn 88% + 2219 lrg 0%, 1803 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1074621 clauses, 93.4 length
c lrnd: 100320234 lits = 136239252 orig - 35919018 removed 26%
c lrnd: 463090 uips 43%, 458505 flips 43%
c mins: 981323 mins 94%, 5561 bin 1%, 44503 size 4%
c mins: 476177534 poisoned searches, 44130746 hits, 9% hit rate
c mins: 547218103 used twice searches, 20095650 hits, 4% hit rate
c move: moved 5051, 599 bin 12%, 4452 trn 88%
c otfs: 21715 driving 62%, 13183 restarting 38%
c otfs: str 34898, 23580 red 68%, 11318 irr 32%
c otfs: str 34898, 0 bin 0%, 12190 trn 35%, 22708 lrg 65%
c otfs: sub 251, 251 red 100%, 0 irr 0%
c otfs: sub 251, 0 bin 0%, 142 trn 57%, 109 lrg 43%
c phas: 5 computed, 75581 set, 23992 pos (32%), 51589 neg (68%)
c prbs: 3 basic, 39534 probed, 24 failed, 0 lifted
c prbs: 4 simple, 503478 probed, 2 failed, 349 eqs
c prbs: 3 treelook, 158 probed, 1 failed, 0 lifted
c prom: 222183 locked 10% out of 2144370 tried
c prps: 1855688067 props, 178 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 11 count, 5867 quat, 432 self1, 8 self2, 52 dup
c queu: 15 sorted, 10359626 next (3668154 steps 0.35)
c queu: 201748151 enq (205499639 steps 1.02), 188410677 deq 93%
c redc: 24991 clauses 11%, 224255 tried 20%, 32 sat 0%
c redc: 35132 lits 2%, 2226163 tried 2%, 32 sat 0%
c redc: 1022 times jump level reduced, 10.0 levels on average
c reds: 20 count, 54773.2 conflicts per reduce
c reds: 0 memlim 0%, 20 arith 100%
c reds: 595911 collected 76%, 190613 retired 24%
c rmbd: 13743 removed, 13659 red 99%
c rsts: 19951 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 15 count, 11 confs 73%, 0 vars 0%
c simp: 1 its 7%, 2 bin 13%, 1 trns 7%
c subl: 1074621 count (1078470 tried 1.0), 58722 sub out of 1051073 (5.6%)
c swps: 8 count, 8 rounds, 824 queries (103.0/round)
c swps: 748 sat calls, 22 unsat (1.2% success rate)
c swps: 20922 decisions 28.0, 873 conflicts 1.2
c swps; 2741.2 avg class size, 166.0 avg environment size
c swps: 0 failed, 158 impls, 98 equivs
c swp0: 271 type 0 queries, 34 unsat (12.5%), 256 sat (94.5%)
c swp1: 553 type 1 queries, 228 unsat (41.2%), 470 sat (85.0%)
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: 22869949 calls to obtain time
c tops: 239 fixed 0%, 65 its, 16853.28 confs/it
c trds: 11 transitive reductions, 3048 removed, 1 failed
c trds: 38946 nodes, 52060 edges, 22005289 steps
c trim: 1314919 words, 5.0 MB
c trnr: 11 count, 2822 bin, 249393 trn, 656048034 steps
c unhd: 6 count, 6 rounds, 17653414 steps
c unhd: 114 non-trivial sccs of average size 2.0
c unhd: 2 units, 2 bin, 0 trn, 0 lrg
c unhd: 14 failed, 14 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 50445 tauts, 256 bin 1%, 10012 trn 20%, 505 lrg 1%
c unhd: 50445 tauts, 39672 stamp 79%, 50218 red 100%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 290589 str, 2 bin 0%, 2208 trn 1%, 288379 lrg 99%, 282376 red 97%
c vars: 52043 remaining 21% and 197284 removed 79% out of 249327
c vars: 239 fixed 0%, 191306 eliminated 77%, 5739 equivalent 2%
c vsts: 29221917611 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 15.7 search visits per propagation, 26507.6 per conflict
c wchs: 2032561452 pushed, 32258795 enlarged, 121 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1056940        595911        190613     190621493      10415609        354101
c 
c  0 0        172635  16     22220   4         0   0 122828315  64   5007696  48    144774  41     5.3
c  1 5         64087   6     38613   6     14565   8  13105882   7<   830962   8     26076   7     0.8
c  2 6        135318  13     89305  15     27216  14  19002429  10   1257856  12<    42896  12     1.7
c  3 9        130974  12     86872  15     25726  13  14234847   7   1026910  10     35573  10<    2.5
c  4 14       106540  10<    71083  12     21286  11   7634088   4    635403   6     24115   7     2.5
c  5 21        92413   9     62834  11<    17889   9<  5645966   3    483026   5     19785   6     2.8
c  6 30        85723   8     58553  10     16737   9   3478455   2    379307   4     16375   5     3.3
c  7 41        77783   7     53169   9     15147   8   1853257   1    239882   2     13075   4     4.6
c  8 54        55916   5     37162   6     11779   6   1042291   1    153170   1      9209   3     3.2
c  9 69        34434   3     21493   4      8722   5    598396   0    103184   1      5067   1     1.9
c 10 86        35668   3     21054   4     10166   5    552112   0    109735   1      5301   1     2.2
c 11 126       39845   4     20146   3     12385   6    445731   0    129778   1      7078   2     3.3
c 12 230       25588   2     13405   2      8988   5    199705   0     58692   1      4777   1     4.9
c 13 534          16   0         2   0         7   0        19   0         8   0         0   0     0.0
c 
c avg                  4.3           4.8           5.5           1.1           2.0           2.6
c std                  3.3           3.0           3.3           1.9           2.7           3.1
c 
c   57.191   6% ternres
c   30.336   3% bump
c   20.199   2% elim
c   19.711   2% cce
c   12.791   1% probe
c   11.860   1% sweep
c    9.799   1% gauss
c    6.881   1% decide
c    4.217   0% block
c 
c   13.305 < 1% rest (below)
c 
c    3.373   0% unhide
c    3.205   0% quatres
c    2.482   0% bca
c    2.069   0% rescore
c    1.840   0% transred
c    0.336   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    4.855   0% preprocessing     3%
c  150.349  15% inprocessing     97%
c ==================================
c  155.204  16% simplifying
c  844.426  84% search
c ==================================
c  999.633 100% all
c 
c       1095463 conflicts,        1095.9 confs/sec
c         16990 ternaries,          64.5 confs/ternary
c          6285 binaries,          174.3 confs/binary
c            65 iterations,      16853.3 confs/iteration
c 
c            20 reductions,          0.0 redus/sec,  54773.2 confs/reduction
c         19951 restarts,           20.0 rests/sec,     54.9 confs/restart
c      10359626 decisions,       10363.4 decis/sec,      9.5 decis/conflict
c    1855688067 propagations,  1856369.2 props/sec,    179.1 props/decision
c 
c 999.6 seconds, 142.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
