c launch: /data/cnf/sc2014/app/12pipe_q0_k.cnf.bz2
c host: atom21
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/12pipe_q0_k.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/12pipe_q0_k.cnf.bz2
c no embedded options
c found 'p cnf 136800 4216460' header
c read 136800 variables, 4216460 clauses, 12513320 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=0
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 136799 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] STATIC (--score=0)
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  136799  4216459         0       0      0     0    0     0   93   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1054114 based on 4216459 irredundant clauses
c [card-1] found 2 at-most-one constraints of average size 3.5
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1054114 for elimination
c [card-1] 2 out of 2 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 14 variables
c [simpleprobe-1] all 136786 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 8430660 based on 4215330 irredundant clauses
c [simpleprobe-1] 118915 variables remain 87% (17871 retained 13%)
c [simpleprobe-1] removed 0 variables, found 2716 hbrs, 0 units
c [unhide-1] limit 263458 based on 4215330 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 136786 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 132418 not tried 97% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 4214 = 3% variables out of 136786 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 4205697 negative 100.0% of 4206884 except 1187 0.0%
c [phase-count-1] 602945 positive 14.3% of 4206884 except 3603939 85.7%
c [phase-count-1] less non-negative clauses 1187 than limit 420600 (10.0%)
c [phase-count-1] non-pos/non-neg = 3603939/1187 = 3036.17 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 132572 negative 100%
c [sort-queue-1] sorted 132572 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 132572 (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 4214 variables 3.1% (132572 remain 97%)
c [simplification-1] removed 9575 irredundant clauses 0.2% (4206884 remain 100%)
c [simplification-1] maximum reduction of 3% = max (3%, 0%)
c [simplification-1] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-1] new conflict interval 5000
c [simplification-1] penalized conflict interval 5000 = 1 * 5000
c [simplification-1] hard conflict limit 15000 (soft 5000 + delta 10000)
c [simplification-1] new conflict limit 5000 (hard 15000)
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   10.1  132571  4206884      1016     900     71  2725    9  1479  141   1%      6 1467   41    1 6445%
c i   10.1  132570  4206884      1017     899     71  2726    9  1479  141   1%      6 1466   41    1 6419%
c i   10.1  132569  4206884      1018     899     71  2726    9  1478  141   1%      6 1466   41    1 6394%
c i   10.1  132568  4206884      1019     898     71  2727    9  1478  141   1%      6 1465   41    1 6370%
c i   10.4  132567  4206884      1133     968    105  2736   10  1535  141   1%      5 1520   37    1 5347%
c i   11.1  132566  4206884      1323    1118    116  2753   11  1878  141   1%      5 1858   37    1 4640%
c i   11.1  132565  4206884      1343    1118    124  2764   11  1869  141   1%      4 1849   34    1 4302%
c i   13.5  132564  4206884      2224    1853    199  2794   18  2294  141   1%      6 2246   49    1 3495%
c i   13.5  132563  4206884      2225    1853    199  2794   18  2293  141   1%      6 2245   48    1 3481%
c i   13.5  132562  4206884      2226    1853    199  2794   18  2293  141   1%      6 2245   48    1 3468%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 1535 variables
c [treelook-1] limit 1049864 based on 4199457 irredundant clauses
c [treelook-1] scheduled 79744 literals 30%
c [treelook-1] scheduling used 1049903 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1049864 based on 4199457 irredundant clauses
c [treelook-1] used 1067769 steps
c [treelook-1] 79717 literals remain 30%
c [treelook-1] 74983 variables remain to probed next time 57%
c [treelook-1] removed 0 variables, found 443 hbrs
c [basicprobe-1] limit 33595656 based on 4199457 irredundant clauses
c [basicprobe-1-0] 69952 probes remain 53% after last round
c [basicprobe-1-0] 80 units = 80 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 80 variables, found 29729 hbrs
c [elim-2] 130803 variables 100% will be scheduled this time
c [elim-2] scheduled 130803 variables 100%
c [elim-2] limit of 7936728 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 125651 not tried 96% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 5152 = 4% variables out of 130803 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 125805 enqueued variables after 2226 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 125805 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 6757 variables 5.1% (125805 remain 92%)
c [simplification-2] removed 34856 irredundant clauses 0.8% (4172028 remain 99%)
c [simplification-2] maximum reduction of 5% = max (5%, 1%)
c [simplification-2] forced so keeping old conflict interval 5000
c [simplification-2] conflict limit remains at 5050 (hard 15000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   19.0  125804  4172028      2233    1824    185 31554   18  2289  139   1%      6 2240   47    1 3377%
c i   19.0  125803  4172028      2234    1824    185 31554   18  2288  139   1%      6 2240   47    1 3364%
c i   19.1  125802  4172028      2273    1846    198 31556   18  2282  140   1%      6 2232   45    1 3209%
c i   19.1  125801  4172028      2274    1846    198 31556   18  2282  140   1%      6 2232   45    1 3196%
c i   19.3  125800  4172028      2336    1893    207 31559   18  2294  140   1%      6 2242   39    1 2729%
c i   19.5  125799  4172028      2399    1951    208 31562   18  2325  140   1%      5 2271   37    1 2521%
c i   19.5  125798  4172028      2408    1957    209 31562   18  2327  140   1%      5 2272   36    1 2461%
c i   19.5  125797  4172028      2409    1957    209 31562   18  2326  140   1%      5 2271   36    1 2451%
c i   19.5  125796  4172028      2412    1957    211 31562   18  2325  140   1%      5 2270   35    1 2424%
c i   20.2  125795  4172028      2595    2117    220 31570   18  2536  140   1%      5 2475   33    2 2148%
c i   20.9  125794  4172028      2808    2314    231 31573   20  2765  140   1%      4 2695   38    2 2269%
c i   21.0  125793  4172028      2857    2353    234 31577   20  2772  140   1%      4 2701   37    2 2216%
c i   21.2  125792  4172028      2922    2415    236 31577   20  2785  140   1%      4 2711   37    2 2151%
c i   21.3  125791  4172028      2964    2444    247 31578   20  2877  140   1%      4 2801   37    2 2140%
c i   21.3  125790  4172028      2965    2444    247 31578   20  2876  140   1%      3 2800   37    2 2132%
c i   21.5  125789  4172028      3018    2478    258 31583   20  2925  140   1%      3 2847   34    2 1940%
c i   21.5  125788  4172028      3019    2478    258 31583   20  2925  140   1%      3 2846   34    2 1933%
c i   21.6  125787  4172028      3056    2510    261 31583   20  2965  140   1%      3 2885   32    2 1822%
c i   21.6  125786  4172028      3057    2510    261 31583   20  2964  140   1%      3 2884   32    2 1815%
c i   21.7  125785  4172028      3075    2525    261 31583   20  2971  140   1%      3 2891   33    2 1829%
c i   21.9  125784  4172028      3143    2583    267 31584   21  2963  140   1%      3 2879   35    2 1902%
c i   21.9  125783  4172028      3144    2583    267 31584   21  2962  140   1%      3 2879   35    2 1894%
c i   23.2  125782  4172028      3575    2923    331 31598   22  3212  140   1%      3 3109   28    2 1407%
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   25.5  125678  4172028      4318    3598    369 31605   24  3758  140   1%      5 3617   40    2 1646%
c i   27.0  125677  4172028      4757    3971    410 31614   25  3779  141   1%      4 3614   34    3 1309%
c i   27.6  125676  4172028      4932    4099    429 31622   25  3770  141   1%      4 3596   28    3 1055%
c i   27.6  125675  4172028      4933    4098    429 31623   25  3769  141   1%      4 3595   28    3 1051%
c 
c [simplification-3] limit 5135 conflicts (hard 15000) hit after 5140 conflicts
c [card-2] limit 1043007 based on 4172028 irredundant clauses
c [card-2] found 1 at-most-one constraints of average size 4.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1043007 for elimination
c [card-2] 1 out of 1 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 6145 variables
c [simpleprobe-2] 104053 schedulable variables 87%
c [simpleprobe-2] limit 8225370 based on 4112685 irredundant clauses
c [simpleprobe-2] 99124 variables remain 83% (20536 retained 17%)
c [simpleprobe-2] removed 0 variables, found 3415 hbrs, 0 units
c [unhide-2] limit 257042 based on 4112685 irredundant clauses
c [unhide-2-2] 1 units, 1 failed, 101 tauts, 0 hbrs, 5739 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 119658 variables 100%
c [elim-3] limit of 18690047 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 113481 not tried 95% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 6177 = 5% variables out of 119658 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 113481 enqueued variables after 5140 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 113481 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 12028 variables 9.6% (113481 remain 83%)
c [simplification-3] removed 72986 irredundant clauses 1.7% (4099042 remain 97%)
c [simplification-3] maximum reduction of 10% = max (10%, 2%)
c [simplification-3] large reduction 10% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 17140 (soft 7140 + delta 10000)
c [simplification-3] new conflict limit 7140 (hard 17140)
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   35.0  113480  4099042      5246    4242    394 32851   26  3805  138   1%      3 3613   28    3  992%
c i   35.6  113479  4099042      5414    4375    417 32853   26  3863  138   1%      3 3663   26    3  928%
c i   35.6  113478  4099042      5416    4375    418 32853   26  3861  138   1%      3 3661   26    3  921%
c i   35.7  113477  4099042      5457    4410    422 32854   26  3850  138   1%      3 3647   26    3  914%
c i   35.7  113476  4099042      5464    4414    424 32854   26  3846  138   1%      3 3643   26    3  894%
c i   37.1  113475  4099042      5874    4757    460 32863   26  4243  138   1%      3 4016   30    3  996%
c i   37.9  113474  4099042      6169    4988    493 32878   26  4301  138   1%      3 4057   28    3  897%
c i   38.1  113473  4099042      6262    5067    495 32879   26  4284  138   1%      2 4034   30    3  947%
c i   38.1  113472  4099042      6265    5068    495 32880   26  4282  138   1%      2 4032   30    3  937%
c i   38.5  113471  4099042      6379    5160    510 32885   26  4327  138   1%      2 4070   29    3  902%
c i   38.5  113470  4099042      6387    5160    512 32890   26  4319  138   1%      2 4062   28    3  875%
c i   38.5  113469  4099042      6393    5161    513 32893   26  4313  138   1%      2 4055   28    3  856%
c i   38.5  113468  4099042      6402    5165    515 32895   26  4304  138   1%      2 4045   27    3  828%
c i   38.5  113419  4099042      6406    5164    518 32896   26  4300  138   1%      2 4041   26    3  816%
c i   39.2  113418  4099042      6666    5388    539 32899   27  4309  138   1%      2 4034   31    3  942%
c i   39.2  113417  4099042      6667    5388    539 32899   27  4307  138   1%      2 4033   31    3  939%
c i   39.7  113416  4099042      6858    5560    544 32901   27  4320  138   1%      2 4034   30    3  886%
c 
c [simplification-4] limit 7164 conflicts (hard 17140) hit after 7164 conflicts
c [decomp-7] removed 2459 variables
c [unhide-3] limit 255032 based on 4080517 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 1004 tauts, 0 hbrs, 7581 literals
c [elim-4] 110875 variables 100% will be scheduled this time
c [elim-4] scheduled 110875 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 505708355 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 39438 not tried 36% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 39302 = 35% variables out of 110875 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 71720 enqueued variables after 7164 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 71720 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 41696 variables 36.8% (71720 remain 52%)
c [simplification-4] removed 101523 irredundant clauses 2.5% (3997519 remain 95%)
c [simplification-4] maximum reduction of 37% = max (37%, 2%)
c [simplification-4] large reduction 37% >= 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 19164 (soft 9164 + delta 10000)
c [simplification-4] new conflict limit 9164 (hard 19164)
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   59.9   71719  3997517      8664    5828    196 15208   29  4740  139   1%     15 4342   34    4  809%
c i   59.9   71718  3997517      8665    5827    196 15209   29  4738  139   1%     15 4341   34    4  806%
c i   60.0   71717  3997517      8693    5849    197 15211   29  4753  139   1%     14 4354   34    4  798%
c 
c [simplification-5] limit 9174 conflicts (hard 19164) hit after 9174 conflicts
c [quatres-1] found 13388 quaternary clauses 8% in total
c [quatres-1-2] added 335 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 15990068 based on 3997517 irredundant clauses
c [ternres-1] all 71717 free variables schedulable
c [ternres-1] 3231 ternary resolvents (0 bin, 3231 trn)
c [ternres-1] 856 variables remain 1% (70861 retained 99%)
c [gauss-1] limit 1998758 based on 3997517 irredundant clauses
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-8] removed 7 variables
c [treelook-2] limit 999029 based on 3996118 irredundant clauses
c [treelook-2] scheduled 69156 literals 48%
c [treelook-2] scheduling used 1000424 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 999029 based on 3996118 irredundant clauses
c [treelook-2] used 5512606 steps
c [treelook-2] 69154 literals remain 48%
c [treelook-2] 62715 variables remain to probed next time 87%
c [treelook-2] removed 0 variables, found 136 hbrs
c [transred-1] limit 3996118 based on 3996118 irredundant clauses
c [transred-1] removed 0 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 71710 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 154517312 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 327588 blocked clauses
c [cce-1] limit of 7725865 steps penalty 2 = 0 + 2
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] allowing another 3862956 steps for small clauses
c [cce-1-1] scheduling 3470574 clauses = 3469138 binary + 1436 ternary
c [cce-1-1] tried to eliminate 32 small clauses 0%
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 0 covered clauses in round 1
c [cce-1] eliminated 0 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 70307 variables 100%
c [elim-5] limit of 30903462 steps penalty 2 = 0 + 2
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 66834 not tried 95% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 3473 = 5% variables out of 70307 scheduled
c [bca-1] limit of 10000000 steps and 7330614 added (scaled 2)
c [bca-1] 113772 out of 133670 literals actually usable 85%
c [bca-1] added 2558 blocked clauses in 356948 steps
c [sweep-1] limit 7330114 based on 3665057 irredundant clauses
c [sweep-1-1] 834 pos 1.2% + 66000 neg 98.8% = 66834 sched 100.0% ret 0
c [sweep-1-1] 7335712 steps 228 queries 1735.94 avg class size
c [sweep-1-1] 7569 decisions 222 SAT calls 266.46 avg env size
c [sweep-1-1] 21628 variables remain 32% (44951 retained 68%)
c [decomp-10] removed 263 variables
c [sweep-1-1] removed 263 vars (0 failed, 10 eqs, 29 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 263 vars in TOTAL (1 rounds, 227 queries)
c [sort-queue-5] sorted 66571 enqueued variables after 9174 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 66571 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 5146 variables 7.2% (66571 remain 49%)
c [simplification-5] removed 373259 irredundant clauses 9.3% (3624258 remain 86%)
c [simplification-5] maximum reduction of 9% = max (7%, 9%)
c [simplification-5] large reduction 9% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 21174 (soft 11174 + delta 10000)
c [simplification-5] new conflict limit 11174 (hard 21174)
c 
c [simplification-6] limit 11174 conflicts (hard 21174) hit after 11175 conflicts
c [quatres-2] found 12909 quaternary clauses 7% in total
c [quatres-2-2] added 296 quaternary resolvents
c [ternres-2] limit 14497032 based on 3624258 irredundant clauses
c [ternres-2] 820 schedulable variables 1%
c [ternres-2] 2817 ternary resolvents (2 bin, 2815 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 906064 based on 3624258 irredundant clauses
c [card-3] no at-most-one constraint found
c [card-3] no at-most-two constraint found
c [basicprobe-2] limit 28994064 based on 3624258 irredundant clauses
c [basicprobe-2-0] 56003 probes remain 84% after last round
c [basicprobe-2-0] 109 units = 109 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 109 variables, found 6950 hbrs
c [bate-1] eliminated 130 asymmetric tautologies during probing
c [unhide-4] limit 226508 based on 3624128 irredundant clauses
c [unhide-4-4] 109 units, 5 failed, 292 tauts, 0 hbrs, 172306 literals
c [block-2] scheduling all variables this time
c [block-2] scheduled 66350 variables 100%
c [block-2] limit of 18183192 steps penalty 2 = 0 + 2
c [block-2] incomplete 10721 not tried 16%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 1705 blocked clauses
c [block-2] 1705 < 1/100 * 3603439 = 36034 considered unsuccessful
c [elim-6] 36580 variables 55% will be scheduled this time
c [elim-6] scheduled 36580 variables 55%
c [elim-6] limit of 36366385 steps penalty 2 = 0 + 2
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 32377 not tried 49% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 130 = 0% variables out of 36580 scheduled
c [elim-6] 130 < 1/100 * 36580 = 365 considered unsuccessful
c [bca-2] limit of 10000000 steps and 7155377 added (scaled 2)
c [bca-2] 106848 out of 132434 literals actually usable 81%
c [bca-2] added 17904 blocked clauses in 356166 steps
c [sweep-2] limit 7153598 based on 3576799 irredundant clauses
c [sweep-2-1] 664 pos 3.1% + 20889 neg 96.9% = 21553 sched 32.5% ret 44663
c [sweep-2-1] 7211769 steps 241 queries 1048.76 avg class size
c [sweep-2-1] 10093 decisions 235 SAT calls 324.35 avg env size
c [sweep-2-1] 11397 variables remain 17% (54224 retained 83%)
c [decomp-12] removed 620 variables
c [sweep-2-1] removed 620 vars (0 failed, 7 eqs, 19 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 620 vars in TOTAL (1 rounds, 240 queries)
c [sort-queue-6] sorted 65596 enqueued variables after 11175 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 65596 (100%)
c [score-dist-6] max exp 0, different 1 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 975 variables 1.5% (65596 remain 48%)
c [simplification-6] removed 146800 irredundant clauses 4.1% (3477458 remain 82%)
c [simplification-6] maximum reduction of 4% = max (1%, 4%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 9000
c [simplification-6] penalized conflict interval 9000 = 1 * 9000
c [simplification-6] hard conflict limit 30175 (soft 20175 + delta 10000)
c [simplification-6] new conflict limit 20175 (hard 30175)
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  108.0   65595  3477457     12279    9494   6087 52655   30  4745  130   1%     39 4116   28    6  498%
c i  115.2   65594  3477456     15824   12748   6149 52733   33  4434  131   1%     38 3599   33    7  454%
c 
c [simplification-7] limit of 382 binary hit after 382 binaries
c [quatres-3] found 13778 quaternary clauses 9% in total
c [quatres-3-2] added 498 single-self-subsuming ternary resolvents
c [quatres-3-2] added 363 quaternary resolvents
c [ternres-3] limit 13909824 based on 3477456 irredundant clauses
c [ternres-3] all 65594 free variables schedulable
c [ternres-3] 635 ternary resolvents (0 bin, 635 trn)
c [ternres-3] 21357 variables remain 33% (44237 retained 67%)
c [gauss-2] limit 1738728 based on 3477456 irredundant clauses
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 2 variables
c [unhide-5] limit 217275 based on 3476412 irredundant clauses
c [unhide-5-5] 0 units, 0 failed, 4311 tauts, 0 hbrs, 4501 literals
c [transred-2] limit 3471330 based on 3471330 irredundant clauses
c [transred-2] removed 4 transitive binary clauses
c [cce-2] limit of 6060060 steps penalty 3 = 1 + 2
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 3043732 steps for small clauses
c [cce-2-1] scheduling 3298752 clauses = 3296802 binary + 1950 ternary
c [cce-2-1] tried to eliminate 27 small clauses 0%
c [cce-2-1] eliminated 1 binary clauses 0%
c [cce-2-1] eliminated 1 small clauses 0%
c [cce-2-1] eliminated 1 small clauses in 6061894 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1 covered clauses in round 1
c [cce-2] eliminated 1 covered clauses in TOTAL during 1 rounds
c [cce-2] 1 < 1/100 * 3471328 = 34713 considered unsuccessful
c [bca-3] limit of 10000000 steps and 6953385 added (scaled 2)
c [bca-3] 93034 out of 131186 literals actually usable 71%
c [bca-3] added 20 blocked clauses in 306782 steps
c [sweep-3] limit 6942654 based on 3471327 irredundant clauses
c [sweep-3-1] 608 pos 5.3% + 10770 neg 94.7% = 11378 sched 17.3% ret 54214
c [sweep-3-1] 7020333 steps 273 queries 1055.27 avg class size
c [sweep-3-1] 13996 decisions 260 SAT calls 319.11 avg env size
c [sweep-3-1] 7596 variables remain 12% (57692 retained 88%)
c [decomp-14] removed 329 variables
c [sweep-3-1] removed 329 vars (0 failed, 15 eqs, 33 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 329 vars in TOTAL (1 rounds, 272 queries)
c [sort-queue-7] sorted 65263 enqueued variables after 16018 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 65263 (100%)
c [score-dist-7] max exp 0, different 1 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 331 variables 0.5% (65263 remain 48%)
c [simplification-7] removed 58684 irredundant clauses 1.7% (3418772 remain 81%)
c [simplification-7] maximum reduction of 2% = max (1%, 2%)
c [simplification-7] forced so keeping old conflict interval 9000
c [simplification-7] conflict limit remains at 20175 (hard 30175)
c [simplification-7] new binary interval 1000
c 
c [simplification-8] limit 20175 conflicts (hard 30175) hit after 20175 conflicts
c [quatres-4] found 14684 quaternary clauses 10% in total
c [quatres-4-2] added 341 single-self-subsuming ternary resolvents
c [quatres-4-2] added 262 quaternary resolvents
c [ternres-4] limit 13675084 based on 3418771 irredundant clauses
c [ternres-4] 21237 schedulable variables 33%
c [ternres-4] 501 ternary resolvents (0 bin, 501 trn)
c [ternres-4] 14 variables remain 0% (65249 retained 100%)
c [transred-3] limit 3418771 based on 3418771 irredundant clauses
c [transred-3] removed 2 transitive binary clauses
c [block-3] 9944 variables 15% will be scheduled this time
c [block-3] scheduled 9944 variables 15%
c [block-3] limit of 14530743 steps penalty 3 = 1 + 2
c [block-3] incomplete 9630 not tried 15%
c [block-3] transition to [ all 0 rem 1 ] state
c [block-3] eliminated 31161 blocked clauses
c [block-3] 31161 < 1/100 * 3418771 = 34187 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 64704 variables 100%
c [elim-7] limit of 29061487 steps penalty 3 = 1 + 2
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 47667 not tried 74% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 618 = 1% variables out of 64704 scheduled
c [elim-7] 618 < 1/100 * 64704 = 647 considered unsuccessful
c [bca-4] limit of 10000000 steps and 6750949 added (scaled 2)
c [bca-4] 84467 out of 128174 literals actually usable 66%
c [bca-4] added 9855 blocked clauses in 283112 steps
c [sweep-4] limit 6740208 based on 3370104 irredundant clauses
c [sweep-4-1] 498 pos 6.8% + 6773 neg 93.2% = 7271 sched 11.3% ret 56815
c [sweep-4-1] 6770373 steps 265 queries 905.48 avg class size
c [sweep-4-1] 14985 decisions 250 SAT calls 269.71 avg env size
c [sweep-4-1] 5068 variables remain 8% (58855 retained 92%)
c [decomp-16] removed 270 variables
c [sweep-4-1] removed 270 vars (0 failed, 18 eqs, 28 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 270 vars in TOTAL (1 rounds, 264 queries)
c [sort-queue-8] sorted 63816 enqueued variables after 20175 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 63816 (100%)
c [score-dist-8] max exp 0, different 1 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 1447 variables 2.2% (63816 remain 47%)
c [simplification-8] removed 73467 irredundant clauses 2.1% (3345304 remain 79%)
c [simplification-8] maximum reduction of 2% = max (2%, 2%)
c [simplification-8] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-8] new conflict interval 15666
c [simplification-8] penalized conflict interval 15666 = 1 * 15666
c [simplification-8] hard conflict limit 45841 (soft 35841 + delta 10000)
c [simplification-8] new conflict limit 35841 (hard 45841)
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  145.7   63815  3345301     25501   21727   5384 57005   35  4256  132   1%    123 2939   38   11  349%
c i  164.5   63766  3345297     34537   29960   5537 57171   35  4091  136   1%    106 2416   32   14  227%
c 
c [simplification-9] limit 35841 conflicts (hard 45841) hit after 35842 conflicts
c [quatres-5] found 11414 quaternary clauses 9% in total
c [quatres-5-2] added 47 single-self-subsuming ternary resolvents
c [quatres-5-2] added 310 quaternary resolvents
c [ternres-5] limit 13381188 based on 3345297 irredundant clauses
c [ternres-5] 11 schedulable variables 0%
c [ternres-5] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-17] removed 170 variables
c [simpleprobe-3] 53016 schedulable variables 83%
c [simpleprobe-3] limit 6645918 based on 3322959 irredundant clauses
c [simpleprobe-3] 53137 variables remain 83% (10509 retained 17%)
c [simpleprobe-3] removed 0 variables, found 691 hbrs, 0 units
c [unhide-6] limit 207684 based on 3322959 irredundant clauses
c [unhide-6-6] 0 units, 0 failed, 2221 tauts, 0 hbrs, 21003 literals
c [transred-4] limit 3320023 based on 3320023 irredundant clauses
c [transred-4] removed 3 transitive binary clauses
c [bca-5] limit of 10000000 steps and 6655710 added (scaled 2)
c [bca-5] 69089 out of 127294 literals actually usable 54%
c [bca-5] added 439 blocked clauses in 237020 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 14494217 penalty 2 = 0 + 2
c [sweep-5-1] 380 pos 7.7% + 4566 neg 92.3% = 4946 sched 7.8% ret 58700
c [sweep-5-1] 14532781 steps 396 queries 508.81 avg class size
c [sweep-5-1] 25320 decisions 386 SAT calls 292.74 avg env size
c [sweep-5-1] 3028 variables remain 5% (60618 retained 95%)
c [decomp-19] removed 13 variables
c [sweep-5-1] removed 13 vars (0 failed, 13 eqs, 28 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 13 vars in TOTAL (1 rounds, 395 queries)
c [sort-queue-9] sorted 63633 enqueued variables after 35842 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 63633 (100%)
c [score-dist-9] max exp 0, different 1 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 58 variables 0.1% (63633 remain 47%)
c [simplification-9] removed 25374 irredundant clauses 0.8% (3319923 remain 79%)
c [simplification-9] maximum reduction of 1% = max (0%, 1%)
c [simplification-9] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-9] new conflict interval 25666
c [simplification-9] penalized conflict interval 25666 = 1 * 25666
c [simplification-9] hard conflict limit 74341 (soft 61508 + delta 12833)
c [simplification-9] new conflict limit 61508 (hard 74341)
c 
c [simplification-10] limit 61508 conflicts (hard 74341) hit after 61509 conflicts
c [quatres-6] found 12732 quaternary clauses 9% in total
c [quatres-6-2] added 40 single-self-subsuming ternary resolvents
c [quatres-6-2] added 308 quaternary resolvents
c [ternres-6] limit 13279576 based on 3319894 irredundant clauses
c [ternres-6] all 63633 free variables schedulable
c [ternres-6] 197 ternary resolvents (0 bin, 197 trn)
c [ternres-6] 19089 variables remain 30% (44544 retained 70%)
c [card-4] limit 829973 based on 3319894 irredundant clauses
c [card-4] found 1 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 829973 for elimination
c [card-4] 1 out of 1 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1659947 based on 3319894 irredundant clauses
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-5] limit 3319894 based on 3319894 irredundant clauses
c [transred-5] removed 0 transitive binary clauses
c [cce-3] limit of 9572179 steps penalty 4 = 2 + 2
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 4786211 steps for small clauses
c [cce-3-1] scheduling 3187836 clauses = 3171097 binary + 16739 ternary
c [cce-3-1] tried to eliminate 16 small clauses 0%
c [cce-3-1] eliminated 5 binary clauses 0%
c [cce-3-1] eliminated 5 small clauses 0%
c [cce-3-1] eliminated 5 small clauses in 9576125 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 5 covered clauses in round 1
c [cce-3] eliminated 5 covered clauses in TOTAL during 1 rounds
c [cce-3] 5 < 1/100 * 3319894 = 33198 considered unsuccessful
c [bca-6] limit of 10000000 steps and 6655666 added (scaled 2)
c [bca-6] 58386 out of 127268 literals actually usable 46%
c [bca-6] added 0 blocked clauses in 219349 steps
c [sweep-6] limit 6639778 based on 3319889 irredundant clauses
c [sweep-6-1] 291 pos 9.6% + 2736 neg 90.4% = 3027 sched 4.8% ret 60606
c [sweep-6-1] 6644967 steps 195 queries 598.60 avg class size
c [sweep-6-1] 13949 decisions 181 SAT calls 445.24 avg env size
c [sweep-6-1] 2479 variables remain 4% (61154 retained 96%)
c [decomp-21] removed 12 variables
c [sweep-6-1] removed 12 vars (0 failed, 13 eqs, 23 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 12 vars in TOTAL (1 rounds, 194 queries)
c [sort-queue-10] sorted 63621 enqueued variables after 61509 conflicts
c [score-dist-10] active 0 (0%), one 0 (0%), zero 63621 (100%)
c [score-dist-10] max exp 0, different 1 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 12 variables 0.0% (63621 remain 47%)
c [simplification-10] removed 9 irredundant clauses 0.0% (3319885 remain 79%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 25666
c [simplification-10] new conflict interval 51332
c [simplification-10] penalized conflict interval 51332 = 1 * 51332
c [simplification-10] hard conflict limit 138507 (soft 112841 + delta 25666)
c [simplification-10] new conflict limit 112841 (hard 138507)
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 -  225.5   63621  3319885     62301   12481   5813 57280   39  4241  123   1%    329 1655   37   22  167%
c 
c [simplification-11] limit 112841 conflicts (hard 138507) hit after 112841 conflicts
c [quatres-7] found 13369 quaternary clauses 10% in total
c [quatres-7-2] added 7 single-self-subsuming ternary resolvents
c [quatres-7-2] added 280 quaternary resolvents
c [ternres-7] limit 13279080 based on 3319770 irredundant clauses
c [ternres-7] 19087 schedulable variables 30%
c [ternres-7] 210 ternary resolvents (0 bin, 210 trn)
c [ternres-7] fully completed ternary resolution
c [block-4] scheduling all variables this time
c [block-4] scheduled 63621 variables 100%
c [block-4] limit of 31329639 steps penalty 4 = 2 + 2
c [block-4] incomplete 11964 not tried 19%
c [block-4] transition to [ all 1 rem 1 ] state
c [block-4] eliminated 78564 blocked clauses
c [elim-8] 30385 variables 49% will be scheduled this time
c [elim-8] scheduled 30385 variables 49%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1000000000 steps penalty 4 = 2 + 2
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1412 variables 2% in round 1 in 479022675 steps
c [elim-8-1] backward subsumption/strengthening limit 479022600
c [elim-8-1-1] backward checking 13868 touched variables 22%
c [elim-8-1-1] incomplete backward checking 14287 remain 103%
c [elim-8-1] subsumed 3 and strengthened 1406 clauses in 479023153 steps
c [elim-8-1] rescheduled 2385 variables 4% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 10271616 steps
c [elim-8-2] backward subsumption/strengthening limit 10271600
c [elim-8-2-1] backward checking 14400 touched variables 23%
c [elim-8-2-1] incomplete backward checking 14410 remain 100%
c [elim-8-2] subsumed 0 and strengthened 70 clauses in 10273514 steps
c [elim-8-2] rescheduled 352 variables 1% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 3046466 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1413 = 5% variables out of 30385 scheduled
c [sweep-7] limit 6185522 based on 3092761 irredundant clauses
c [sweep-7-1] 184 pos 7.5% + 2281 neg 92.5% = 2465 sched 4.1% ret 58270
c [sweep-7-1] 6215638 steps 238 queries 358.92 avg class size
c [sweep-7-1] 15581 decisions 229 SAT calls 328.24 avg env size
c [sweep-7-1] 1801 variables remain 3% (58934 retained 97%)
c [decomp-23] removed 7 variables
c [sweep-7-1] removed 7 vars (0 failed, 8 eqs, 9 impls)
c [sweep-7] 7 < 1/1000 * 60735 = 60 considered unsuccessful
c [sweep-7] removed 7 vars in TOTAL (1 rounds, 237 queries)
c [sort-queue-11] sorted 60728 enqueued variables after 112841 conflicts
c [score-dist-11] active 0 (0%), one 0 (0%), zero 60728 (100%)
c [score-dist-11] max exp 0, different 1 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 2893 variables 4.5% (60728 remain 44%)
c [simplification-11] removed 227019 irredundant clauses 6.8% (3092751 remain 73%)
c [simplification-11] maximum reduction of 7% = max (5%, 7%)
c [simplification-11] large reduction 7% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 124841 (soft 114841 + delta 10000)
c [simplification-11] new conflict limit 114841 (hard 124841)
c 
c [simplification-12] limit 114841 conflicts (hard 124841) hit after 114843 conflicts
c [quatres-8] found 17995 quaternary clauses 10% in total
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 443 quaternary resolvents
c [ternres-8] limit 12703024 with penalty 2 = 0 + 2
c [ternres-8] all 60728 free variables schedulable
c [ternres-8] 2122 ternary resolvents (0 bin, 2122 trn)
c [ternres-8] 39782 variables remain 66% (20946 retained 34%)
c [treelook-3] limit 773181 based on 3092725 irredundant clauses
c [treelook-3] scheduled 57306 literals 47%
c [treelook-3] scheduling used 775414 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 773181 based on 3092725 irredundant clauses
c [treelook-3] used 2687647 steps
c [treelook-3] 57304 literals remain 47%
c [treelook-3] 51936 variables remain to probed next time 86%
c [treelook-3] removed 0 variables, found 32 hbrs
c [unhide-7] limit 193295 based on 3092725 irredundant clauses
c [unhide-7-7] 0 units, 0 failed, 22850 tauts, 0 hbrs, 16541 literals
c [transred-6] limit 3069197 based on 3069197 irredundant clauses
c [transred-6] removed 6 transitive binary clauses
c [bca-7] limit of 10000000 steps and 6154274 added (scaled 2)
c [bca-7] 60165 out of 121458 literals actually usable 50%
c [bca-7] added 272 blocked clauses in 155492 steps
c [sort-queue-12] sorted 60728 enqueued variables after 114843 conflicts
c [score-dist-12] active 0 (0%), one 0 (0%), zero 60728 (100%)
c [score-dist-12] max exp 0, different 1 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 0 variables 0.0% (60728 remain 44%)
c [simplification-12] removed 23532 irredundant clauses 0.8% (3069193 remain 73%)
c [simplification-12] maximum reduction of 1% = max (0%, 1%)
c [simplification-12] geometric conflict interval increment 25666 = 51332 / 2
c [simplification-12] new conflict interval 76998
c [simplification-12] penalized conflict interval 76998 = 1 * 76998
c [simplification-12] hard conflict limit 230340 (soft 191841 + delta 38499)
c [simplification-12] new conflict limit 191841 (hard 230340)
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 -  335.8   60728  3069193    118922   20600   8401 34613   37  4745  121   1%    731 1297   36   31  115%
c -  382.1   60728  3069123    165335   26126   8746 35016   38  3815  122   1%    880   77   39   35  111%
c 
c [simplification-13] limit 191841 conflicts (hard 230340) hit after 191848 conflicts
c [quatres-9] found 19033 quaternary clauses 10% in total
c [quatres-9-2] added 52 single-self-subsuming ternary resolvents
c [quatres-9-2] added 334 quaternary resolvents
c [ternres-9] limit 18270082 with penalty 2 = 0 + 2
c [ternres-9] 39782 schedulable variables 66%
c [ternres-9] 1612 ternary resolvents (0 bin, 1612 trn)
c [ternres-9] 1 variables remain 0% (60727 retained 100%)
c [decomp-26] removed 1 variables
c [basicprobe-3] limit 91350414 penalty 2 = 0 + 2
c [basicprobe-3-0] 39297 probes remain 65% after last round
c [basicprobe-3-0] 30 units = 30 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 30 variables, found 21347 hbrs
c [bate-2] eliminated 2 asymmetric tautologies during probing
c [transred-7] limit 3069099 based on 3069099 irredundant clauses
c [transred-7] removed 5 transitive binary clauses
c [block-5] 8029 variables 13% will be scheduled this time
c [block-5] scheduled 8029 variables 13%
c [block-5] limit of 91350414 steps penalty 3 = 1 + 2
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 48284 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 60564 variables 100%
c [elim-9] limit of 100000000 steps penalty 3 = 1 + 2
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 35362 not tried 58% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 5306 = 9% variables out of 60564 scheduled
c [bca-8] limit of 10000000 steps and 5899790 added (scaled 2)
c [bca-8] 53634 out of 110518 literals actually usable 49%
c [bca-8] added 3760 blocked clauses in 166424 steps
c [sweep-8] limit 5883766 based on 2941883 irredundant clauses
c [sweep-8-1] 74 pos 5.7% + 1230 neg 94.3% = 1304 sched 2.4% ret 53954
c [sweep-8-1] 5912696 steps 117 queries 281.66 avg class size
c [sweep-8-1] 9336 decisions 115 SAT calls 353.52 avg env size
c [sweep-8-1] 1038 variables remain 2% (54220 retained 98%)
c [decomp-27] removed 1 variables
c [sweep-8-1] removed 1 vars (0 failed, 1 eqs, 4 impls)
c [sweep-8] 1 < 1/1000 * 55258 = 55 considered unsuccessful
c [sweep-8] removed 1 vars in TOTAL (1 rounds, 116 queries)
c [sort-queue-13] sorted 55257 enqueued variables after 191848 conflicts
c [score-dist-13] active 0 (0%), one 0 (0%), zero 55257 (100%)
c [score-dist-13] max exp 0, different 1 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 5471 variables 9.0% (55257 remain 40%)
c [simplification-13] removed 127231 irredundant clauses 4.1% (2941881 remain 70%)
c [simplification-13] maximum reduction of 9% = max (9%, 4%)
c [simplification-13] large reduction 9% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 203848 (soft 193848 + delta 10000)
c [simplification-13] new conflict limit 193848 (hard 203848)
c 
c [simplification-14] limit 193848 conflicts (hard 203848) hit after 199723 conflicts
c [quatres-10] found 17124 quaternary clauses 10% in total
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [quatres-10-2] added 161 quaternary resolvents
c [ternres-10] limit 37490823 with penalty 1 = 0 + 1
c [ternres-10] 1 schedulable variables 0%
c [ternres-10] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1470939 based on 2941878 irredundant clauses
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-8] limit 2941878 based on 2941878 irredundant clauses
c [transred-8] removed 2 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 55257 variables 100%
c [block-6] limit of 374908236 steps penalty 1 = 0 + 1
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 348221 blocked clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 234317647 steps penalty 4 = 3 + 1
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 340
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 339
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 317
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 305
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 304
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 303
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 301
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 300
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 299
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 298
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 297
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 294
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 283
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 282
c [cce-4-1] eliminated 3 clauses out of 5 (60%) of length 281
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 280
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 279
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 278
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 277
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 276
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 275
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 274
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 271
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 263
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 261
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 260
c [cce-4-1] eliminated 7 clauses out of 7 (100%) of length 259
c [cce-4-1] eliminated 12 clauses out of 14 (86%) of length 258
c [cce-4-1] eliminated 7 clauses out of 7 (100%) of length 257
c [cce-4-1] eliminated 7 clauses out of 9 (78%) of length 256
c [cce-4-1] eliminated 8 clauses out of 8 (100%) of length 255
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 254
c [cce-4-1] eliminated 8 clauses out of 8 (100%) of length 253
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 251
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 243
c [cce-4-1] eliminated 5 clauses out of 5 (100%) of length 241
c [cce-4-1] eliminated 3 clauses out of 7 (43%) of length 240
c [cce-4-1] eliminated 18 clauses out of 22 (82%) of length 239
c [cce-4-1] eliminated 7 clauses out of 9 (78%) of length 238
c [cce-4-1] eliminated 8 clauses out of 11 (73%) of length 237
c [cce-4-1] eliminated 9 clauses out of 10 (90%) of length 236
c [cce-4-1] eliminated 14 clauses out of 20 (70%) of length 235
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 234
c [cce-4-1] eliminated 2 clauses out of 9 (22%) of length 231
c [cce-4-1] eliminated 1 clauses out of 6 (17%) of length 227
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 226
c [cce-4-1] eliminated 2 clauses out of 21 (10%) of length 225
c [cce-4-1] eliminated 4 clauses out of 18 (22%) of length 224
c [cce-4-1] eliminated 3 clauses out of 13 (23%) of length 223
c [cce-4-1] eliminated 19 clauses out of 26 (73%) of length 222
c [cce-4-1] eliminated 8 clauses out of 14 (57%) of length 221
c [cce-4-1] eliminated 1 clauses out of 76 (1%) of length 220
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 217 large clauses in 234319883 steps
c [cce-4-1] allowing another 117159941 steps for small clauses
c [cce-4-1] scheduling 2430920 clauses = 2418287 binary + 12633 ternary
c [cce-4-1] tried to eliminate 214 small clauses 0%
c [cce-4-1] eliminated 15 binary clauses 0%
c [cce-4-1] eliminated 15 small clauses 0%
c [cce-4-1] eliminated 15 small clauses in 234321618 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 232 covered clauses in round 1
c [cce-4] eliminated 232 covered clauses in TOTAL during 1 rounds
c [cce-4] 232 < 1/100 * 2593655 = 25936 considered unsuccessful
c [elim-10] 31292 variables 61% will be scheduled this time
c [elim-10] scheduled 31292 variables 61%
c [elim-10] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 1241 not tried 2% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 77 = 0% variables out of 31292 scheduled
c [elim-10] 77 < 1/100 * 31292 = 312 considered unsuccessful
c [bca-9] limit of 10000000 steps and 5198160 added (scaled 2)
c [bca-9] 45184 out of 102224 literals actually usable 44%
c [bca-9] added 1149 blocked clauses in 172113 steps
c [sort-queue-14] sorted 51111 enqueued variables after 199723 conflicts
c [score-dist-14] active 0 (0%), one 0 (0%), zero 51111 (100%)
c [score-dist-14] max exp 0, different 1 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 4146 variables 7.5% (51111 remain 37%)
c [simplification-14] removed 351750 irredundant clauses 12.0% (2590128 remain 61%)
c [simplification-14] maximum reduction of 12% = max (8%, 12%)
c [simplification-14] large reduction 12% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 211723 (soft 201723 + delta 10000)
c [simplification-14] new conflict limit 201723 (hard 211723)
c 
c [simplification-15] limit 201723 conflicts (hard 211723) hit after 205562 conflicts
c [quatres-11] found 17082 quaternary clauses 10% in total
c [quatres-11-2] added 168 quaternary resolvents
c [card-5] limit 1192233 penalty 5 = 4 + 1
c [card-5] found 1 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1192233 for elimination
c [card-5] 1 out of 1 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [transred-9] limit 2590104 based on 2590104 irredundant clauses
c [transred-9] removed 3 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 51111 variables 100%
c [block-7] limit of 381514638 steps penalty 1 = 0 + 1
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 102 blocked clauses
c [block-7] 102 < 1/100 * 2590102 = 25901 considered unsuccessful
c [bca-10] limit of 10000000 steps and 5198478 added (scaled 2)
c [bca-10] 44272 out of 102224 literals actually usable 43%
c [bca-10] added 0 blocked clauses in 174045 steps
c [sort-queue-15] sorted 51111 enqueued variables after 205562 conflicts
c [score-dist-15] active 0 (0%), one 0 (0%), zero 51111 (100%)
c [score-dist-15] max exp 0, different 1 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 0 variables 0.0% (51111 remain 37%)
c [simplification-15] removed 104 irredundant clauses 0.0% (2590000 remain 61%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 76998
c [simplification-15] new conflict interval 153996
c [simplification-15] penalized conflict interval 153996 = 1 * 153996
c [simplification-15] hard conflict limit 436556 (soft 359558 + delta 76998)
c [simplification-15] new conflict limit 359558 (hard 436556)
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 -  472.9   51111  2589982    212190   30285   8739 55178   42  3650  117   1%    953 -142   44   37  119%
c -  502.1   51111  2589914    254954   32993   8883 55402   44  3475  117   1%    987  -62   47   39  123%
c -  527.8   51111  2589815    297776   34525   9111 55728   41  4577  117   1%   1005 1045   47   39  119%
c -  554.7   51111  2589742    341711   36340   9327 55988   41  2783  118   1%   1014 -850   49   41  120%
c 
c [simplification-16] limit of 3687 binary hit after 3687 binaries
c [quatres-12] found 17710 quaternary clauses 10% in total
c [quatres-12-2] added 259 quaternary resolvents
c [ternres-11] limit 27178361 with penalty 2 = 1 + 1
c [ternres-11] all 51111 free variables schedulable
c [ternres-11] 145 ternary resolvents (0 bin, 145 trn)
c [ternres-11] 17 variables remain 0% (51094 retained 100%)
c [decomp-30] removed 1 variables
c [unhide-8] limit 312500 with penalty 6 = 3 + 3
c [unhide-8-8] 0 units, 0 failed, 1920 tauts, 0 hbrs, 37615 literals
c [transred-10] limit 2589531 based on 2589531 irredundant clauses
c [transred-10] removed 1 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 51110 variables 100%
c [elim-11] limit of 200000000 steps penalty 2 = 1 + 1
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 7204 not tried 14% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 40 = 0% variables out of 51110 scheduled
c [elim-11] 40 < 1/100 * 51110 = 511 considered unsuccessful
c [sweep-9] limit 5178426 based on 2589213 irredundant clauses
c [sweep-9-1] 35 pos 3.4% + 995 neg 96.6% = 1030 sched 2.0% ret 50040
c [sweep-9-1] 5207997 steps 132 queries 217.11 avg class size
c [sweep-9-1] 8991 decisions 115 SAT calls 334.62 avg env size
c [sweep-9-1] 745 variables remain 1% (50325 retained 99%)
c [decomp-31] removed 15 variables
c [sweep-9-1] removed 15 vars (0 failed, 16 eqs, 22 impls)
c [sweep-9] 15 < 1/1000 * 51070 = 51 considered unsuccessful
c [sweep-9] removed 15 vars in TOTAL (1 rounds, 131 queries)
c [sort-queue-16] sorted 51055 enqueued variables after 356631 conflicts
c [score-dist-16] active 0 (0%), one 0 (0%), zero 51055 (100%)
c [score-dist-16] max exp 0, different 1 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 56 variables 0.1% (51055 remain 37%)
c [simplification-16] removed 532 irredundant clauses 0.0% (2589197 remain 61%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] forced so keeping old conflict interval 153996
c [simplification-16] conflict limit remains at 359558 (hard 436556)
c [simplification-16] new binary interval 10000
c 
c [simplification-17] limit 359558 conflicts (hard 436556) hit after 359559 conflicts
c [quatres-13] found 17986 quaternary clauses 10% in total
c [quatres-13-2] added 10 single-self-subsuming ternary resolvents
c [quatres-13-2] added 119 quaternary resolvents
c [ternres-12] limit 54621684 with penalty 1 = 0 + 1
c [ternres-12] 17 schedulable variables 0%
c [ternres-12] 31 ternary resolvents (0 bin, 31 trn)
c [ternres-12] fully completed ternary resolution
c [simpleprobe-4] 42624 schedulable variables 83%
c [simpleprobe-4] limit 12500000 penalty 4 = 3 + 1
c [decomp-33] removed 1 variables
c [simpleprobe-4] 42986 variables remain 84% (8068 retained 16%)
c [simpleprobe-4] removed 1 variables, found 2388 hbrs, 0 units
c [transred-11] limit 2589180 based on 2589180 irredundant clauses
c [transred-11] removed 3 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 51054 variables 100%
c [block-8] limit of 200000000 steps penalty 2 = 1 + 1
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 594 blocked clauses
c [block-8] 594 < 1/100 * 2589179 = 25891 considered unsuccessful
c [bca-11] limit of 10000000 steps and 5195648 added (scaled 2)
c [bca-11] 48036 out of 102110 literals actually usable 47%
c [bca-11] added 763 blocked clauses in 187059 steps
c [sort-queue-17] sorted 51054 enqueued variables after 359559 conflicts
c [score-dist-17] active 0 (0%), one 0 (0%), zero 51054 (100%)
c [score-dist-17] max exp 0, different 1 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 1 variables 0.0% (51054 remain 37%)
c [simplification-17] removed 612 irredundant clauses 0.0% (2588585 remain 61%)
c [simplification-17] maximum reduction of 0% = max (0%, 0%)
c [simplification-17] full geometric conflict interval increment 153996
c [simplification-17] new conflict interval 307992
c [simplification-17] penalized conflict interval 307992 = 1 * 307992
c [simplification-17] hard conflict limit 821547 (soft 667551 + delta 153996)
c [simplification-17] new conflict limit 667551 (hard 821547)
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 -  602.6   51054  2588566    386922   38226   9614 56881   43  3880  117   1%   1019  112   40   41   98%
c -  627.6   51054  2588520    432557   39992   9721 57085   44  3780  118   1%   1022  288   48   42  116%
c -  653.5   51054  2588488    478572   41477   9839 57322   43  3131  117   1%   1023 -322   45   43  106%
c -  678.1   51054  2588463    524862   42626   9996 57610   44  3904  117   1%   1023  344   49   42  115%
c -  704.5   51054  2588420    571871   44065  10103 57860   43  4044  117   1%   1024  559   33   43   78%
c -  731.8   51054  2588404    619381   45719  10157 58067   43  5141  118   1%   1024 1575   49   42  117%
c -  760.7   51054  2588392    668061   46433  10244 58289   44  2636  118   2%   1024 -910   37   43   85%
c 
c [simplification-18] limit 667551 conflicts (hard 821547) hit after 669094 conflicts
c [quatres-14] found 18689 quaternary clauses 10% in total
c [quatres-14-2] added 2 single-self-subsuming ternary resolvents
c [quatres-14-2] added 327 quaternary resolvents
c [ternres-13] limit 84588708 with penalty 1 = 0 + 1
c [ternres-13] all 51054 free variables schedulable
c [ternres-13] 45 ternary resolvents (0 bin, 45 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-34] removed 1 variables
c [transred-12] limit 2588392 based on 2588392 irredundant clauses
c [transred-12] removed 9 transitive binary clauses
c [bca-12] limit of 10000000 steps and 5195636 added (scaled 2)
c [bca-12] 49800 out of 102108 literals actually usable 49%
c [bca-12] added 410 blocked clauses in 195071 steps
c [sort-queue-18] sorted 51053 enqueued variables after 669094 conflicts
c [score-dist-18] active 0 (0%), one 0 (0%), zero 51053 (100%)
c [score-dist-18] max exp 0, different 1 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 1 variables 0.0% (51053 remain 37%)
c [simplification-18] removed 4 irredundant clauses 0.0% (2588388 remain 61%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 307992
c [simplification-18] new conflict interval 615984
c [simplification-18] penalized conflict interval 615984 = 1 * 615984
c [simplification-18] hard conflict limit 1593070 (soft 1285078 + delta 307992)
c [simplification-18] new conflict limit 1285078 (hard 1593070)
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 -  787.7   51053  2588369    717113   47664  10401 59008   44  3441  117   1%   1024 -180   41   43   95%
c -  814.4   51053  2588354    766875   49310  10465 59227   46  2886  118   2%   1024 -606   51   44  117%
c i  818.5   51052  2588347    774947   56255  10495 59279   44  2490  128   2%   1024 -927   34   44   77%
c -  840.6   51052  2588332    817165   50545  10551 59458   45  4133  118   1%  -5147  672   36   44   83%
c -  866.8   51052  2588304    868672   51685  10736 59703   44  3315  118   1%  -1788   99   38   44   85%
c -  894.3   51052  2588300    920752   52807  10812 59965   44  3248  119   1%   -246 -260   44   44  101%
c -  923.4   51052  2588288    973667   53221  10863 60209   42  3375  118   1%    457   20   52   44  116%
c -  951.5   51052  2588277   1027071   54850  10903 60437   42  2600  118   2%    773 -518   37   44   85%
c -  979.1   51052  2588269   1079986   54952  10984 60676   46  2786  118   2%    912 -258   51   44  116%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 132 basic ate = 0 trn 0% + 132 lrg 100% in 2 updates
c bcas: 12 count, 37130 added (26349 skipped), 2809581 steps
c bkwd: tried 157129 clauses, 313724 lits, 2.00 lits/clause
c bkwd: checked 356890438 occs, 2271.32 occs/clause, 1137.59 occs/lit
c bkwd: subsumed 3 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1476 large (0% self)
c blkd: 8 bces, 836219 removed, 107209437 resolutions, 439650475 steps
c blkd: 23193 blocking literals 8%, 7641 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 5 count, 0 units, 0 am1, 29845011 steps
c card: 1 rescheduled, 2 eliminated, 390 resolved, 80 subsumed
c card: 5 at-most-one constraints found, average size 3.60
c card: 5 at-most-one constraints used 100%, average size 3.60
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 4 cces, 238 eliminated, 233 ate 98%, 5 abce 2%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 16729780 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 80 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 34 decompositions, 10039 equivalent 7%
c deco: 11 decision-only clauses 0%, 53% reduction
c decs: 274524034 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 11 elims, 73543 eliminated 54%, 276 pure 0%
c elms: 13 rounds, 1.2 rounds/bve
c elms: 44480 small 60%, 21146 large 29%
c elms: 44512 tried small, 44480 succeeded 100%, 32 failed 0%
c elms: 4324 subsumed, 225464 strengthened, 61740 blocked
c elms: 11228598 copies, 30183575 resolutions, 832057 ipos
c elms: 72570849 subchks, 23296827 strchks
c gaus: 4 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 13802854 steps, 6901427 extr 50%, 0 elim 0%
c glue: 42.0 orig avg, 42.0 real avg, 6.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 72795 = 9210 simple 13% + 63342 trn 87% + 243 lrg 0%, 1688 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1072508 clauses, 134.0 length
c lrnd: 143737934 lits = 163543417 orig - 19805483 removed 12%
c lrnd: 690873 uips 64%, 75535 flips 7%
c mins: 1053165 mins 98%, 6736 bin 1%, 10541 size 1%
c mins: 86183435 poisoned searches, 26490176 hits, 31% hit rate
c mins: 218828250 used twice searches, 25021668 hits, 11% hit rate
c move: moved 780990, 779292 bin 100%, 1698 trn 0%
c otfs: 42041 driving 19%, 182611 restarting 81%
c otfs: str 224652, 219098 red 98%, 5554 irr 2%
c otfs: str 224652, 0 bin 0%, 235 trn 0%, 224417 lrg 100%
c otfs: sub 1000, 126 red 13%, 874 irr 87%
c otfs: sub 1000, 0 bin 0%, 7 trn 1%, 993 lrg 99%
c phas: 1 computed, 132572 set, 0 pos (0%), 132572 neg (100%)
c prbs: 3 basic, 33400 probed, 219 failed, 0 lifted
c prbs: 4 simple, 155801 probed, 0 failed, 1 eqs
c prbs: 3 treelook, 31 probed, 0 failed, 0 lifted
c prom: 72550 locked 12% out of 605959 tried
c prps: 2215902418 props, 8 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 14 count, 3965 quat, 999 self1, 0 self2, 0 dup
c queu: 18 sorted, 274524034 next (0 steps 0.00)
c queu: 1400975 enq (1400956 steps 1.00), 0 deq 0%
c redc: 7464 clauses 19%, 39397 tried 4%, 131 sat 0%
c redc: 30573 lits 7%, 453436 tried 0%, 131 sat 0%
c redc: 933 times jump level reduced, 1265.0 levels on average
c reds: 22 count, 50639.0 conflicts per reduce
c reds: 0 memlim 0%, 22 arith 100%
c reds: 666091 collected 74%, 237269 retired 26%
c rmbd: 7285 removed, 1826 red 25%
c rsts: 14113 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 18 count, 15 confs 83%, 0 vars 0%
c simp: 1 its 6%, 2 bin 11%, 0 trns 0%
c subl: 1072508 count (1233813 tried 1.2), 64528 sub out of 1060321 (6.1%)
c swps: 9 count, 9 rounds, 2076 queries (230.7/round)
c swps: 1993 sat calls, 19 unsat (0.2% success rate)
c swps: 119820 decisions 60.1, 491 conflicts 0.2
c swps; 790.9 avg class size, 317.9 avg environment size
c swps: 0 failed, 195 impls, 101 equivs
c swp0: 688 type 0 queries, 30 unsat (4.4%), 676 sat (98.3%)
c swp1: 1388 type 1 queries, 272 unsat (19.6%), 1299 sat (93.6%)
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: 549048436 calls to obtain time
c tops: 2166 fixed 2%, 62 its, 17968.69 confs/it
c trds: 12 transitive reductions, 38 removed, 0 failed
c trds: 1333 nodes, 38042 edges, 36973793 steps
c trim: 2079601 words, 7.9 MB
c trnr: 13 count, 2 bin, 11546 trn, 163374930 steps
c unhd: 8 count, 8 rounds, 46830431 steps
c unhd: 2 non-trivial sccs of average size 2.0
c unhd: 110 units, 110 bin, 0 trn, 0 lrg
c unhd: 6 failed, 6 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 32699 tauts, 23 bin 0%, 298 trn 1%, 1849 lrg 6%
c unhd: 32699 tauts, 30529 stamp 93%, 4562 red 14%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 265286 str, 110 bin 0%, 1198 trn 0%, 263978 lrg 100%, 82320 red 31%
c vars: 51052 remaining 37% and 85748 removed 63% out of 136800
c vars: 2166 fixed 2%, 73543 eliminated 54%, 10039 equivalent 7%
c vsts: 25411863843 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 11.6 search visits per propagation, 22663.8 per conflict
c wchs: 2126749627 pushed, 190872884 enlarged, 132 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1064286        666091        237269      62376624       5680168        690640
c 
c  0 0         37421   4      4900   1         0   0  37754079  61   1204389  21     40759   6     1.5
c  1 5          9859   1      3306   0      4487   2   3132957   5    178686   3     10233   1     0.3
c  2 6         33227   3     15846   2     11837   5   5848514   9<   427323   8     33041   5     1.0
c  3 9         67897   6     41541   6     17333   7   4394753   7    674130  12     73167  11     2.0
c  4 14       117324  11     83748  13     21177   9   3209654   5    907564  16<   111302  16     3.2
c  5 21       157775  15    114340  17     27167  11   2384294   4    853578  15    125665  18<    3.9
c  6 30       168392  16<   115389  17<    32668  14<  1823589   3    607814  11    121685  18     4.4
c  7 41       167313  16    108847  16     35841  15   1440426   2    404164   7     90769  13     5.5
c  8 54       136509  13     85074  13     33056  14   1083588   2    229407   4     48615   7     5.3
c  9 69        82761   8     48086   7     23586  10    547744   1    106079   2     20213   3     3.6
c 10 86        66188   6     35535   5     22166   9    721934   1     71095   1     12657   2     3.8
c 11 126       18618   2      9086   1      7453   3     33695   0     15234   0      2380   0     1.8
c 12 230        1001   0       393   0       497   0      1396   0       705   0       154   0     0.2
c 13 534           1   0         0   0         1   0         1   0         0   0         0   0     0.0
c 
c avg                  6.0           6.1           6.5           1.5           3.7           5.0
c std                  2.4           2.1           2.5           2.4           2.6           2.3
c 
c  179.438  18% decide
c   72.527   7% block
c   61.901   6% elim
c   18.517   2% probe
c    9.987   1% unhide
c    9.301   1% sweep
c    6.103   1% bca
c 
c   12.921 < 1% rest (below)
c 
c    4.269   0% quatres
c    4.206   0% cce
c    2.454   0% gauss
c    0.755   0% card
c    0.619   0% ternres
c    0.617   0% transred
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    6.684   1% preprocessing     3%
c  204.710  21% inprocessing     97%
c ==================================
c  211.394  21% simplifying
c  786.224  79% search
c ==================================
c  997.623 100% all
c 
c       1114059 conflicts,        1116.7 confs/sec
c          4529 ternaries,         246.0 confs/ternary
c          7411 binaries,          150.3 confs/binary
c            62 iterations,      17968.7 confs/iteration
c 
c            22 reductions,          0.0 redus/sec,  50639.0 confs/reduction
c         14113 restarts,           14.1 rests/sec,     78.9 confs/restart
c     274524034 decisions,      275178.2 decis/sec,    246.4 decis/conflict
c    2215902418 propagations,  2221183.0 props/sec,      8.1 props/decision
c 
c 997.6 seconds, 271.7 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
