c launch: /data/cnf/sc2014/app/partial-10-17-s.cnf.bz2
c host: atom29
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/partial-10-17-s.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/partial-10-17-s.cnf.bz2
c no embedded options
c found 'p cnf 298900 1409628' header
c read 298900 variables, 1409628 clauses, 3261218 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=4
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 287740 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] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
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  287740  1385857         0       0      0     0    0     0   64   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 11220 at-most-one constraints of average size 5.2
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 11220 out of 11220 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 129705 variables
c [simpleprobe-1] all 169195 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 1390 variables
c [simpleprobe-1] 7799 variables remain 5% (160006 retained 95%)
c [simpleprobe-1] removed 1390 variables, found 18529 hbrs, 9 units
c [unhide-1] limit 60588 based on 969417 irredundant clauses
c [unhide-1-1] 1 units, 196 failed, 8012 tauts, 0 hbrs, 9081 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 167330 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 60911 not tried 36% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 62796 = 38% variables out of 167330 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 733852 negative 99.2% of 739575 except 5723 0.8%
c [phase-count-1] 592701 positive 80.1% of 739575 except 146874 19.9%
c [phase-count-1] less non-negative clauses 5723 than limit 73900 (10.0%)
c [phase-count-1] non-pos/non-neg = 146874/5723 = 25.66 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 104534 negative 100%
c [sort-queue-1] sorted 104534 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 104534 (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 136559 variables 56.6% (104534 remain 36%)
c [simplification-1] removed 646282 irredundant clauses 46.6% (739575 remain 53%)
c [simplification-1] maximum reduction of 57% = max (57%, 47%)
c [simplification-1] large reduction 57% >= 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    5.0  104533   739575       165     138     17 10791    1    12   56   9%      0   12   12    0 18818%
c i    5.3  104431   739575       327     260     42 10799    1    24   56   5%      0   24   10    0 11893%
c i    5.3  104356   739575       329     261     42 10799    1    24   56   5%      0   24   10    0 11810%
c i    5.3  104129   739575       333     264     42 10799    1    24   56   5%      0   24   10    0 11666%
c i    5.4  103914   739575       349     273     44 10803    1    26   56   5%      0   25    9    0 11191%
c i    5.5  103141   739575       395     310     44 10808    1    28   56   5%      0   28    9    0 10273%
c i    5.5  101670   739575       399     313     44 10808    1    28   56   5%      0   28    9    0 10224%
c i    5.5  101350   739575       413     315     44 10808    1    28   56   5%      0   28    9    0 10307%
c i    6.1  101304   739575       663     526     57 10823    3    50   56   5%      1   50   19    0 11368%
c i    7.1  100975   739575       990     812     69 10838   16   132   57  12%      1  131  150    1 14271%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 5065 variables
c [simpleprobe-2] 7481 schedulable variables 8%
c [simpleprobe-2] limit 2304004 penalty 0 = 0 + 0
c [simpleprobe-2] 8710 variables remain 9% (90759 retained 91%)
c [simpleprobe-2] removed 0 variables, found 2154 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 71987 literals 36%
c [treelook-1] scheduling used 503018 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 354010 steps
c [treelook-1] 71855 literals remain 36%
c [treelook-1] 71387 variables remain to probed next time 72%
c [decomp-5] removed 1 variables
c [treelook-1] removed 129 variables, found 1673 hbrs
c [basicprobe-1] limit 5645544 based on 705693 irredundant clauses
c [basicprobe-1-0] 34123 probes remain 35% after last round
c [basicprobe-1-0] 25 units = 25 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 2803 variables, found 17948 hbrs
c [unhide-2] limit 115200 with penalty 0 = 0 + 0
c [unhide-2-2] 1 units, 282 failed, 4454 tauts, 0 hbrs, 16372 literals
c [elim-2] 57650 variables 60% will be scheduled this time
c [elim-2] scheduled 57650 variables 60%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 19123 not tried 20% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 452 = 1% variables out of 57650 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 656919 negative 99.1% of 662642 except 5723 0.9%
c [phase-count-2] 530867 positive 80.1% of 662642 except 131775 19.9%
c [phase-count-2] less non-negative clauses 5723 than limit 66200 (10.0%)
c [phase-count-2] non-pos/non-neg = 131775/5723 = 23.03 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 3075 negative 100%
c [sort-queue-2] sorted 69524 enqueued variables after 990 conflicts
c [score-dist-2] active 26010 (27%), one 0 (0%), zero 69524 (73%)
c [score-dist-2] max exp 508, different 11 (2%)
c [score-dist-2] median active exp 502, avg 502.7
c [simplification-2] removed 4059 variables 4.1% (95534 remain 33%)
c [simplification-2] removed 76933 irredundant clauses 10.4% (662642 remain 48%)
c [simplification-2] maximum reduction of 10% = max (4%, 10%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1009 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c [simplification-3] limit 1009 conflicts (hard 11000) hit after 1009 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4060 at-most-one constraints of average size 4.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4060 out of 4060 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 145 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 47058 literals 25%
c [treelook-2] scheduling used 302359 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 303110 steps
c [treelook-2] 47042 literals remain 25%
c [treelook-2] 42461 variables remain to probed next time 45%
c [treelook-2] removed 7 variables, found 1381 hbrs
c [unhide-3] limit 117631 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 131 failed, 11030 tauts, 0 hbrs, 1940 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 95138 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 25674 not tried 27% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2809 = 3% variables out of 95138 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 640069 negative 99.1% of 645702 except 5633 0.9%
c [phase-count-3] 517476 positive 80.1% of 645702 except 128226 19.9%
c [phase-count-3] less non-negative clauses 5633 than limit 64500 (10.0%)
c [phase-count-3] non-pos/non-neg = 128226/5633 = 22.76 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 3048 negative 100%
c [sort-queue-3] sorted 67170 enqueued variables after 1009 conflicts
c [score-dist-3] active 25159 (27%), one 0 (0%), zero 67170 (73%)
c [score-dist-3] max exp 508, different 11 (2%)
c [score-dist-3] median active exp 502, avg 502.7
c [simplification-3] removed 3205 variables 3.4% (92329 remain 32%)
c [simplification-3] removed 16940 irredundant clauses 2.6% (645702 remain 47%)
c [simplification-3] maximum reduction of 3% = max (3%, 3%)
c [simplification-3] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-3] new conflict interval 5000
c [simplification-3] penalized conflict interval 5000 = 1 * 5000
c [simplification-3] hard conflict limit 16009 (soft 6009 + delta 10000)
c [simplification-3] new conflict limit 6009 (hard 16009)
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   13.2   92328   645702      1215     669     66 21840   26   211   52  12%      1  210  191    2 10865%
c i   14.3   92195   645702      1624    1056     72 21847   49   360   53  14%      2  357  245    3 7257%
c i   14.3   92135   645702      1641    1066     72 21847   49   360   53  14%      2  357  242    3 7072%
c i   15.6   92134   645702      2076    1442     79 21858   98   474   55  21%      3  468  577    7 8439%
c i   15.8   92127   645702      2131    1481     79 21858  106   483   55  22%      2  477  610    7 8166%
c i   17.2   92126   645702      2631    1910     96 21874  138   581   58  24%      3  571  474   10 4595%
c i   17.7   92028   645702      2771    2022    101 21876  168   621   59  27%      3  610  698   12 5605%
c i   18.8   91994   645702      3131    2267    105 21881  251   718   60  35%      3  703 1042   19 5560%
c i   18.9   91993   645702      3134    2269    105 21881  251   719   60  35%      3  704 1031   19 5503%
c i   18.9   91992   645702      3143    2276    105 21881  253   720   60  35%      3  705 1035   19 5479%
c i   22.1   91991   645702      4176    3092    125 21903  438   979   70  45%      7  951 1015   36 2859%
c i   22.1   91990   645702      4190    3103    125 21903  439   981   70  45%      7  953 1008   36 2823%
c i   22.1   91989   645702      4192    3104    125 21903  439   981   70  45%      7  953 1006   36 2817%
c i   22.9   91949   645702      4456    3311    126 21911  460  1023   70  45%      6  991  882   39 2282%
c i   23.0   91948   645702      4458    3312    126 21911  461  1023   70  45%      6  991  881   39 2278%
c i   23.0   91947   645702      4460    3313    126 21911  461  1023   70  45%      6  991  880   39 2275%
c i   23.4   91946   645702      4558    3373    126 21911  482  1038   70  46%      5 1004 1037   41 2549%
c i   23.4   91945   645702      4560    3374    126 21911  482  1038   70  46%      5 1004 1035   41 2544%
c i   27.3   91944   645702      5777    3985    130 21924  662  1175   88  56%      9 1121 1126   62 1825%
c 
c [simplification-4] limit 6033 conflicts (hard 16009) hit after 6033 conflicts
c [decomp-8] removed 402 variables
c [basicprobe-2] limit 18012197 penalty 0 = 0 + 0
c [basicprobe-2-0] 29333 probes remain 33% after last round
c [basicprobe-2-0] 91 units = 91 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 4180 variables, found 46343 hbrs
c [unhide-4] limit 360243 with penalty 1 = 0 + 1
c [unhide-4-4] 0 units, 205 failed, 5419 tauts, 0 hbrs, 218755 literals
c [elim-4] 18898 variables 22% will be scheduled this time
c [elim-4] scheduled 18898 variables 22%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1440975800 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 34755987 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 18898 scheduled
c [phase-count-4] 604957 negative 99.1% of 610590 except 5633 0.9%
c [phase-count-4] 491032 positive 80.4% of 610590 except 119558 19.6%
c [phase-count-4] less non-negative clauses 5633 than limit 61000 (10.0%)
c [phase-count-4] non-pos/non-neg = 119558/5633 = 21.22 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1390 negative 100%
c [sort-queue-4] sorted 47737 enqueued variables after 6033 conflicts
c [score-dist-4] active 39676 (45%), one 0 (0%), zero 47737 (55%)
c [score-dist-4] max exp 510, different 33 (6%)
c [score-dist-4] median active exp 497, avg 495.9
c [simplification-4] removed 4525 variables 4.9% (87413 remain 30%)
c [simplification-4] removed 35112 irredundant clauses 5.4% (610590 remain 44%)
c [simplification-4] maximum reduction of 5% = max (5%, 5%)
c [simplification-4] large reduction 5% >= 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 18033 (soft 8033 + delta 10000)
c [simplification-4] new conflict limit 8033 (hard 18033)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   32.2   87412   610590      6122    4213    118 56950  692  1204   78  57%      7 1144 1037   67 1553%
c i   33.7   87411   610590      6658    4508    123 56950  755  1238   79  61%      6 1169 1179   76 1553%
c i   37.3   87410   610590      7834    5205    135 56966  854  1307   79  65%      9 1217 1198   95 1262%
c 
c [simplification-5] limit 8033 conflicts (hard 18033) hit after 8034 conflicts
c [quatres-1] found 37270 quaternary clauses 38% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 23454720 with penalty 0 = 0 + 0
c [ternres-1] all 87410 free variables schedulable
c [ternres-1] 74 ternary resolvents (0 bin, 74 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 53 xors of average arity 2.3
c [gauss-1] connected 121 occurrences of 85 variables (average 1.4)
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 70 variables
c [unhide-5] limit 234547 with penalty 2 = 0 + 2
c [unhide-5-5] 0 units, 74 failed, 8238 tauts, 0 hbrs, 98976 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 135 transitive binary clauses
c [transred-1] found 1 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 87156 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 11122 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 4 clauses out of 66 (6%) of length 10
c [cce-1-1] eliminated 936 clauses out of 2572 (36%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 940 large clauses in 30000000 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 401921 clauses = 282508 binary + 119413 ternary
c [cce-1-1] tried to eliminate 386 small clauses 0%
c [cce-1-1] eliminated 103 binary clauses 0%
c [cce-1-1] eliminated 14 ternary clauses 0%
c [cce-1-1] eliminated 117 small clauses 0%
c [cce-1-1] eliminated 117 small clauses in 30000008 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1057 covered clauses in round 1
c [cce-1] eliminated 1057 covered clauses in TOTAL during 1 rounds
c [cce-1] 1057 < 1/100 * 590641 = 5906 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1179668 added (scaled 2)
c [bca-1] 156197 out of 174314 literals actually usable 90%
c [bca-1] added 221 blocked clauses in 453665 steps
c [sweep-1] limit 1407283 penalty 0 = 0 + 0
c [sweep-1-1] 4421 pos 5.1% + 82735 neg 94.9% = 87156 sched 100.0% ret 0
c [sweep-1-1] 1727567 steps 18 queries 16562.89 avg class size
c [sweep-1-1] 93 decisions 11 SAT calls 90.18 avg env size
c [sweep-1-1] 87075 variables remain 100% (81 retained 0%)
c [decomp-10] removed 5 variables
c [sweep-1-1] removed 5 vars (0 failed, 6 eqs, 10 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 5 vars in TOTAL (1 rounds, 17 queries)
c [phase-count-5] 583967 negative 99.0% of 589580 except 5613 1.0%
c [phase-count-5] 481782 positive 81.7% of 589580 except 107798 18.3%
c [phase-count-5] less non-negative clauses 5613 than limit 58900 (10.0%)
c [phase-count-5] non-pos/non-neg = 107798/5613 = 19.21 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 1379 negative 100%
c [sort-queue-5] sorted 46576 enqueued variables after 8034 conflicts
c [score-dist-5] active 40575 (47%), one 0 (0%), zero 46576 (53%)
c [score-dist-5] max exp 510, different 41 (8%)
c [score-dist-5] median active exp 493, avg 492.2
c [simplification-5] removed 259 variables 0.3% (87151 remain 30%)
c [simplification-5] removed 21010 irredundant clauses 3.4% (589580 remain 43%)
c [simplification-5] maximum reduction of 3% = max (0%, 3%)
c [simplification-5] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-5] new conflict interval 10000
c [simplification-5] penalized conflict interval 10000 = 1 * 10000
c [simplification-5] hard conflict limit 28034 (soft 18034 + delta 10000)
c [simplification-5] new conflict limit 18034 (hard 28034)
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   43.7   87150   589580      8137    5392    244 70036  866  1323   90  65%      7 1228 1101   99 1112%
c i   44.0   87137   589580      8238    5440    244 70039  874  1327   90  66%      6 1230 1137  101 1128%
c i   44.3   87128   589580      8315    5472    245 70039  879  1331   90  66%      6 1232 1133  102 1111%
c i   45.5   87118   589580      8675    5631    246 70043  908  1343   90  68%      5 1237 1212  108 1122%
c i   48.0   86979   589580      9451    6002    249 70046  954  1368   90  70%      6 1248 1107  121  919%
c i   49.6   86968   589580     10012    6434    253 70052  954  1434   90  67%      5 1303  984  128  772%
c i   49.6   86967   589580     10019    6440    253 70052  954  1435   90  66%      5 1304  978  128  766%
c i   53.0   86966   589580     10948    7150    257 70059  992  1524   90  65%      6 1374 1139  142  803%
c i   53.2   86965   589580     10994    7176    257 70060  994  1525  100  65%      6 1374 1143  143  802%
c i   58.3   86964   589580     12444    7938    261 70068 1049  1541  124  68%     11 1360 1112  165  674%
c i   58.4   86963   589580     12476    7967    261 70068 1048  1542  124  68%     11 1361 1087  165  657%
c i   58.5   86962   589580     12478    7968    261 70068 1048  1542  124  68%     11 1360 1085  165  656%
c i   65.7   86961   589580     14549    9135    275 70092 1100  1582  127  70%     19 1358 1345  196  685%
c i   67.6   86960   589580     15172    9589    285 70105 1118  1664  147  67%     12 1427 1220  206  592%
c i   67.7   86886   589580     15184    9596    285 70106 1119  1665  147  67%     12 1427 1238  206  600%
c i   67.7   86876   589580     15190    9600    285 70107 1119  1665  147  67%     12 1427 1234  206  598%
c i   68.7   86875   589580     15461    9774    287 70119 1146  1696  147  68%      9 1453 1479  212  698%
c 
c [simplification-6] limit of 258 binary hit after 258 binaries
c [ternres-2] limit 9360269 with penalty 0 = 0 + 0
c [ternres-2] all 86875 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 20265 variables remain 23% (66610 retained 77%)
c [card-3] limit 1170033 penalty 2 = 2 + 0
c [card-3] found 4361 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1170033 for elimination
c [card-3] 4361 out of 4361 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 577 variables
c [simpleprobe-3] 8325 schedulable variables 10%
c [simpleprobe-3] limit 18720538 penalty 1 = 1 + 0
c [decomp-12] removed 173 variables
c [simpleprobe-3] 3439 variables remain 4% (82962 retained 96%)
c [simpleprobe-3] removed 173 variables, found 23918 hbrs, 62 units
c [unhide-6] limit 468013 with penalty 2 = 0 + 2
c [unhide-6-6] 0 units, 98 failed, 5485 tauts, 0 hbrs, 461692 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 214 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 86219 variables 100%
c [block-2] limit of 93602692 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 735 blocked clauses
c [block-2] 735 < 1/100 * 585665 = 5856 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 86219 variables 100%
c [elim-5] limit of 93602692 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 1531 variables 2% in round 1 in 54761770 steps
c [elim-5-1] backward subsumption/strengthening limit 38840922
c [elim-5-1-1] backward checking 6116 touched variables 7%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 170 clauses in 1926937 steps
c [elim-5-1] rescheduled 368 variables 0% by backward subsumption
c [elim-5-2] eliminated 53 variables 0% in round 2 in 464667 steps
c [elim-5-2] backward subsumption/strengthening limit 464600
c [elim-5-2-1] backward checking 372 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 298308 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 1588 = 2% variables out of 86219 scheduled
c [bca-2] limit of 10000000 steps and 1160476 added (scaled 2)
c [bca-2] 153008 out of 169264 literals actually usable 90%
c [bca-2] added 200 blocked clauses in 445893 steps
c [sweep-2] limit 2808080 penalty 0 = 0 + 0
c [sweep-2-1] 4380 pos 5.2% + 80186 neg 94.8% = 84566 sched 99.9% ret 65
c [sweep-2-1] 2853005 steps 30 queries 10482.43 avg class size
c [sweep-2-1] 233 decisions 26 SAT calls 61.88 avg env size
c [sweep-2-1] 83616 variables remain 99% (980 retained 1%)
c [decomp-13] removed 40 variables
c [sweep-2-1] removed 40 vars (0 failed, 4 eqs, 9 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 40 vars in TOTAL (1 rounds, 29 queries)
c [phase-count-6] 574166 negative 99.1% of 579651 except 5485 0.9%
c [phase-count-6] 472651 positive 81.5% of 579651 except 107000 18.5%
c [phase-count-6] less non-negative clauses 5485 than limit 57900 (10.0%)
c [phase-count-6] non-pos/non-neg = 107000/5485 = 19.51 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 1067 negative 100%
c [sort-queue-6] sorted 42830 enqueued variables after 15868 conflicts
c [score-dist-6] active 41761 (49%), one 0 (0%), zero 42830 (51%)
c [score-dist-6] max exp 510, different 71 (14%)
c [score-dist-6] median active exp 497, avg 485.6
c [simplification-6] removed 2284 variables 2.6% (84591 remain 29%)
c [simplification-6] removed 9929 irredundant clauses 1.7% (579651 remain 42%)
c [simplification-6] maximum reduction of 3% = max (3%, 2%)
c [simplification-6] forced so keeping old conflict interval 10000
c [simplification-6] conflict limit remains at 18041 (hard 28034)
c [simplification-6] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   79.1   84590   579651     16027    2990    279 85619 1188  1770   57  67%      7 1514 1374  223  617%
c i   82.0   84589   579651     17051    3899    287 85639 1178  1897   65  62%      7 1616 1100  237  464%
c i   83.9   84588   579651     17690    4497    290 85647 1153  2009   67  57%      6 1713 1005  244  411%
c i   84.4   84575   579651     17836    4625    294 85652 1163  2027   75  57%      5 1726 1193  247  483%
c i   84.5   84571   579651     17883    4660    294 85652 1172  2031   75  58%      5 1730 1314  248  530%
c i   84.6   84559   579651     17908    4673    296 85652 1175  2034   76  58%      4 1732 1357  249  546%
c i   84.7   84558   579651     17942    4705    296 85652 1175  2037   76  58%      4 1734 1336  249  536%
c 
c [simplification-7] limit 18041 conflicts (hard 28034) hit after 18041 conflicts
c [quatres-2] found 37626 quaternary clauses 39% in total
c [gauss-2] limit 1061369 penalty 1 = 1 + 0
c [gauss-2] extracted 10 xors of average arity 3.0
c [gauss-2] connected 30 occurrences of 30 variables (average 1.0)
c [gauss-2] limit 1061369 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 3 variables
c [treelook-3] limit 1061369 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 116363 literals 69%
c [treelook-3] scheduling used 1061780 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1061369 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 1153897 steps
c [treelook-3] 116348 literals remain 69%
c [treelook-3] 35451 variables remain to probed next time 42%
c [treelook-3] removed 2 variables, found 8239 hbrs
c [unhide-7] limit 1061369 with penalty 1 = 0 + 1
c [unhide-7-7] 1 units, 152 failed, 9183 tauts, 0 hbrs, 420819 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 162 transitive binary clauses
c [transred-3] found 1 units
c [cce-2] limit of 26534226 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 17 clauses out of 1533 (1%) of length 9
c [cce-2-1] eliminated 31 clauses out of 902 (3%) of length 8
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 48 large clauses in 26534228 steps
c [cce-2-1] allowing another 13267114 steps for small clauses
c [cce-2-1] scheduling 388159 clauses = 271422 binary + 116737 ternary
c [cce-2-1] tried to eliminate 281 small clauses 0%
c [cce-2-1] eliminated 52 binary clauses 0%
c [cce-2-1] eliminated 33 ternary clauses 0%
c [cce-2-1] eliminated 85 small clauses 0%
c [cce-2-1] eliminated 1296 small clauses in 26534241 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1344 covered clauses in round 1
c [cce-2] eliminated 1344 covered clauses in TOTAL during 1 rounds
c [cce-2] 1344 < 1/100 * 573905 = 5739 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 84410 variables 100%
c [elim-6] limit of 212273813 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 265 variables 0% in round 1 in 53566162 steps
c [elim-6-1] backward subsumption/strengthening limit 53566100
c [elim-6-1-1] backward checking 1702 touched variables 2%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 21 clauses in 512287 steps
c [elim-6-1] rescheduled 43 variables 0% by backward subsumption
c [elim-6-2] eliminated 7 variables 0% in round 2 in 64358 steps
c [elim-6-2] backward subsumption/strengthening limit 64300
c [elim-6-2-1] backward checking 48 touched variables 0%
c [elim-6-2-1] incomplete backward checking 0 remain 0%
c [elim-6-2] subsumed 0 and strengthened 0 clauses in 64301 steps
c [elim-6-2] fully rescheduled 84138 variables 100%
c [elim-6-3] eliminated 4 variables 0% in round 3 in 53477075 steps
c [elim-6-3] backward subsumption/strengthening limit 53477000
c [elim-6-3-1] backward checking 30 touched variables 0%
c [elim-6-3-1] fully completed backward checking in 1 rounds
c [elim-6-3] subsumed 0 and strengthened 0 clauses in 117023 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 276 = 0% variables out of 84410 scheduled
c [elim-6] 276 < 1/100 * 84410 = 844 considered unsuccessful
c [bca-3] limit of 10000000 steps and 1144360 added (scaled 2)
c [bca-3] 151442 out of 168270 literals actually usable 90%
c [bca-3] added 173 blocked clauses in 440327 steps
c [sweep-3] limit 3184107 penalty 0 = 0 + 0
c [sweep-3-1] 4147 pos 5.0% + 79038 neg 95.0% = 83185 sched 98.9% ret 949
c [sweep-3-1] 3301574 steps 17 queries 13884.94 avg class size
c [sweep-3-1] 192 decisions 11 SAT calls 53.00 avg env size
c [sweep-3-1] 83104 variables remain 99% (999 retained 1%)
c [decomp-16] removed 36 variables
c [sweep-3-1] removed 36 vars (0 failed, 5 eqs, 10 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 36 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-7] 566042 negative 99.0% of 571531 except 5489 1.0%
c [phase-count-7] 465969 positive 81.5% of 571531 except 105562 18.5%
c [phase-count-7] less non-negative clauses 5489 than limit 57100 (10.0%)
c [phase-count-7] non-pos/non-neg = 105562/5489 = 19.23 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 944 negative 100%
c [sort-queue-7] sorted 41101 enqueued variables after 18041 conflicts
c [score-dist-7] active 42997 (51%), one 0 (0%), zero 41101 (49%)
c [score-dist-7] max exp 509, different 79 (15%)
c [score-dist-7] median active exp 498, avg 486.3
c [simplification-7] removed 448 variables 0.5% (84098 remain 29%)
c [simplification-7] removed 8120 irredundant clauses 1.4% (571531 remain 41%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-7] new conflict interval 20000
c [simplification-7] penalized conflict interval 20000 = 1 * 20000
c [simplification-7] hard conflict limit 48041 (soft 38041 + delta 10000)
c [simplification-7] new conflict limit 38041 (hard 48041)
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   92.9   84097   571531     18205    3515    340 90024 1160  2072   58  56%      3 1762 1110  252  441%
c i   93.1   84096   571531     18255    3555    340 90026 1169  2079   58  56%      3 1768 1247  253  493%
c i   93.7   84095   571531     18405    3695    341 90027 1192  2100   60  57%      3 1785 1490  257  581%
c i   93.7   84094   571531     18407    3696    341 90027 1191  2100   60  57%      3 1785 1479  257  576%
c i   93.7   84093   571531     18409    3697    341 90027 1191  2099   60  57%      3 1784 1467  257  572%
c i   96.7   84092   571531     19238    4428    345 90052 1276  2171   72  59%      4 1834 1621  274  592%
c i   97.1   84085   571531     19332    4507    347 90060 1268  2170   72  58%      4 1829 1394  275  507%
c i   97.3   84084   571531     19415    4582    347 90062 1257  2171   72  58%      3 1828 1200  275  436%
c i  107.7   84081   571531     23040    7084    378 90104 1316  1976   93  67%     39 1540 1349  333  406%
c i  110.6   84080   571531     24026    7726    383 90115 1280  1925  123  66%     18 1468 1166  345  338%
c i  110.6   84079   571531     24045    7741    383 90118 1277  1924  123  66%     18 1466 1134  345  329%
c i  118.6   84078   571531     26763    9481    403 90151 1209  1832  126  66%     25 1317  643  378  170%
c i  119.6   83991   571531     27103    9786    407 90156 1184  1868  135  63%     18 1346  808  381  212%
c i  119.6   83990   571531     27104    9786    407 90156 1184  1867  135  63%     18 1345  805  381  211%
c i  119.6   83989   571531     27106    9787    407 90156 1183  1867  135  63%     18 1345  799  381  210%
c i  119.7   83988   571531     27112    9792    407 90156 1182  1867  135  63%     18 1345  794  381  208%
c i  119.7   83987   571531     27113    9792    407 90156 1182  1867  135  63%     18 1345  791  381  208%
c i  119.7   83986   571531     27116    9794    407 90156 1182  1867  135  63%     18 1345  792  381  208%
c i  119.7   83985   571531     27118    9795    407 90156 1181  1866  135  63%     18 1344  786  381  206%
c i  124.1   83984   571531     28450   10865    413 90170 1250  1945  135  64%     11 1395 1270  402  316%
c i  128.1   83983   571531     29830   11844    433 90185 1223  1936  136  63%      9 1357 1050  418  251%
c i  128.1   83982   571531     29835   11847    434 90185 1222  1935  136  63%      9 1356 1040  418  249%
c i  130.4   83969   571531     30589   12355    437 90190 1226  1922  195  64%      6 1328 1147  427  269%
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  133.2   83968   571531     31550   13108    438 90202 1200  1947  213  62%      5 1333 1312  437  301%
c i  133.5   83967   571531     31644   13174    439 90202 1211  1951  213  62%      4 1336 1430  438  326%
c i  134.3   83966   571531     31898   13339    439 90202 1232  1962  217  63%      3 1342 1518  443  343%
c i  134.3   83965   571531     31901   13339    439 90202 1232  1962  217  63%      3 1341 1517  443  343%
c i  135.6   83964   571531     32322   13576    440 90204 1263  1970  217  64%      2 1341 1523  450  339%
c i  144.3   83963   571531     35070   15321    445 90219 1375  2006  217  69%     24 1322 1530  492  311%
c i  146.2   83962   571531     35651   15689    447 90221 1393  2011  217  69%     13 1315 1440  501  287%
c i  148.1   83918   571531     36235   16031    449 90227 1382  1998  217  69%      8 1291 1290  508  254%
c i  148.7   83906   571531     36428   16148    451 90227 1366  1987  217  69%      6 1276 1151  510  226%
c i  149.4   83905   571531     36634   16246    451 90227 1361  1973  217  69%      4 1258 1223  512  239%
c 
c [simplification-8] limit 38090 conflicts (hard 48041) hit after 38091 conflicts
c [ternres-3] limit 10675759 with penalty 1 = 1 + 0
c [ternres-3] 19570 schedulable variables 23%
c [ternres-3] 38 ternary resolvents (0 bin, 38 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-17] removed 223 variables
c [basicprobe-3] limit 106757597 penalty 0 = 0 + 0
c [basicprobe-3-0] 23936 probes remain 30% after last round
c [basicprobe-3-0] 407 units = 406 failed (100%) + 1 lifted (0%)
c [basicprobe-3-0] removed 3257 variables, found 227445 hbrs
c [bate-1] eliminated 193 asymmetric tautologies during probing
c [unhide-8] limit 533787 with penalty 3 = 0 + 3
c [unhide-8-8] 3 units, 259 failed, 17098 tauts, 0 hbrs, 1697629 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 129 transitive binary clauses
c [transred-4] found 2 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 80291 variables 100%
c [block-3] limit of 106757597 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 21 blocked clauses
c [block-3] 21 < 1/100 * 551866 = 5518 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1098233 added (scaled 2)
c [bca-4] 138945 out of 160582 literals actually usable 87%
c [bca-4] added 60 blocked clauses in 397703 steps
c [sweep-4] limit 6405455 penalty 0 = 0 + 0
c [sweep-4-1] 4028 pos 5.1% + 75430 neg 94.9% = 79458 sched 99.0% ret 832
c [sweep-4-1] 6441373 steps 72 queries 6804.33 avg class size
c [sweep-4-1] 913 decisions 54 SAT calls 250.83 avg env size
c [sweep-4-1] 74373 variables remain 93% (5830 retained 7%)
c [decomp-18] removed 179 variables
c [sweep-4-1] removed 179 vars (0 failed, 19 eqs, 37 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 179 vars in TOTAL (1 rounds, 71 queries)
c [phase-count-8] 542367 negative 99.0% of 547856 except 5489 1.0%
c [phase-count-8] 446428 positive 81.5% of 547856 except 101428 18.5%
c [phase-count-8] less non-negative clauses 5489 than limit 54700 (10.0%)
c [phase-count-8] non-pos/non-neg = 101428/5489 = 18.48 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 669 negative 100%
c [sort-queue-8] sorted 34473 enqueued variables after 38091 conflicts
c [score-dist-8] active 45638 (57%), one 0 (0%), zero 34473 (43%)
c [score-dist-8] max exp 510, different 157 (31%)
c [score-dist-8] median active exp 481, avg 464.2
c [simplification-8] removed 3794 variables 4.5% (80111 remain 28%)
c [simplification-8] removed 23675 irredundant clauses 4.1% (547856 remain 40%)
c [simplification-8] maximum reduction of 5% = max (5%, 4%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 50091 (soft 40091 + delta 10000)
c [simplification-8] new conflict limit 40091 (hard 50091)
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  169.6   80110   547856     38211   17077    586 289805 1300  1877  212  69%      9 1133 1129  527  214%
c i  170.0   80109   547856     38345   17165    586 289805 1298  1870  213  69%      7 1124 1180  529  223%
c i  172.6   80108   547856     39289   17683    588 289815 1278  1836  214  70%      5 1075 1006  539  187%
c i  172.9   80107   547856     39385   17759    588 289815 1263  1833  214  69%      4 1071  894  539  166%
c i  173.5   80106   547856     39613   17925    589 289817 1254  1830  214  69%      3 1063 1006  541  186%
c 
c [simplification-9] limit 40091 conflicts (hard 50091) hit after 40091 conflicts
c [ternres-4] limit 22357619 with penalty 0 = 0 + 0
c [ternres-4] all 80106 free variables schedulable
c [ternres-4] 62 ternary resolvents (0 bin, 62 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-19] removed 5 variables
c [simpleprobe-4] 3350 schedulable variables 4%
c [simpleprobe-4] limit 89430478 penalty 0 = 0 + 0
c [decomp-20] removed 696 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 696 variables, found 43613 hbrs, 248 units
c [unhide-9] limit 558940 with penalty 3 = 0 + 3
c [unhide-9-9] 5 units, 42 failed, 10273 tauts, 0 hbrs, 882337 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 265 transitive binary clauses
c [transred-5] found 3 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 79315 variables 100%
c [elim-7] limit of 223576195 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 1721 variables 2% in round 1 in 49441748 steps
c [elim-7-1] backward subsumption/strengthening limit 49441700
c [elim-7-1-1] backward checking 6583 touched variables 8%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 53 clauses in 2321236 steps
c [elim-7-1] rescheduled 123 variables 0% by backward subsumption
c [elim-7-2] eliminated 16 variables 0% in round 2 in 128894 steps
c [elim-7-2] backward subsumption/strengthening limit 128800
c [elim-7-2-1] backward checking 103 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 0 and strengthened 2 clauses in 128801 steps
c [elim-7-2] rescheduled 5 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 2976 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1741 = 2% variables out of 79315 scheduled
c [bca-5] limit of 10000000 steps and 1060809 added (scaled 2)
c [bca-5] 138518 out of 155150 literals actually usable 89%
c [bca-5] added 86 blocked clauses in 391653 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 67072850 penalty 0 = 0 + 0
c [sweep-5-1] 4061 pos 5.6% + 68424 neg 94.4% = 72485 sched 93.4% ret 5089
c [sweep-5-1] 67107641 steps 906 queries 1049.77 avg class size
c [sweep-5-1] 8045 decisions 846 SAT calls 88.44 avg env size
c [sweep-5-1] 40549 variables remain 53% (36467 retained 47%)
c [decomp-21] removed 735 variables
c [sweep-5-1] removed 735 vars (1 failed, 67 eqs, 146 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 735 vars in TOTAL (1 rounds, 905 queries)
c [phase-count-9] 520753 negative 99.0% of 526169 except 5416 1.0%
c [phase-count-9] 427622 positive 81.3% of 526169 except 98547 18.7%
c [phase-count-9] less non-negative clauses 5416 than limit 52600 (10.0%)
c [phase-count-9] non-pos/non-neg = 98547/5416 = 18.20 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 484 negative 100%
c [sort-queue-9] sorted 30897 enqueued variables after 40091 conflicts
c [score-dist-9] active 45942 (60%), one 0 (0%), zero 30897 (40%)
c [score-dist-9] max exp 510, different 165 (32%)
c [score-dist-9] median active exp 499, avg 473.0
c [simplification-9] removed 3267 variables 4.1% (76839 remain 27%)
c [simplification-9] removed 21687 irredundant clauses 4.0% (526169 remain 38%)
c [simplification-9] maximum reduction of 4% = max (4%, 4%)
c [simplification-9] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-9] new conflict interval 24000
c [simplification-9] penalized conflict interval 24000 = 1 * 24000
c [simplification-9] hard conflict limit 76091 (soft 64091 + delta 12000)
c [simplification-9] new conflict limit 64091 (hard 76091)
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  190.3   76838   526169     40225    5140    674 361259 1199  1842   61  65%      1 1066  757  544  139%
c i  198.0   76837   526169     43138    7213    703 361299 1127  1771   78  64%     25  949  931  566  164%
c i  199.1   76836   526169     43539    7460    703 361301 1128  1756   86  64%     16  928 1156  570  203%
c i  203.3   76835   526169     45029    8272    712 361317 1129  1692   95  67%     10  843  995  582  171%
c i  203.7   76834   526169     45173    8343    712 361318 1131  1684   95  67%      8  834 1065  584  183%
c i  203.9   76833   526169     45232    8368    712 361318 1131  1680   95  67%      7  829 1078  584  185%
c i  206.1   76832   526169     45957    8664    713 361319 1137  1640   95  69%      4  780 1232  590  209%
c i  212.3   76831   526169     48154    9738    726 361330 1120  1563  115  72%     15  679 1084  607  179%
c i  214.6   76830   526169     48953   10058    734 361338 1122  1546  115  73%      7  654 1085  613  177%
c i  215.5   76822   526169     49264   10186    734 361340 1121  1538  118  73%      4  643 1085  615  176%
c i  215.8   76821   526169     49347   10220    734 361347 1122  1538  118  73%      4  642 1108  616  180%
c i  225.4   76820   526169     53738   11955    746 361377 1150  1461  155  79%     45  526  977  652  150%
c i  232.9   76811   526169     57504   13744    757 361399 1181  1509  175  78%     36  542 1000  682  147%
c 
c [simplification-10] limit 64091 conflicts (hard 76091) hit after 64091 conflicts
c [quatres-3] found 35234 quaternary clauses 42% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1 quaternary resolvents
c [ternres-5] limit 32259836 with penalty 0 = 0 + 0
c [ternres-5] all 76811 free variables schedulable
c [ternres-5] 94 ternary resolvents (0 bin, 94 trn)
c [ternres-5] fully completed ternary resolution
c [card-4] limit 2016239 penalty 3 = 3 + 0
c [card-4] found 3469 at-most-one constraints of average size 4.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2016239 for elimination
c [card-4] 3469 out of 3469 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1612991 penalty 2 = 2 + 0
c [gauss-3] extracted 23 xors of average arity 3.0
c [gauss-3] connected 68 occurrences of 64 variables (average 1.1)
c [gauss-3] limit 1612991 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 1 variables
c [treelook-4] limit 3225983 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 138457 literals 90%
c [treelook-4] scheduling used 2203537 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 3225983 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 3242198 steps
c [treelook-4] 138361 literals remain 90%
c [treelook-4] 31213 variables remain to probed next time 41%
c [decomp-23] removed 3 variables
c [treelook-4] removed 17 variables, found 7823 hbrs
c [unhide-10] limit 806495 with penalty 3 = 0 + 3
c [unhide-10-10] 7 units, 212 failed, 23918 tauts, 0 hbrs, 765938 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 183 transitive binary clauses
c [transred-6] found 1 units
c [cce-3] limit of 40324795 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 11 clauses out of 1140 (1%) of length 9
c [cce-3-1] eliminated 134 clauses out of 667 (20%) of length 8
c [cce-3-1] eliminated 1399 clauses out of 2237 (63%) of length 7
c [cce-3-1] eliminated 854 clauses out of 6533 (13%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2398 large clauses in 40324796 steps
c [cce-3-1] allowing another 20162398 steps for small clauses
c [cce-3-1] scheduling 356871 clauses = 250002 binary + 106869 ternary
c [cce-3-1] tried to eliminate 559 small clauses 0%
c [cce-3-1] eliminated 134 binary clauses 0%
c [cce-3-1] eliminated 42 ternary clauses 0%
c [cce-3-1] eliminated 176 small clauses 0%
c [cce-3-1] eliminated 2680 small clauses in 40324801 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 5078 covered clauses in round 1
c [cce-3] eliminated 5078 covered clauses in TOTAL during 1 rounds
c [cce-3] 5078 < 1/100 * 523806 = 5238 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 76488 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 12903934400 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 982 variables 1% in round 1 in 49375225 steps
c [elim-8-1] backward subsumption/strengthening limit 49375200
c [elim-8-1-1] backward checking 4042 touched variables 5%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 2 and strengthened 33 clauses in 1525918 steps
c [elim-8-1] rescheduled 85 variables 0% by backward subsumption
c [elim-8-2] eliminated 13 variables 0% in round 2 in 121519 steps
c [elim-8-2] backward subsumption/strengthening limit 121500
c [elim-8-2-1] backward checking 106 touched variables 0%
c [elim-8-2-1] incomplete backward checking 0 remain 0%
c [elim-8-2] subsumed 5 and strengthened 1 clauses in 121501 steps
c [elim-8-2] rescheduled 7 variables 0% by backward subsumption
c [elim-8-3] eliminated 2 variables 0% in round 3 in 13451 steps
c [elim-8-3] backward subsumption/strengthening limit 13400
c [elim-8-3-1] backward checking 31 touched variables 0%
c [elim-8-3-1] incomplete backward checking 12 remain 39%
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 13403 steps
c [elim-8] fully completed in 3 rounds
c [gc-65] reconnected 341449 binary clauses (produced 0 empty 3 units)
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1011 = 1% variables out of 76488 scheduled
c [bca-6] limit of 10000000 steps and 1033152 added (scaled 2)
c [bca-6] 132474 out of 150956 literals actually usable 88%
c [bca-6] added 229 blocked clauses in 370913 steps
c [sweep-6] limit 9677950 penalty 0 = 0 + 0
c [sweep-6-1] 3360 pos 8.4% + 36641 neg 91.6% = 40001 sched 53.0% ret 35476
c [sweep-6-1] 9775600 steps 138 queries 3184.58 avg class size
c [sweep-6-1] 1505 decisions 130 SAT calls 101.43 avg env size
c [sweep-6-1] 39015 variables remain 52% (36420 retained 48%)
c [decomp-24] removed 93 variables
c [sweep-6-1] removed 93 vars (0 failed, 9 eqs, 18 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 93 vars in TOTAL (1 rounds, 137 queries)
c [phase-count-10] 511405 negative 99.2% of 515731 except 4326 0.8%
c [phase-count-10] 417674 positive 81.0% of 515731 except 98057 19.0%
c [phase-count-10] less non-negative clauses 4326 than limit 51500 (10.0%)
c [phase-count-10] non-pos/non-neg = 98057/4326 = 22.67 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 208 negative 100%
c [sort-queue-10] sorted 26682 enqueued variables after 64091 conflicts
c [score-dist-10] active 48702 (65%), one 0 (0%), zero 26682 (35%)
c [score-dist-10] max exp 510, different 258 (50%)
c [score-dist-10] median active exp 458, avg 439.1
c [simplification-10] removed 1427 variables 1.9% (75384 remain 26%)
c [simplification-10] removed 10438 irredundant clauses 2.0% (515731 remain 37%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] geometric conflict interval increment 8000 = 24000 / 3
c [simplification-10] new conflict interval 32000
c [simplification-10] penalized conflict interval 32000 = 1 * 32000
c [simplification-10] hard conflict limit 112091 (soft 96091 + delta 16000)
c [simplification-10] new conflict limit 96091 (hard 112091)
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  259.4   75383   515731     65100    8179    913 342728 1117  1565   71  71%     89  535  848  734  116%
c i  259.6   75382   515731     65255    8309    913 342731 1102  1568   75  70%     75  537  771  734  105%
c i  259.7   75381   515731     65314    8360    913 342732 1094  1568   75  70%     70  537  713  733   97%
c i  259.9   75374   515731     65407    8422    914 342732 1089  1568   77  69%     62  536  761  734  104%
c i  259.9   75373   515731     65425    8437    915 342732 1085  1568   77  69%     61  536  733  734  100%
c i  260.5   75372   515731     65723    8616    915 342735 1083  1572   77  69%     42  538  961  735  131%
c i  260.5   75371   515731     65765    8646    915 342737 1081  1572   77  69%     40  538  939  735  128%
c i  261.4   75360   515731     66164    8881    916 342739 1083  1583   81  68%     23  545 1095  737  148%
c i  261.6   75359   515731     66275    8967    916 342744 1077  1587   81  68%     20  548 1016  737  138%
c i  262.1   75358   515731     66495    9115    917 342749 1074  1597   81  67%     13  556 1040  738  141%
c i  263.1   75357   515731     66943    9439    919 342756 1093  1644   81  67%      5  599 1251  742  169%
c i  263.6   75356   515731     67123    9584    919 342757 1090  1666   81  65%      2  620 1156  743  156%
c i  265.9   75355   515731     68212   10358    922 342762 1060  1662  100  64%     -2  605  976  746  131%
c i  266.5   75354   515731     68535   10540    923 342762 1051  1641  100  64%     -5  582  916  747  123%
c i  266.6   75353   515731     68546   10549    923 342762 1049  1640  100  64%     -5  580  890  747  119%
c i  266.6   75352   515731     68550   10552    923 342762 1048  1640  100  64%     -5  580  882  747  118%
c i  266.6   75351   515731     68551   10552    923 342762 1048  1639  100  64%     -5  579  879  747  118%
c i  266.8   75350   515731     68626   10590    923 342762 1044  1633  100  64%     -6  572  870  747  116%
c i  266.8   75349   515731     68627   10590    923 342762 1044  1632  100  64%     -6  572  867  747  116%
c i  267.7   75348   515731     69490   11192    924 342769  975  1576  100  62%     -6  508  738  746   99%
c i  267.7   75347   515731     69519   11217    925 342769  970  1574  100  62%     -6  506  692  746   93%
c i  267.7   75346   515731     69520   11217    925 342769  970  1574  100  62%     -6  506  689  746   92%
c i  267.7   75345   515731     69522   11217    926 342769  970  1573  100  62%     -7  505  683  746   92%
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  267.8   75344   515731     69523   11217    926 342769  970  1573  100  62%     -7  505  681  746   91%
c i  267.8   75343   515731     69524   11217    926 342769  969  1572  100  62%     -7  505  678  746   91%
c i  267.8   75342   515731     69586   11275    927 342770  961  1570  100  61%     -7  501  629  746   84%
c i  268.1   75338   515731     69761   11430    928 342772  945  1566  100  60%     -8  496  619  745   83%
c i  269.5   75337   515731     70775   12214    933 342792  901  1524  114  59%     -6  447  699  745   94%
c i  270.0   75330   515731     71298   12605    937 342798  871  1491  114  58%     -8  411  543  744   73%
c i  270.0   75329   515731     71302   12608    937 342798  870  1491  114  58%     -8  410  537  744   72%
c i  270.1   75328   515731     71325   12628    938 342798  868  1490  114  58%     -8  410  537  744   72%
c i  270.3   75327   515731     71527   12801    938 342802  857  1489  114  58%     -9  407  590  744   79%
c i  270.3   75326   515731     71558   12827    938 342802  858  1491  114  58%     -9  409  634  744   85%
c i  270.4   75325   515731     71560   12828    938 342802  858  1490  114  58%     -9  408  636  744   85%
c i  270.8   75309   515731     71902   13106    938 342803  865  1506  114  57%     -9  422  872  745  117%
c i  272.8   75308   515731     73481   14392    950 342823  821  1562  114  53%     -1  468  629  745   84%
c i  277.1   75307   515731     75900   16198    963 342861  833  1576  143  53%     11  464  784  748  105%
c i  277.4   75306   515731     76174   16364    965 342862  831  1566  143  53%      5  452  797  749  106%
c i  277.5   75305   515731     76215   16403    966 342862  826  1564  143  53%      5  450  723  748   97%
c i  278.1   75304   515731     76635   16702    972 342867  829  1556  143  53%     -1  438  857  749  114%
c i  279.0   75303   515731     77216   17123    982 342877  829  1571  171  53%     -4  449  869  750  116%
c i  279.0   75302   515731     77237   17140    982 342877  829  1571  171  53%     -4  450  867  750  116%
c i  279.4   75301   515731     77368   17254    984 342879  835  1587  171  53%     -5  464  938  750  125%
c i  279.5   75290   515731     77402   17283    985 342879  838  1589  171  53%     -6  467  962  751  128%
c i  279.5   75289   515731     77410   17290    985 342879  838  1589  171  53%     -6  467  961  751  128%
c i  279.5   75288   515731     77411   17290    985 342879  838  1589  171  53%     -6  466  957  751  128%
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  279.5   75287   515731     77416   17293    986 342879  838  1589  171  53%     -6  466  954  751  127%
c i  279.6   75286   515731     77425   17301    986 342879  838  1589  171  53%     -6  466  950  751  127%
c i  279.6   75285   515731     77429   17304    986 342879  837  1589  171  53%     -6  466  942  751  126%
c i  279.6   75284   515731     77430   17304    986 342879  837  1589  171  53%     -6  466  939  751  125%
c i  280.2   75280   515731     77649   17498    990 342882  849  1601  171  53%     -7  477  998  752  133%
c i  280.4   75279   515731     77759   17599    990 342884  842  1605  171  52%     -8  480  845  751  112%
c i  283.1   75253   515731     79264   18692   1004 342905  850  1615  171  53%     -1  479  928  754  123%
c i  284.0   75252   515731     79804   18880   1011 342913  851  1557  171  55%     -4  417  897  755  119%
c i  284.0   75251   515731     79805   18880   1011 342913  851  1557  171  55%     -4  416  894  755  118%
c i  284.1   75250   515731     79806   18880   1011 342913  851  1556  171  55%     -4  416  890  755  118%
c i  285.3   75249   515731     80817   19349   1014 342936  827  1444  171  57%     -4  298  710  755   94%
c i  285.5   75001   515731     80922   19425   1014 342937  819  1432  171  57%     -5  285  632  754   84%
c i  286.1   74999   515731     81432   19737   1019 342941  797  1382  171  58%     -7  233  686  753   91%
c i  287.1   74998   515731     82286   20034   1022 342945  789  1301  171  61%     -6  150  769  753  102%
c i  287.2   74997   515731     82378   20057   1023 342946  790  1294  171  61%     -7  143  788  753  105%
c i  287.8   74996   515731     82909   20276   1024 342948  787  1258  171  63%     -8  106  758  753  101%
c i  288.1   74995   515731     83083   20343   1025 342948  790  1248  171  63%     -8   96  811  754  108%
c i  288.4   74994   515731     83239   20390   1025 342950  791  1238  171  64%     -9   85  805  754  107%
c i  290.0   74993   515731     84513   20970   1036 342954  754  1157  171  65%     -3    4  571  752   76%
c i  290.7   74992   515731     85129   21282   1047 342955  738  1131  172  65%     -5  -22  635  751   85%
c i  290.7   74991   515731     85137   21286   1047 342955  737  1130  172  65%     -6  -23  634  751   84%
c i  290.7   74990   515731     85138   21286   1047 342955  737  1130  172  65%     -6  -23  632  751   84%
c i  293.2   74989   515731     87441   22375   1053 342971  697  1048  172  67%      9 -103  678  747   91%
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  293.9   74988   515731     87979   22758   1055 342975  688  1078  173  64%      2  -72  586  746   79%
c i  294.2   74987   515731     88218   22862   1055 342977  694  1078  190  64%     -1  -72  720  746   96%
c i  294.5   74986   515731     88450   23000   1055 342980  693  1078  190  64%     -3  -71  678  746   91%
c i  295.0   74985   515731     88846   23237   1057 342981  693  1079  190  64%     -5  -70  694  745   93%
c i  295.0   74984   515731     88851   23240   1057 342981  693  1079  190  64%     -5  -70  691  745   93%
c i  295.0   74983   515731     88853   23241   1057 342981  693  1078  190  64%     -5  -71  690  745   93%
c i  295.1   74982   515731     88855   23242   1057 342981  693  1078  190  64%     -5  -71  688  745   92%
c i  295.4   74969   515731     89118   23380   1059 342984  693  1076  247  64%     -7  -73  682  745   92%
c i  295.5   74968   515731     89171   23399   1059 342984  694  1075  247  65%     -7  -73  702  745   94%
c i  295.8   74967   515731     89359   23485   1060 342985  695  1073  247  65%     -8  -75  710  745   95%
c i  303.0   74966   515731     94215   25334   1089 343001  722   989  248  73%     46 -151  606  745   81%
c i  303.7   74955   515731     94802   25601   1090 343002  708   972  248  73%     22 -167  576  744   77%
c i  303.8   74925   515731     94862   25621   1090 343003  706   969  248  73%     20 -170  577  744   78%
c i  307.1   74920   515731     98075   26662   1098 343029  630   827  248  76%     21 -301  494  736   67%
c i  307.4   74919   515731     98405   26761   1099 343036  624   815  248  77%     12 -311  543  735   74%
c i  307.6   74918   515731     98579   26795   1101 343037  622   809  248  77%      8 -316  560  734   76%
c i  313.1   74917   515731    104143   28605   1120 343061  561   703  257  80%     54 -392  530  719   74%
c 
c [simplification-11] limit 96224 conflicts (hard 112091) hit after 112096 conflicts
c [ternres-6] limit 42848148 with penalty 0 = 0 + 0
c [ternres-6] all 74917 free variables schedulable
c [ternres-6] 141 ternary resolvents (0 bin, 141 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-25] removed 510 variables
c [basicprobe-4] limit 214240741 penalty 0 = 0 + 0
c [basicprobe-4-0] 17723 probes remain 24% after last round
c [basicprobe-4-0] 739 units = 736 failed (100%) + 3 lifted (0%)
c [basicprobe-4-0] removed 1425 variables, found 380830 hbrs
c [bate-2] eliminated 282 asymmetric tautologies during probing
c [unhide-11] limit 1071203 with penalty 3 = 0 + 3
c [unhide-11-11] 4 units, 53 failed, 6971 tauts, 0 hbrs, 1405073 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 149 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 73298 variables 100%
c [block-4] limit of 107120370 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 43 blocked clauses
c [block-4] 43 < 1/100 * 499677 = 4996 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 73298 variables 100%
c [elim-9] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1189 variables 2% in round 1 in 47019565 steps
c [elim-9-1] backward subsumption/strengthening limit 47019500
c [elim-9-1-1] backward checking 4874 touched variables 7%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 9 and strengthened 79 clauses in 1629097 steps
c [elim-9-1] rescheduled 207 variables 0% by backward subsumption
c [elim-9-2] eliminated 25 variables 0% in round 2 in 213465 steps
c [elim-9-2] backward subsumption/strengthening limit 213400
c [elim-9-2-1] backward checking 188 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 171760 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1224 = 2% variables out of 73298 scheduled
c [bca-7] limit of 10000000 steps and 991242 added (scaled 2)
c [bca-7] 121938 out of 144150 literals actually usable 85%
c [bca-7] added 51 blocked clauses in 328833 steps
c [sweep-7] limit 12854444 penalty 0 = 0 + 0
c [sweep-7-1] 3700 pos 9.8% + 34199 neg 90.2% = 37899 sched 52.6% ret 34175
c [sweep-7-1] 12909343 steps 232 queries 1649.32 avg class size
c [sweep-7-1] 3111 decisions 202 SAT calls 148.03 avg env size
c [sweep-7-1] 35273 variables remain 49% (36674 retained 51%)
c [decomp-26] removed 316 variables
c [sweep-7-1] removed 316 vars (0 failed, 31 eqs, 43 impls)
c [sweep-7] removed 316 vars in TOTAL (1 rounds, 231 queries)
c [phase-count-11] 490009 negative 99.1% of 494245 except 4236 0.9%
c [phase-count-11] 399983 positive 80.9% of 494245 except 94262 19.1%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 9 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 21268 enqueued variables after 112096 conflicts
c [score-dist-11] active 50490 (70%), one 0 (0%), zero 21268 (30%)
c [score-dist-11] max exp 510, different 438 (86%)
c [score-dist-11] median active exp 388, avg 397.0
c [simplification-11] removed 3159 variables 4.2% (71758 remain 25%)
c [simplification-11] removed 21486 irredundant clauses 4.2% (494245 remain 36%)
c [simplification-11] maximum reduction of 4% = max (4%, 4%)
c [simplification-11] geometric conflict interval increment 6400 = 32000 / 5
c [simplification-11] new conflict interval 38400
c [simplification-11] penalized conflict interval 38400 = 1 * 38400
c [simplification-11] hard conflict limit 169696 (soft 150496 + delta 19200)
c [simplification-11] new conflict limit 150496 (hard 169696)
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  343.7   71757   494245    112355   12423   1309 700185  590   716   83  82%     91 -334  448  704   64%
c i  345.5   71756   494245    114387   13377   1316 700193  547   700   95  78%     11 -340  471  697   67%
c i  346.1   71755   494245    114880   13575   1319 700195  544   696   95  78%     -1 -342  521  696   75%
c i  348.1   71754   494245    116651   14235   1332 700198  531   677   95  78%     -4 -351  498  691   72%
c i  355.6   71753   494245    124607   16123   1369 700234  426   499  114  85%     82 -479  401  661   61%
c i  360.8   71752   494245    129436   17290   1380 700250  420   482  136  87%     33 -462  417  643   65%
c i  361.2   71751   494245    129901   17450   1383 700253  415   482  136  86%     12 -459  386  641   60%
c i  361.6   71750   494245    130245   17624   1384 700254  414   490  136  84%      2 -449  398  640   62%
c i  362.0   71749   494245    130759   17796   1386 700254  409   488  136  84%     -8 -447  364  638   57%
c i  362.1   71748   494245    130864   17860   1386 700254  406   488  136  83%    -10 -447  344  637   54%
c i  362.3   71747   494245    131141   17979   1386 700255  409   494  136  83%    -14 -439  408  637   64%
c i  362.9   71746   494245    131696   18174   1388 700256  428   517  136  83%    -17 -412  542  636   85%
c i  362.9   71745   494245    131729   18188   1389 700256  429   518  136  83%    -18 -411  546  636   86%
c i  363.6   71741   494245    132504   18574   1395 700264  446   558  136  80%    -19 -367  518  635   82%
c i  363.6   71740   494245    132523   18582   1396 700265  445   558  136  80%    -19 -366  508  635   80%
c i  365.5   71737   494245    134122   19544   1408 700276  478   671  153  71%    -13 -246  613  632   97%
c i  366.5   71736   494245    134916   20068   1414 700278  517   752  153  69%    -16 -162  759  633  120%
c i  367.5   71735   494245    135464   20387   1414 700278  556   805  153  69%    -18 -109  840  635  132%
c i  369.5   71734   494245    136517   20805   1414 700284  626   868  153  72%    -17  -44  870  638  136%
c i  370.9   71732   494245    137302   21132   1416 700289  648   888  161  73%    -18  -24  735  640  115%
c i  373.4   71731   494245    139041   21805   1422 700292  676   904  161  75%    -10   -7  781  642  122%
c i  374.8   71730   494245    139955   22233   1425 700294  673   913  164  74%    -14    2  660  642  103%
c i  379.3   71729   494245    143486   23309   1428 700306  667   844  199  79%     15  -66  617  643   96%
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  380.2   71728   494245    144344   23593   1431 700308  657   831  199  79%     -3  -78  595  643   93%
c i  381.4   71727   494245    145283   23904   1433 700313  662   832  199  80%    -11  -75  679  643  106%
c i  381.9   71726   494245    145729   24050   1434 700314  661   828  199  80%    -15  -79  668  643  104%
c i  385.6   71725   494245    148707   24814   1440 700321  665   803  199  83%      8 -100  683  645  106%
c i  385.6   71721   494245    148708   24814   1440 700321  665   803  199  83%      8 -100  680  645  106%
c i  386.2   71718   494245    149101   24916   1442 700322  662   798  199  83%     -2 -104  644  645  100%
c i  386.3   71717   494245    149201   24929   1442 700322  663   797  199  83%     -4 -105  659  645  102%
c i  387.7   71716   494245    150337   25253   1448 700330  652   787  200  83%    -10 -113  597  644   93%
c i  390.4   71715   494245    152209   25785   1454 700334  675   802  200  84%     -6  -95  699  646  108%
c i  391.3   71714   494245    152851   25954   1454 700334  681   806  200  85%    -12  -91  690  647  107%
c i  407.7   71713   494245    165399   29340   1475 700357  685   792  271  87%    145  -90  547  656   83%
c i  410.5   71712   494245    167660   30079   1480 700361  681   805  271  85%      4  -74  695  657  106%
c i  412.1   71711   494245    168882   30588   1487 700364  679   829  271  82%    -16  -49  760  657  116%
c i  414.0   71710   494245    169668   30796   1492 700365  701   837  271  84%    -23  -40  792  659  120%
c 
c [simplification-12] limit 150506 conflicts (hard 169696) hit after 169696 conflicts
c [quatres-4] found 34420 quaternary clauses 45% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 2 single-self-subsuming ternary resolvents
c [quatres-4-2] added 5 quaternary resolvents
c [ternres-7] limit 55027850 with penalty 0 = 0 + 0
c [ternres-7] all 71710 free variables schedulable
c [ternres-7] 274 ternary resolvents (0 bin, 274 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 69 variables
c [simpleprobe-5] all 71689 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-28] removed 1217 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1217 variables, found 50395 hbrs, 456 units
c [unhide-12] limit 1375696 with penalty 3 = 0 + 3
c [unhide-12-12] 4 units, 329 failed, 60495 tauts, 0 hbrs, 573429 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 142 transitive binary clauses
c [transred-8] found 1 units
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 70380 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 900 variables 1% in round 1 in 46338928 steps
c [elim-10-1] backward subsumption/strengthening limit 46338900
c [elim-10-1-1] backward checking 3468 touched variables 5%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 28 and strengthened 84 clauses in 1329922 steps
c [elim-10-1] rescheduled 255 variables 0% by backward subsumption
c [elim-10-2] eliminated 24 variables 0% in round 2 in 261625 steps
c [elim-10-2] backward subsumption/strengthening limit 261600
c [elim-10-2-1] backward checking 185 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 3 and strengthened 4 clauses in 159341 steps
c [elim-10-2] rescheduled 7 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 3611 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 924 = 1% variables out of 70380 scheduled
c [bca-8] limit of 10000000 steps and 961086 added (scaled 2)
c [bca-8] 116541 out of 138914 literals actually usable 84%
c [bca-8] added 55 blocked clauses in 310973 steps
c [sweep-8] limit 16508355 penalty 0 = 0 + 0
c [sweep-8-1] 3272 pos 9.5% + 31287 neg 90.5% = 34559 sched 49.8% ret 34897
c [sweep-8-1] 16517979 steps 263 queries 1458.78 avg class size
c [sweep-8-1] 2523 decisions 242 SAT calls 108.87 avg env size
c [sweep-8-1] 32478 variables remain 47% (36951 retained 53%)
c [decomp-29] removed 154 variables
c [sweep-8-1] removed 154 vars (0 failed, 24 eqs, 37 impls)
c [sweep-8] removed 154 vars in TOTAL (1 rounds, 262 queries)
c [phase-count-12] 475546 negative 99.2% of 479607 except 4061 0.8%
c [phase-count-12] 386351 positive 80.6% of 479607 except 93256 19.4%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-12] sorted 22034 enqueued variables after 169696 conflicts
c [score-dist-12] active 47268 (68%), one 3175 (5%), zero 18859 (27%)
c [score-dist-12] max exp 510, different 497 (97%)
c [score-dist-12] median active exp 444, avg 378.6
c [simplification-12] removed 2408 variables 3.4% (69302 remain 24%)
c [simplification-12] removed 14638 irredundant clauses 3.0% (479607 remain 35%)
c [simplification-12] maximum reduction of 3% = max (3%, 3%)
c [simplification-12] geometric conflict interval increment 9600 = 38400 / 4
c [simplification-12] new conflict interval 48000
c [simplification-12] penalized conflict interval 48000 = 1 * 48000
c [simplification-12] hard conflict limit 241696 (soft 217696 + delta 24000)
c [simplification-12] new conflict limit 217696 (hard 241696)
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  425.5   69301   479607    169930   10752   1650 660297  686   837   77  82%    -25  -40  593  658   90%
c i  428.1   69300   479607    171914   11609   1658 660300  664   830   82  80%    -16  -46  620  657   94%
c i  429.3   69299   479607    172881   12065   1661 660304  652   831   88  79%    -22  -45  610  656   93%
c i  429.4   69298   479607    172911   12084   1662 660304  651   831   88  78%    -23  -44  598  656   91%
c i  430.1   69297   479607    173482   12385   1667 660310  648   843   88  77%    -25  -32  646  656   99%
c i  430.2   69296   479607    173526   12411   1667 660313  649   845   88  77%    -26  -30  660  656  101%
c i  430.6   69295   479607    173825   12569   1671 660315  655   859   93  76%    -27  -16  725  656  111%
c i  431.2   69294   479607    174368   12881   1675 660317  652   880   93  74%    -28    5  649  656   99%
c i  437.2   69293   479607    178861   14612   1686 660322  709   907  105  78%     21   30  793  662  120%
c i  440.4   69292   479607    180721   15568   1695 660334  724   937  128  77%     -9   58  669  664  101%
c i  441.9   69291   479607    181992   16224   1696 660342  697   930  128  75%    -18   51  528  664   80%
c i  444.5   69282   479607    183803   17231   1700 660348  720   981  138  73%    -15   99  848  666  127%
c i  444.6   69281   479607    183850   17260   1700 660348  721   982  138  73%    -16  100  833  666  125%
c i  465.7   69280   479607    197181   22277   1718 660388  849   984  185  86%    148   87  889  691  129%
c i  465.9   69279   479607    197398   22313   1719 660389  848   980  185  87%    112   83  856  691  124%
c i  466.1   69278   479607    197489   22322   1719 660389  849   979  185  87%     98   82  865  692  125%
c i  472.3   69277   479607    202103   23364   1723 660393  816   913  191  89%     13   12  778  699  111%
c i  477.5   69276   479607    205979   24169   1731 660397  867   954  286  91%      2   51  889  711  125%
c i  483.9   69275   479607    210432   25142   1737 660398  863   938  286  92%     11   32  783  721  109%
c i  486.1   69274   479607    212484   25845   1742 660399  878   996  304  88%    -18   88  872  727  120%
c i  487.8   69273   479607    213921   26227   1744 660402  898  1027  304  87%    -26  117  902  731  123%
c 
c [simplification-13] limit 217696 conflicts (hard 241696) hit after 217696 conflicts
c [quatres-5] found 32745 quaternary clauses 45% in total
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [quatres-5-2] added 3 quaternary resolvents
c [ternres-8] limit 66152706 with penalty 0 = 0 + 0
c [ternres-8] all 69273 free variables schedulable
c [ternres-8] 334 ternary resolvents (0 bin, 334 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-30] removed 29 variables
c [treelook-5] limit 6615270 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 124010 literals 90%
c [treelook-5] scheduling used 2626663 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 6615270 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 6632535 steps
c [treelook-5] 123773 literals remain 89%
c [treelook-5] 27115 variables remain to probed next time 39%
c [treelook-5] removed 64 variables, found 15182 hbrs
c [unhide-13] limit 1653817 with penalty 3 = 0 + 3
c [unhide-13-13] 4 units, 24 failed, 8104 tauts, 0 hbrs, 595273 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 93 transitive binary clauses
c [transred-9] found 2 units
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 69155 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 334 variables 0% in round 1 in 46347373 steps
c [elim-11-1] backward subsumption/strengthening limit 46347300
c [elim-11-1-1] backward checking 1961 touched variables 3%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 187 and strengthened 12 clauses in 967670 steps
c [elim-11-1] rescheduled 294 variables 0% by backward subsumption
c [elim-11-2] eliminated 87 variables 0% in round 2 in 883817 steps
c [elim-11-2] backward subsumption/strengthening limit 883800
c [elim-11-2-1] backward checking 298 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 13 and strengthened 0 clauses in 301138 steps
c [elim-11-2] rescheduled 40 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 697518 steps
c [elim-11] fully completed in 3 rounds
c [gc-87] reconnected 666291 binary clauses (produced 0 empty 1 units)
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 451 = 1% variables out of 69155 scheduled
c [elim-11] 451 < 1/100 * 69155 = 691 considered unsuccessful
c [bca-9] limit of 10000000 steps and 943467 added (scaled 2)
c [bca-9] 114758 out of 137410 literals actually usable 84%
c [bca-9] added 55 blocked clauses in 309368 steps
c [sweep-9] limit 19845811 penalty 0 = 0 + 0
c [sweep-9-1] 3040 pos 9.4% + 29171 neg 90.6% = 32211 sched 46.9% ret 36493
c [sweep-9-1] 19939963 steps 374 queries 1373.21 avg class size
c [sweep-9-1] 3958 decisions 344 SAT calls 100.31 avg env size
c [sweep-9-1] 29611 variables remain 43% (38954 retained 57%)
c [decomp-32] removed 247 variables
c [sweep-9-1] removed 247 vars (0 failed, 32 eqs, 62 impls)
c [sweep-9] removed 247 vars in TOTAL (1 rounds, 373 queries)
c [phase-count-13] 466089 negative 99.1% of 470097 except 4008 0.9%
c [phase-count-13] 378935 positive 80.6% of 470097 except 91162 19.4%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 28698 enqueued variables after 217696 conflicts
c [score-dist-13] active 39759 (58%), one 10470 (15%), zero 18228 (27%)
c [score-dist-13] max exp 510, different 487 (95%)
c [score-dist-13] median active exp 487, avg 408.8
c [simplification-13] removed 816 variables 1.2% (68457 remain 24%)
c [simplification-13] removed 9510 irredundant clauses 2.0% (470097 remain 34%)
c [simplification-13] maximum reduction of 2% = max (1%, 2%)
c [simplification-13] geometric conflict interval increment 16000 = 48000 / 3
c [simplification-13] new conflict interval 64000
c [simplification-13] penalized conflict interval 64000 = 1 * 64000
c [simplification-13] hard conflict limit 313696 (soft 281696 + delta 32000)
c [simplification-13] new conflict limit 281696 (hard 313696)
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  506.1   68456   470097    219790   14721   1988 676479  823  1044   94  79%     34  123  580  739   78%
c i  517.6   68455   470097    227339   18003   2010 676522  823  1034  119  80%     58  105  807  743  109%
c i  519.2   68454   470097    228962   19139   2023 676533  709  1005  119  71%    -10   74  572  737   78%
c i  520.1   68453   470097    229511   19447   2026 676535  717  1017  152  70%    -22   85  790  737  107%
c i  521.5   68452   470097    230621   20136   2031 676539  706  1028  164  69%    -29   95  662  736   90%
c i  529.6   68447   470097    236504   22967   2044 676561  683   961  164  71%     33   22  537  732   73%
c i  530.4   68446   470097    237101   23262   2048 676568  677   954  164  71%      2   15  646  731   88%
c i  559.4   68445   470097    257775   30929   2076 676629  710   880  260  81%    233  -49  673  724   93%
c i  559.5   68444   470097    257847   30966   2076 676629  707   879  260  80%    212  -50  646  724   89%
c i  582.6   68443   470097    276730   36513   2102 676682  706   816  395  87%    185  -89  726  716  101%
c i  583.0   68442   470097    276967   36622   2108 676685  700   820  395  85%    128  -84  662  716   92%
c i  587.2   68441   470097    279972   37609   2115 676697  716   849  395  84%    -50  -51  814  716  114%
c i  589.1   68440   470097    281046   37945   2119 676705  740   879  395  84%    -71  -21  836  718  117%
c i  589.3   68439   470097    281105   37963   2119 676705  741   880  395  84%    -72  -20  832  718  116%
c i  598.6   68438   470097    286489   39320   2128 676724  751   861  395  87%    -20  -37  716  721   99%
c i  620.9   68437   470097    300221   42179   2143 676758  766   836  395  92%    108  -51  726  727  100%
c 
c [simplification-14] limit 281696 conflicts (hard 313696) hit after 313696 conflicts
c [quatres-6] found 30293 quaternary clauses 43% in total
c [quatres-6-2] added 1 quaternary resolvents
c [ternres-9] limit 90372325 with penalty 0 = 0 + 0
c [ternres-9] all 68437 free variables schedulable
c [ternres-9] 234 ternary resolvents (0 bin, 234 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 2259308 penalty 3 = 3 + 0
c [gauss-4] extracted 36 xors of average arity 3.0
c [gauss-4] connected 108 occurrences of 102 variables (average 1.1)
c [gauss-4] limit 2259308 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-33] removed 2 variables
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 9176 probes remain 14% after last round
c [basicprobe-5-0] 1316 units = 1291 failed (98%) + 25 lifted (2%)
c [basicprobe-5-0] removed 2022 variables, found 570431 hbrs
c [bate-3] eliminated 537 asymmetric tautologies during probing
c [unhide-14] limit 1129654 with penalty 4 = 0 + 4
c [unhide-14-14] 4 units, 701 failed, 87239 tauts, 0 hbrs, 1438057 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 101 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 564827032 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 430 (0%) of length 8
c [cce-4-1] eliminated 7 clauses out of 675 (1%) of length 7
c [cce-4-1] eliminated 2565 clauses out of 4846 (53%) of length 6
c [cce-4-1] eliminated 18972 clauses out of 28065 (68%) of length 5
c [cce-4-1] eliminated 16873 clauses out of 28040 (60%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 38418 large clauses in 481358687 steps
c [cce-4-1] allowing another 240679343 steps for small clauses
c [cce-4-1] scheduling 313599 clauses = 220025 binary + 93574 ternary
c [cce-4-1] tried to eliminate 9875 small clauses 3%
c [cce-4-1] eliminated 2039 binary clauses 1%
c [cce-4-1] eliminated 372 ternary clauses 0%
c [cce-4-1] eliminated 2411 small clauses 1%
c [cce-4-1] eliminated 4085 small clauses in 564827041 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 42503 covered clauses in round 1
c [cce-4] eliminated 42503 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 830583 added (scaled 2)
c [bca-10] 107239 out of 132482 literals actually usable 81%
c [bca-10] added 96 blocked clauses in 275677 steps
c [sweep-10] limit 27111697 penalty 0 = 0 + 0
c [sweep-10-1] 3196 pos 11.0% + 25833 neg 89.0% = 29029 sched 43.8% ret 37211
c [sweep-10-1] 27143056 steps 530 queries 591.28 avg class size
c [sweep-10-1] 6740 decisions 473 SAT calls 177.93 avg env size
c [sweep-10-1] 25443 variables remain 38% (40692 retained 62%)
c [decomp-34] removed 554 variables
c [sweep-10-1] removed 554 vars (0 failed, 59 eqs, 102 impls)
c [sweep-10] removed 554 vars in TOTAL (1 rounds, 529 queries)
c [phase-count-14] 412413 negative 99.8% of 413298 except 885 0.2%
c [phase-count-14] 325012 positive 78.6% of 413298 except 88286 21.4%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-14] sorted 25942 enqueued variables after 313696 conflicts
c [score-dist-14] active 39744 (61%), one 10621 (16%), zero 15321 (23%)
c [score-dist-14] max exp 510, different 481 (94%)
c [score-dist-14] median active exp 502, avg 407.8
c [simplification-14] removed 2751 variables 4.0% (65686 remain 23%)
c [simplification-14] removed 56799 irredundant clauses 12.1% (413298 remain 30%)
c [simplification-14] maximum reduction of 12% = max (4%, 12%)
c [simplification-14] large reduction 12% >= 5% limit
c [simplification-14] next conflict interval 3136 = min (313696/100, 64000)
c [simplification-14] penalized conflict interval 3136 = 1 * 3136
c [simplification-14] hard conflict limit 326832 (soft 316832 + delta 10000)
c [simplification-14] new conflict limit 316832 (hard 326832)
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  693.3   65685   413298    314513   45153   2873 1132775  810   935  265  87%    112   56  995  736  135%
c 
c [simplification-15] limit 316832 conflicts (hard 326832) hit after 321444 conflicts
c [quatres-7] found 11527 quaternary clauses 45% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [ternres-10] limit 92407575 with penalty 0 = 0 + 0
c [ternres-10] all 65685 free variables schedulable
c [ternres-10] 38 ternary resolvents (0 bin, 38 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 2887736 penalty 4 = 4 + 0
c [card-5] found 1927 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2887736 for elimination
c [card-5] 1927 out of 1927 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 1 variables
c [simpleprobe-6] all 65685 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-36] removed 621 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 621 variables, found 69514 hbrs, 255 units
c [unhide-15] limit 2310189 with penalty 3 = 0 + 3
c [unhide-15-15] 3 units, 23 failed, 8773 tauts, 0 hbrs, 204326 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 87 transitive binary clauses
c [transred-11] found 2 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 65028 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 845 blocked clauses
c [block-5] 845 < 1/100 * 402708 = 4027 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 64959 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 15645 variables 24% in round 1 in 37464974 steps
c [elim-12-1] backward subsumption/strengthening limit 37464900
c [elim-12-1-1] backward checking 33612 touched variables 52%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 19 and strengthened 13 clauses in 5331188 steps
c [elim-12-1] rescheduled 82 variables 0% by backward subsumption
c [elim-12-2] eliminated 5 variables 0% in round 2 in 597308 steps
c [elim-12-2] backward subsumption/strengthening limit 597300
c [elim-12-2-1] backward checking 68 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 11 and strengthened 0 clauses in 496387 steps
c [elim-12-2] rescheduled 11 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 22523 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 15650 = 24% variables out of 64959 scheduled
c [bca-11] limit of 10000000 steps and 740363 added (scaled 2)
c [bca-11] 91782 out of 98620 literals actually usable 93%
c [bca-11] added 56 blocked clauses in 212620 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 277222720 penalty 0 = 0 + 0
c [sweep-11-1] 2588 pos 10.7% + 21597 neg 89.3% = 24185 sched 49.0% ret 25124
c [sweep-11-1] 269872080 steps 8543 queries 52.29 avg class size
c [sweep-11-1] 28462 decisions 6429 SAT calls 70.60 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-37] removed 2438 variables
c [sweep-11-1] removed 2438 vars (0 failed, 2123 eqs, 2117 impls)
c [sweep-11-2] 3969 pos 8.5% + 42902 neg 91.5% = 46871 sched 100.0% ret 0
c [sweep-11-2] 7371046 steps 104 queries 2796.48 avg class size
c [sweep-11-2] 1640 decisions 99 SAT calls 123.14 avg env size
c [sweep-11-2] 38136 variables remain 81% (8674 retained 19%)
c [decomp-38] removed 66 variables
c [sweep-11-2] removed 66 vars (0 failed, 4 eqs, 13 impls)
c [sweep-11] removed 2504 vars in TOTAL (2 rounds, 8645 queries)
c [phase-count-15] 363449 negative 99.8% of 364228 except 779 0.2%
c [phase-count-15] 279970 positive 76.9% of 364228 except 84258 23.1%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 14776 enqueued variables after 321444 conflicts
c [score-dist-15] active 32029 (68%), one 3222 (7%), zero 11554 (25%)
c [score-dist-15] max exp 510, different 429 (84%)
c [score-dist-15] median active exp 503, avg 472.1
c [simplification-15] removed 18880 variables 28.7% (46805 remain 16%)
c [simplification-15] removed 49070 irredundant clauses 11.9% (364228 remain 26%)
c [simplification-15] maximum reduction of 29% = max (29%, 12%)
c [simplification-15] large reduction 29% >= 5% limit
c [simplification-15] next conflict interval 3214 = min (321444/100, 64000)
c [simplification-15] penalized conflict interval 3214 = 1 * 3214
c [simplification-15] hard conflict limit 334658 (soft 324658 + delta 10000)
c [simplification-15] new conflict limit 324658 (hard 334658)
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  730.0   46804   364228    321560    3559   2741 1028623  756   927   61  82%      2   42  568  738   77%
c i  730.0   46803   364228    321609    3600   2742 1028627  748   925   61  81%     -3   39  487  738   66%
c i  730.1   46644   364228    321749    3708   2750 1028631  729   919   61  79%    -14   34  364  736   49%
c i  731.9   46638   364228    324879    6417   2803 1028686  460   885   69  52%    -53   -2  233  713   33%
c i  735.0   46630   364228    328247    9370   2825 1028721  632  1180   91  54%    -48  288 1142  713  160%
c i  736.8   46627   364228    329239   10235   2836 1028735  772  1356   95  57%    -66  458 1356  721  188%
c i  737.0   46626   364228    329322   10316   2836 1028736  789  1370  103  58%    -67  472 1420  722  197%
c i  739.9   46625   364228    330906   11796   2845 1028746 1018  1590  119  64%    -68  678 1513  741  204%
c i  740.0   46624   364228    330908   11797   2845 1028746 1018  1590  119  64%    -68  678 1509  741  204%
c 
c [simplification-16] limit 324663 conflicts (hard 334658) hit after 334658 conflicts
c [quatres-8] found 20897 quaternary clauses 54% in total
c [quatres-8-1] removed 2 duplicate quaternary clauses
c [quatres-8-2] added 16 quaternary resolvents
c [ternres-11] limit 95484970 with penalty 0 = 0 + 0
c [ternres-11] all 46621 free variables schedulable
c [ternres-11] 585 ternary resolvents (0 bin, 585 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-39] removed 280 variables
c [treelook-6] limit 9548497 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 76980 literals 83%
c [treelook-6] scheduling used 2606933 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 9548497 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 9591922 steps
c [treelook-6] 76723 literals remain 83%
c [treelook-6] 14031 variables remain to probed next time 30%
c [treelook-6] removed 93 variables, found 17588 hbrs
c [unhide-16] limit 4774248 with penalty 2 = 0 + 2
c [unhide-16-17] 4 units, 297 failed, 156272 tauts, 0 hbrs, 820350 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 254 transitive binary clauses
c [cce-5] limit of 119356212 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 33
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 32
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 31
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 30
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 29
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 28
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 27
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 26
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 25
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 24
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 23
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 22
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 21
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 20
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 19
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 18
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 17
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 16
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 15
c [cce-5-1] eliminated 2 clauses out of 5 (40%) of length 14
c [cce-5-1] eliminated 9 clauses out of 9 (100%) of length 13
c [cce-5-1] eliminated 4 clauses out of 8 (50%) of length 12
c [cce-5-1] eliminated 8 clauses out of 8 (100%) of length 11
c [cce-5-1] eliminated 4 clauses out of 8 (50%) of length 10
c [cce-5-1] eliminated 7 clauses out of 8 (88%) of length 9
c [cce-5-1] eliminated 5 clauses out of 9 (56%) of length 8
c [cce-5-1] eliminated 16 clauses out of 77 (21%) of length 7
c [cce-5-1] eliminated 577 clauses out of 3533 (16%) of length 6
c [cce-5-1] eliminated 1612 clauses out of 12061 (13%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 2282 large clauses in 119356215 steps
c [cce-5-1] allowing another 59678107 steps for small clauses
c [cce-5-1] scheduling 230710 clauses = 162393 binary + 68317 ternary
c [cce-5-1] tried to eliminate 2598 small clauses 1%
c [cce-5-1] eliminated 504 binary clauses 0%
c [cce-5-1] eliminated 183 ternary clauses 0%
c [cce-5-1] eliminated 687 small clauses 0%
c [cce-5-1] eliminated 1574 small clauses in 119356218 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 3856 covered clauses in round 1
c [cce-5] eliminated 3856 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 46157 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 830 variables 2% in round 1 in 43148876 steps
c [elim-13-1] backward subsumption/strengthening limit 43148800
c [elim-13-1-1] backward checking 4395 touched variables 10%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 3 and strengthened 5 clauses in 1748623 steps
c [elim-13-1] rescheduled 29 variables 0% by backward subsumption
c [elim-13-2] eliminated 2 variables 0% in round 2 in 9745 steps
c [elim-13-2] backward subsumption/strengthening limit 9700
c [elim-13-2-1] backward checking 38 touched variables 0%
c [elim-13-2-1] incomplete backward checking 9 remain 24%
c [elim-13-2] subsumed 2 and strengthened 0 clauses in 9721 steps
c [elim-13-2] rescheduled 3 variables 0% by backward subsumption
c [elim-13-3] no variable eliminated in round 3 in 2720 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 832 = 2% variables out of 46157 scheduled
c [bca-12] limit of 10000000 steps and 690003 added (scaled 2)
c [bca-12] 74535 out of 90652 literals actually usable 82%
c [bca-12] added 112 blocked clauses in 170390 steps
c [sweep-12] limit 28645491 penalty 0 = 0 + 0
c [sweep-12-1] 4039 pos 10.9% + 33010 neg 89.1% = 37049 sched 81.7% ret 8276
c [sweep-12-1] 28710151 steps 647 queries 663.92 avg class size
c [sweep-12-1] 7659 decisions 635 SAT calls 110.77 avg env size
c [sweep-12-1] 25719 variables remain 57% (19495 retained 43%)
c [decomp-41] removed 122 variables
c [sweep-12-1] removed 122 vars (0 failed, 12 eqs, 67 impls)
c [sweep-12] removed 122 vars in TOTAL (1 rounds, 646 queries)
c [sort-queue-16] sorted 12514 enqueued variables after 334658 conflicts
c [score-dist-16] active 32689 (72%), one 1649 (4%), zero 10865 (24%)
c [score-dist-16] max exp 510, different 365 (71%)
c [score-dist-16] median active exp 489, avg 472.3
c [simplification-16] removed 1418 variables 3.0% (45203 remain 16%)
c [simplification-16] removed 21050 irredundant clauses 5.8% (343178 remain 25%)
c [simplification-16] maximum reduction of 6% = max (3%, 6%)
c [simplification-16] large reduction 6% >= 5% limit
c [simplification-16] next conflict interval 3346 = min (334658/100, 64000)
c [simplification-16] penalized conflict interval 3346 = 1 * 3346
c [simplification-16] hard conflict limit 348004 (soft 338004 + delta 10000)
c [simplification-16] new conflict limit 338004 (hard 348004)
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  761.3   45202   343178    335350    8284   3344 773550  891  1563   72  57%    -26  605  163  754   22%
c i  762.7   45201   343178    336996    9669   3348 773559  824  1473   82  56%    -55  501  797  752  106%
c 
c [simplification-17] limit 338004 conflicts (hard 348004) hit after 342844 conflicts
c [quatres-9] found 20461 quaternary clauses 56% in total
c [quatres-9-2] added 2 quaternary resolvents
c [ternres-12] limit 96848858 with penalty 0 = 0 + 0
c [ternres-12] all 45201 free variables schedulable
c [ternres-12] 213 ternary resolvents (0 bin, 213 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-42] removed 2 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 10648 sched 24%, 846 failed, 66 lifted, 403221 hbrs
c [decomp-43] removed 1218 variables
c [basicprobe-6-1] 6113 probes remain 14% after last round
c [basicprobe-6-1] 1304 units = 1223 failed (94%) + 81 lifted (6%)
c [basicprobe-6-1] removed 1706 variables, found 546263 hbrs
c [bate-4] eliminated 2020 asymmetric tautologies during probing
c [unhide-17] limit 4842442 with penalty 2 = 0 + 2
c [unhide-17-19] 3 units, 32 failed, 135958 tauts, 0 hbrs, 353508 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 303 transitive binary clauses
c [transred-13] found 2 units
c [cce-6] limit of 242122146 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 142
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 141
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 140
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 139
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 138
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 137
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 136
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 135
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 134
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 133
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 132
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 131
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 130
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 129
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 128
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 127
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 126
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 125
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 124
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 123
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 122
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 121
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 120
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 119
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 118
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 117
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 116
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 115
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 114
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 113
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 112
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 111
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 110
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 109
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 108
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 107
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 106
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 105
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 104
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 103
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 102
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 101
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 100
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 99
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 98
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 97
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 96
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 95
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 94
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 93
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 92
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 90
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 89
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 88
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 87
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 86
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 85
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 84
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 83
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 82
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 81
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 80
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 79
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 78
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 77
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 76
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 75
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 74
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 73
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 72
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 71
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 70
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 69
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 68
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 67
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 66
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 65
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 64
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 63
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 62
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 61
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 60
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 59
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 58
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 57
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 56
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 55
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 54
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 53
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 52
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 51
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 50
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 49
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 48
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 47
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 46
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 45
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 44
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 43
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 42
c [cce-6-1] eliminated 6 clauses out of 7 (86%) of length 41
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 40
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 39
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 38
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 37
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 36
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 35
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 34
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 33
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 32
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 31
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 30
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 29
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 28
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 27
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 26
c [cce-6-1] eliminated 7 clauses out of 10 (70%) of length 25
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 24
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 23
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 22
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 21
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 20
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 19
c [cce-6-1] eliminated 6 clauses out of 11 (55%) of length 18
c [cce-6-1] eliminated 9 clauses out of 12 (75%) of length 17
c [cce-6-1] eliminated 9 clauses out of 13 (69%) of length 16
c [cce-6-1] eliminated 9 clauses out of 14 (64%) of length 15
c [cce-6-1] eliminated 11 clauses out of 17 (65%) of length 14
c [cce-6-1] eliminated 10 clauses out of 14 (71%) of length 13
c [cce-6-1] eliminated 12 clauses out of 20 (60%) of length 12
c [cce-6-1] eliminated 12 clauses out of 16 (75%) of length 11
c [cce-6-1] eliminated 12 clauses out of 19 (63%) of length 10
c [cce-6-1] eliminated 12 clauses out of 18 (67%) of length 9
c [cce-6-1] eliminated 11 clauses out of 18 (61%) of length 8
c [cce-6-1] eliminated 14 clauses out of 78 (18%) of length 7
c [cce-6-1] eliminated 13 clauses out of 2959 (0%) of length 6
c [cce-6-1] eliminated 1095 clauses out of 9626 (11%) of length 5
c [cce-6-1] eliminated 1103 clauses out of 18337 (6%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 2716 large clauses in 242122148 steps
c [cce-6-1] allowing another 121061074 steps for small clauses
c [cce-6-1] scheduling 229745 clauses = 156873 binary + 72872 ternary
c [cce-6-1] tried to eliminate 4980 small clauses 2%
c [cce-6-1] eliminated 859 binary clauses 1%
c [cce-6-1] eliminated 148 ternary clauses 0%
c [cce-6-1] eliminated 1007 small clauses 0%
c [cce-6-1] eliminated 1327 small clauses in 242122153 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 4043 covered clauses in round 1
c [cce-6] eliminated 4043 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 43439 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 827 variables 2% in round 1 in 34249221 steps
c [elim-14-1] backward subsumption/strengthening limit 34249200
c [elim-14-1-1] backward checking 4493 touched variables 10%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 3 and strengthened 21 clauses in 1613637 steps
c [elim-14-1] rescheduled 61 variables 0% by backward subsumption
c [elim-14-2] eliminated 2 variables 0% in round 2 in 1334585 steps
c [elim-14-2] backward subsumption/strengthening limit 1334500
c [elim-14-2-1] backward checking 40 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 1 clauses in 155821 steps
c [elim-14-2] rescheduled 5 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 88721 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 829 = 2% variables out of 43439 scheduled
c [bca-13] limit of 10000000 steps and 629209 added (scaled 2)
c [bca-13] 68701 out of 85222 literals actually usable 81%
c [bca-13] added 75 blocked clauses in 157148 steps
c [sweep-13] limit 29054657 penalty 0 = 0 + 0
c [sweep-13-1] 2988 pos 12.0% + 21934 neg 88.0% = 24922 sched 58.5% ret 17688
c [sweep-13-1] 29059420 steps 1087 queries 458.55 avg class size
c [sweep-13-1] 8852 decisions 1055 SAT calls 77.69 avg env size
c [sweep-13-1] 18274 variables remain 43% (24325 retained 57%)
c [decomp-44] removed 122 variables
c [sweep-13-1] removed 122 vars (0 failed, 31 eqs, 122 impls)
c [sweep-13] removed 122 vars in TOTAL (1 rounds, 1086 queries)
c [sort-queue-17] sorted 10834 enqueued variables after 342844 conflicts
c [score-dist-17] active 31654 (75%), one 1454 (3%), zero 9380 (22%)
c [score-dist-17] max exp 510, different 353 (69%)
c [score-dist-17] median active exp 483, avg 466.2
c [simplification-17] removed 2713 variables 6.0% (42488 remain 15%)
c [simplification-17] removed 29391 irredundant clauses 8.6% (313787 remain 23%)
c [simplification-17] maximum reduction of 9% = max (6%, 9%)
c [simplification-17] large reduction 9% >= 5% limit
c [simplification-17] next conflict interval 3428 = min (342844/100, 64000)
c [simplification-17] penalized conflict interval 3428 = 1 * 3428
c [simplification-17] hard conflict limit 356272 (soft 346272 + delta 10000)
c [simplification-17] new conflict limit 346272 (hard 356272)
c 
c [simplification-18] limit 346272 conflicts (hard 356272) hit after 346272 conflicts
c [quatres-10] found 17881 quaternary clauses 56% in total
c [quatres-10-1] removed 1 duplicate quaternary clauses
c [quatres-10-2] added 3 quaternary resolvents
c [ternres-13] limit 97494501 with penalty 0 = 0 + 0
c [ternres-13] all 42488 free variables schedulable
c [ternres-13] 390 ternary resolvents (2 bin, 388 trn)
c [ternres-13] fully completed ternary resolution
c [simpleprobe-7] all 42488 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-46] removed 462 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 462 variables, found 123720 hbrs, 151 units
c [unhide-18] limit 9749450 with penalty 1 = 0 + 1
c [unhide-18-23] 0 units, 66 failed, 113586 tauts, 0 hbrs, 141951 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 234 transitive binary clauses
c [cce-7] limit of 487472507 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 134
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 133
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 132
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 131
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 130
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 129
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 128
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 127
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 126
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 125
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 124
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 123
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 122
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 121
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 120
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 119
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 118
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 117
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 116
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 115
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 114
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 113
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 112
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 111
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 110
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 109
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 108
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 107
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 106
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 105
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 104
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 103
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 102
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 101
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 100
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 99
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 98
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 97
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 96
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 95
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 94
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 93
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 92
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 90
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 89
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 88
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 87
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 86
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 85
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 84
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 83
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 82
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 81
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 80
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 79
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 78
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 77
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 76
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 75
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 74
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 73
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 71
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 70
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 69
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 68
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 67
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 66
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 65
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 64
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 63
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 62
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 61
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 60
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 59
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 58
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 57
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 56
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 55
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 54
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 53
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 52
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 51
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 50
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 49
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 48
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 47
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 46
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 45
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 44
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 43
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 42
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 41
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 40
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 39
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 38
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 37
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 36
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 35
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 34
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 33
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 32
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 31
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 30
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 29
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 28
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 27
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 26
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 25
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 24
c [cce-7-1] eliminated 3 clauses out of 9 (33%) of length 23
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 22
c [cce-7-1] eliminated 3 clauses out of 10 (30%) of length 21
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 20
c [cce-7-1] eliminated 3 clauses out of 9 (33%) of length 19
c [cce-7-1] eliminated 7 clauses out of 13 (54%) of length 18
c [cce-7-1] eliminated 6 clauses out of 12 (50%) of length 17
c [cce-7-1] eliminated 7 clauses out of 12 (58%) of length 16
c [cce-7-1] eliminated 7 clauses out of 13 (54%) of length 15
c [cce-7-1] eliminated 7 clauses out of 14 (50%) of length 14
c [cce-7-1] eliminated 6 clauses out of 14 (43%) of length 13
c [cce-7-1] eliminated 8 clauses out of 17 (47%) of length 12
c [cce-7-1] eliminated 8 clauses out of 15 (53%) of length 11
c [cce-7-1] eliminated 10 clauses out of 22 (45%) of length 10
c [cce-7-1] eliminated 8 clauses out of 19 (42%) of length 9
c [cce-7-1] eliminated 14 clauses out of 22 (64%) of length 8
c [cce-7-1] eliminated 13 clauses out of 78 (17%) of length 7
c [cce-7-1] eliminated 15 clauses out of 2966 (1%) of length 6
c [cce-7-1] eliminated 137 clauses out of 8441 (2%) of length 5
c [cce-7-1] eliminated 1309 clauses out of 16690 (8%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 1784 large clauses in 379047398 steps
c [cce-7-1] allowing another 189523699 steps for small clauses
c [cce-7-1] scheduling 206693 clauses = 149827 binary + 56866 ternary
c [cce-7-1] tried to eliminate 14402 small clauses 7%
c [cce-7-1] eliminated 2477 binary clauses 2%
c [cce-7-1] eliminated 461 ternary clauses 1%
c [cce-7-1] eliminated 2938 small clauses 1%
c [cce-7-1] eliminated 2960 small clauses in 487472516 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 4744 covered clauses in round 1
c [cce-7] eliminated 4744 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 41972 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 455 variables 1% in round 1 in 31424666 steps
c [elim-15-1] backward subsumption/strengthening limit 31424600
c [elim-15-1-1] backward checking 2655 touched variables 6%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 9 and strengthened 14 clauses in 1022216 steps
c [elim-15-1] rescheduled 45 variables 0% by backward subsumption
c [elim-15-2] eliminated 2 variables 0% in round 2 in 999632 steps
c [elim-15-2] backward subsumption/strengthening limit 999600
c [elim-15-2-1] backward checking 20 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 33418 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 457 = 1% variables out of 41972 scheduled
c [bca-14] limit of 10000000 steps and 601748 added (scaled 2)
c [bca-14] 65881 out of 83032 literals actually usable 79%
c [bca-14] added 146 blocked clauses in 152775 steps
c [sweep-14] limit 29248350 penalty 0 = 0 + 0
c [sweep-14-1] 2459 pos 13.8% + 15325 neg 86.2% = 17784 sched 42.8% ret 23731
c [sweep-14-1] 29266238 steps 1245 queries 365.42 avg class size
c [sweep-14-1] 9035 decisions 1205 SAT calls 65.65 avg env size
c [sweep-14-1] 11557 variables remain 28% (29947 retained 72%)
c [decomp-47] removed 55 variables
c [sweep-14-1] removed 55 vars (0 failed, 39 eqs, 148 impls)
c [sweep-14] removed 55 vars in TOTAL (1 rounds, 1244 queries)
c [sort-queue-18] sorted 10322 enqueued variables after 346272 conflicts
c [score-dist-18] active 31138 (75%), one 1369 (3%), zero 8953 (22%)
c [score-dist-18] max exp 509, different 338 (66%)
c [score-dist-18] median active exp 497, avg 471.2
c [simplification-18] removed 1028 variables 2.4% (41460 remain 14%)
c [simplification-18] removed 13677 irredundant clauses 4.4% (300110 remain 22%)
c [simplification-18] maximum reduction of 4% = max (2%, 4%)
c [simplification-18] geometric conflict interval increment 12800 = 64000 / 5
c [simplification-18] new conflict interval 76800
c [simplification-18] penalized conflict interval 76800 = 1 * 76800
c [simplification-18] hard conflict limit 461472 (soft 423072 + delta 38400)
c [simplification-18] new conflict limit 423072 (hard 461472)
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  826.1   41459   300110    347103   12234   5098 806547  644  1114   86  58%     64  101  576  743   78%
c i  839.6   41455   300110    363810   24032   5163 806592  671  1068  141  63%    156   55  718  710  101%
c i  859.0   41453   300110    382989   34889   5228 806635  754   946  213  80%    178  -69  782  720  109%
c -  893.7   41452   300110    414099   24334   5270 806677  829  1069   97  78%    309   59  974  736  132%
c 
c [simplification-19] limit 423072 conflicts (hard 461472) hit after 423078 conflicts
c [quatres-11] found 16062 quaternary clauses 54% in total
c [ternres-14] limit 113529935 with penalty 0 = 0 + 0
c [ternres-14] all 41452 free variables schedulable
c [ternres-14] 194 ternary resolvents (2 bin, 192 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-5] limit 1419124 penalty 4 = 4 + 0
c [gauss-5] extracted 16 xors of average arity 3.0
c [gauss-5] connected 48 occurrences of 44 variables (average 1.1)
c [gauss-5] limit 1419124 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-48] removed 1 variables
c [treelook-7] limit 11352993 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 66954 literals 81%
c [treelook-7] scheduling used 2005156 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 11352993 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 11358394 steps
c [treelook-7] 66597 literals remain 80%
c [treelook-7] 11537 variables remain to probed next time 28%
c [treelook-7] removed 13 variables, found 31609 hbrs
c [unhide-19] limit 2500000 with penalty 3 = 0 + 3
c [unhide-19-25] 0 units, 10 failed, 34032 tauts, 0 hbrs, 756279 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 188 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 5676496790 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 66 (2%) of length 7
c [cce-8-1] eliminated 3 clauses out of 2966 (0%) of length 6
c [cce-8-1] eliminated 8 clauses out of 8294 (0%) of length 5
c [cce-8-1] eliminated 59 clauses out of 15422 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 71 large clauses in 373556337 steps
c [cce-8-1] allowing another 186778168 steps for small clauses
c [cce-8-1] scheduling 216771 clauses = 146872 binary + 69899 ternary
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 3032 basic ate = 2826 trn 93% + 206 lrg 7% in 4 updates
c bcas: 14 count, 1615 added (3017 skipped), 4417938 steps
c bkwd: tried 447448 clauses, 894569 lits, 2.00 lits/clause
c bkwd: checked 14321176 occs, 32.01 occs/clause, 16.01 occs/lit
c bkwd: subsumed 6 binary, 247 ternary, 41 large
c bkwd: strengthened 2 binary, 0 ternary (0% self), 511 large (0% self)
c blkd: 5 bces, 12766 removed, 8761241 resolutions, 24401201 steps
c blkd: 19669 blocking literals 3%, 70 pure
c bump: 422737 bumped seen, 749072839 lits 1772.0 on average
c card: 5 count, 0 units, 0 am1, 179038578 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 54412 subsumed
c card: 25037 at-most-one constraints found, average size 4.73
c card: 25037 at-most-one constraints used 100%, average size 4.73
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: 8 cces, 86046 eliminated, 85116 ate 99%, 930 abce 1%
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: 4670846 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 141 gcs, 0 rescored clauses, 1635 rescored vars
c dcps: 49 decompositions, 77832 equivalent 26%
c deco: 229490 decision-only clauses 54%, 55% reduction
c decs: 14278594 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 91048 eliminated 30%, 7 pure 0%
c elms: 39 rounds, 2.6 rounds/bve
c elms: 60899 small 67%, 30072 large 33%
c elms: 191866 tried small, 60899 succeeded 32%, 130967 failed 68%
c elms: 51770 subsumed, 117082 strengthened, 1193 blocked
c elms: 25115658 copies, 24795716 resolutions, 5151296 ipos
c elms: 7363985 subchks, 4631261 strchks
c gaus: 5 extractions, 138 extracted, 2.7 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 16707638 steps, 8353819 extr 50%, 805 elim 0%
c glue: 776.7 orig avg, 776.7 real avg, 12.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2635913 = 331843 simple 13% + 2265879 trn 86% + 38191 lrg 1%, 4164 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 422737 clauses, 956.0 length
c lrnd: 404124242 lits = 686164975 orig - 282040733 removed 41%
c lrnd: 195844 uips 46%, 210148 flips 50%
c mins: 58598 mins 20%, 1776 bin 1%, 2785 size 1%
c mins: 23220490 poisoned searches, 4965447 hits, 21% hit rate
c mins: 29080178 used twice searches, 4090402 hits, 14% hit rate
c move: moved 56550, 43480 bin 77%, 13070 trn 23%
c otfs: 4212 driving 39%, 6727 restarting 61%
c otfs: str 10939, 10840 red 99%, 99 irr 1%
c otfs: str 10939, 0 bin 0%, 71 trn 1%, 10868 lrg 99%
c otfs: sub 38, 38 red 100%, 0 irr 0%
c otfs: sub 38, 0 bin 0%, 0 trn 0%, 38 lrg 100%
c phas: 15 computed, 116810 set, 10 pos (0%), 116800 neg (100%)
c prbs: 6 basic, 59212 probed, 3772 failed, 110 lifted
c prbs: 7 simple, 924339 probed, 1181 failed, 2846 eqs
c prbs: 7 treelook, 674 probed, 90 failed, 0 lifted
c prom: 656 locked 0% out of 142266 tried
c prps: 1746962064 props, 114 props/dec
c prps: 93% srch, 7% simp, 0% lkhd
c quat: 11 count, 31 quat, 5 self1, 0 self2, 1663 dup
c queu: 18 sorted, 14278594 next (49977 steps 0.00)
c queu: 818414162 enq (1092151260 steps 1.33), 749072839 deq 92%
c redc: 1617 clauses 24%, 6825 tried 2%, 35 sat 1%
c redc: 3774 lits 7%, 51110 tried 0%, 35 sat 0%
c redc: 216 times jump level reduced, 139.6 levels on average
c reds: 1 count, 423078.0 conflicts per reduce
c reds: 0 memlim 0%, 1 arith 100%
c reds: 25010 collected 88%, 3523 retired 12%
c rmbd: 56853 removed, 21767 red 38%
c rsts: 7398 restarts 88%, 1013 skipped 12%
c rsts: 1013 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: 19 count, 17 confs 89%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 422737 count (698087 tried 1.7), 215782 sub out of 417851 (51.6%)
c swps: 14 count, 15 rounds, 14191 queries (946.1/round)
c swps: 11762 sat calls, 59 unsat (0.3% success rate)
c swps: 82961 decisions 7.1, 3871 conflicts 0.3
c swps; 454.0 avg class size, 83.1 avg environment size
c swps: 1 failed, 2941 impls, 2465 equivs
c swp0: 4724 type 0 queries, 3229 unsat (68.4%), 3722 sat (78.8%)
c swp1: 9467 type 1 queries, 6255 unsat (66.1%), 8004 sat (84.5%)
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: 29406559 calls to obtain time
c tops: 88601 fixed 30%, 282 its, 1500.28 confs/it
c trds: 15 transitive reductions, 2639 removed, 18 failed
c trds: 13050 nodes, 37937 edges, 30030920 steps
c trim: 1124782 words, 4.3 MB
c trnr: 14 count, 4 bin, 2667 trn, 204942644 steps
c unhd: 19 count, 25 rounds, 83723517 steps
c unhd: 678 non-trivial sccs of average size 2.2
c unhd: 44 units, 44 bin, 0 trn, 0 lrg
c unhd: 3186 failed, 2999 stamp, 0 lits, 98 bin, 11 trn, 0 lrg
c unhd: 714540 tauts, 27594 bin 4%, 8607 trn 1%, 483 lrg 0%
c unhd: 714540 tauts, 677856 stamp 95%, 652894 red 91%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 10861785 str, 44 bin 0%, 1880 trn 0%, 10859861 lrg 100%, 10832120 red 100%
c vars: 41419 remaining 14% and 257481 removed 86% out of 298900
c vars: 88601 fixed 30%, 91048 eliminated 30%, 77832 equivalent 26%
c vsts: 12511121471 visits, 91% srch, 9% simp, 0% lkhd
c vsts: 7.0 search visits per propagation, 26834.3 per conflict
c wchs: 961605553 pushed, 56285327 enlarged, 208 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         417882         25010          3523      29077482       4699850        169483
c 
c  0 0          5045   1         0   0         0   0   6888739  24    307896   7      6218   4     0.1
c  1 5           758   0         0   0        57   2   1513363   5     82056   2      1238   1     0.0
c  2 6          1617   0        12   0        51   1   2034581   7    138993   3      2288   1     0.1
c  3 9          2401   1        87   0        71   2   2314004   8    210727   4      4778   3     0.2
c  4 14         2936   1       104   0        85   2   1906975   7    227653   5      6996   4     0.4
c  5 21         2924   1       112   0        46   1   1082859   4    144155   3      6028   4     0.6
c  6 30         3984   1       126   1        97   3   1428955   5<   244303   5      6815   4     0.9
c  7 41         3881   1       127   1        75   2    903079   3    149353   3      6864   4     0.9
c  8 54         3687   1       231   1        55   2    980492   3    207390   4      6407   4     1.2
c  9 69         4283   1       264   1        62   2    743570   3    196530   4<     6623   4     1.4
c 10 86         9714   2       423   2       156   4   1822601   6    457010  10     12854   8<    4.3
c 11 126       23364   6      1584   6       242   7<  3193562  11    783378  17     24520  14    13.8
c 12 230       57868  14<     5590  22<      536  15   2781257  10    931321  20     39348  23    46.5
c 13 534      264735  63     16350  65      1990  56   1347967   5    564835  12     33799  20   252.2
c 14 1526      30685   7         0   0         0   0    135478   0     54250   1      4707   3    92.0
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                 12.1          12.3          11.2           5.5           8.7           9.8
c std                  2.3           1.4           3.1           4.7           4.1           3.7
c 
c  147.548  15% bump
c  126.295  13% cce
c   74.678   7% unhide
c   69.500   7% probe
c   31.217   3% sweep
c   22.386   2% elim
c    9.266   1% rescore
c    8.739   1% decide
c    4.150   0% block
c 
c   11.215 < 1% rest (below)
c 
c    3.924   0% bca
c    2.752   0% gauss
c    1.977   0% transred
c    1.463   0% ternres
c    0.575   0% quatres
c    0.525   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    4.722   0% preprocessing     1%
c  352.374  35% inprocessing     99%
c ==================================
c  357.096  36% simplifying
c  642.117  64% search
c ==================================
c  999.223 100% all
c 
c        423078 conflicts,         423.4 confs/sec
c          1537 ternaries,         275.3 confs/ternary
c          2019 binaries,          209.5 confs/binary
c           282 iterations,       1500.3 confs/iteration
c 
c             1 reductions,          0.0 redus/sec, 423078.0 confs/reduction
c          7398 restarts,            7.4 rests/sec,     57.2 confs/restart
c      14278594 decisions,       14289.7 decis/sec,     33.7 decis/conflict
c    1746962064 propagations,  1748321.3 props/sec,    122.3 props/decision
c 
c 999.2 seconds, 433.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
