c launch: /data/cnf/sc2014/app/atco_enc3_opt2_18_44.cnf.bz2
c host: atom20
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/atco_enc3_opt2_18_44.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc3_opt2_18_44.cnf.bz2
c no embedded options
c found 'p cnf 1322728 5284664' header
c read 1322728 variables, 5284664 clauses, 13187506 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 1322320 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 1322320  5284254         0       0      0     0    0     0  259   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1321063 based on 5284254 irredundant clauses
c [card-1] found 327 at-most-one constraints of average size 4.1
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1321063 for elimination
c [card-1] 327 out of 327 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 240824 variables
c [simpleprobe-1] all 1081904 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 8651080 based on 4325540 irredundant clauses
c [decomp-2] removed 27 variables
c [simpleprobe-1] 1081877 variables remain 100% (0 retained 0%)
c [simpleprobe-1] removed 27 variables, found 16 hbrs, 0 units
c [unhide-1] limit 270340 based on 4325451 irredundant clauses
c [unhide-1-1] 5 units, 267 failed, 4536 tauts, 0 hbrs, 744 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1080139 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 1053886 not tried 98% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 26245 = 2% variables out of 1080139 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 4280359 negative 99.9% of 4283481 except 3122 0.1%
c [phase-count-1] 4264664 positive 99.6% of 4283481 except 18817 0.4%
c [phase-count-1] less non-negative clauses 3122 than limit 428300 (10.0%)
c [phase-count-1] non-pos/non-neg = 18817/3122 = 6.03 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 1053894 negative 100%
c [sort-queue-1] sorted 1053894 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1053894 (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 28664 variables 2.6% (1053894 remain 80%)
c [simplification-1] removed 1000773 irredundant clauses 18.9% (4283481 remain 81%)
c [simplification-1] maximum reduction of 19% = max (3%, 19%)
c [simplification-1] large reduction 19% >= 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  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   28.2 1053893  4283481       913     650    164    71    1    40  310   3%      5   40    6    0 6895%
c i   28.5 1053688  4283481       953     659    191    74    1    40  310   3%      5   40    5    0 6199%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 563 variables
c [simpleprobe-2] all 1053331 free variables schedulable
c [simpleprobe-2] limit 8561804 based on 4280902 irredundant clauses
c [decomp-4] removed 77 variables
c [simpleprobe-2] 1053254 variables remain 100% (0 retained 0%)
c [simpleprobe-2] removed 77 variables, found 57 hbrs, 0 units
c [treelook-1] limit 1070148 based on 4280595 irredundant clauses
c [treelook-1] scheduled 193821 literals 9%
c [treelook-1] scheduling used 1203520 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1070148 based on 4280595 irredundant clauses
c [treelook-1] used 1416646 steps
c [treelook-1] 193561 literals remain 9%
c [treelook-1] 193342 variables remain to probed next time 18%
c [decomp-5] removed 133 variables
c [treelook-1] removed 259 variables, found 1002 hbrs
c [basicprobe-1] limit 34236152 based on 4279519 irredundant clauses
c [basicprobe-1-0] 889 probes remain 0% after last round
c [basicprobe-1-0] 61 units = 60 failed (98%) + 1 lifted (2%)
c [basicprobe-1-0] removed 695 variables, found 39352 hbrs
c [unhide-2] limit 267469 based on 4279519 irredundant clauses
c [unhide-2-2] 0 units, 583 failed, 21142 tauts, 0 hbrs, 1231 literals
c [elim-2] 1051086 variables 100% will be scheduled this time
c [elim-2] scheduled 1051086 variables 100%
c [elim-2] limit of 24292286 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 950259 not tried 90% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 100820 = 10% variables out of 1051086 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 4239051 negative 99.9% of 4242215 except 3164 0.1%
c [phase-count-2] 4220976 positive 99.5% of 4242215 except 21239 0.5%
c [phase-count-2] less non-negative clauses 3164 than limit 424200 (10.0%)
c [phase-count-2] non-pos/non-neg = 21239/3164 = 6.71 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 88128 negative 100%
c [sort-queue-2] sorted 943773 enqueued variables after 1000 conflicts
c [score-dist-2] active 6501 (1%), one 0 (0%), zero 943773 (99%)
c [score-dist-2] max exp 759, different 234 (31%)
c [score-dist-2] median active exp 676, avg 659.6
c [simplification-2] removed 103273 variables 9.8% (950274 remain 72%)
c [simplification-2] removed 41266 irredundant clauses 1.0% (4242215 remain 80%)
c [simplification-2] maximum reduction of 10% = max (10%, 1%)
c [simplification-2] large reduction 10% >= 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 3000 conflicts
c [card-2] limit 1060553 based on 4242215 irredundant clauses
c [card-2] found 283 at-most-one constraints of average size 3.4
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1060553 for elimination
c [card-2] 283 out of 283 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 245 variables
c [treelook-2] limit 1060410 based on 4241641 irredundant clauses
c [treelook-2] scheduled 162853 literals 9%
c [treelook-2] scheduling used 1072725 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1060410 based on 4241641 irredundant clauses
c [treelook-2] used 1319207 steps
c [treelook-2] 162764 literals remain 9%
c [treelook-2] 41762 variables remain to probed next time 4%
c [decomp-7] removed 10 variables
c [treelook-2] removed 96 variables, found 288 hbrs
c [unhide-3] limit 265068 based on 4241090 irredundant clauses
c [unhide-3-3] 1 units, 112 failed, 25792 tauts, 0 hbrs, 1305 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 949242 variables 100%
c [elim-3] limit of 56974476 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 720037 not tried 76% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 228772 = 24% variables out of 949242 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 4186033 negative 99.9% of 4189380 except 3347 0.1%
c [phase-count-3] 4169862 positive 99.5% of 4189380 except 19518 0.5%
c [phase-count-3] less non-negative clauses 3347 than limit 418900 (10.0%)
c [phase-count-3] non-pos/non-neg = 19518/3347 = 5.83 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 47953 negative 100%
c [sort-queue-3] sorted 705624 enqueued variables after 3000 conflicts
c [score-dist-3] active 14846 (2%), one 0 (0%), zero 705624 (98%)
c [score-dist-3] max exp 778, different 670 (86%)
c [score-dist-3] median active exp 548, avg 486.0
c [simplification-3] removed 229804 variables 24.2% (720470 remain 54%)
c [simplification-3] removed 52835 irredundant clauses 1.2% (4189380 remain 79%)
c [simplification-3] maximum reduction of 24% = max (24%, 1%)
c [simplification-3] large reduction 24% >= 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 15000 (soft 5000 + delta 10000)
c [simplification-3] new conflict limit 5000 (hard 15000)
c 
c [simplification-4] limit 5000 conflicts (hard 15000) hit after 5000 conflicts
c [decomp-8] removed 62 variables
c [basicprobe-2] limit 33513968 based on 4189246 irredundant clauses
c [basicprobe-2-0] 315 probes remain 0% after last round
c [basicprobe-2-0] 914 units = 124 failed (14%) + 790 lifted (86%)
c [basicprobe-2-0] removed 1341 variables, found 10563 hbrs
c [unhide-4] limit 261827 based on 4189246 irredundant clauses
c [unhide-4-4] 1 units, 228 failed, 3928 tauts, 0 hbrs, 3095 literals
c [elim-4] 716671 variables 100% will be scheduled this time
c [elim-4] scheduled 716671 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 2000724695 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 1256 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 92070 = 13% variables out of 716671 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 4085094 negative 99.9% of 4089611 except 4517 0.1%
c [phase-count-4] 4069610 positive 99.5% of 4089611 except 20001 0.5%
c [phase-count-4] less non-negative clauses 4517 than limit 408900 (10.0%)
c [phase-count-4] non-pos/non-neg = 20001/4517 = 4.43 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 13169 negative 100%
c [sort-queue-4] sorted 614054 enqueued variables after 5000 conflicts
c [score-dist-4] active 10982 (2%), one 2996 (0%), zero 611058 (98%)
c [score-dist-4] max exp 793, different 652 (82%)
c [score-dist-4] median active exp 397, avg 425.7
c [simplification-4] removed 95434 variables 13.2% (625036 remain 47%)
c [simplification-4] removed 99769 irredundant clauses 2.4% (4089611 remain 77%)
c [simplification-4] maximum reduction of 13% = max (13%, 2%)
c [simplification-4] large reduction 13% >= 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 17000 (soft 7000 + delta 10000)
c [simplification-4] new conflict limit 7000 (hard 17000)
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  192.7  625035  4089611      5964    2371    713 10694    5   140  319   3%     60  133    6    0 1223%
c 
c [simplification-5] limit 7000 conflicts (hard 17000) hit after 7000 conflicts
c [quatres-1] found 748232 quaternary clauses 99% in total
c [quatres-1-1] removed 7 duplicate quaternary clauses
c [quatres-1-2] added 30 single-self-subsuming ternary resolvents
c [quatres-1-2] added 68 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 34946145 with penalty 2 = 0 + 2
c [ternres-1] all 624870 free variables schedulable
c [ternres-1] 3330 ternary resolvents (0 bin, 3330 trn)
c [ternres-1] 592561 variables remain 95% (32309 retained 5%)
c [gauss-1] limit 2044805 based on 4089611 irredundant clauses
c [gauss-1] extracted 74 xors of average arity 2.1
c [gauss-1] connected 155 occurrences of 143 variables (average 1.1)
c [gauss-1] limit 2044234 based on 4088469 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 546 variables
c [simpleprobe-3] all 624324 free variables schedulable
c [simpleprobe-3] limit 27956916 penalty 2 = 0 + 2
c [decomp-10] removed 41 variables
c [simpleprobe-3] 624283 variables remain 100% (0 retained 0%)
c [simpleprobe-3] removed 41 variables, found 1662 hbrs, 1 units
c [unhide-5] limit 349461 with penalty 4 = 0 + 4
c [unhide-5-5] 1 units, 88 failed, 23246 tauts, 0 hbrs, 34901 literals
c [transred-1] limit 4061504 based on 4061504 irredundant clauses
c [transred-1] removed 6 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 622547 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 698922912 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 667 blocked clauses
c [block-1] 667 < 1/100 * 4061498 = 40614 considered unsuccessful
c [cce-1] limit of 34946145 steps penalty 2 = 0 + 2
c [cce-1-1] eliminated 17 clauses out of 110 (15%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 17 large clauses in 34946152 steps
c [cce-1-1] allowing another 17473076 steps for small clauses
c [cce-1-1] scheduling 1862586 clauses = 1301214 binary + 561372 ternary
c [cce-1-1] tried to eliminate 133 small clauses 0%
c [cce-1-1] eliminated 5 binary clauses 0%
c [cce-1-1] eliminated 1 ternary clauses 0%
c [cce-1-1] eliminated 6 small clauses 0%
c [cce-1-1] eliminated 6 small clauses in 34946145 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 23 covered clauses in round 1
c [cce-1] eliminated 23 covered clauses in TOTAL during 1 rounds
c [cce-1] 23 < 1/100 * 4050302 = 40503 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 622547 variables 100%
c [elim-5] limit of 139784582 steps penalty 2 = 0 + 2
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 169400 not tried 27% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 16352 = 3% variables out of 622547 scheduled
c [bca-1] limit of 10000000 steps and 8059314 added (scaled 2)
c [bca-1] 1208175 out of 1212392 literals actually usable 100%
c [bca-1] added 0 blocked clauses in 2419836 steps
c [sweep-1] limit 8058814 based on 4029407 irredundant clauses
c [sweep-1-1] 379375 pos 62.6% + 226820 neg 37.4% = 606195 sched 100.0% ret 0
c [sweep-1-1] 8147603 steps 37 queries 124281.03 avg class size
c [sweep-1-1] 285 decisions 20 SAT calls 117.60 avg env size
c [sweep-1-1] 606157 variables remain 100% (38 retained 0%)
c [decomp-11] removed 43 variables
c [sweep-1-1] removed 43 vars (0 failed, 16 eqs, 20 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 43 vars in TOTAL (1 rounds, 36 queries)
c [phase-count-5] 4026082 negative 99.9% of 4029328 except 3246 0.1%
c [phase-count-5] 4011588 positive 99.6% of 4029328 except 17740 0.4%
c [phase-count-5] less non-negative clauses 3246 than limit 402900 (10.0%)
c [phase-count-5] non-pos/non-neg = 17740/3246 = 5.47 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 257 negative 100%
c [sort-queue-5] sorted 594895 enqueued variables after 7000 conflicts
c [score-dist-5] active 11257 (2%), one 6175 (1%), zero 588720 (97%)
c [score-dist-5] max exp 813, different 604 (74%)
c [score-dist-5] median active exp 573, avg 559.0
c [simplification-5] removed 18718 variables 3.0% (606152 remain 46%)
c [simplification-5] removed 60283 irredundant clauses 1.5% (4029328 remain 76%)
c [simplification-5] maximum reduction of 3% = max (3%, 1%)
c [simplification-5] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-5] new conflict interval 5000
c [simplification-5] penalized conflict interval 5000 = 1 * 5000
c [simplification-5] hard conflict limit 22000 (soft 12000 + delta 10000)
c [simplification-5] new conflict limit 12000 (hard 22000)
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  310.1  606151  4029328     10672    6153   3644 11478    7   160  316   4%     54  143    7    1  736%
c i  310.6  605059  4029328     10720    6178   3664 11480    7   159  316   4%     51  141    7    1  650%
c 
c [simplification-6] limit 12000 conflicts (hard 22000) hit after 12000 conflicts
c [quatres-2] found 709316 quaternary clauses 99% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-2] added 185 single-self-subsuming ternary resolvents
c [quatres-2-2] added 264 quaternary resolvents
c [ternres-2] limit 16117268 based on 4029317 irredundant clauses
c [ternres-2] 573564 schedulable variables 95%
c [ternres-2] 3449 ternary resolvents (2 bin, 3447 trn)
c [ternres-2] 556855 variables remain 92% (48004 retained 8%)
c [card-3] limit 1443256 penalty 4 = 2 + 2
c [card-3] found 248 at-most-one constraints of average size 3.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1443256 for elimination
c [card-3] 248 out of 248 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 1337 variables
c [treelook-3] limit 1154605 penalty 2 = 0 + 2 boost 1
c [treelook-3] scheduled 122809 literals 10%
c [treelook-3] scheduling used 1197047 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1154605 penalty 2 = 0 + 2 boost 1
c [treelook-3] used 1172309 steps
c [treelook-3] 122776 literals remain 10%
c [treelook-3] 23027 variables remain to probed next time 4%
c [decomp-13] removed 8 variables
c [treelook-3] removed 33 variables, found 375 hbrs
c [unhide-6] limit 577302 with penalty 4 = 0 + 4
c [unhide-6-6] 4 units, 120 failed, 1506 tauts, 0 hbrs, 24114 literals
c [transred-2] limit 4016339 based on 4016339 irredundant clauses
c [transred-2] removed 3 transitive binary clauses
c [elim-6] 1217 variables 0% will be scheduled this time
c [elim-6] scheduled 1217 variables 0%
c [elim-6] limit of 200000000 steps penalty 2 = 0 + 2
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 1024 not tried 0% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 1 = 0% variables out of 1217 scheduled
c [elim-6] 1 < 1/100 * 1217 = 12 considered unsuccessful
c [sweep-2] limit 8000886 based on 4000443 irredundant clauses
c [sweep-2-1] 365073 pos 60.6% + 237328 neg 39.4% = 602401 sched 100.0% ret 19
c [sweep-2-1] 8188721 steps 32 queries 139135.75 avg class size
c [sweep-2-1] 316 decisions 27 SAT calls 108.48 avg env size
c [sweep-2-1] 602271 variables remain 100% (149 retained 0%)
c [decomp-14] removed 294 variables
c [sweep-2-1] removed 294 vars (0 failed, 4 eqs, 8 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 294 vars in TOTAL (1 rounds, 31 queries)
c [phase-count-6] 3996363 negative 99.9% of 3999704 except 3341 0.1%
c [phase-count-6] 3982229 positive 99.6% of 3999704 except 17475 0.4%
c [phase-count-6] less non-negative clauses 3341 than limit 399900 (10.0%)
c [phase-count-6] non-pos/non-neg = 17475/3341 = 5.23 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 124 negative 100%
c [sort-queue-6] sorted 586975 enqueued variables after 12000 conflicts
c [score-dist-6] active 15151 (3%), one 13547 (2%), zero 573428 (95%)
c [score-dist-6] max exp 621, different 552 (89%)
c [score-dist-6] median active exp 423, avg 385.5
c [simplification-6] removed 2733 variables 0.5% (602126 remain 46%)
c [simplification-6] removed 29624 irredundant clauses 0.7% (3999704 remain 76%)
c [simplification-6] maximum reduction of 1% = max (0%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 15000
c [simplification-6] penalized conflict interval 15000 = 1 * 15000
c [simplification-6] hard conflict limit 37000 (soft 27000 + delta 10000)
c [simplification-6] new conflict limit 27000 (hard 37000)
c 
c [simplification-7] limit of 402 binary hit after 402 binaries
c [quatres-3] found 683373 quaternary clauses 99% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-2] added 16 single-self-subsuming ternary resolvents
c [quatres-3-2] added 16 quaternary resolvents
c [ternres-3] limit 15998796 based on 3999699 irredundant clauses
c [ternres-3] 554345 schedulable variables 92%
c [ternres-3] 5146 ternary resolvents (63 bin, 5083 trn)
c [ternres-3] 539936 variables remain 90% (62190 retained 10%)
c [gauss-2] limit 1999849 based on 3999699 irredundant clauses
c [gauss-2] extracted 6 xors of average arity 2.0
c [gauss-2] connected 12 occurrences of 8 variables (average 1.5)
c [gauss-2] limit 1999849 based on 3999699 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 41 variables
c [basicprobe-3] limit 73453222 penalty 2 = 0 + 2
c [basicprobe-3-0] 590 sched 0%, 245 failed, 8 lifted, 4978 hbrs
c [decomp-16] removed 2464 variables
c [basicprobe-3-1] 518 probes remain 0% after last round
c [basicprobe-3-1] 566 units = 496 failed (88%) + 70 lifted (12%)
c [basicprobe-3-1] removed 4216 variables, found 11716 hbrs
c [bate-1] eliminated 1448 asymmetric tautologies during probing
c [unhide-7] limit 734532 with penalty 4 = 0 + 4
c [unhide-7-7] 4 units, 281 failed, 19988 tauts, 0 hbrs, 11647 literals
c [transred-3] limit 3950647 based on 3950647 irredundant clauses
c [transred-3] removed 8 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 596568 variables 100%
c [block-2] limit of 73453222 steps penalty 3 = 1 + 2
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 153 blocked clauses
c [block-2] 153 < 1/100 * 3950639 = 39506 considered unsuccessful
c [cce-2] limit of 36726611 steps penalty 3 = 1 + 2
c [cce-2-1] eliminated 1 clauses out of 398 (0%) of length 8
c [cce-2-1] eliminated 5 clauses out of 83 (6%) of length 7
c [cce-2-1] eliminated 30 clauses out of 124 (24%) of length 6
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 36 large clauses in 36726619 steps
c [cce-2-1] allowing another 18363309 steps for small clauses
c [cce-2-1] scheduling 1828722 clauses = 1257123 binary + 571599 ternary
c [cce-2-1] tried to eliminate 148 small clauses 0%
c [cce-2-1] eliminated 3 binary clauses 0%
c [cce-2-1] eliminated 7 ternary clauses 0%
c [cce-2-1] eliminated 10 small clauses 0%
c [cce-2-1] eliminated 10 small clauses in 36726615 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 46 covered clauses in round 1
c [cce-2] eliminated 46 covered clauses in TOTAL during 1 rounds
c [cce-2] 46 < 1/100 * 3942581 = 39425 considered unsuccessful
c [bca-2] limit of 10000000 steps and 7885570 added (scaled 2)
c [bca-2] 1180770 out of 1193138 literals actually usable 99%
c [bca-2] added 1 blocked clauses in 2372641 steps
c [sweep-3] limit 7885070 based on 3942535 irredundant clauses
c [sweep-3-1] 336523 pos 56.4% + 259903 neg 43.6% = 596426 sched 100.0% ret 142
c [sweep-3-1] 7907165 steps 25 queries 157865.52 avg class size
c [sweep-3-1] 399 decisions 22 SAT calls 154.50 avg env size
c [sweep-3-1] 596355 variables remain 100% (213 retained 0%)
c [decomp-17] removed 282 variables
c [sweep-3-1] removed 282 vars (0 failed, 2 eqs, 4 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 282 vars in TOTAL (1 rounds, 24 queries)
c [phase-count-7] 3938821 negative 99.9% of 3941942 except 3121 0.1%
c [phase-count-7] 3925699 positive 99.6% of 3941942 except 16243 0.4%
c [phase-count-7] less non-negative clauses 3121 than limit 394100 (10.0%)
c [phase-count-7] non-pos/non-neg = 16243/3121 = 5.20 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 124 negative 100%
c [sort-queue-7] sorted 574878 enqueued variables after 16529 conflicts
c [score-dist-7] active 21408 (4%), one 19356 (3%), zero 555522 (93%)
c [score-dist-7] max exp 809, different 759 (94%)
c [score-dist-7] median active exp 459, avg 437.5
c [simplification-7] removed 5840 variables 1.0% (596286 remain 45%)
c [simplification-7] removed 57762 irredundant clauses 1.4% (3941942 remain 75%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] forced so keeping old conflict interval 15000
c [simplification-7] conflict limit remains at 27000 (hard 37000)
c [simplification-7] new binary interval 1000
c 
c [simplification-8] limit of 4126 ternary hit after 4126 ternaries
c [quatres-4] found 664524 quaternary clauses 99% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 26 single-self-subsuming ternary resolvents
c [quatres-4-2] added 15 quaternary resolvents
c [ternres-4] limit 22824129 with penalty 2 = 0 + 2
c [ternres-4] 534737 schedulable variables 90%
c [ternres-4] 5423 ternary resolvents (10 bin, 5413 trn)
c [ternres-4] 513382 variables remain 86% (82904 retained 14%)
c [decomp-18] removed 63 variables
c [simpleprobe-4] all 596223 free variables schedulable
c [simpleprobe-4] limit 50000000 penalty 2 = 0 + 2
c [decomp-19] removed 75 variables
c [simpleprobe-4] 495291 variables remain 83% (100857 retained 17%)
c [simpleprobe-4] removed 75 variables, found 1546 hbrs, 24 units
c [unhide-8] limit 1141206 with penalty 4 = 0 + 4
c [unhide-8-8] 3 units, 120 failed, 4182 tauts, 0 hbrs, 31911 literals
c [transred-4] limit 3937976 based on 3937976 irredundant clauses
c [transred-4] removed 9 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 592842 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 1 + 2
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 245374 not tried 41% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 8521 = 1% variables out of 592842 scheduled
c [bca-3] limit of 10000000 steps and 7816510 added (scaled 2)
c [bca-3] 1151635 out of 1168644 literals actually usable 99%
c [bca-3] added 2 blocked clauses in 2322043 steps
c [sweep-4] limit 7816010 based on 3908005 irredundant clauses
c [sweep-4-1] 347699 pos 59.5% + 236425 neg 40.5% = 584124 sched 100.0% ret 197
c [sweep-4-1] 7911224 steps 25 queries 156262.20 avg class size
c [sweep-4-1] 206 decisions 21 SAT calls 104.57 avg env size
c [sweep-4-1] 584054 variables remain 100% (267 retained 0%)
c [decomp-20] removed 60 variables
c [sweep-4-1] removed 60 vars (0 failed, 3 eqs, 6 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 60 vars in TOTAL (1 rounds, 24 queries)
c [phase-count-8] 3904477 negative 99.9% of 3907820 except 3343 0.1%
c [phase-count-8] 3891377 positive 99.6% of 3907820 except 16443 0.4%
c [phase-count-8] less non-negative clauses 3343 than limit 390700 (10.0%)
c [phase-count-8] non-pos/non-neg = 16443/3343 = 4.92 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 44 negative 100%
c [sort-queue-8] sorted 566715 enqueued variables after 25952 conflicts
c [score-dist-8] active 17546 (3%), one 34810 (6%), zero 531905 (91%)
c [score-dist-8] max exp 768, different 623 (81%)
c [score-dist-8] median active exp 587, avg 529.9
c [simplification-8] removed 12025 variables 2.0% (584261 remain 44%)
c [simplification-8] removed 34122 irredundant clauses 0.9% (3907820 remain 74%)
c [simplification-8] maximum reduction of 2% = max (2%, 1%)
c [simplification-8] forced so keeping old conflict interval 15000
c [simplification-8] conflict limit remains at 27000 (hard 37000)
c [simplification-8] new ternary interval 10000
c 
c [simplification-9] limit 27000 conflicts (hard 37000) hit after 27001 conflicts
c [quatres-5] found 637812 quaternary clauses 99% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 134 single-self-subsuming ternary resolvents
c [quatres-5-2] added 78 quaternary resolvents
c [ternres-5] limit 23673450 with penalty 2 = 0 + 2
c [ternres-5] 503056 schedulable variables 86%
c [ternres-5] 7071 ternary resolvents (45 bin, 7026 trn)
c [ternres-5] 482322 variables remain 83% (101939 retained 17%)
c [decomp-21] removed 7 variables
c [treelook-4] limit 2367345 penalty 2 = 0 + 2 boost 1
c [treelook-4] scheduled 200168 literals 17%
c [treelook-4] scheduling used 2440152 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 2367345 penalty 2 = 0 + 2 boost 1
c [treelook-4] used 2368019 steps
c [treelook-4] 197138 literals remain 17%
c [treelook-4] 20404 variables remain to probed next time 3%
c [decomp-22] removed 32 variables
c [treelook-4] removed 1301 variables, found 1152 hbrs
c [unhide-9] limit 1183672 with penalty 4 = 0 + 4
c [unhide-9-9] 0 units, 53 failed, 14205 tauts, 0 hbrs, 11816 literals
c [transred-5] limit 3886522 based on 3886522 irredundant clauses
c [transred-5] removed 7 transitive binary clauses
c [elim-8] 1009 variables 0% will be scheduled this time
c [elim-8] scheduled 1009 variables 0%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 0 + 2
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 1203004936 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 2 = 0% variables out of 1009 scheduled
c [elim-8] 2 < 1/100 * 1009 = 10 considered unsuccessful
c [bca-4] limit of 10000000 steps and 7746415 added (scaled 2)
c [bca-4] 1146140 out of 1163732 literals actually usable 98%
c [bca-4] added 0 blocked clauses in 2311871 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 71020350 penalty 2 = 0 + 2
c [sweep-5-1] 352489 pos 60.6% + 229114 neg 39.4% = 581603 sched 100.0% ret 262
c [sweep-5-1] 71106333 steps 233 queries 27171.49 avg class size
c [sweep-5-1] 3085 decisions 186 SAT calls 109.77 avg env size
c [sweep-5-1] 579029 variables remain 100% (2511 retained 0%)
c [decomp-23] removed 660 variables
c [sweep-5-1] removed 660 vars (0 failed, 50 eqs, 69 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 660 vars in TOTAL (1 rounds, 232 queries)
c [phase-count-9] 3866708 negative 99.9% of 3870013 except 3305 0.1%
c [phase-count-9] 3854279 positive 99.6% of 3870013 except 15734 0.4%
c [phase-count-9] less non-negative clauses 3305 than limit 387000 (10.0%)
c [phase-count-9] non-pos/non-neg = 15734/3305 = 4.76 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 24 negative 100%
c [sort-queue-9] sorted 562671 enqueued variables after 27001 conflicts
c [score-dist-9] active 18534 (3%), one 36194 (6%), zero 526477 (91%)
c [score-dist-9] max exp 586, different 552 (94%)
c [score-dist-9] median active exp 344, avg 328.7
c [simplification-9] removed 3056 variables 0.5% (581205 remain 44%)
c [simplification-9] removed 37807 irredundant clauses 1.0% (3870013 remain 73%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-9] new conflict interval 25000
c [simplification-9] penalized conflict interval 25000 = 1 * 25000
c [simplification-9] hard conflict limit 64501 (soft 52001 + delta 12500)
c [simplification-9] new conflict limit 52001 (hard 64501)
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  726.1  581204  3870013     35742   26713  26422 16760    8   162  311   5%    310  100    9    3  284%
c i  808.1  580456  3870013     42161   32280  26989 16855    9   161  312   5%     17   90    8    4  226%
c i  810.9  579456  3870013     42401   32497  27007 16857    9   161  312   5%      0   90    8    4  227%
c 
c [simplification-10] limit 52001 conflicts (hard 64501) hit after 52001 conflicts
c [quatres-6] found 618495 quaternary clauses 98% in total
c [quatres-6-1] removed 2 duplicate quaternary clauses
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 56 single-self-subsuming ternary resolvents
c [quatres-6-2] added 32 quaternary resolvents
c [ternres-6] limit 45425036 with penalty 2 = 0 + 2
c [ternres-6] 477492 schedulable variables 82%
c [ternres-6] 14728 ternary resolvents (15 bin, 14713 trn)
c [ternres-6] 436021 variables remain 75% (142366 retained 25%)
c [card-4] limit 2839064 penalty 5 = 3 + 2
c [card-4] found 367 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2839064 for elimination
c [card-4] 367 out of 367 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 2271251 penalty 4 = 2 + 2
c [gauss-3] extracted 18 xors of average arity 2.0
c [gauss-3] connected 36 occurrences of 34 variables (average 1.1)
c [gauss-3] limit 2271251 penalty 4 = 2 + 2
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-24] removed 132 variables
c [basicprobe-4] limit 100000000 penalty 2 = 0 + 2
c [basicprobe-4-0] 889 sched 0%, 323 failed, 31 lifted, 6286 hbrs
c [decomp-25] removed 3472 variables
c [basicprobe-4-1] 105 probes remain 0% after last round
c [basicprobe-4-1] 717 units = 666 failed (93%) + 51 lifted (7%)
c [basicprobe-4-1] removed 7206 variables, found 14496 hbrs
c [bate-2] eliminated 635 asymmetric tautologies during probing
c [unhide-10] limit 1250000 with penalty 4 = 0 + 4
c [unhide-10-10] 13 units, 1174 failed, 6213 tauts, 0 hbrs, 54501 literals
c [transred-6] limit 3794339 based on 3794339 irredundant clauses
c [transred-6] removed 10 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 567559 variables 100%
c [block-3] limit of 50000000 steps penalty 4 = 2 + 2
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 124 blocked clauses
c [block-3] 124 < 1/100 * 3794331 = 37943 considered unsuccessful
c [cce-3] limit of 56781295 steps penalty 4 = 2 + 2
c [cce-3-1] eliminated 1 clauses out of 397 (0%) of length 8
c [cce-3-1] eliminated 3 clauses out of 78 (4%) of length 7
c [cce-3-1] eliminated 15 clauses out of 116 (13%) of length 6
c [cce-3-1] eliminated 593 clauses out of 1410 (42%) of length 5
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 612 large clauses in 56781297 steps
c [cce-3-1] allowing another 28390648 steps for small clauses
c [cce-3-1] scheduling 2626363 clauses = 1204027 binary + 1422336 ternary
c [cce-3-1] tried to eliminate 263 small clauses 0%
c [cce-3-1] eliminated 21 binary clauses 0%
c [cce-3-1] eliminated 10 ternary clauses 0%
c [cce-3-1] eliminated 31 small clauses 0%
c [cce-3-1] eliminated 31 small clauses in 56781300 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 643 covered clauses in round 1
c [cce-3] eliminated 643 covered clauses in TOTAL during 1 rounds
c [cce-3] 643 < 1/100 * 3772904 = 37729 considered unsuccessful
c [sweep-6] limit 13627511 penalty 2 = 0 + 2
c [sweep-6-1] 350843 pos 62.0% + 214585 neg 38.0% = 565428 sched 99.6% ret 2130
c [sweep-6-1] 13895995 steps 42 queries 124243.67 avg class size
c [sweep-6-1] 576 decisions 34 SAT calls 109.62 avg env size
c [sweep-6-1] 565245 variables remain 100% (2313 retained 0%)
c [decomp-26] removed 377 variables
c [sweep-6-1] removed 377 vars (0 failed, 7 eqs, 10 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 377 vars in TOTAL (1 rounds, 41 queries)
c [phase-count-10] 3768120 negative 99.9% of 3771544 except 3424 0.1%
c [phase-count-10] 3755994 positive 99.6% of 3771544 except 15550 0.4%
c [phase-count-10] less non-negative clauses 3424 than limit 377100 (10.0%)
c [phase-count-10] non-pos/non-neg = 15550/3424 = 4.54 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 19 negative 100%
c [sort-queue-10] sorted 548695 enqueued variables after 52001 conflicts
c [score-dist-10] active 18486 (3%), one 53091 (9%), zero 495604 (87%)
c [score-dist-10] max exp 615, different 553 (90%)
c [score-dist-10] median active exp 413, avg 379.4
c [simplification-10] removed 11206 variables 1.9% (567181 remain 43%)
c [simplification-10] removed 98469 irredundant clauses 2.5% (3771544 remain 71%)
c [simplification-10] maximum reduction of 3% = max (2%, 3%)
c [simplification-10] geometric conflict interval increment 6250 = 25000 / 4
c [simplification-10] new conflict interval 31250
c [simplification-10] penalized conflict interval 31250 = 1 * 31250
c [simplification-10] hard conflict limit 98876 (soft 83251 + delta 15625)
c [simplification-10] new conflict limit 83251 (hard 98876)
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  988.3  567180  3771544     53652   42319  41618 18948    9   153  311   6%     90   68   10    5  216%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2083 basic ate = 1254 trn 60% + 829 lrg 40% in 2 updates
c bcas: 4 count, 3 added (111 skipped), 9426391 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 3 bces, 944 removed, 37123943 resolutions, 108009792 steps
c blkd: 762 blocking literals 0%, 1 pure
c bump: 54096 bumped seen, 2092658 lits 38.7 on average
c card: 4 count, 0 units, 0 am1, 13963086 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 10912 subsumed
c card: 1225 at-most-one constraints found, average size 3.50
c card: 1225 at-most-one constraints used 100%, average size 3.50
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 3 cces, 712 eliminated, 698 ate 98%, 14 abce 2%
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: 18472170 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 61 gcs, 0 rescored clauses, 28 rescored vars
c dcps: 26 decompositions, 3900 equivalent 0%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1465264 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 472756 eliminated 36%, 1 pure 0%
c elms: 8 rounds, 1.0 rounds/bve
c elms: 472629 small 100%, 125 large 0%
c elms: 1829127 tried small, 472629 succeeded 26%, 1356498 failed 74%
c elms: 45196 subsumed, 13322 strengthened, 0 blocked
c elms: 41882510 copies, 32255945 resolutions, 108856157 ipos
c elms: 48190300 subchks, 12284013 strchks
c gaus: 3 extractions, 98 extracted, 2.1 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12632046 steps, 6316023 extr 50%, 320 elim 0%
c glue: 8.0 orig avg, 8.0 real avg, 1.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 86026 = 3281 simple 4% + 82167 trn 96% + 578 lrg 1%, 7959 sub 9%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 54096 clauses, 14.7 length
c lrnd: 795427 lits = 901018 orig - 105591 removed 12%
c lrnd: 29395 uips 54%, 16440 flips 30%
c mins: 45273 mins 84%, 698 bin 1%, 8125 size 15%
c mins: 1193381 poisoned searches, 147165 hits, 12% hit rate
c mins: 1866267 used twice searches, 232820 hits, 12% hit rate
c move: moved 13173, 180 bin 1%, 12993 trn 99%
c otfs: 561 driving 54%, 482 restarting 46%
c otfs: str 1043, 878 red 84%, 165 irr 16%
c otfs: str 1043, 0 bin 0%, 120 trn 12%, 923 lrg 88%
c otfs: sub 2, 2 red 100%, 0 irr 0%
c otfs: sub 2, 0 bin 0%, 0 trn 0%, 2 lrg 100%
c phas: 10 computed, 1203736 set, 0 pos (0%), 1203736 neg (100%)
c prbs: 4 basic, 10212 probed, 1346 failed, 912 lifted
c prbs: 4 simple, 1634545 probed, 25 failed, 61 eqs
c prbs: 4 treelook, 597 probed, 20 failed, 0 lifted
c prom: 0 locked 0% out of 15891 tried
c prps: 2459326929 props, 1662 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 6 count, 473 quat, 447 self1, 2 self2, 69 dup
c queu: 10 sorted, 1465264 next (334406 steps 0.23)
c queu: 10773109 enq (10739936 steps 1.00), 2092658 deq 19%
c redc: 3384 clauses 18%, 18981 tried 35%, 17 sat 0%
c redc: 4710 lits 3%, 146974 tried 16%, 17 sat 0%
c redc: 403 times jump level reduced, 13.1 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 17430 removed, 1016 red 6%
c rsts: 5135 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: 10 count, 8 confs 80%, 0 vars 0%
c simp: 0 its 0%, 1 bin 10%, 1 trns 10%
c subl: 54096 count (15203 tried 0.3), 1072 sub out of 46534 (2.3%)
c swps: 6 count, 6 rounds, 388 queries (64.7/round)
c swps: 310 sat calls, 6 unsat (1.0% success rate)
c swps: 4867 decisions 15.7, 302 conflicts 1.0
c swps; 73332.8 avg class size, 113.0 avg environment size
c swps: 0 failed, 117 impls, 82 equivs
c swp0: 128 type 0 queries, 23 unsat (18.0%), 123 sat (96.1%)
c swp1: 260 type 1 queries, 231 unsat (88.8%), 183 sat (70.4%)
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: 3038959 calls to obtain time
c tops: 278932 fixed 21%, 9 its, 6039.44 confs/it
c trds: 6 transitive reductions, 43 removed, 0 failed
c trds: 2940 nodes, 3086 edges, 23689917 steps
c trim: 7224 words, 0.0 MB
c trnr: 6 count, 135 bin, 39012 trn, 158984826 steps
c unhd: 10 count, 10 rounds, 203468220 steps
c unhd: 268 non-trivial sccs of average size 3.1
c unhd: 32 units, 26 bin, 1 trn, 5 lrg
c unhd: 3026 failed, 2820 stamp, 0 lits, 4 bin, 179 trn, 5 lrg
c unhd: 124738 tauts, 370 bin 0%, 23388 trn 19%, 1241 lrg 1%
c unhd: 124738 tauts, 99739 stamp 80%, 48899 red 39%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 175265 str, 26 bin 0%, 12827 trn 7%, 162412 lrg 93%, 16036 red 9%
c vars: 567140 remaining 43% and 755588 removed 57% out of 1322728
c vars: 278932 fixed 21%, 472756 eliminated 36%, 3900 equivalent 0%
c vsts: 19239745928 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 7.8 search visits per propagation, 349377.2 per conflict
c wchs: 1046952667 pushed, 184972532 enlarged, 97 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          47007             0             0       1628807        104183         13938
c 
c  0 0         13103  28         0   0<        0   0<  1261841  77<    48615  47      4850  35     0.3
c  1 5          3621   8         0   0         0   0    125013   8     10055  10<     1375  10<    0.1
c  2 6         10933  23<        0   0         0   0    162493  10     26062  25      4766  34     0.6
c  3 9         10660  23         0   0         0   0     65391   4     14677  14      2581  19     0.8
c  4 14         5756  12         0   0         0   0     10408   1      3480   3       279   2     0.6
c  5 21         2158   5         0   0         0   0      2745   0       993   1        64   0     0.3
c  6 30          634   1         0   0         0   0       745   0       247   0        20   0     0.1
c  7 41          123   0         0   0         0   0       143   0        44   0         2   0     0.0
c  8 54           18   0         0   0         0   0        27   0        10   0         1   0     0.0
c  9 69            1   0         0   0         0   0         1   0         0   0         0   0     0.0
c 
c avg                  2.0           0.0           0.0           0.4           1.2           1.5
c std                  1.6           0.0           0.0           0.9           1.3           1.2
c 
c  118.585  12% elim
c   34.361   3% probe
c   27.946   3% quatres
c   18.996   2% unhide
c   18.958   2% sweep
c   10.694   1% block
c    9.493   1% cce
c    6.241   1% bca
c 
c   12.418 < 1% rest (below)
c 
c    5.061   1% gauss
c    2.703   0% transred
c    1.704   0% ternres
c    1.096   0% card
c    0.873   0% decide
c    0.767   0% rescore
c    0.213   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c   11.288   1% preprocessing     4%
c  280.565  28% inprocessing     96%
c ==================================
c  291.853  29% simplifying
c  704.957  71% search
c ==================================
c  996.833 100% all
c 
c         54355 conflicts,          54.5 confs/sec
c          6447 ternaries,           8.4 confs/ternary
c           875 binaries,           62.1 confs/binary
c             9 iterations,       6039.4 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          5135 restarts,            5.2 rests/sec,     10.6 confs/restart
c       1465264 decisions,        1469.9 decis/sec,     27.0 decis/conflict
c    2459326929 propagations,  2467139.7 props/sec,   1678.4 props/decision
c 
c 996.8 seconds, 455.9 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
