c launch: /data/cnf/sc2014/app/9dlx_vliw_at_b_iq4.cnf.bz2
c host: atom08
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/9dlx_vliw_at_b_iq4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/9dlx_vliw_at_b_iq4.cnf.bz2
c no embedded options
c found 'p cnf 106013 1598301' header
c read 106013 variables, 1598301 clauses, 4617403 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=3
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 106012 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] SUM (--score=3)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  106012  1598300         0       0      0     0    0     0   48   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 19 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 19 out of 19 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 7 variables
c [simpleprobe-1] all 106006 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 533 variables
c [simpleprobe-1] 74690 variables remain 71% (30783 retained 29%)
c [simpleprobe-1] removed 533 variables, found 15999 hbrs, 532 units
c [unhide-1] limit 99313 based on 1589016 irredundant clauses
c [unhide-1-1] 27 units, 2 failed, 2334 tauts, 0 hbrs, 16640 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 105445 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 99852 not tried 95% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 5593 = 5% variables out of 105445 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 1574931 negative 100.0% of 1575313 except 382 0.0%
c [phase-count-1] 433508 positive 27.5% of 1575313 except 1141805 72.5%
c [phase-count-1] less non-negative clauses 382 than limit 157500 (10.0%)
c [phase-count-1] non-pos/non-neg = 1141805/382 = 2989.02 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 99852 negative 100%
c [sort-queue-1] sorted 99852 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 99852 (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 6154 variables 5.8% (99852 remain 94%)
c [simplification-1] removed 22987 irredundant clauses 1.4% (1575313 remain 99%)
c [simplification-1] maximum reduction of 6% = max (6%, 1%)
c [simplification-1] large reduction 6% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [simpleprobe-2] 70968 schedulable variables 71%
c [simpleprobe-2] limit 3150626 based on 1575313 irredundant clauses
c [decomp-4] removed 176 variables
c [simpleprobe-2] 71813 variables remain 72% (27863 retained 28%)
c [simpleprobe-2] removed 176 variables, found 3303 hbrs, 176 units
c [treelook-1] limit 392949 based on 1571798 irredundant clauses
c [treelook-1] scheduled 74226 literals 37%
c [treelook-1] scheduling used 392984 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 392949 based on 1571798 irredundant clauses
c [treelook-1] used 438884 steps
c [treelook-1] 74221 literals remain 37%
c [treelook-1] 72002 variables remain to probed next time 72%
c [treelook-1] removed 0 variables, found 11 hbrs
c [basicprobe-1] limit 12574384 based on 1571798 irredundant clauses
c [basicprobe-1-0] 94017 probes remain 98% after last round
c [basicprobe-1-0] 38 units = 38 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3811 variables, found 11953 hbrs
c [unhide-2] limit 98237 based on 1571798 irredundant clauses
c [unhide-2-2] 1508 units, 12 failed, 615 tauts, 0 hbrs, 26824 literals
c [elim-2] 93324 variables 100% will be scheduled this time
c [elim-2] scheduled 93324 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 83321 not tried 89% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 9938 = 11% variables out of 93324 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 75437 enqueued variables after 1000 conflicts
c [score-dist-2] active 7949 (10%), one 0 (0%), zero 75437 (90%)
c [score-dist-2] max exp 519, different 17 (3%)
c [score-dist-2] median active exp 512, avg 512.2
c [simplification-2] removed 16466 variables 16.5% (83386 remain 79%)
c [simplification-2] removed 128468 irredundant clauses 8.2% (1446845 remain 91%)
c [simplification-2] maximum reduction of 16% = max (16%, 8%)
c [simplification-2] large reduction 16% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3001 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 19 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] 19 out of 19 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 355 variables
c [unhide-3] limit 90383 based on 1446135 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 5583 tauts, 0 hbrs, 11972 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 83031 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 65850 not tried 79% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 7799 = 9% variables out of 83031 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 61085 enqueued variables after 3001 conflicts
c [score-dist-3] active 14147 (19%), one 0 (0%), zero 61085 (81%)
c [score-dist-3] max exp 523, different 20 (4%)
c [score-dist-3] median active exp 514, avg 514.2
c [simplification-3] removed 8154 variables 9.8% (75232 remain 71%)
c [simplification-3] removed 22279 irredundant clauses 1.5% (1424566 remain 89%)
c [simplification-3] maximum reduction of 10% = max (10%, 2%)
c [simplification-3] large reduction 10% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15001 (soft 5001 + delta 10000)
c [simplification-3] new conflict limit 5001 (hard 15001)
c 
c [simplification-4] limit 5001 conflicts (hard 15001) hit after 5001 conflicts
c [decomp-7] removed 3 variables
c [treelook-2] limit 356115 based on 1424461 irredundant clauses
c [treelook-2] scheduled 60358 literals 40%
c [treelook-2] scheduling used 356186 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 356115 based on 1424461 irredundant clauses
c [treelook-2] used 436856 steps
c [treelook-2] 60352 literals remain 40%
c [treelook-2] 52569 variables remain to probed next time 70%
c [treelook-2] removed 1 variables, found 34 hbrs
c [elim-4] 65847 variables 88% will be scheduled this time
c [elim-4] scheduled 65847 variables 88%
c [elim-4] boosting limit by 20
c [elim-4] limit of 456274200 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 5928 variables 8% in round 1 in 312855104 steps
c [elim-4-1] backward subsumption/strengthening limit 143419096
c [elim-4-1-1] backward checking 50104 touched variables 67%
c [elim-4-1-1] incomplete backward checking 50106 remain 100%
c [elim-4-1] subsumed 90 and strengthened 23 clauses in 143423022 steps
c [elim-4] incomplete 167 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 5928 = 9% variables out of 65847 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 51071 enqueued variables after 5001 conflicts
c [score-dist-4] active 18229 (26%), one 0 (0%), zero 51071 (74%)
c [score-dist-4] max exp 524, different 21 (4%)
c [score-dist-4] median active exp 515, avg 515.3
c [simplification-4] removed 5932 variables 7.9% (69300 remain 65%)
c [simplification-4] removed 59480 irredundant clauses 4.2% (1365086 remain 85%)
c [simplification-4] maximum reduction of 8% = max (8%, 4%)
c [simplification-4] large reduction 8% >= 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 17001 (soft 7001 + delta 10000)
c [simplification-4] new conflict limit 7001 (hard 17001)
c 
c [simplification-5] limit 7001 conflicts (hard 17001) hit after 7003 conflicts
c [quatres-1] found 15551 quaternary clauses 15% in total
c [quatres-1-2] added 56 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1000 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 69300 free variables schedulable
c [ternres-1] 43500 ternary resolvents (0 bin, 43500 trn)
c [ternres-1] 584 variables remain 1% (68716 retained 99%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 1 xors of average arity 2.0
c [gauss-1] connected 2 occurrences of 2 variables (average 1.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 4 variables
c [basicprobe-2] limit 10920600 based on 1365075 irredundant clauses
c [basicprobe-2-0] 64759 probes remain 95% after last round
c [basicprobe-2-0] 31 units = 31 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 819 variables, found 15515 hbrs
c [unhide-4] limit 85317 based on 1365075 irredundant clauses
c [unhide-4-4] 1249 units, 21 failed, 819 tauts, 0 hbrs, 28453 literals
c [transred-1] limit 1634698 with penalty 0 = 0 + 0
c [transred-1] removed 5 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 65347 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 103006 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 4 clauses out of 5 (80%) of length 112
c [cce-1-1] eliminated 1 clauses out of 5 (20%) of length 111
c [cce-1-1] eliminated 8 clauses out of 9 (89%) of length 110
c [cce-1-1] eliminated 1 clauses out of 7 (14%) of length 109
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 108
c [cce-1-1] eliminated 1 clauses out of 5 (20%) of length 106
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 105
c [cce-1-1] eliminated 5 clauses out of 11 (45%) of length 104
c [cce-1-1] eliminated 7 clauses out of 7 (100%) of length 103
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 102
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 101
c [cce-1-1] eliminated 1 clauses out of 5 (20%) of length 100
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 99
c [cce-1-1] eliminated 3 clauses out of 18 (17%) of length 98
c [cce-1-1] eliminated 13 clauses out of 22 (59%) of length 97
c [cce-1-1] eliminated 2 clauses out of 17 (12%) of length 96
c [cce-1-1] eliminated 1 clauses out of 16 (6%) of length 94
c [cce-1-1] eliminated 3 clauses out of 28 (11%) of length 93
c [cce-1-1] eliminated 2 clauses out of 38 (5%) of length 92
c [cce-1-1] eliminated 10 clauses out of 36 (28%) of length 91
c [cce-1-1] eliminated 1 clauses out of 32 (3%) of length 90
c [cce-1-1] eliminated 2 clauses out of 57 (4%) of length 89
c [cce-1-1] eliminated 3 clauses out of 40 (8%) of length 87
c [cce-1-1] eliminated 5 clauses out of 72 (7%) of length 86
c [cce-1-1] eliminated 11 clauses out of 61 (18%) of length 85
c [cce-1-1] eliminated 6 clauses out of 84 (7%) of length 84
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 103 large clauses in 30000000 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 1097673 clauses = 1056968 binary + 40705 ternary
c [cce-1-1] tried to eliminate 244 small clauses 0%
c [cce-1-1] eliminated 38 binary clauses 0%
c [cce-1-1] eliminated 38 small clauses 0%
c [cce-1-1] eliminated 38 small clauses in 30000012 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 141 covered clauses in round 1
c [cce-1] eliminated 141 covered clauses in TOTAL during 1 rounds
c [cce-1] 141 < 1/100 * 1202925 = 12029 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 63572 variables 100%
c [elim-5] limit of 32693962 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 31072 not tried 49% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 4000 = 6% variables out of 63572 scheduled
c [bca-1] limit of 10000000 steps and 2375672 added (scaled 2)
c [bca-1] 104188 out of 119146 literals actually usable 87%
c [bca-1] added 13330 blocked clauses in 420856 steps
c [sweep-1] limit 2375172 based on 1187586 irredundant clauses
c [sweep-1-1] 5240 pos 8.8% + 54332 neg 91.2% = 59572 sched 100.0% ret 0
c [sweep-1-1] 2537864 steps 26 queries 6833.85 avg class size
c [sweep-1-1] 961 decisions 23 SAT calls 222.87 avg env size
c [sweep-1-1] 59325 variables remain 100% (246 retained 0%)
c [decomp-10] removed 72 variables
c [sweep-1-1] removed 72 vars (1 failed, 1 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 72 vars in TOTAL (1 rounds, 25 queries)
c [sort-queue-5] sorted 37797 enqueued variables after 7003 conflicts
c [score-dist-5] active 21703 (36%), one 0 (0%), zero 37797 (64%)
c [score-dist-5] max exp 525, different 22 (4%)
c [score-dist-5] median active exp 516, avg 516.1
c [simplification-5] removed 9800 variables 14.1% (59500 remain 56%)
c [simplification-5] removed 178565 irredundant clauses 13.1% (1186521 remain 74%)
c [simplification-5] maximum reduction of 14% = max (14%, 13%)
c [simplification-5] large reduction 14% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 19003 (soft 9003 + delta 10000)
c [simplification-5] new conflict limit 9003 (hard 19003)
c 
c [simplification-6] limit 9003 conflicts (hard 19003) hit after 9004 conflicts
c [quatres-2] found 14709 quaternary clauses 16% in total
c [quatres-2-2] added 18 single-self-subsuming ternary resolvents
c [quatres-2-2] added 592 quaternary resolvents
c [ternres-2] limit 4746072 based on 1186518 irredundant clauses
c [ternres-2] 570 schedulable variables 1%
c [ternres-2] 4823 ternary resolvents (6 bin, 4817 trn)
c [ternres-2] 182 variables remain 0% (59318 retained 100%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 9 at-most-one constraints of average size 3.6
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 9 out of 9 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 43278 schedulable variables 73%
c [simpleprobe-3] limit 8451963 penalty 0 = 0 + 0
c [decomp-12] removed 2 variables
c [simpleprobe-3] 43911 variables remain 74% (15587 retained 26%)
c [simpleprobe-3] removed 2 variables, found 2757 hbrs, 0 units
c [unhide-5] limit 105649 with penalty 2 = 0 + 2
c [unhide-5-5] 49 units, 3 failed, 16549 tauts, 0 hbrs, 15960 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 7 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 59446 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 68427 blocked clauses
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 59174 variables 100%
c [elim-6] limit of 42259816 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 20876 not tried 35% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 1937 = 3% variables out of 59174 scheduled
c [bca-2] limit of 10000000 steps and 2204613 added (scaled 2)
c [bca-2] 97279 out of 114476 literals actually usable 85%
c [bca-2] added 2274 blocked clauses in 379214 steps
c [sweep-2] limit 2197448 based on 1098724 irredundant clauses
c [sweep-2-1] 5684 pos 10.0% + 51320 neg 90.0% = 57004 sched 99.6% ret 233
c [sweep-2-1] 2380920 steps 22 queries 8833.36 avg class size
c [sweep-2-1] 747 decisions 21 SAT calls 204.62 avg env size
c [sweep-2-1] 56400 variables remain 99% (418 retained 1%)
c [decomp-13] removed 887 variables
c [sweep-2-1] removed 887 vars (0 failed, 1 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 887 vars in TOTAL (1 rounds, 21 queries)
c [sort-queue-6] sorted 32610 enqueued variables after 9004 conflicts
c [score-dist-6] active 23740 (42%), one 0 (0%), zero 32610 (58%)
c [score-dist-6] max exp 526, different 23 (4%)
c [score-dist-6] median active exp 516, avg 516.6
c [simplification-6] removed 3150 variables 5.3% (56350 remain 53%)
c [simplification-6] removed 103436 irredundant clauses 8.7% (1083085 remain 68%)
c [simplification-6] maximum reduction of 9% = max (5%, 9%)
c [simplification-6] large reduction 9% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 21004 (soft 11004 + delta 10000)
c [simplification-6] new conflict limit 11004 (hard 21004)
c 
c [simplification-7] limit 11004 conflicts (hard 21004) hit after 11005 conflicts
c [quatres-3] found 13300 quaternary clauses 16% in total
c [quatres-3-2] added 26 single-self-subsuming ternary resolvents
c [quatres-3-2] added 184 quaternary resolvents
c [ternres-3] limit 4332336 based on 1083084 irredundant clauses
c [ternres-3] 182 schedulable variables 0%
c [ternres-3] 1518 ternary resolvents (16 bin, 1502 trn)
c [ternres-3] 104 variables remain 0% (56246 retained 100%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 43170 literals 38%
c [treelook-3] scheduling used 300011 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 2680202 steps
c [treelook-3] 43167 literals remain 38%
c [treelook-3] 35712 variables remain to probed next time 63%
c [treelook-3] removed 0 variables, found 271 hbrs
c [unhide-6] limit 130390 with penalty 2 = 0 + 2
c [unhide-6-6] 315 units, 4 failed, 1249 tauts, 0 hbrs, 18577 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 10 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 56010 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 37734 blocked clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 109
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 107
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 104
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 101
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 5 large clauses in 15000026 steps
c [cce-2-1] allowing another 7500013 steps for small clauses
c [cce-2-1] scheduling 942342 clauses = 904331 binary + 38011 ternary
c [cce-2-1] tried to eliminate 642 small clauses 0%
c [cce-2-1] eliminated 11 binary clauses 0%
c [cce-2-1] eliminated 1 ternary clauses 0%
c [cce-2-1] eliminated 12 small clauses 0%
c [cce-2-1] eliminated 12 small clauses in 15000236 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 17 covered clauses in round 1
c [cce-2] eliminated 17 covered clauses in TOTAL during 1 rounds
c [cce-2] 17 < 1/100 * 1038803 = 10388 considered unsuccessful
c [elim-7] 20433 variables 37% will be scheduled this time
c [elim-7] scheduled 20433 variables 37%
c [elim-7] limit of 52156093 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 7944 not tried 14% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 401 = 2% variables out of 20433 scheduled
c [elim-7] 401 < 1/100 * 20433 = 204 considered unsuccessful
c [bca-3] limit of 10000000 steps and 2077730 added (scaled 2)
c [bca-3] 92175 out of 110256 literals actually usable 84%
c [bca-3] added 9126 blocked clauses in 360312 steps
c [sweep-3] limit 2069428 based on 1034714 irredundant clauses
c [sweep-3-1] 5627 pos 10.3% + 49089 neg 89.7% = 54716 sched 99.3% ret 411
c [sweep-3-1] 2091219 steps 18 queries 7639.72 avg class size
c [sweep-3-1] 914 decisions 17 SAT calls 377.29 avg env size
c [sweep-3-1] 54620 variables remain 99% (507 retained 1%)
c [decomp-16] removed 75 variables
c [sweep-3-1] removed 75 vars (0 failed, 1 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 75 vars in TOTAL (1 rounds, 17 queries)
c [sort-queue-7] sorted 30242 enqueued variables after 11005 conflicts
c [score-dist-7] active 24810 (45%), one 0 (0%), zero 30242 (55%)
c [score-dist-7] max exp 526, different 23 (4%)
c [score-dist-7] median active exp 517, avg 516.9
c [simplification-7] removed 1298 variables 2.3% (55052 remain 52%)
c [simplification-7] removed 48629 irredundant clauses 4.5% (1034456 remain 65%)
c [simplification-7] maximum reduction of 4% = max (2%, 4%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 4000
c [simplification-7] penalized conflict interval 4000 = 1 * 4000
c [simplification-7] hard conflict limit 25005 (soft 15005 + delta 10000)
c [simplification-7] new conflict limit 15005 (hard 25005)
c 
c [simplification-8] limit 15005 conflicts (hard 25005) hit after 15005 conflicts
c [quatres-4] found 13830 quaternary clauses 17% in total
c [quatres-4-2] added 11 single-self-subsuming ternary resolvents
c [quatres-4-2] added 364 quaternary resolvents
c [ternres-4] limit 4137796 based on 1034449 irredundant clauses
c [ternres-4] 104 schedulable variables 0%
c [ternres-4] 1300 ternary resolvents (1 bin, 1299 trn)
c [ternres-4] 18 variables remain 0% (55034 retained 100%)
c [basicprobe-3] limit 16388453 penalty 0 = 0 + 0
c [basicprobe-3-0] 50021 probes remain 91% after last round
c [basicprobe-3-0] 21 units = 21 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 279 variables, found 5590 hbrs
c [bate-1] eliminated 37 asymmetric tautologies during probing
c [unhide-7] limit 163884 with penalty 2 = 0 + 2
c [unhide-7-7] 4 units, 1 failed, 13196 tauts, 0 hbrs, 24429 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 7 transitive binary clauses
c [transred-4] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 54766 variables 100%
c [block-4] limit of 50000000 steps penalty 0 = 0 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 16633 blocked clauses
c [bca-4] limit of 10000000 steps and 2000673 added (scaled 2)
c [bca-4] 89560 out of 108522 literals actually usable 83%
c [bca-4] added 11205 blocked clauses in 361407 steps
c [sweep-4] limit 1987808 based on 993904 irredundant clauses
c [sweep-4-1] 5216 pos 9.7% + 48557 neg 90.3% = 53773 sched 99.1% ret 487
c [sweep-4-1] 2094667 steps 12 queries 9443.00 avg class size
c [sweep-4-1] 360 decisions 10 SAT calls 582.80 avg env size
c [sweep-4-1] 53747 variables remain 99% (513 retained 1%)
c [decomp-18] removed 629 variables
c [sweep-4-1] removed 629 vars (0 failed, 1 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 629 vars in TOTAL (1 rounds, 11 queries)
c [sort-queue-8] sorted 29495 enqueued variables after 15005 conflicts
c [score-dist-8] active 24136 (45%), one 0 (0%), zero 29495 (55%)
c [score-dist-8] max exp 528, different 25 (5%)
c [score-dist-8] median active exp 517, avg 517.3
c [simplification-8] removed 1421 variables 2.6% (53631 remain 51%)
c [simplification-8] removed 42266 irredundant clauses 4.1% (992190 remain 62%)
c [simplification-8] maximum reduction of 4% = max (3%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 8000
c [simplification-8] penalized conflict interval 8000 = 1 * 8000
c [simplification-8] hard conflict limit 33005 (soft 23005 + delta 10000)
c [simplification-8] new conflict limit 23005 (hard 33005)
c 
c [simplification-9] limit 23005 conflicts (hard 33005) hit after 23006 conflicts
c [quatres-5] found 10816 quaternary clauses 14% in total
c [quatres-5-2] added 44 single-self-subsuming ternary resolvents
c [quatres-5-2] added 47 quaternary resolvents
c [ternres-5] limit 4335342 with penalty 0 = 0 + 0
c [ternres-5] 18 schedulable variables 0%
c [ternres-5] 117 ternary resolvents (0 bin, 117 trn)
c [ternres-5] 5 variables remain 0% (53626 retained 100%)
c [simpleprobe-4] 39693 schedulable variables 74%
c [simpleprobe-4] limit 17341371 penalty 0 = 0 + 0
c [decomp-20] removed 142 variables
c [simpleprobe-4] 39238 variables remain 73% (14251 retained 27%)
c [simpleprobe-4] removed 142 variables, found 26292 hbrs, 137 units
c [unhide-8] limit 216767 with penalty 2 = 0 + 2
c [unhide-8-8] 683 units, 9 failed, 3335 tauts, 0 hbrs, 78807 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 7 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 52793 variables 100%
c [block-5] limit of 50000000 steps penalty 0 = 0 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 5594 blocked clauses
c [block-5] 5594 < 1/100 * 990097 = 9900 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 52726 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 867068550 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1943 variables 4% in round 1 in 476955716 steps
c [elim-8-1] backward subsumption/strengthening limit 390112834
c [elim-8-1-1] backward checking 15595 touched variables 30%
c [elim-8-1-1] incomplete backward checking 15626 remain 100%
c [elim-8-1] subsumed 0 and strengthened 279 clauses in 390114612 steps
c [elim-8] incomplete 374 not tried 1% in round 1
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 1944 = 4% variables out of 52726 scheduled
c [bca-5] limit of 10000000 steps and 1907335 added (scaled 2)
c [bca-5] 83127 out of 101566 literals actually usable 82%
c [bca-5] added 2358 blocked clauses in 321097 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 13006020 penalty 0 = 0 + 0
c [sweep-5-1] 4611 pos 9.2% + 45677 neg 90.8% = 50288 sched 99.0% ret 494
c [sweep-5-1] 13019700 steps 116 queries 1952.47 avg class size
c [sweep-5-1] 3513 decisions 108 SAT calls 162.41 avg env size
c [sweep-5-1] 47321 variables remain 93% (3460 retained 7%)
c [decomp-21] removed 16 variables
c [sweep-5-1] removed 16 vars (0 failed, 7 eqs, 16 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 16 vars in TOTAL (1 rounds, 115 queries)
c [sort-queue-9] sorted 27673 enqueued variables after 23006 conflicts
c [score-dist-9] active 23093 (45%), one 0 (0%), zero 27673 (55%)
c [score-dist-9] max exp 529, different 26 (5%)
c [score-dist-9] median active exp 517, avg 517.9
c [simplification-9] removed 2865 variables 5.3% (50766 remain 48%)
c [simplification-9] removed 47782 irredundant clauses 4.8% (944408 remain 59%)
c [simplification-9] maximum reduction of 5% = max (5%, 5%)
c [simplification-9] large reduction 5% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 35006 (soft 25006 + delta 10000)
c [simplification-9] new conflict limit 25006 (hard 35006)
c 
c [simplification-10] limit 25006 conflicts (hard 35006) hit after 25007 conflicts
c [quatres-6] found 11286 quaternary clauses 16% in total
c [quatres-6-2] added 49 single-self-subsuming ternary resolvents
c [quatres-6-2] added 86 quaternary resolvents
c [ternres-6] limit 4566324 with penalty 0 = 0 + 0
c [ternres-6] 5 schedulable variables 0%
c [ternres-6] 311 ternary resolvents (0 bin, 311 trn)
c [ternres-6] 2 variables remain 0% (50764 retained 100%)
c [card-4] limit 285395 penalty 3 = 3 + 0
c [card-4] found 12 at-most-one constraints of average size 5.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 285395 for elimination
c [card-4] 12 out of 12 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-9] limit 228316 with penalty 2 = 0 + 2
c [unhide-9-9] 78 units, 2 failed, 7518 tauts, 0 hbrs, 11366 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 8 transitive binary clauses
c [cce-3] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 3750088 steps for small clauses
c [cce-3-1] scheduling 840708 clauses = 828491 binary + 12217 ternary
c [cce-3-1] tried to eliminate 101 small clauses 0%
c [cce-3-1] eliminated 77 binary clauses 0%
c [cce-3-1] eliminated 77 small clauses 0%
c [cce-3-1] eliminated 1672 small clauses in 7501293 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1672 covered clauses in round 1
c [cce-3] eliminated 1672 covered clauses in TOTAL during 1 rounds
c [cce-3] 1672 < 1/100 * 937717 = 9377 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 50685 variables 100%
c [elim-9] limit of 91326485 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 3707 not tried 7% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1203 = 2% variables out of 50685 scheduled
c [bca-6] limit of 10000000 steps and 1837284 added (scaled 2)
c [bca-6] 80407 out of 98966 literals actually usable 81%
c [bca-6] added 160 blocked clauses in 303701 steps
c [sweep-6] limit 1817638 based on 908819 irredundant clauses
c [sweep-6-1] 4120 pos 8.9% + 42047 neg 91.1% = 46167 sched 93.3% ret 3315
c [sweep-6-1] 1837669 steps 22 queries 5643.45 avg class size
c [sweep-6-1] 607 decisions 20 SAT calls 77.20 avg env size
c [sweep-6-1] 45971 variables remain 93% (3511 retained 7%)
c [sweep-6-1] removed 0 vars (0 failed, 1 eqs, 0 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 21 queries)
c [sort-queue-10] sorted 26438 enqueued variables after 25007 conflicts
c [score-dist-10] active 23044 (47%), one 0 (0%), zero 26438 (53%)
c [score-dist-10] max exp 529, different 26 (5%)
c [score-dist-10] median active exp 518, avg 518.0
c [simplification-10] removed 1284 variables 2.5% (49482 remain 47%)
c [simplification-10] removed 35589 irredundant clauses 3.8% (908819 remain 57%)
c [simplification-10] maximum reduction of 4% = max (3%, 4%)
c [simplification-10] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-10] new conflict interval 12000
c [simplification-10] penalized conflict interval 12000 = 1 * 12000
c [simplification-10] hard conflict limit 47007 (soft 37007 + delta 10000)
c [simplification-10] new conflict limit 37007 (hard 47007)
c 
c [simplification-11] limit 37007 conflicts (hard 47007) hit after 37008 conflicts
c [quatres-7] found 11334 quaternary clauses 16% in total
c [quatres-7-2] added 39 quaternary resolvents
c [ternres-7] limit 5925863 with penalty 0 = 0 + 0
c [ternres-7] 2 schedulable variables 0%
c [ternres-7] 59 ternary resolvents (0 bin, 59 trn)
c [ternres-7] fully completed ternary resolution
c [treelook-4] limit 296293 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 38720 literals 39%
c [treelook-4] scheduling used 302194 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 296293 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 2658455 steps
c [treelook-4] 38718 literals remain 39%
c [treelook-4] 30323 variables remain to probed next time 61%
c [treelook-4] removed 0 variables, found 21 hbrs
c [unhide-10] limit 296293 with penalty 2 = 0 + 2
c [unhide-10-10] 39 units, 23 failed, 1062 tauts, 0 hbrs, 118160 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 49427 variables 100%
c [block-6] limit of 29629315 steps penalty 1 = 1 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 6389 blocked clauses
c [block-6] 6389 < 1/100 * 908737 = 9087 considered unsuccessful
c [elim-10] 3707 variables 8% will be scheduled this time
c [elim-10] scheduled 3707 variables 8%
c [elim-10] limit of 118517263 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 1060 not tried 2% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 0 = 0% variables out of 3707 scheduled
c [bca-7] limit of 10000000 steps and 1821026 added (scaled 2)
c [bca-7] 79698 out of 98628 literals actually usable 81%
c [bca-7] added 550 blocked clauses in 303296 steps
c [sweep-7] limit 1801300 based on 900650 irredundant clauses
c [sweep-7-1] 3789 pos 8.3% + 42037 neg 91.7% = 45826 sched 92.9% ret 3487
c [sweep-7-1] 1837934 steps 20 queries 6020.40 avg class size
c [sweep-7-1] 857 decisions 19 SAT calls 134.79 avg env size
c [sweep-7-1] 45700 variables remain 93% (3612 retained 7%)
c [decomp-26] removed 3 variables
c [sweep-7-1] removed 3 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] 3 < 1/1000 * 49313 = 49 considered unsuccessful
c [sweep-7] removed 3 vars in TOTAL (1 rounds, 19 queries)
c [sort-queue-11] sorted 26159 enqueued variables after 37008 conflicts
c [score-dist-11] active 23151 (47%), one 0 (0%), zero 26159 (53%)
c [score-dist-11] max exp 531, different 28 (5%)
c [score-dist-11] median active exp 518, avg 518.5
c [simplification-11] removed 172 variables 0.3% (49310 remain 47%)
c [simplification-11] removed 8229 irredundant clauses 0.9% (900590 remain 56%)
c [simplification-11] maximum reduction of 1% = max (0%, 1%)
c [simplification-11] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-11] new conflict interval 22000
c [simplification-11] penalized conflict interval 22000 = 1 * 22000
c [simplification-11] hard conflict limit 70008 (soft 59008 + delta 11000)
c [simplification-11] new conflict limit 59008 (hard 70008)
c 
c [simplification-12] limit 59008 conflicts (hard 70008) hit after 59009 conflicts
c [quatres-8] found 11358 quaternary clauses 16% in total
c [quatres-8-2] added 7 quaternary resolvents
c [ternres-8] limit 7063302 with penalty 0 = 0 + 0
c [ternres-8] all 49310 free variables schedulable
c [ternres-8] 883 ternary resolvents (1 bin, 882 trn)
c [ternres-8] 34110 variables remain 69% (15200 retained 31%)
c [basicprobe-4] limit 35316514 penalty 0 = 0 + 0
c [basicprobe-4-0] 43281 probes remain 88% after last round
c [basicprobe-4-0] 13 units = 13 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 13 variables, found 2748 hbrs
c [bate-2] eliminated 9 asymmetric tautologies during probing
c [unhide-11] limit 353165 with penalty 2 = 0 + 2
c [unhide-11-11] 0 units, 0 failed, 4540 tauts, 0 hbrs, 23263 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 17 transitive binary clauses
c [transred-8] found 1 units
c [bca-8] limit of 10000000 steps and 1812035 added (scaled 2)
c [bca-8] 79505 out of 98594 literals actually usable 81%
c [bca-8] added 50 blocked clauses in 310215 steps
c [sort-queue-12] sorted 26101 enqueued variables after 59009 conflicts
c [score-dist-12] active 23195 (47%), one 0 (0%), zero 26101 (53%)
c [score-dist-12] max exp 532, different 29 (5%)
c [score-dist-12] median active exp 518, avg 519.1
c [simplification-12] removed 14 variables 0.0% (49296 remain 47%)
c [simplification-12] removed 4573 irredundant clauses 0.5% (896017 remain 56%)
c [simplification-12] maximum reduction of 1% = max (0%, 1%)
c [simplification-12] geometric conflict interval increment 11000 = 22000 / 2
c [simplification-12] new conflict interval 33000
c [simplification-12] penalized conflict interval 33000 = 1 * 33000
c [simplification-12] hard conflict limit 108509 (soft 92009 + delta 16500)
c [simplification-12] new conflict limit 92009 (hard 108509)
c 
c [simplification-13] limit 92009 conflicts (hard 108509) hit after 92009 conflicts
c [quatres-9] found 11392 quaternary clauses 17% in total
c [ternres-9] limit 9381197 with penalty 0 = 0 + 0
c [ternres-9] 34101 schedulable variables 69%
c [ternres-9] 1289 ternary resolvents (0 bin, 1289 trn)
c [ternres-9] 11333 variables remain 23% (37963 retained 77%)
c [simpleprobe-5] 35924 schedulable variables 73%
c [simpleprobe-5] limit 37524788 penalty 0 = 0 + 0
c [decomp-29] removed 16 variables
c [simpleprobe-5] 32496 variables remain 66% (16784 retained 34%)
c [simpleprobe-5] removed 16 variables, found 37832 hbrs, 15 units
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 14 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 49280 variables 100%
c [elim-11] limit of 93811972 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 3559 not tried 7% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 494 = 1% variables out of 49280 scheduled
c [bca-9] limit of 10000000 steps and 1792104 added (scaled 2)
c [bca-9] 78318 out of 97574 literals actually usable 80%
c [bca-9] added 38 blocked clauses in 318615 steps
c [sweep-8] limit 1772078 based on 886039 irredundant clauses
c [sweep-8-1] 3414 pos 7.5% + 41823 neg 92.5% = 45237 sched 92.7% ret 3549
c [sweep-8-1] 2163395 steps 22 queries 4683.86 avg class size
c [sweep-8-1] 547 decisions 20 SAT calls 155.00 avg env size
c [sweep-8-1] 45073 variables remain 92% (3713 retained 8%)
c [decomp-30] removed 4 variables
c [sweep-8-1] removed 4 vars (0 failed, 1 eqs, 2 impls)
c [sweep-8] 4 < 1/1000 * 48786 = 48 considered unsuccessful
c [sweep-8] removed 4 vars in TOTAL (1 rounds, 21 queries)
c [sort-queue-13] sorted 25580 enqueued variables after 92009 conflicts
c [score-dist-13] active 23202 (48%), one 0 (0%), zero 25580 (52%)
c [score-dist-13] max exp 533, different 30 (6%)
c [score-dist-13] median active exp 519, avg 519.6
c [simplification-13] removed 514 variables 1.0% (48782 remain 46%)
c [simplification-13] removed 9984 irredundant clauses 1.1% (886033 remain 55%)
c [simplification-13] maximum reduction of 1% = max (1%, 1%)
c [simplification-13] geometric conflict interval increment 16500 = 33000 / 2
c [simplification-13] new conflict interval 49500
c [simplification-13] penalized conflict interval 49500 = 1 * 49500
c [simplification-13] hard conflict limit 166259 (soft 141509 + delta 24750)
c [simplification-13] new conflict limit 141509 (hard 166259)
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 -  121.4   48782   886033     95035   25174  29255 88945  179   239   58  75%    780   34  156  110  142%
c 
c [simplification-14] limit 141509 conflicts (hard 166259) hit after 141509 conflicts
c [ternres-10] limit 12471805 with penalty 0 = 0 + 0
c [ternres-10] 11214 schedulable variables 23%
c [ternres-10] 1415 ternary resolvents (0 bin, 1415 trn)
c [ternres-10] 123 variables remain 0% (48659 retained 100%)
c [gauss-4] limit 443016 based on 886033 irredundant clauses
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-12] limit 311795 with penalty 3 = 1 + 2
c [unhide-12-12] 8 units, 5 failed, 2045 tauts, 0 hbrs, 227311 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 17 transitive binary clauses
c [transred-10] found 2 units
c [block-7] scheduling all variables this time
c [block-7] scheduled 48767 variables 100%
c [block-7] limit of 31179512 steps penalty 2 = 2 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 4997 blocked clauses
c [block-7] 4997 < 1/100 * 886013 = 8860 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 77948781 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 3 clauses out of 24 (12%) of length 91
c [cce-4-1] eliminated 3 clauses out of 53 (6%) of length 89
c [cce-4-1] eliminated 6 clauses out of 36 (17%) of length 88
c [cce-4-1] eliminated 8 clauses out of 58 (14%) of length 86
c [cce-4-1] eliminated 2 clauses out of 61 (3%) of length 84
c [cce-4-1] eliminated 7 clauses out of 93 (8%) of length 83
c [cce-4-1] eliminated 7 clauses out of 74 (9%) of length 81
c [cce-4-1] eliminated 2 clauses out of 78 (3%) of length 80
c [cce-4-1] eliminated 5 clauses out of 57 (9%) of length 79
c [cce-4-1] eliminated 4 clauses out of 105 (4%) of length 78
c [cce-4-1] eliminated 9 clauses out of 134 (7%) of length 77
c [cce-4-1] eliminated 12 clauses out of 100 (12%) of length 76
c [cce-4-1] eliminated 4 clauses out of 117 (3%) of length 75
c [cce-4-1] eliminated 12 clauses out of 128 (9%) of length 74
c [cce-4-1] eliminated 4 clauses out of 145 (3%) of length 72
c [cce-4-1] eliminated 9 clauses out of 201 (4%) of length 71
c [cce-4-1] eliminated 2 clauses out of 119 (2%) of length 70
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 99 large clauses in 77949940 steps
c [cce-4-1] allowing another 38974970 steps for small clauses
c [cce-4-1] scheduling 801865 clauses = 772891 binary + 28974 ternary
c [cce-4-1] tried to eliminate 753 small clauses 0%
c [cce-4-1] eliminated 96 binary clauses 0%
c [cce-4-1] eliminated 96 small clauses 0%
c [cce-4-1] eliminated 96 small clauses in 77949355 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 195 covered clauses in round 1
c [cce-4] eliminated 195 covered clauses in TOTAL during 1 rounds
c [cce-4] 195 < 1/100 * 880828 = 8808 considered unsuccessful
c [elim-12] 1059 variables 2% will be scheduled this time
c [elim-12] scheduled 1059 variables 2%
c [elim-12] limit of 249436103 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 129 not tried 0% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 0 = 0% variables out of 1059 scheduled
c [bca-10] limit of 10000000 steps and 1778855 added (scaled 2)
c [bca-10] 82264 out of 97454 literals actually usable 84%
c [bca-10] added 880 blocked clauses in 328788 steps
c [sort-queue-14] sorted 25492 enqueued variables after 141509 conflicts
c [score-dist-14] active 23234 (48%), one 0 (0%), zero 25492 (52%)
c [score-dist-14] max exp 535, different 32 (6%)
c [score-dist-14] median active exp 520, avg 520.5
c [simplification-14] removed 56 variables 0.1% (48726 remain 46%)
c [simplification-14] removed 6628 irredundant clauses 0.7% (879405 remain 55%)
c [simplification-14] maximum reduction of 1% = max (0%, 1%)
c [simplification-14] geometric conflict interval increment 24750 = 49500 / 2
c [simplification-14] new conflict interval 74250
c [simplification-14] penalized conflict interval 74250 = 1 * 74250
c [simplification-14] hard conflict limit 252884 (soft 215759 + delta 37125)
c [simplification-14] new conflict limit 215759 (hard 252884)
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 -  143.3   48726   879405    155561   26750  30635 91988  208   220   57  95%    927   -0  215  143  150%
c -  149.3   48726   879405    197204   27572  30635 91988   76   238   59  32%    973    9   79  133   59%
c 
c [simplification-15] limit 215759 conflicts (hard 252884) hit after 215759 conflicts
c [quatres-10] found 11686 quaternary clauses 17% in total
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [quatres-10-2] added 7 quaternary resolvents
c [ternres-11] limit 14564328 with penalty 0 = 0 + 0
c [ternres-11] 123 schedulable variables 0%
c [ternres-11] 290 ternary resolvents (0 bin, 290 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 455135 penalty 4 = 4 + 0
c [card-5] found 16 at-most-one constraints of average size 3.3
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 455135 for elimination
c [card-5] 16 out of 16 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [unhide-13] limit 728216 with penalty 2 = 0 + 2
c [unhide-13-13] 24 units, 1 failed, 3928 tauts, 0 hbrs, 27910 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 6 transitive binary clauses
c [bca-11] limit of 10000000 steps and 1770701 added (scaled 2)
c [bca-11] 83049 out of 97404 literals actually usable 85%
c [bca-11] added 95 blocked clauses in 327445 steps
c [sort-queue-15] sorted 25416 enqueued variables after 215759 conflicts
c [score-dist-15] active 23285 (48%), one 0 (0%), zero 25416 (52%)
c [score-dist-15] max exp 536, different 33 (6%)
c [score-dist-15] median active exp 520, avg 520.9
c [simplification-15] removed 25 variables 0.1% (48701 remain 46%)
c [simplification-15] removed 4297 irredundant clauses 0.5% (875108 remain 55%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 74250
c [simplification-15] new conflict interval 148500
c [simplification-15] penalized conflict interval 148500 = 1 * 148500
c [simplification-15] hard conflict limit 438509 (soft 364259 + delta 74250)
c [simplification-15] new conflict limit 364259 (hard 438509)
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 -  154.7   48701   875108    225196   25525  30911 91663   79   232   57  34%    991    1   78  113   69%
c -  158.6   48701   875108    256242   25244  30911 91663   75   223   58  34%   1003   -7   77   99   78%
c -  162.7   48701   875108    288576   26279  30912 91664   97   293   58  33%   1011   62   91   93   98%
c -  172.0   48701   875092    326796   27934  30917 91678  109   304   58  36%   1017   54   74   99   75%
c -  188.2   48701   875087    400164   28110  30919 91680  145   221   60  66%   1022  -17   99  146   68%
c 
c [simplification-16] limit 364259 conflicts (hard 438509) hit after 422147 conflicts
c [quatres-11] found 11619 quaternary clauses 17% in total
c [ternres-12] limit 24947426 with penalty 0 = 0 + 0
c [ternres-12] all 48701 free variables schedulable
c [ternres-12] 151 ternary resolvents (0 bin, 151 trn)
c [ternres-12] 11 variables remain 0% (48690 retained 100%)
c [treelook-5] limit 623685 penalty 2 = 2 + 0 boost 1
c [treelook-5] scheduled 48147 literals 49%
c [treelook-5] scheduling used 623732 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 623685 penalty 2 = 2 + 0 boost 1
c [treelook-5] used 1055499 steps
c [treelook-5] 48143 literals remain 49%
c [treelook-5] 29688 variables remain to probed next time 61%
c [treelook-5] removed 0 variables, found 150 hbrs
c [unhide-14] limit 1247371 with penalty 2 = 0 + 2
c [unhide-14-14] 29 units, 1 failed, 1449 tauts, 0 hbrs, 291604 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 14 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 48671 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 367 variables 1% in round 1 in 1053058967 steps
c [elim-13-1] backward subsumption/strengthening limit 1053058900
c [elim-13-1-1] backward checking 8706 touched variables 18%
c [elim-13-1-1] incomplete backward checking 8735 remain 100%
c [elim-13-1] subsumed 0 and strengthened 17 clauses in 1053064497 steps
c [elim-13-1] rescheduled 55 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 98974715 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 367 = 1% variables out of 48671 scheduled
c [elim-13] 367 < 1/100 * 48671 = 486 considered unsuccessful
c [bca-12] limit of 10000000 steps and 1757555 added (scaled 2)
c [bca-12] 83401 out of 96610 literals actually usable 86%
c [bca-12] added 736 blocked clauses in 323961 steps
c [sweep-9] limit 1871056 penalty 2 = 2 + 0
c [sweep-9-1] 2915 pos 6.5% + 41728 neg 93.5% = 44643 sched 92.4% ret 3661
c [sweep-9-1] 1902830 steps 17 queries 5597.06 avg class size
c [sweep-9-1] 275 decisions 15 SAT calls 65.20 avg env size
c [sweep-9-1] 44587 variables remain 92% (3717 retained 8%)
c [decomp-35] removed 5 variables
c [sweep-9-1] removed 5 vars (0 failed, 1 eqs, 3 impls)
c [sweep-9] 5 < 1/1000 * 48304 = 48 considered unsuccessful
c [sweep-9] removed 5 vars in TOTAL (1 rounds, 16 queries)
c [sort-queue-16] sorted 24671 enqueued variables after 422147 conflicts
c [score-dist-16] active 23628 (49%), one 0 (0%), zero 24671 (51%)
c [score-dist-16] max exp 538, different 35 (6%)
c [score-dist-16] median active exp 523, avg 523.2
c [simplification-16] removed 402 variables 0.8% (48299 remain 46%)
c [simplification-16] removed 6578 irredundant clauses 0.8% (868509 remain 54%)
c [simplification-16] maximum reduction of 1% = max (1%, 1%)
c [simplification-16] geometric conflict interval increment 74250 = 148500 / 2
c [simplification-16] new conflict interval 222750
c [simplification-16] penalized conflict interval 222750 = 1 * 222750
c [simplification-16] hard conflict limit 756272 (soft 644897 + delta 111375)
c [simplification-16] new conflict limit 644897 (hard 756272)
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 -  235.4   48299   868509    474448   27212  30927 84411   97   221   59  44%   1023    0   90  153   59%
c -  241.4   48299   868509    508444   28038  30927 84411   89   215   60  42%   1024   -3   88  128   68%
c -  246.2   48299   868509    543302   28890  30927 84411   84   200   60  42%   1024  -14   83  110   76%
c -  257.6   48299   868509    601586   29596  30929 84424   93   217   57  43%   1024   12   62  100   62%
c -  269.8   48299   868509    669392   31854  30929 84424  152   180   58  84%   1024  -18  172  121  142%
c 
c [simplification-17] limit 644897 conflicts (hard 756272) hit after 673989 conflicts
c [ternres-13] limit 37575143 with penalty 0 = 0 + 0
c [ternres-13] 11 schedulable variables 0%
c [ternres-13] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-13] fully completed ternary resolution
c [basicprobe-5] limit 187875715 penalty 0 = 0 + 0
c [basicprobe-5-0] 36010 probes remain 75% after last round
c [basicprobe-5-0] 68 units = 68 failed (100%) + 0 lifted (0%)
c [basicprobe-5-0] removed 68 variables, found 11593 hbrs
c [bate-3] eliminated 91 asymmetric tautologies during probing
c [unhide-15] limit 1878757 with penalty 2 = 0 + 2
c [unhide-15-15] 0 units, 1 failed, 2911 tauts, 0 hbrs, 45799 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 17 transitive binary clauses
c [transred-13] found 1 units
c [bca-13] limit of 10000000 steps and 1750181 added (scaled 2)
c [bca-13] 83506 out of 96460 literals actually usable 87%
c [bca-13] added 640 blocked clauses in 324727 steps
c [sort-queue-17] sorted 24443 enqueued variables after 673989 conflicts
c [score-dist-17] active 23786 (49%), one 0 (0%), zero 24443 (51%)
c [score-dist-17] max exp 539, different 36 (7%)
c [score-dist-17] median active exp 525, avg 524.5
c [simplification-17] removed 70 variables 0.1% (48229 remain 45%)
c [simplification-17] removed 3869 irredundant clauses 0.4% (864640 remain 54%)
c [simplification-17] maximum reduction of 0% = max (0%, 0%)
c [simplification-17] full geometric conflict interval increment 222750
c [simplification-17] new conflict interval 445500
c [simplification-17] penalized conflict interval 445500 = 1 * 445500
c [simplification-17] hard conflict limit 1342239 (soft 1119489 + delta 222750)
c [simplification-17] new conflict limit 1119489 (hard 1342239)
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 -  294.0   48229   864640    749886   30513  30827 95602  141   167   58  84%   1024  -13   66  131   50%
c -  300.7   48229   864640    791049   30170  30827 95602   63   198   57  32%   1024    4   67   98   68%
c -  325.9   48229   864640    913784   31383  30827 95602   75   188   58  40%   1024   17   66  123   54%
c -  339.4   48229   864640    984400   31392  30827 95602   65   182   58  35%   1024    7   55  107   52%
c -  350.3   48229   864640   1035637   32935  30827 95602  108   161   59  68%   1024  -13   90   96   93%
c -  367.9   48229   864640   1105958   34263  30827 95602  135   142   60  95%   1024  -24  137  105  131%
c 
c [simplification-18] limit 1119489 conflicts (hard 1342239) hit after 1120249 conflicts
c [quatres-12] found 10899 quaternary clauses 17% in total
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [quatres-12-2] added 15 quaternary resolvents
c [decomp-37] removed 1 variables
c [simpleprobe-6] 31665 schedulable variables 66%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-38] removed 299 variables
c [simpleprobe-6] 20393 variables remain 43% (27536 retained 57%)
c [simpleprobe-6] removed 299 variables, found 304418 hbrs, 250 units
c [unhide-16] limit 3266118 with penalty 2 = 0 + 2
c [unhide-16-16] 1 units, 0 failed, 11160 tauts, 0 hbrs, 140854 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 6 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 47928 variables 100%
c [block-8] limit of 81652956 steps penalty 3 = 3 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 10304 blocked clauses
c [bca-14] limit of 10000000 steps and 1724057 added (scaled 2)
c [bca-14] 84294 out of 95708 literals actually usable 88%
c [bca-14] added 5459 blocked clauses in 340760 steps
c [sort-queue-18] sorted 23970 enqueued variables after 1120249 conflicts
c [score-dist-18] active 23883 (50%), one 0 (0%), zero 23970 (50%)
c [score-dist-18] max exp 541, different 38 (7%)
c [score-dist-18] median active exp 525, avg 525.1
c [simplification-18] removed 376 variables 0.8% (47853 remain 45%)
c [simplification-18] removed 13222 irredundant clauses 1.5% (851418 remain 53%)
c [simplification-18] maximum reduction of 2% = max (1%, 2%)
c [simplification-18] geometric conflict interval increment 148500 = 445500 / 3
c [simplification-18] new conflict interval 594000
c [simplification-18] penalized conflict interval 594000 = 1 * 594000
c [simplification-18] hard conflict limit 2011249 (soft 1714249 + delta 297000)
c [simplification-18] new conflict limit 1714249 (hard 2011249)
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 -  380.9   47853   851418   1151956   34027  30827 370802   41   249   63  16%   1024   51   35   79   44%
c -  416.2   47853   851412   1287520   34876  30827 370807   69   255   63  27%   1024   32   51  160   32%
c -  428.4   47853   851412   1327893   35729  30827 370807   52   239   63  22%   1024    6   52  111   47%
c -  435.0   47853   851412   1367788   33810  30827 370807   49   226   62  22%   1024   -7   50   83   60%
c -  441.0   47853   851412   1410617   31486  30827 370807   50   221   62  23%   1024   -9   48   69   71%
c -  448.0   47853   851412   1456295   35150  30827 370807   53   208   63  25%   1024  -13   51   61   84%
c -  455.4   47853   851412   1499306   35907  30827 370807   57   202   64  28%   1024  -12   57   58   98%
c -  462.3   47853   851412   1542893   36829  30827 370807   59   201   64  29%   1024   -7   60   57  106%
c -  468.8   47853   851412   1586171   38187  30827 370807   52   198   65  26%   1024   -6   50   55   91%
c -  473.9   47853   851412   1629545   39203  30827 370807   50   201   65  25%   1024   -1   55   54  103%
c 
c [simplification-19] limit 1714249 conflicts (hard 2011249) hit after 1714250 conflicts
c [quatres-13] found 11185 quaternary clauses 17% in total
c [quatres-13-2] added 23 quaternary resolvents
c [ternres-14] limit 52944453 with penalty 1 = 1 + 0
c [ternres-14] all 47853 free variables schedulable
c [ternres-14] 242 ternary resolvents (0 bin, 242 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-5] limit 1323611 penalty 4 = 4 + 0
c [gauss-5] extracted 0 xors of average arity 0.0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-17] limit 5000000 with penalty 2 = 0 + 2
c [unhide-17-18] 2 units, 1 failed, 9364 tauts, 0 hbrs, 456589 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 48 transitive binary clauses
c [transred-15] found 1 units
c [cce-5] limit of 33090283 steps penalty 4 = 4 + 0
c [cce-5-1] eliminated 1 clauses out of 35 (3%) of length 88
c [cce-5-1] eliminated 1 clauses out of 52 (2%) of length 86
c [cce-5-1] eliminated 2 clauses out of 26 (8%) of length 85
c [cce-5-1] eliminated 2 clauses out of 74 (3%) of length 83
c [cce-5-1] eliminated 1 clauses out of 41 (2%) of length 82
c [cce-5-1] eliminated 1 clauses out of 73 (1%) of length 80
c [cce-5-1] eliminated 1 clauses out of 92 (1%) of length 78
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 9 large clauses in 33090285 steps
c [cce-5-1] allowing another 16545142 steps for small clauses
c [cce-5-1] scheduling 773738 clauses = 746427 binary + 27311 ternary
c [cce-5-1] tried to eliminate 267 small clauses 0%
c [cce-5-1] eliminated 91 binary clauses 0%
c [cce-5-1] eliminated 91 small clauses 0%
c [cce-5-1] eliminated 204 small clauses in 33095466 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 213 covered clauses in round 1
c [cce-5] eliminated 213 covered clauses in TOTAL during 1 rounds
c [cce-5] 213 < 1/100 * 847499 = 8474 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 47849 variables 100%
c [elim-14] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14] incomplete 901 not tried 2% in round 1
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 880 = 2% variables out of 47849 scheduled
c [bca-15] limit of 10000000 steps and 1706848 added (scaled 2)
c [bca-15] 83674 out of 93940 literals actually usable 89%
c [bca-15] added 1867 blocked clauses in 361120 steps
c [sort-queue-19] sorted 20008 enqueued variables after 1714250 conflicts
c [score-dist-19] active 26961 (57%), one 0 (0%), zero 20008 (43%)
c [score-dist-19] max exp 542, different 39 (7%)
c [score-dist-19] median active exp 526, avg 526.5
c [simplification-19] removed 884 variables 1.8% (46969 remain 44%)
c [simplification-19] removed 9963 irredundant clauses 1.2% (841449 remain 53%)
c [simplification-19] maximum reduction of 2% = max (2%, 1%)
c [simplification-19] geometric conflict interval increment 198000 = 594000 / 3
c [simplification-19] new conflict interval 792000
c [simplification-19] penalized conflict interval 792000 = 1 * 792000
c [simplification-19] hard conflict limit 2902250 (soft 2506250 + delta 396000)
c [simplification-19] new conflict limit 2506250 (hard 2902250)
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 -  566.4   46969   841449   1886800   35880  30683 300326  263   352   65  75%   1024  -19  138  346   40%
c 
c [simplification-20] limit 2506250 conflicts (hard 2902250) hit after 2519702 conflicts
c [quatres-14] found 12345 quaternary clauses 19% in total
c [quatres-14-2] added 30 quaternary resolvents
c [ternres-15] limit 127818540 with penalty 0 = 0 + 0
c [ternres-15] all 46969 free variables schedulable
c [ternres-15] 301 ternary resolvents (0 bin, 301 trn)
c [ternres-15] fully completed ternary resolution
c [unhide-18] limit 2500000 with penalty 3 = 0 + 3
c [unhide-18-19] 0 units, 2 failed, 4905 tauts, 0 hbrs, 329040 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 20 transitive binary clauses
c [transred-16] found 1 units
c [block-9] scheduling all variables this time
c [block-9] scheduled 46967 variables 100%
c [block-9] limit of 200000000 steps penalty 2 = 2 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 2141 blocked clauses
c [block-9] 2141 < 1/100 * 841445 = 8414 considered unsuccessful
c [bca-16] limit of 10000000 steps and 1703464 added (scaled 2)
c [bca-16] 80507 out of 93900 literals actually usable 86%
c [bca-16] added 1069 blocked clauses in 339920 steps
c [sweep-10] limit 4793195 penalty 3 = 3 + 0
c [sweep-10-1] 4054 pos 9.4% + 39271 neg 90.6% = 43325 sched 92.3% ret 3624
c [sweep-10-1] 4872967 steps 47 queries 5190.32 avg class size
c [sweep-10-1] 1520 decisions 45 SAT calls 241.40 avg env size
c [sweep-10-1] 42822 variables remain 91% (4127 retained 9%)
c [decomp-41] removed 3 variables
c [sweep-10-1] removed 3 vars (0 failed, 1 eqs, 5 impls)
c [sweep-10] 3 < 1/1000 * 46949 = 46 considered unsuccessful
c [sweep-10] removed 3 vars in TOTAL (1 rounds, 46 queries)
c [sort-queue-20] sorted 16850 enqueued variables after 2519702 conflicts
c [score-dist-20] active 30096 (64%), one 0 (0%), zero 16850 (36%)
c [score-dist-20] max exp 543, different 40 (7%)
c [score-dist-20] median active exp 527, avg 527.6
c [simplification-20] removed 23 variables 0.0% (46946 remain 44%)
c [simplification-20] removed 2167 irredundant clauses 0.3% (839282 remain 53%)
c [simplification-20] maximum reduction of 0% = max (0%, 0%)
c [simplification-20] full geometric conflict interval increment 792000
c [simplification-20] conflict interval soft limit 1000000 reached
c [simplification-20] new conflict interval 1000000
c [simplification-20] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-20] hard conflict limit 4019702 (soft 3519702 + delta 500000)
c [simplification-20] new conflict limit 3519702 (hard 4019702)
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 -  809.8   46946   839282   2825891   21315  31197 297913  220   239   60  92%   1024   -5  137  224   61%
c -  891.9   46946   839282   3180268   41015  31197 297913   74   244   69  30%   1024   12   76  168   45%
c -  964.6   46946   839282   3501806   39536  31197 297913   72   250   67  29%   1024   20   71  166   43%
c 
c [simplification-21] limit 3519702 conflicts (hard 4019702) hit after 3519703 conflicts
c [quatres-15] found 12561 quaternary clauses 19% in total
c [quatres-15-2] added 10 quaternary resolvents
c [ternres-16] limit 152333595 with penalty 0 = 0 + 0
c [ternres-16] all 46946 free variables schedulable
c [ternres-16] 60 ternary resolvents (0 bin, 60 trn)
c [ternres-16] fully completed ternary resolution
c [card-6] limit 4760424 penalty 4 = 4 + 0
c [card-6] found 86 at-most-one constraints of average size 3.6
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 4760424 for elimination
c [card-6] 86 out of 86 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [unhide-19] limit 5000000 with penalty 2 = 0 + 2
c [unhide-19-21] 60 units, 2 failed, 5439 tauts, 0 hbrs, 167271 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 35 transitive binary clauses
c [elim-15] 900 variables 2% will be scheduled this time
c [elim-15] scheduled 900 variables 2%
c [elim-15] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15] incomplete 45 not tried 0% in round 1
c [elim-15] transition to [ all 0 rem 1 ] state
c [elim-15] eliminated 1 = 0% variables out of 900 scheduled
c [elim-15] 1 < 1/100 * 900 = 9 considered unsuccessful
c [bca-17] limit of 10000000 steps and 1692634 added (scaled 2)
c [bca-17] 80834 out of 93770 literals actually usable 86%
c [bca-17] added 1205 blocked clauses in 325640 steps
c [sort-queue-21] sorted 16555 enqueued variables after 3519703 conflicts
c [score-dist-21] active 30329 (65%), one 0 (0%), zero 16555 (35%)
c [score-dist-21] max exp 544, different 41 (8%)
c [score-dist-21] median active exp 528, avg 528.2
c [simplification-21] removed 62 variables 0.1% (46884 remain 44%)
c [simplification-21] removed 5674 irredundant clauses 0.7% (833608 remain 52%)
c [simplification-21] maximum reduction of 1% = max (0%, 1%)
c [simplification-21] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-21] conflict interval soft limit 1000000 reached
c [simplification-21] new conflict interval 1000000
c [simplification-21] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-21] hard conflict limit 5019703 (soft 4519703 + delta 500000)
c [simplification-21] new conflict limit 4519703 (hard 5019703)
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 -  982.9   46884   833608   3552391   40941  31209 295596   75   256   65  29%   1024   13   73  116   63%
c -  991.7   46884   833608   3599833   40050  31209 295596   71   251   65  28%   1024    3   71   91   78%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 137 basic ate = 80 trn 58% + 57 lrg 42% in 3 updates
c bcas: 17 count, 51042 added (6941 skipped), 5751074 steps
c bkwd: tried 291570 clauses, 582742 lits, 2.00 lits/clause
c bkwd: checked 1337315118 occs, 4586.60 occs/clause, 2294.87 occs/lit
c bkwd: subsumed 0 binary, 84 ternary, 6 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 319 large (0% self)
c blkd: 9 bces, 255225 removed, 45387066 resolutions, 126100426 steps
c blkd: 18621 blocking literals 9%, 3350 pure
c bump: 3641555 bumped seen, 1727662705 lits 474.4 on average
c card: 6 count, 0 units, 0 am1, 94941842 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 760 subsumed
c card: 161 at-most-one constraints found, average size 3.55
c card: 161 at-most-one constraints used 100%, average size 3.55
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: 5 cces, 530 eliminated, 499 ate 94%, 31 abce 6%
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: 6215704 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 109 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 42 decompositions, 1674 equivalent 2%
c deco: 2214184 decision-only clauses 61%, 60% reduction
c decs: 41989377 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 43834 eliminated 41%, 1230 pure 3%
c elms: 18 rounds, 1.2 rounds/bve
c elms: 17241 small 39%, 22013 large 50%
c elms: 28455 tried small, 17241 succeeded 61%, 11214 failed 39%
c elms: 49139 subsumed, 271302 strengthened, 2060 blocked
c elms: 16666632 copies, 28039355 resolutions, 541075 ipos
c elms: 108836386 subchks, 150005052 strchks
c gaus: 5 extractions, 1 extracted, 2.0 size, 2 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10550152 steps, 5275076 extr 50%, 3 elim 0%
c glue: 184.1 orig avg, 184.1 real avg, 10.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 444598 = 390601 simple 88% + 53834 trn 12% + 163 lrg 0%, 2355 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3641554 clauses, 201.7 length
c lrnd: 734662435 lits = 1615609552 orig - 880947117 removed 55%
c lrnd: 863632 uips 24%, 2034610 flips 56%
c mins: 1403246 mins 39%, 54 bin 0%, 714 size 0%
c mins: 105798305 poisoned searches, 22663528 hits, 21% hit rate
c mins: 261898516 used twice searches, 73744550 hits, 28% hit rate
c move: moved 230170, 220097 bin 96%, 10073 trn 4%
c otfs: 3642 driving 32%, 7690 restarting 68%
c otfs: str 11332, 11260 red 99%, 72 irr 1%
c otfs: str 11332, 0 bin 0%, 10 trn 0%, 11322 lrg 100%
c otfs: sub 935, 908 red 97%, 27 irr 3%
c otfs: sub 935, 0 bin 0%, 0 trn 0%, 935 lrg 100%
c phas: 1 computed, 99852 set, 0 pos (0%), 99852 neg (100%)
c prbs: 5 basic, 14772 probed, 171 failed, 0 lifted
c prbs: 6 simple, 270563 probed, 1110 failed, 93 eqs
c prbs: 5 treelook, 20 probed, 1 failed, 0 lifted
c prom: 4846 locked 0% out of 2723102 tried
c prps: 1771583268 props, 41 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 15 count, 2404 quat, 206 self1, 0 self2, 26 dup
c queu: 21 sorted, 41989377 next (672697 steps 0.02)
c queu: 1728495663 enq (2434540113 steps 1.41), 1727662705 deq 100%
c redc: 435 clauses 43%, 1011 tried 0%, 26 sat 3%
c redc: 2624 lits 19%, 13652 tried 0%, 26 sat 0%
c redc: 87 times jump level reduced, 248.1 levels on average
c reds: 35 count, 104144.9 conflicts per reduce
c reds: 0 memlim 0%, 35 arith 100%
c reds: 1172540 collected 91%, 113959 retired 9%
c rmbd: 27479 removed, 26210 red 95%
c rsts: 9120 restarts 64%, 5138 skipped 36%
c rsts: 5138 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 21 count, 21 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 3641554 count (7079604 tried 1.9), 2263747 sub out of 3641215 (62.2%)
c swps: 10 count, 10 rounds, 312 queries (31.2/round)
c swps: 298 sat calls, 2 unsat (0.4% success rate)
c swps: 10301 decisions 34.6, 124 conflicts 0.4
c swps; 4923.2 avg class size, 195.5 avg environment size
c swps: 1 failed, 30 impls, 15 equivs
c swp0: 101 type 0 queries, 6 unsat (5.9%), 99 sat (98.0%)
c swp1: 211 type 1 queries, 50 unsat (23.7%), 198 sat (93.8%)
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: 91262267 calls to obtain time
c tops: 13621 fixed 13%, 0 its, 0.00 confs/it
c trds: 17 transitive reductions, 239 removed, 8 failed
c trds: 3187 nodes, 24785 edges, 33661299 steps
c trim: 30450734 words, 116.2 MB
c trnr: 16 count, 24 bin, 56235 trn, 226339953 steps
c unhd: 19 count, 21 rounds, 63737428 steps
c unhd: 2256 non-trivial sccs of average size 2.3
c unhd: 4076 units, 4076 bin, 0 trn, 0 lrg
c unhd: 90 failed, 85 stamp, 0 lits, 1 bin, 3 trn, 0 lrg
c unhd: 98001 tauts, 1027 bin 1%, 8847 trn 9%, 9566 lrg 10%
c unhd: 98001 tauts, 78561 stamp 80%, 39329 red 40%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 2060829 str, 4076 bin 0%, 7281 trn 0%, 2049472 lrg 99%, 1922398 red 93%
c vars: 46884 remaining 44% and 59129 removed 56% out of 106013
c vars: 13621 fixed 13%, 43834 eliminated 41%, 1674 equivalent 2%
c vsts: 16082022429 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 9.1 search visits per propagation, 4350.6 per conflict
c wchs: 1932747783 pushed, 79347632 enlarged, 172 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3643619       1172540        113959      63019896      41401210       2016950
c 
c  0 0          2935   0        26   0         0   0   1478753   2    303475   1      1939   0     0.1
c  1 5           219   0        28   0       143   0    941306   1    226459   1      1716   0     0.0
c  2 6          2051   0       282   0      1376   1   8499943  13   2577826   6     31002   2     0.1
c  3 9          9361   0      2227   0      5903   5  12609537  20   6688725  16     99694   5     0.6
c  4 14        10666   0      3608   0      5167   5   7521471  12   5237188  13    344513  17     0.4
c  5 21        18675   1      8381   1      7918   7   2572413   4   1922664   5    188545   9     1.3
c  6 30        57393   2     36450   3     13308  12   2101334   3<  1439089   3     37069   2     4.0
c  7 41       300008   8    263670  22     21729  19   2861464   5   2471497   6<   152461   8    13.7
c  8 54       337410   9    256706  22<    11984  11<  2749149   4   2185604   5     64854   3<   13.8
c  9 69       399142  11    332151  28     14069  12   3448834   5   2409846   6    160209   8    21.9
c 10 86       223056   6<   202224  17      6214   5   7619464  12   6787469  16    367437  18    18.7
c 11 126     1039121  29     51710   4      5043   4   9123199  14   7877408  19    507252  25   237.9
c 12 230     1017112  28     14676   1     20782  18   1256806   2   1072700   3     60247   3   512.0
c 13 534      226470   6       401   0       323   0    236223   0    201260   0        12   0   149.3
c 
c avg                 10.4           8.5           8.0           6.0           7.0           7.9
c std                  1.9           1.4           2.7           3.6           3.4           3.0
c 
c  330.287  33% bump
c   83.159   8% elim
c   27.477   3% decide
c   19.326   2% probe
c   18.966   2% unhide
c   18.663   2% block
c    4.738   0% bca
c    4.541   0% sweep
c 
c   10.116 < 1% rest (below)
c 
c    3.487   0% quatres
c    3.277   0% cce
c    1.171   0% gauss
c    1.153   0% ternres
c    0.820   0% transred
c    0.209   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.109   1% preprocessing     3%
c  164.501  16% inprocessing     97%
c ==================================
c  169.610  17% simplifying
c  829.502  83% search
c ==================================
c  999.116 100% all
c 
c       3645073 conflicts,        3648.3 confs/sec
c           159 ternaries,       22925.0 confs/ternary
c           107 binaries,        34066.1 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            35 reductions,          0.0 redus/sec, 104144.9 confs/reduction
c          9120 restarts,            9.1 rests/sec,    399.7 confs/restart
c      41989377 decisions,       42026.5 decis/sec,     11.5 decis/conflict
c    1771583268 propagations,  1773151.3 props/sec,     42.2 props/decision
c 
c 999.1 seconds, 1350.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
