%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : GRA173-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n031.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 06:27:35 PM UTC 2026
% Result : Unsatisfiable 98.43s 98.62s
% Output : Refutation 98.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRA173-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.16/0.33 % Computer : n031.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 01:06:53 EDT 2026
% 0.16/0.34 % CPUTime :
% 98.43/98.62 GeoParameters:
% 98.43/98.62
% 98.43/98.62 tptp_input = 1
% 98.43/98.62 tptp_output = 0
% 98.43/98.62 nonempty = 1
% 98.43/98.62 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.43/98.62 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 98.43/98.62
% 98.43/98.62
% 98.43/98.62 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.43/98.62 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.43/98.62
% 98.43/98.62 RuleSystem INPUT:
% 98.43/98.62
% 98.43/98.62 Initial Rules:
% 98.43/98.62 #0: input, references = 16, size of lhs = 2:
% 98.43/98.62 P_z-{F}(V0), P_s-{F}(V1,V0) | FALSE
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1: input, references = 7, size of lhs = 4:
% 98.43/98.62 P_z-{F}(V0), P_s-{F}(V1,V4), P_s-{F}(V2,V4), V1 == V2 | FALSE
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2: input, references = 3, size of lhs = 2:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V1) | FALSE
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #3: input, references = 3, size of lhs = 2:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V1,V1) | FALSE
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #4: input, references = 33, size of lhs = 4:
% 98.43/98.62 P_z-{F}(V0), #-{F} V1, #-{F} V2, V1 == V2 | r-{T}(V1,V2), b-{T}(V1,V2)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #5: input, references = 24, size of lhs = 4:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V3,V1), r-{F}(V3,V2) | FALSE
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #6: input, references = 9, size of lhs = 8:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V1,V3), b-{F}(V3,V2), b-{F}(V4,V1), b-{F}(V4,V2), b-{F}(V5,V4), b-{F}(V5,V1), b-{F}(V5,V2) | FALSE
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #7: input, references = 18, size of lhs = 1:
% 98.43/98.62 #-{F} V0 | EXISTS V1: P_s-{T}(V0,V1)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #8: input, references = 4, size of lhs = 0:
% 98.43/98.62 FALSE | EXISTS V0: P_z-{T}(V0)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 number of initial rules = 9
% 98.43/98.62
% 98.43/98.62 Simplifiers:
% 98.43/98.62 #9: unsound, references = 3, size of lhs = 3:
% 98.43/98.62 P_s-{F}(V0,V1), P_s-{F}(V0,V3), V1 == V3 | FALSE
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #10: unsound, references = 3, size of lhs = 3:
% 98.43/98.62 P_z-{F}(V0), P_z-{F}(V1), V0 == V1 | FALSE
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 number of simplifiers = 2
% 98.43/98.62
% 98.43/98.62 Learnt:
% 98.43/98.62 #13: mergings( V0 == V3; #11 ), references = 17, size of lhs = 6:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, b-{F}(V3,V4), b-{F}(V4,V3) | r-{T}(V2,V3)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #16: mergings( V0 == V3; #14 ), references = 2, size of lhs = 8:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V3,V2), b-{F}(V3,V4), b-{F}(V4,V2), b-{F}(V4,V5), V5 == V1, b-{F}(V3,V5) | r-{T}(V5,V1)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #24: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #19 ), references = 7, size of lhs = 11:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V2), r-{F}(V4,V2), b-{F}(V4,V5), V1 == V5, V5 == V2, V5 == V4, b-{F}(V1,V6), b-{F}(V6,V5) | r-{T}(V1,V5)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #29: mergings( V0 == V3, V3 == V4; #26 ), references = 4, size of lhs = 8:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V2), r-{F}(V4,V2), r-{F}(V4,V5), V1 == V5, V5 == V2 | r-{T}(V1,V5)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #36: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #31 ), references = 6, size of lhs = 10:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V2), r-{F}(V1,V4), b-{F}(V4,V2), #-{F} V5, V1 == V5, V5 == V2, V4 == V5 | b-{T}(V1,V5)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #41: mergings( V0 == V3, V3 == V4; #38 ), references = 7, size of lhs = 8:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, b-{F}(V4,V3), V3 == V4, r-{F}(V5,V2), r-{F}(V5,V3) | r-{T}(V3,V4)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #44: mergings( V0 == V3; #42 ), references = 11, size of lhs = 4:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V3,V2), V3 == V1 | b-{T}(V3,V1)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #58: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9; #50 ), references = 3, size of lhs = 29:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V2), r-{F}(V4,V2), b-{F}(V4,V5), V1 == V5, V5 == V2, V5 == V4, b-{F}(V6,V5), V1 == V6, b-{F}(V1,V7), b-{F}(V7,V8), b-{F}(V8,V7), r-{F}(V9,V7), b-{F}(V9,V10), V1 == V10, V10 == V7, V10 == V9, V10 == V5, b-{F}(V6,V10), b-{F}(V11,V10), b-{F}(V11,V5), b-{F}(V12,V5), b-{F}(V12,V10), b-{F}(V13,V5), V5 == V13, r-{F}(V14,V13), V5 == V14 | r-{T}(V1,V6)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #75: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10; #66 ), references = 1, size of lhs = 22:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V2), r-{F}(V4,V2), r-{F}(V5,V4), r-{F}(V5,V6), V1 == V6, V6 == V2, V6 == V4, b-{F}(V4,V6), b-{F}(V7,V6), b-{F}(V7,V8), V6 == V8, V8 == V5, V8 == V4, b-{F}(V9,V8), b-{F}(V9,V10), V10 == V8, V10 == V6, b-{F}(V11,V10), b-{F}(V11,V6) | r-{T}(V1,V6)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #82: mergings( V0 == V3, V3 == V4, V4 == V5; #78 ), references = 2, size of lhs = 36:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V2), r-{F}(V1,V4), V4 == V2, b-{F}(V2,V5), b-{F}(V5,V2), r-{F}(V6,V2), b-{F}(V6,V7), V7 == V2, V7 == V6, b-{F}(V2,V8), b-{F}(V8,V2), r-{F}(V9,V2), b-{F}(V9,V10), V10 == V2, V10 == V9, V10 == V7, b-{F}(V11,V10), b-{F}(V11,V7), b-{F}(V12,V7), b-{F}(V12,V10), r-{F}(V4,V13), b-{F}(V13,V7), b-{F}(V13,V10), b-{F}(V14,V7), V7 == V14, r-{F}(V15,V14), V7 == V15, #-{F} V16, V16 == V2, V16 == V4, V16 == V7, V16 == V10, V16 == V13 | r-{T}(V16,V2)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #115: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25; #91 ), references = 1, size of lhs = 31:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), V3 == V2, r-{F}(V2,V4), V3 == V4, b-{F}(V4,V3), r-{F}(V5,V4), r-{F}(V5,V3), r-{F}(V6,V4), r-{F}(V6,V3), r-{F}(V7,V2), r-{F}(V8,V2), #-{F} V9, V9 == V1, V9 == V4, V9 == V3, V9 == V2, #-{F} V10, V10 == V3, V10 == V4, V10 == V2, V9 == V10, #-{F} V11, V3 == V11, V11 == V4, V10 == V11, V9 == V11, V11 == V7, V11 == V2, V11 == V8 | r-{T}(V3,V4)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #143: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27; #117 ), references = 2, size of lhs = 32:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), V3 == V2, r-{F}(V2,V4), V3 == V4, r-{F}(V5,V4), r-{F}(V5,V3), r-{F}(V6,V4), r-{F}(V6,V3), r-{F}(V7,V2), r-{F}(V8,V2), r-{F}(V9,V3), r-{F}(V9,V4), #-{F} V10, V10 == V1, V10 == V4, V10 == V3, V10 == V2, #-{F} V11, V11 == V3, V11 == V4, V11 == V2, V10 == V11, #-{F} V12, V3 == V12, V12 == V4, V11 == V12, V10 == V12, V12 == V7, V12 == V2, V12 == V8 | r-{T}(V4,V3)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #172: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28; #145 ), references = 1, size of lhs = 28:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), V3 == V2, r-{F}(V2,V4), V3 == V4, r-{F}(V5,V4), r-{F}(V5,V3), r-{F}(V6,V4), r-{F}(V6,V3), r-{F}(V7,V2), r-{F}(V8,V2), r-{F}(V9,V3), r-{F}(V9,V4), r-{F}(V10,V4), r-{F}(V10,V3), #-{F} V11, #-{F} V12, V12 == V3, V12 == V4, V12 == V2, #-{F} V13, V3 == V13, V13 == V4, V12 == V13, V13 == V7, V13 == V2, V13 == V8 | P_s-{T}(V11,V1), P_s-{T}(V11,V4), P_s-{T}(V11,V3), P_s-{T}(V11,V2), P_s-{T}(V11,V12), P_s-{T}(V11,V13)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #204: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V40, V40 == V42, V42 == V44, V44 == V46; #173 ), references = 1, size of lhs = 34:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), V3 == V2, r-{F}(V2,V4), V3 == V4, r-{F}(V5,V4), r-{F}(V5,V3), r-{F}(V6,V4), r-{F}(V6,V3), r-{F}(V7,V2), r-{F}(V8,V2), r-{F}(V9,V3), r-{F}(V9,V4), r-{F}(V10,V4), r-{F}(V10,V3), P_s-{F}(V11,V4), P_s-{F}(V12,V2), P_s-{F}(V13,V14), V14 == V3, V14 == V4, V14 == V2, P_s-{F}(V15,V16), V3 == V16, V16 == V4, V14 == V16, V16 == V7, V16 == V2, V16 == V8, #-{F} V17, V11 == V17, V12 == V17, V13 == V17, V15 == V17 | P_s-{T}(V17,V1), P_s-{T}(V17,V3)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #237: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31; #205 ), references = 1, size of lhs = 34:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V2), V2 == V1, r-{F}(V1,V3), V2 == V3, r-{F}(V4,V3), r-{F}(V4,V2), r-{F}(V5,V3), r-{F}(V5,V2), r-{F}(V6,V1), r-{F}(V7,V1), r-{F}(V8,V2), r-{F}(V8,V3), r-{F}(V9,V3), r-{F}(V9,V2), P_s-{F}(V10,V3), P_s-{F}(V11,V1), P_s-{F}(V12,V13), V13 == V2, V13 == V3, V13 == V1, P_s-{F}(V14,V15), V2 == V15, V15 == V3, V13 == V15, V15 == V6, V15 == V1, V15 == V7, #-{F} V16, V10 == V16, V11 == V16, V12 == V16, V14 == V16 | P_s-{T}(V16,V2)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #273: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35; #239 ), references = 7, size of lhs = 26:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V6), V1 == V6, V0 == V6, P_s-{F}(V7,V8), V8 == V0, V8 == V6, V8 == V1, P_s-{F}(V9,V10), V0 == V10, V10 == V6, V8 == V10, V10 == V2, V10 == V1, V10 == V3, #-{F} V11, V5 == V11, V4 == V11, V7 == V11, V9 == V11 | b-{T}(V1,V6)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #292: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8; #284 ), references = 7, size of lhs = 14:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V1,V3), V3 == V2, V3 == V1, b-{F}(V4,V3), b-{F}(V4,V5), V5 == V3, b-{F}(V6,V3), b-{F}(V6,V7), V7 == V3, V5 == V7, b-{F}(V8,V7), b-{F}(V8,V5) | b-{T}(V3,V2)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #299: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8; #285 ), references = 1, size of lhs = 14:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V1,V3), V3 == V2, V3 == V1, b-{F}(V4,V3), b-{F}(V4,V5), V5 == V3, b-{F}(V6,V3), b-{F}(V6,V7), V7 == V3, V5 == V7, b-{F}(V8,V7), b-{F}(V8,V5) | b-{T}(V3,V2)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #303: mergings( V2 == V3; #301 ), references = 1, size of lhs = 28:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), V3 == V2, r-{F}(V2,V4), V3 == V4, r-{F}(V5,V4), r-{F}(V5,V3), r-{F}(V6,V4), r-{F}(V6,V3), r-{F}(V7,V2), r-{F}(V8,V2), r-{F}(V9,V3), r-{F}(V9,V4), r-{F}(V4,V10), r-{F}(V10,V3), #-{F} V11, #-{F} V12, V12 == V3, V12 == V4, V12 == V2, #-{F} V13, V3 == V13, V13 == V4, V12 == V13, V13 == V7, V13 == V2, V13 == V8 | P_s-{T}(V11,V1), P_s-{T}(V11,V4), P_s-{T}(V11,V3), P_s-{T}(V11,V2), P_s-{T}(V11,V12), P_s-{T}(V11,V13)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #311: mergings( V0 == V1, V1 == V15, V15 == V17, V17 == V19, V19 == V21, V21 == V23; #304 ), references = 1, size of lhs = 36:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V3 == V2, r-{F}(V4,V2), r-{F}(V4,V3), r-{F}(V5,V3), r-{F}(V5,V2), r-{F}(V2,V6), r-{F}(V6,V3), P_s-{F}(V7,V2), P_s-{F}(V8,V3), r-{F}(V9,V3), V3 == V9, r-{F}(V9,V2), r-{F}(V10,V9), r-{F}(V11,V9), r-{F}(V12,V9), P_s-{F}(V13,V12), P_s-{F}(V14,V15), V15 == V3, V15 == V2, V15 == V9, P_s-{F}(V16,V17), V3 == V17, V17 == V2, V15 == V17, V17 == V10, V17 == V9, V17 == V11, #-{F} V18, V13 == V18, V7 == V18, V8 == V18, V14 == V18, V16 == V18 | P_s-{T}(V18,V9)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #322: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V1; #313 ), references = 4, size of lhs = 28:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), r-{F}(V3,V0), r-{F}(V4,V0), r-{F}(V5,V0), P_s-{F}(V6,V5), P_s-{F}(V7,V8), V8 == V0, V8 == V1, P_s-{F}(V9,V10), V10 == V8, V10 == V1, V10 == V0, P_s-{F}(V11,V12), V8 == V12, V12 == V1, V10 == V12, V12 == V3, V12 == V0, V12 == V4, #-{F} V13, V6 == V13, V2 == V13, V7 == V13, V9 == V13, V11 == V13 | b-{T}(V0,V8)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #405: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V36, V36 == V40, V40 == V44, V44 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74; #345 ), references = 1, size of lhs = 51:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), P_s-{F}(V4,V1), r-{F}(V5,V1), r-{F}(V6,V1), P_s-{F}(V7,V1), r-{F}(V8,V1), r-{F}(V9,V1), P_s-{F}(V10,V1), r-{F}(V0,V11), r-{F}(V11,V0), P_s-{F}(V12,V11), r-{F}(V13,V0), r-{F}(V14,V0), r-{F}(V15,V0), P_s-{F}(V16,V15), P_s-{F}(V17,V18), V18 == V0, V18 == V11, V18 == V1, P_s-{F}(V19,V18), P_s-{F}(V20,V21), V21 == V0, V21 == V18, V21 == V1, P_s-{F}(V22,V23), V23 == V0, V23 == V1, V23 == V18, P_s-{F}(V24,V25), V25 == V0, V25 == V23, V25 == V1, P_s-{F}(V26,V27), V27 == V0, V27 == V1, P_s-{F}(V28,V29), V0 == V29, V27 == V29, V29 == V8, V29 == V1, V29 == V9, P_s-{F}(V30,V31), V31 == V18, V31 == V11, V31 == V0, #-{F} V32 | P_s-{T}(V32,V0), P_s-{T}(V32,V18), P_s-{T}(V32,V21), P_s-{T}(V32,V2), P_s-{T}(V32,V1), P_s-{T}(V32,V3), P_s-{T}(V32,V23), P_s-{T}(V32,V25), P_s-{T}(V32,V5), P_s-{T}(V32,V6), P_s-{T}(V32,V27), P_s-{T}(V32,V29), P_s-{T}(V32,V11), P_s-{T}(V32,V31), P_s-{T}(V32,V13), P_s-{T}(V32,V14), P_s-{T}(V32,V17), P_s-{T}(V32,V4), P_s-{T}(V32,V20), P_s-{T}(V32,V32), P_s-{T}(V32,V22), P_s-{T}(V32,V7), P_s-{T}(V32,V24), P_s-{T}(V32,V10), P_s-{T}(V32,V26), P_s-{T}(V32,V28), P_s-{T}(V32,V16), P_s-{T}(V32,V12), P_s-{T}(V32,V19), P_s-{T}(V32,V30)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #485: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V34, V34 == V38, V38 == V42, V42 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V91, V91 == V93, V93 == V95, V95 == V97, V97 == V99, V99 == V101, V101 == V103, V103 == V105, V105 == V107, V107 == V109, V109 == V111, V111 == V113, V113 == V115, V115 == V117, V117 == V119, V119 == V121, V121 == V123, V123 == V125, V125 == V127, V127 == V129; #406 ), references = 1, size of lhs = 90:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), P_s-{F}(V4,V1), r-{F}(V5,V1), r-{F}(V6,V1), P_s-{F}(V7,V1), r-{F}(V8,V1), r-{F}(V9,V1), P_s-{F}(V10,V1), r-{F}(V0,V11), r-{F}(V11,V0), P_s-{F}(V12,V11), P_s-{F}(V13,V1), P_s-{F}(V14,V11), r-{F}(V15,V0), P_s-{F}(V16,V15), r-{F}(V17,V0), P_s-{F}(V18,V17), r-{F}(V19,V0), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V22 == V0, V22 == V11, V22 == V1, P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V22), P_s-{F}(V26,V25), P_s-{F}(V27,V28), V28 == V0, V28 == V22, V28 == V1, P_s-{F}(V29,V28), P_s-{F}(V30,V29), P_s-{F}(V31,V32), V32 == V0, V32 == V1, V32 == V22, P_s-{F}(V33,V32), P_s-{F}(V34,V33), P_s-{F}(V35,V36), V36 == V0, V36 == V32, V36 == V1, P_s-{F}(V37,V36), P_s-{F}(V38,V37), P_s-{F}(V39,V40), V40 == V0, V40 == V1, P_s-{F}(V41,V40), P_s-{F}(V42,V41), P_s-{F}(V43,V44), V0 == V44, V40 == V44, V44 == V8, V44 == V1, V44 == V9, P_s-{F}(V45,V44), P_s-{F}(V46,V45), P_s-{F}(V47,V48), V48 == V22, V48 == V11, V48 == V0, P_s-{F}(V49,V48), P_s-{F}(V50,V49), P_s-{F}(V51,V52), V21 == V52, V27 == V52, V13 == V52, V31 == V52, V35 == V52, V39 == V52, V43 == V52, V14 == V52, V47 == V52, V16 == V52, V18 == V52, V24 == V52, V30 == V52, V51 == V52, V34 == V52, V38 == V52, V42 == V52, V46 == V52, V26 == V52, V50 == V52 | P_s-{T}(V52,V0), P_s-{T}(V52,V2), P_s-{T}(V52,V3), P_s-{T}(V52,V5), P_s-{T}(V52,V6), P_s-{T}(V52,V4), P_s-{T}(V52,V7), P_s-{T}(V52,V10), P_s-{T}(V52,V20), P_s-{T}(V52,V12)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #574: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V34, V34 == V38, V38 == V42, V42 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V35, V35 == V36, V36 == V39, V39 == V40, V40 == V37, V37 == V41, V41 == V45, V45 == V98, V33 == V97; #486 ), references = 1, size of lhs = 82:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), r-{F}(V0,V4), V0 == V4, P_s-{F}(V0,V4), r-{F}(V4,V0), r-{F}(V5,V4), r-{F}(V6,V4), P_s-{F}(V7,V4), r-{F}(V8,V0), P_s-{F}(V9,V8), r-{F}(V10,V0), P_s-{F}(V11,V10), P_s-{F}(V12,V13), V13 == V0, V13 == V1, V13 == V4, P_s-{F}(V14,V13), P_s-{F}(V15,V14), P_s-{F}(V16,V13), P_s-{F}(V17,V16), P_s-{F}(V18,V19), V19 == V0, V19 == V13, V19 == V4, P_s-{F}(V20,V19), P_s-{F}(V21,V20), P_s-{F}(V22,V23), V23 == V0, V23 == V4, V23 == V13, P_s-{F}(V24,V23), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V27 == V0, V27 == V23, V27 == V4, P_s-{F}(V28,V27), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V31 == V0, V31 == V4, P_s-{F}(V32,V31), P_s-{F}(V33,V32), P_s-{F}(V34,V35), V0 == V35, V31 == V35, V35 == V5, V35 == V4, V35 == V6, P_s-{F}(V36,V35), P_s-{F}(V37,V36), P_s-{F}(V38,V39), V39 == V13, V39 == V1, V39 == V0, P_s-{F}(V40,V39), P_s-{F}(V41,V40), P_s-{F}(V42,V43), V12 == V43, V18 == V43, V7 == V43, V22 == V43, V26 == V43, V30 == V43, V34 == V43, V3 == V43, V38 == V43, V9 == V43, V11 == V43, V15 == V43, V21 == V43, V42 == V43, V25 == V43, V29 == V43, V33 == V43, V37 == V43, V17 == V43, V41 == V43 | P_s-{T}(V43,V2)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #659: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V1, V1 == V80, V80 == V81, V81 == V82, V82 == V83, V2 == V84, V83 == V85; #576 ), references = 1, size of lhs = 73:
% 98.43/98.62 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), r-{F}(V4,V0), P_s-{F}(V5,V4), r-{F}(V6,V0), P_s-{F}(V7,V6), P_s-{F}(V8,V9), V9 == V0, V9 == V1, P_s-{F}(V10,V9), P_s-{F}(V11,V10), P_s-{F}(V12,V9), P_s-{F}(V13,V12), P_s-{F}(V14,V15), V15 == V0, V15 == V9, V15 == V1, P_s-{F}(V16,V15), P_s-{F}(V17,V16), P_s-{F}(V18,V19), V19 == V0, V19 == V1, V19 == V9, P_s-{F}(V20,V19), P_s-{F}(V21,V20), P_s-{F}(V22,V23), V23 == V0, V23 == V19, V23 == V1, P_s-{F}(V24,V23), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V27 == V0, V27 == V1, P_s-{F}(V28,V27), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V27 == V31, V31 == V1, V31 == V0, P_s-{F}(V32,V31), P_s-{F}(V33,V32), P_s-{F}(V34,V35), V35 == V9, V35 == V1, V35 == V0, P_s-{F}(V36,V35), P_s-{F}(V37,V36), P_s-{F}(V38,V39), V8 == V39, V14 == V39, V2 == V39, V18 == V39, V22 == V39, V26 == V39, V30 == V39, V3 == V39, V34 == V39, V5 == V39, V7 == V39, V11 == V39, V17 == V39, V38 == V39, V21 == V39, V25 == V39, V29 == V39, V33 == V39, V13 == V39, V37 == V39 | b-{T}(V0,V1)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #676: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10; #667 ), references = 1, size of lhs = 19:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V1,V2), V1 == V2, r-{F}(V2,V3), b-{F}(V1,V4), V4 == V3, r-{F}(V2,V4), b-{F}(V3,V4), #-{F} V5, V5 == V3, V1 == V5, V5 == V4, V5 == V2, #-{F} V6, V6 == V3, V1 == V6, V6 == V4, V6 == V2, V5 == V6 | r-{T}(V4,V3)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #689: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12; #678 ), references = 3, size of lhs = 17:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, b-{F}(V3,V4), V3 == V4, r-{F}(V4,V3), r-{F}(V4,V2), #-{F} V5, V3 == V5, V5 == V2, V5 == V4, #-{F} V6, V3 == V6, V6 == V2, V6 == V4, V5 == V6 | r-{T}(V3,V2)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #703: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13; #691 ), references = 1, size of lhs = 15:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, b-{F}(V3,V4), V3 == V4, r-{F}(V4,V3), r-{F}(V4,V2), r-{F}(V5,V3), r-{F}(V5,V2), #-{F} V6, #-{F} V7, V3 == V7, V7 == V2, V7 == V4 | P_s-{T}(V6,V3), P_s-{T}(V6,V2), P_s-{T}(V6,V4), P_s-{T}(V6,V7)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #719: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V19, V19 == V21, V21 == V23; #704 ), references = 2, size of lhs = 20:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, b-{F}(V3,V4), V3 == V4, r-{F}(V4,V3), r-{F}(V4,V2), r-{F}(V5,V3), r-{F}(V5,V2), P_s-{F}(V6,V2), P_s-{F}(V7,V4), P_s-{F}(V8,V9), V3 == V9, V9 == V2, V9 == V4, #-{F} V10, V6 == V10, V7 == V10, V8 == V10 | P_s-{T}(V10,V3)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #738: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18; #721 ), references = 6, size of lhs = 16:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V4), V1 == V4, V4 == V0, P_s-{F}(V5,V6), V0 == V6, V6 == V4, V6 == V1, #-{F} V7, V3 == V7, V2 == V7, V5 == V7 | b-{T}(V1,V4)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #741: mergings( V0 == V3; #739 ), references = 2, size of lhs = 5:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V1,V2), V2 == V1, b-{F}(V2,V3), b-{F}(V3,V1) | r-{T}(V2,V1)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #751: mergings( V2 == V5, V5 == V6, V6 == V7, V7 == V8; #746 ), references = 1, size of lhs = 30:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), b-{F}(V1,V3), b-{F}(V4,V3), V3 == V4, r-{F}(V4,V5), V3 == V5, b-{F}(V6,V3), b-{F}(V6,V7), V7 == V3, b-{F}(V1,V7), b-{F}(V5,V8), b-{F}(V8,V3), r-{F}(V5,V9), V9 == V3, P_s-{F}(V10,V11), V0 == V11, V11 == V1, #-{F} V12, #-{F} V13, V12 == V13, V2 == V13, V10 == V13, #-{F} V14, V3 == V14, V14 == V9, V14 == V5 | P_s-{T}(V12,V1), P_s-{T}(V12,V0), P_s-{T}(V12,V3), P_s-{T}(V12,V7), P_s-{T}(V12,V11), P_s-{T}(V12,V9), P_s-{T}(V12,V5), P_s-{T}(V12,V14)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #763: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V19, V19 == V21, V21 == V23, V23 == V25, V25 == V27, V27 == V29; #752 ), references = 1, size of lhs = 41:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), b-{F}(V1,V3), b-{F}(V4,V3), V3 == V4, r-{F}(V4,V5), V3 == V5, b-{F}(V6,V3), b-{F}(V6,V7), V7 == V3, b-{F}(V1,V7), b-{F}(V5,V8), b-{F}(V8,V3), r-{F}(V5,V9), V9 == V3, P_s-{F}(V10,V1), P_s-{F}(V11,V3), P_s-{F}(V12,V7), P_s-{F}(V13,V9), P_s-{F}(V14,V15), V0 == V15, V15 == V1, P_s-{F}(V16,V15), P_s-{F}(V17,V18), V3 == V18, V18 == V9, V18 == V5, #-{F} V19, V10 == V19, V11 == V19, V12 == V19, V16 == V19, V13 == V19, V17 == V19, #-{F} V20, V19 == V20, V2 == V20, V14 == V20 | P_s-{T}(V19,V0), P_s-{T}(V19,V5)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #775: mergings( V3 == V4, V4 == V5, V5 == V6, V6 == V14, V14 == V16, V16 == V18, V18 == V20, V20 == V21, V21 == V23, V23 == V0; #764 ), references = 2, size of lhs = 41:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), b-{F}(V1,V3), b-{F}(V4,V3), V3 == V4, r-{F}(V4,V5), V3 == V5, b-{F}(V6,V3), b-{F}(V6,V7), V7 == V3, b-{F}(V1,V7), b-{F}(V5,V8), b-{F}(V8,V3), r-{F}(V5,V9), V9 == V3, P_s-{F}(V10,V1), P_s-{F}(V11,V3), P_s-{F}(V12,V7), P_s-{F}(V13,V9), P_s-{F}(V14,V15), V0 == V15, V15 == V1, P_s-{F}(V16,V15), P_s-{F}(V17,V18), V3 == V18, V18 == V9, V18 == V5, #-{F} V19, V10 == V19, V11 == V19, V12 == V19, V16 == V19, V13 == V19, V17 == V19, #-{F} V20, V19 == V20, V2 == V20, V14 == V20 | P_s-{T}(V19,V5)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #790: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V1; #777 ), references = 2, size of lhs = 41:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), b-{F}(V1,V3), V3 == V0, b-{F}(V4,V3), V3 == V4, r-{F}(V4,V0), b-{F}(V5,V3), b-{F}(V5,V6), V6 == V3, b-{F}(V1,V6), b-{F}(V0,V7), b-{F}(V7,V3), P_s-{F}(V8,V1), P_s-{F}(V9,V3), P_s-{F}(V10,V6), P_s-{F}(V11,V12), V0 == V12, V12 == V3, P_s-{F}(V13,V14), V0 == V14, V14 == V1, P_s-{F}(V15,V14), P_s-{F}(V16,V17), V3 == V17, V17 == V12, V17 == V0, #-{F} V18, V8 == V18, V9 == V18, V10 == V18, V15 == V18, V11 == V18, V16 == V18, #-{F} V19, V18 == V19, V2 == V19, V13 == V19 | b-{T}(V0,V12)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #909: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V82, V82 == V83, V83 == V84, V79 == V85, V84 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V113, V113 == V114, V114 == V115, V115 == V116, V116 == V121, V121 == V122; #797 ), references = 1, size of lhs = 68:
% 98.43/98.62 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), P_s-{F}(V8,V1), P_s-{F}(V9,V1), r-{F}(V10,V0), P_s-{F}(V11,V10), r-{F}(V12,V0), P_s-{F}(V13,V12), P_s-{F}(V14,V15), V15 == V0, V15 == V1, P_s-{F}(V16,V15), P_s-{F}(V17,V16), P_s-{F}(V18,V15), P_s-{F}(V19,V18), P_s-{F}(V20,V21), P_s-{F}(V22,V21), P_s-{F}(V23,V21), P_s-{F}(V24,V21), P_s-{F}(V25,V26), V26 == V0, V26 == V1, P_s-{F}(V27,V26), P_s-{F}(V28,V27), P_s-{F}(V29,V30), V30 == V0, V30 == V1, P_s-{F}(V31,V30), P_s-{F}(V32,V31), P_s-{F}(V33,V34), V34 == V0, V34 == V1, P_s-{F}(V35,V34), P_s-{F}(V36,V34), P_s-{F}(V37,V38), V0 == V38, V38 == V1, P_s-{F}(V39,V40), V0 == V40, V1 == V40, P_s-{F}(V41,V42), V0 == V42, V42 == V1, P_s-{F}(V43,V42), P_s-{F}(V44,V45), V45 == V40, V45 == V0, P_s-{F}(V46,V47), V0 == V47, V47 == V1, P_s-{F}(V48,V47), P_s-{F}(V49,V50), V34 == V50, V50 == V0, #-{F} V51, V6 == V51, V41 == V51, #-{F} V52, V8 == V52, V46 == V52 | P_s-{T}(V21,V0), P_s-{T}(V21,V15), P_s-{T}(V21,V1), P_s-{T}(V21,V26), P_s-{T}(V21,V30), P_s-{T}(V21,V14), P_s-{T}(V21,V21), P_s-{T}(V21,V2), P_s-{T}(V21,V25), P_s-{T}(V21,V29), P_s-{T}(V21,V3), P_s-{T}(V21,V11), P_s-{T}(V21,V13), P_s-{T}(V21,V17), P_s-{T}(V21,V20), P_s-{T}(V21,V22), P_s-{T}(V21,V28), P_s-{T}(V21,V32), P_s-{T}(V21,V23), P_s-{T}(V21,V19), P_s-{T}(V21,V24), P_s-{T}(V21,V34), P_s-{T}(V21,V38), P_s-{T}(V21,V40), P_s-{T}(V21,V45), P_s-{T}(V21,V50), P_s-{T}(V21,V33), P_s-{T}(V21,V4), P_s-{T}(V21,V5), P_s-{T}(V21,V37), P_s-{T}(V21,V7), P_s-{T}(V21,V35), P_s-{T}(V21,V43), P_s-{T}(V21,V39), P_s-{T}(V21,V44), P_s-{T}(V21,V51), P_s-{T}(V21,V9), P_s-{T}(V21,V36), P_s-{T}(V21,V48), P_s-{T}(V21,V49), P_s-{T}(V21,V52)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1071: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V33, V33 == V80, V80 == V81, V81 == V82, V77 == V83, V82 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V113, V113 == V114, V114 == V119, V119 == V120, V120 == V164, V164 == V166, V166 == V168, V168 == V170, V170 == V172, V172 == V174, V174 == V78, V78 == V176, V176 == V178, V178 == V79, V79 == V122, V83 == V121, V122 == V124, V121 == V123, V124 == V128, V123 == V127, V128 == V180, V180 == V182, V182 == V139, V127 == V138, V126 == V137, V139 == V143, V138 == V142, V137 == V141, V143 == V184, V184 == V130, V142 == V129, V130 == V186, V186 == V188, V188 == V190, V190 == V192, V192 == V194, V194 == V196, V196 == V198, V198 == V102, V102 == V103, V103 == V200, V200 == V116, V116 == V202, V202 == V204, V204 == V206, V206 == V155, V129 == V156, V155 == V208, V208 == V118, V118 == V210, V210 == V212, V212 == V160, V156 == V161; #910 ), references = 1, size of lhs = 90:
% 98.43/98.62 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V1,V5), V5 == V0, V5 == V1, P_s-{F}(V6,V5), P_s-{F}(V7,V5), P_s-{F}(V8,V5), P_s-{F}(V9,V1), P_s-{F}(V10,V1), P_s-{F}(V11,V5), P_s-{F}(V12,V11), P_s-{F}(V13,V5), P_s-{F}(V14,V13), P_s-{F}(V15,V5), P_s-{F}(V16,V15), P_s-{F}(V17,V18), V0 == V18, V18 == V1, P_s-{F}(V19,V18), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V0 == V22, V22 == V1, P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V6 == V26, V4 == V26, V7 == V26, V8 == V26, V12 == V26, V25 == V26, V14 == V26, V16 == V26, V9 == V26, V10 == V26, V20 == V26, V24 == V26, P_s-{F}(V27,V26), P_s-{F}(V28,V27), V28 == V26, P_s-{F}(V29,V26), P_s-{F}(V30,V29), V30 == V26, P_s-{F}(V31,V26), P_s-{F}(V32,V31), V32 == V26, P_s-{F}(V33,V26), P_s-{F}(V34,V33), V34 == V26, P_s-{F}(V35,V36), V36 == V0, V36 == V1, V35 == V26, P_s-{F}(V37,V36), P_s-{F}(V38,V37), V38 == V26, P_s-{F}(V39,V36), P_s-{F}(V40,V39), V40 == V26, P_s-{F}(V41,V36), P_s-{F}(V42,V41), V42 == V26, P_s-{F}(V43,V44), V0 == V44, V44 == V1, V43 == V26, P_s-{F}(V45,V44), P_s-{F}(V46,V45), V46 == V26, P_s-{F}(V47,V48), V0 == V48, V1 == V48, V47 == V26, P_s-{F}(V49,V48), P_s-{F}(V50,V49), V50 == V26, P_s-{F}(V51,V52), V2 == V52, V17 == V52, V51 == V26, #-{F} V53, V3 == V53, V21 == V53 | P_s-{T}(V26,V53)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1232: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V2, V2 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V112, V112 == V113, V113 == V114, V114 == V115, V115 == V117, V117 == V118, V118 == V119, V119 == V120, V120 == V121, V121 == V122, V122 == V123, V123 == V124, V124 == V125, V125 == V126, V126 == V127, V1 == V128, V127 == V131, V131 == V132, V132 == V133, V128 == V134, V129 == V135, V133 == V137, V134 == V138, V135 == V139, V137 == V141, V141 == V142, V138 == V143, V142 == V144, V144 == V145, V145 == V146, V146 == V147, V147 == V148, V148 == V149, V149 == V150, V150 == V151, V151 == V152, V152 == V153, V153 == V154, V154 == V155, V155 == V156, V156 == V157, V157 == V158, V143 == V159, V158 == V161, V161 == V162, V162 == V163, V163 == V164, V164 == V165, V159 == V166, V165 == V168; #1073 ), references = 2, size of lhs = 90:
% 98.43/98.62 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V1,V5), V5 == V0, V5 == V1, P_s-{F}(V6,V5), P_s-{F}(V7,V5), P_s-{F}(V8,V5), P_s-{F}(V9,V1), P_s-{F}(V10,V1), P_s-{F}(V11,V5), P_s-{F}(V12,V11), P_s-{F}(V13,V5), P_s-{F}(V14,V13), P_s-{F}(V15,V5), P_s-{F}(V16,V15), P_s-{F}(V17,V18), V0 == V18, V18 == V1, P_s-{F}(V19,V18), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V0 == V22, V22 == V1, P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V6 == V26, V4 == V26, V7 == V26, V8 == V26, V12 == V26, V25 == V26, V14 == V26, V16 == V26, V9 == V26, V10 == V26, V20 == V26, V24 == V26, P_s-{F}(V27,V26), P_s-{F}(V28,V27), V28 == V26, P_s-{F}(V29,V26), P_s-{F}(V30,V29), V30 == V26, P_s-{F}(V31,V26), P_s-{F}(V32,V31), V32 == V26, P_s-{F}(V33,V26), P_s-{F}(V34,V33), V34 == V26, P_s-{F}(V35,V36), V36 == V0, V36 == V1, V35 == V26, P_s-{F}(V37,V36), P_s-{F}(V38,V37), V38 == V26, P_s-{F}(V39,V36), P_s-{F}(V40,V39), V40 == V26, P_s-{F}(V41,V36), P_s-{F}(V42,V41), V42 == V26, P_s-{F}(V43,V44), V0 == V44, V44 == V1, V43 == V26, P_s-{F}(V45,V44), P_s-{F}(V46,V45), V46 == V26, P_s-{F}(V47,V48), V0 == V48, V1 == V48, V47 == V26, P_s-{F}(V49,V48), P_s-{F}(V50,V49), V50 == V26, P_s-{F}(V51,V52), V2 == V52, V17 == V52, V51 == V26, P_s-{F}(V53,V54), V3 == V54, V21 == V54, V53 == V26 | b-{T}(V1,V0)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1240: mergings( V0 == V1, V1 == V4; #1236 ), references = 2, size of lhs = 18:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), b-{F}(V1,V3), b-{F}(V3,V1), r-{F}(V4,V0), V0 == V4, V4 == V1, P_s-{F}(V5,V4), P_s-{F}(V6,V7), V0 == V7, V7 == V1, V7 == V4, #-{F} V8, V2 == V8, V5 == V8, V6 == V8 | r-{T}(V0,V4)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1244: mergings( V0 == V3, V3 == V4, V4 == V1; #1237 ), references = 1, size of lhs = 18:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), V1 == V0, b-{F}(V1,V2), b-{F}(V2,V1), P_s-{F}(V3,V1), r-{F}(V4,V0), V0 == V4, V4 == V1, P_s-{F}(V5,V4), P_s-{F}(V6,V7), V0 == V7, V7 == V1, V7 == V4, #-{F} V8, V3 == V8, V5 == V8, V6 == V8 | r-{T}(V0,V4)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1263: mergings( V2 == V7, V7 == V8, V8 == V13, V13 == V14, V14 == V23, V23 == V24, V24 == V25, V25 == V26; #1254 ), references = 1, size of lhs = 78:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), P_s-{F}(V4,V1), r-{F}(V0,V5), V0 == V5, r-{F}(V5,V0), r-{F}(V6,V5), r-{F}(V7,V5), P_s-{F}(V8,V5), r-{F}(V0,V9), r-{F}(V9,V0), P_s-{F}(V10,V9), r-{F}(V11,V0), r-{F}(V12,V0), r-{F}(V0,V13), r-{F}(V13,V0), P_s-{F}(V14,V13), r-{F}(V15,V0), r-{F}(V16,V0), r-{F}(V1,V17), b-{F}(V18,V17), b-{F}(V18,V0), b-{F}(V18,V5), b-{F}(V18,V19), r-{F}(V5,V19), b-{F}(V19,V20), b-{F}(V20,V19), b-{F}(V17,V21), b-{F}(V21,V17), b-{F}(V0,V22), r-{F}(V23,V0), P_s-{F}(V24,V23), r-{F}(V25,V0), P_s-{F}(V26,V25), P_s-{F}(V27,V28), V28 == V0, V28 == V5, P_s-{F}(V29,V30), V0 == V30, V28 == V30, V30 == V6, V30 == V5, V30 == V7, P_s-{F}(V31,V32), V32 == V9, V32 == V1, V32 == V17, V18 == V32, V32 == V22, V5 == V32, V32 == V0, P_s-{F}(V33,V32), P_s-{F}(V34,V35), V32 == V35, V35 == V9, V35 == V11, V35 == V0, V35 == V12, P_s-{F}(V36,V37), V0 == V37, V37 == V32, V37 == V2, V37 == V1, V37 == V3, P_s-{F}(V38,V39), V39 == V13, V39 == V0, P_s-{F}(V40,V41), V41 == V13, V39 == V41, V41 == V15, V41 == V0, V41 == V16, #-{F} V42 | P_s-{T}(V42,V0), P_s-{T}(V42,V18), P_s-{T}(V42,V19), P_s-{T}(V42,V13), P_s-{T}(V42,V5), P_s-{T}(V42,V22), P_s-{T}(V42,V28), P_s-{T}(V42,V30), P_s-{T}(V42,V32), P_s-{T}(V42,V9), P_s-{T}(V42,V35), P_s-{T}(V42,V1), P_s-{T}(V42,V37), P_s-{T}(V42,V39), P_s-{T}(V42,V41), P_s-{T}(V42,V42), P_s-{T}(V42,V8), P_s-{T}(V42,V27), P_s-{T}(V42,V29), P_s-{T}(V42,V24), P_s-{T}(V42,V10), P_s-{T}(V42,V31), P_s-{T}(V42,V34), P_s-{T}(V42,V33), P_s-{T}(V42,V4), P_s-{T}(V42,V36), P_s-{T}(V42,V26), P_s-{T}(V42,V14), P_s-{T}(V42,V38), P_s-{T}(V42,V40)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1297: mergings( V0 == V5, V5 == V6, V6 == V11, V11 == V12, V12 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V51, V51 == V53, V53 == V55, V55 == V57, V57 == V59, V59 == V61, V61 == V63, V63 == V65, V65 == V67, V67 == V69, V69 == V71, V71 == V73, V73 == V75, V75 == V77, V77 == V79, V79 == V81, V81 == V83, V83 == V85, V85 == V87, V87 == V89, V89 == V91, V91 == V93, V93 == V95, V95 == V97; #1264 ), references = 1, size of lhs = 125:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), r-{F}(V0,V4), V0 == V4, r-{F}(V4,V0), r-{F}(V5,V4), r-{F}(V6,V4), r-{F}(V0,V7), r-{F}(V7,V0), r-{F}(V8,V0), r-{F}(V9,V0), r-{F}(V0,V10), r-{F}(V10,V0), r-{F}(V11,V0), r-{F}(V12,V0), r-{F}(V1,V13), r-{F}(V4,V14), b-{F}(V14,V15), b-{F}(V15,V14), b-{F}(V13,V16), b-{F}(V16,V13), b-{F}(V0,V17), P_s-{F}(V18,V10), P_s-{F}(V19,V4), P_s-{F}(V20,V17), P_s-{F}(V21,V7), P_s-{F}(V22,V1), P_s-{F}(V23,V4), P_s-{F}(V24,V23), P_s-{F}(V25,V1), P_s-{F}(V26,V25), P_s-{F}(V27,V7), P_s-{F}(V28,V27), P_s-{F}(V29,V10), P_s-{F}(V30,V29), b-{F}(V31,V13), b-{F}(V31,V0), b-{F}(V31,V4), b-{F}(V31,V14), P_s-{F}(V32,V31), r-{F}(V33,V0), P_s-{F}(V34,V33), P_s-{F}(V35,V34), r-{F}(V36,V0), P_s-{F}(V37,V36), P_s-{F}(V38,V37), P_s-{F}(V39,V40), V0 == V40, V40 == V5, V40 == V4, V40 == V6, P_s-{F}(V41,V40), P_s-{F}(V42,V43), V43 == V7, V43 == V8, V43 == V0, V43 == V9, P_s-{F}(V44,V43), P_s-{F}(V45,V46), V0 == V46, V46 == V2, V46 == V1, V46 == V3, P_s-{F}(V47,V46), P_s-{F}(V48,V49), V49 == V10, V49 == V11, V49 == V0, V49 == V12, P_s-{F}(V50,V49), P_s-{F}(V51,V52), V52 == V0, V52 == V4, V52 == V40, P_s-{F}(V53,V52), P_s-{F}(V54,V53), P_s-{F}(V55,V56), V56 == V7, V56 == V1, V56 == V13, V31 == V56, V56 == V17, V4 == V56, V56 == V0, V56 == V43, V46 == V56, P_s-{F}(V57,V56), P_s-{F}(V58,V57), P_s-{F}(V59,V56), P_s-{F}(V60,V59), P_s-{F}(V61,V62), V62 == V10, V62 == V0, V62 == V49, P_s-{F}(V63,V62), P_s-{F}(V64,V63), P_s-{F}(V65,V66), V32 == V66, V18 == V66, V19 == V66, V20 == V66, V51 == V66, V41 == V66, V55 == V66, V21 == V66, V44 == V66, V22 == V66, V47 == V66, V61 == V66, V50 == V66, V65 == V66, V24 == V66, V54 == V66, V35 == V66, V28 == V66, V58 == V66, V60 == V66, V26 == V66, V38 == V66, V30 == V66, V64 == V66 | P_s-{T}(V66,V0), P_s-{T}(V66,V14), P_s-{T}(V66,V39), P_s-{T}(V66,V42), P_s-{T}(V66,V45), P_s-{T}(V66,V48)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1337: mergings( V4 == V9, V9 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V26, V26 == V27, V27 == V29, V29 == V31, V31 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V38, V38 == V39, V39 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V0, V0 == V10, V10 == V22, V22 == V5, V5 == V71, V71 == V74, V72 == V75, V74 == V77, V75 == V78; #1298 ), references = 1, size of lhs = 118:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), r-{F}(V0,V4), r-{F}(V4,V0), r-{F}(V5,V0), r-{F}(V6,V0), r-{F}(V0,V7), r-{F}(V7,V0), r-{F}(V8,V0), r-{F}(V9,V0), b-{F}(V0,V10), b-{F}(V10,V0), b-{F}(V0,V11), P_s-{F}(V12,V7), P_s-{F}(V13,V1), P_s-{F}(V14,V11), P_s-{F}(V15,V4), r-{F}(V0,V16), V0 == V16, r-{F}(V16,V0), r-{F}(V17,V16), r-{F}(V18,V16), r-{F}(V16,V19), b-{F}(V19,V20), b-{F}(V20,V19), P_s-{F}(V21,V16), P_s-{F}(V0,V22), V22 == V2, V22 == V1, V22 == V3, V22 == V4, V22 == V5, V22 == V6, V0 == V22, V22 == V17, V22 == V16, V22 == V18, P_s-{F}(V23,V22), P_s-{F}(V24,V22), P_s-{F}(V25,V22), P_s-{F}(V26,V1), P_s-{F}(V27,V26), P_s-{F}(V28,V16), P_s-{F}(V29,V28), P_s-{F}(V30,V4), P_s-{F}(V31,V30), P_s-{F}(V32,V7), P_s-{F}(V33,V32), b-{F}(V34,V19), b-{F}(V34,V1), b-{F}(V34,V0), P_s-{F}(V35,V34), r-{F}(V36,V0), P_s-{F}(V37,V36), P_s-{F}(V38,V37), r-{F}(V39,V0), P_s-{F}(V40,V39), P_s-{F}(V41,V40), P_s-{F}(V42,V43), V43 == V7, V43 == V8, V43 == V0, V43 == V9, P_s-{F}(V44,V43), P_s-{F}(V45,V46), V46 == V0, V46 == V1, V46 == V22, P_s-{F}(V47,V46), P_s-{F}(V48,V47), P_s-{F}(V49,V50), V50 == V4, V50 == V16, V50 == V19, V34 == V50, V50 == V11, V1 == V50, V50 == V0, V22 == V50, P_s-{F}(V51,V50), P_s-{F}(V52,V51), P_s-{F}(V53,V50), P_s-{F}(V54,V53), P_s-{F}(V55,V56), V56 == V7, V56 == V0, V56 == V43, P_s-{F}(V57,V56), P_s-{F}(V58,V57), P_s-{F}(V59,V60), V35 == V60, V12 == V60, V13 == V60, V14 == V60, V45 == V60, V23 == V60, V49 == V60, V15 == V60, V24 == V60, V21 == V60, V25 == V60, V55 == V60, V44 == V60, V59 == V60, V27 == V60, V48 == V60, V38 == V60, V31 == V60, V52 == V60, V54 == V60, V29 == V60, V41 == V60, V33 == V60, V58 == V60 | P_s-{T}(V60,V42)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1383: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V44, V44 == V47, V45 == V48, V47 == V50, V48 == V51, V50 == V53, V51 == V54; #1341 ), references = 6, size of lhs = 98:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V0,V3), V3 == V0, P_s-{F}(V4,V3), b-{F}(V3,V5), b-{F}(V5,V3), b-{F}(V0,V6), P_s-{F}(V7,V6), P_s-{F}(V0,V8), V8 == V0, P_s-{F}(V9,V8), P_s-{F}(V10,V8), P_s-{F}(V11,V8), P_s-{F}(V12,V8), b-{F}(V0,V13), b-{F}(V13,V0), b-{F}(V14,V0), P_s-{F}(V15,V14), P_s-{F}(V16,V17), V14 == V17, V0 == V17, V17 == V3, V8 == V17, P_s-{F}(V18,V17), P_s-{F}(V19,V17), P_s-{F}(V20,V17), P_s-{F}(V21,V17), P_s-{F}(V22,V17), P_s-{F}(V23,V22), P_s-{F}(V24,V17), P_s-{F}(V25,V24), P_s-{F}(V26,V17), P_s-{F}(V27,V26), P_s-{F}(V28,V17), P_s-{F}(V29,V28), P_s-{F}(V30,V17), P_s-{F}(V31,V30), P_s-{F}(V32,V17), P_s-{F}(V33,V32), P_s-{F}(V34,V35), V0 == V35, V35 == V3, V35 == V17, P_s-{F}(V36,V37), V37 == V0, V37 == V17, V37 == V8, P_s-{F}(V38,V37), P_s-{F}(V39,V38), P_s-{F}(V40,V41), V14 == V41, V41 == V6, V17 == V41, V41 == V0, V8 == V41, P_s-{F}(V42,V41), P_s-{F}(V43,V42), P_s-{F}(V44,V41), P_s-{F}(V45,V44), P_s-{F}(V46,V47), V47 == V17, V47 == V0, V47 == V8, P_s-{F}(V48,V47), P_s-{F}(V49,V48), P_s-{F}(V50,V51), V15 == V51, V18 == V51, V19 == V51, V7 == V51, V36 == V51, V9 == V51, V40 == V51, V20 == V51, V10 == V51, V21 == V51, V11 == V51, V46 == V51, V12 == V51, V50 == V51, V23 == V51, V39 == V51, V31 == V51, V27 == V51, V43 == V51, V45 == V51, V25 == V51, V33 == V51, V29 == V51, V49 == V51, #-{F} V52, V4 == V52, V16 == V52, V34 == V52 | r-{T}(V14,V17)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1390: mergings( V2 == V16, V10 == V24, V16 == V30; #1386 ), references = 1, size of lhs = 126:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V0,V3), V3 == V0, P_s-{F}(V4,V3), b-{F}(V3,V5), b-{F}(V5,V3), b-{F}(V0,V6), P_s-{F}(V7,V6), b-{F}(V0,V8), b-{F}(V8,V0), b-{F}(V0,V9), b-{F}(V9,V0), b-{F}(V0,V10), b-{F}(V10,V0), b-{F}(V0,V11), V11 == V0, P_s-{F}(V12,V11), b-{F}(V11,V13), b-{F}(V13,V11), b-{F}(V0,V14), P_s-{F}(V15,V14), P_s-{F}(V0,V16), V16 == V0, P_s-{F}(V17,V16), P_s-{F}(V18,V16), P_s-{F}(V19,V16), P_s-{F}(V20,V16), P_s-{F}(V21,V16), P_s-{F}(V22,V16), P_s-{F}(V23,V16), P_s-{F}(V24,V16), b-{F}(V0,V25), b-{F}(V25,V0), b-{F}(V26,V0), P_s-{F}(V27,V26), r-{F}(V26,V28), b-{F}(V28,V0), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V26 == V31, V31 == V3, V28 == V31, V0 == V31, V31 == V11, V16 == V31, P_s-{F}(V32,V31), P_s-{F}(V33,V31), P_s-{F}(V34,V31), P_s-{F}(V35,V31), P_s-{F}(V36,V31), P_s-{F}(V37,V31), P_s-{F}(V38,V31), P_s-{F}(V39,V31), P_s-{F}(V40,V31), P_s-{F}(V41,V31), P_s-{F}(V42,V41), P_s-{F}(V43,V31), P_s-{F}(V44,V43), P_s-{F}(V45,V31), P_s-{F}(V46,V45), P_s-{F}(V47,V31), P_s-{F}(V48,V47), P_s-{F}(V49,V31), P_s-{F}(V50,V49), P_s-{F}(V51,V31), P_s-{F}(V52,V51), P_s-{F}(V53,V31), P_s-{F}(V54,V53), P_s-{F}(V55,V31), P_s-{F}(V56,V55), P_s-{F}(V57,V31), P_s-{F}(V58,V57), P_s-{F}(V59,V31), P_s-{F}(V60,V59), P_s-{F}(V61,V31), P_s-{F}(V62,V61), P_s-{F}(V63,V31), P_s-{F}(V64,V63), P_s-{F}(V65,V66), V0 == V66, V66 == V3, V66 == V31, P_s-{F}(V67,V68), V68 == V0, V68 == V31, V68 == V16, P_s-{F}(V69,V68), P_s-{F}(V70,V69), P_s-{F}(V71,V72), P_s-{F}(V73,V72), P_s-{F}(V74,V72), P_s-{F}(V75,V72), P_s-{F}(V76,V77), V77 == V31, V77 == V0, V77 == V16, P_s-{F}(V78,V77), P_s-{F}(V79,V78), P_s-{F}(V80,V81), V0 == V81, V81 == V11, V81 == V31, P_s-{F}(V82,V83), V83 == V0, V83 == V31, V83 == V16, P_s-{F}(V84,V83), P_s-{F}(V85,V84), P_s-{F}(V86,V87), V87 == V31, V87 == V0, V87 == V16, P_s-{F}(V88,V87), P_s-{F}(V89,V88), #-{F} V90, V4 == V90, V30 == V90, V65 == V90, #-{F} V91, V12 == V91, V36 == V91, V80 == V91 | P_s-{T}(V72,V26), P_s-{T}(V72,V6), P_s-{T}(V72,V31), P_s-{T}(V72,V0), P_s-{T}(V72,V16), P_s-{T}(V72,V27), P_s-{T}(V72,V32), P_s-{T}(V72,V33), P_s-{T}(V72,V7), P_s-{T}(V72,V67), P_s-{T}(V72,V17), P_s-{T}(V72,V72), P_s-{T}(V72,V34), P_s-{T}(V72,V18), P_s-{T}(V72,V35), P_s-{T}(V72,V19), P_s-{T}(V72,V76), P_s-{T}(V72,V20), P_s-{T}(V72,V42), P_s-{T}(V72,V70), P_s-{T}(V72,V50), P_s-{T}(V72,V46), P_s-{T}(V72,V71), P_s-{T}(V72,V73), P_s-{T}(V72,V44), P_s-{T}(V72,V52), P_s-{T}(V72,V48), P_s-{T}(V72,V79), P_s-{T}(V72,V28), P_s-{T}(V72,V14), P_s-{T}(V72,V29), P_s-{T}(V72,V37), P_s-{T}(V72,V38), P_s-{T}(V72,V15), P_s-{T}(V72,V82), P_s-{T}(V72,V21), P_s-{T}(V72,V39), P_s-{T}(V72,V22), P_s-{T}(V72,V40), P_s-{T}(V72,V23), P_s-{T}(V72,V86), P_s-{T}(V72,V24), P_s-{T}(V72,V54), P_s-{T}(V72,V85), P_s-{T}(V72,V62), P_s-{T}(V72,V58), P_s-{T}(V72,V74), P_s-{T}(V72,V75), P_s-{T}(V72,V56), P_s-{T}(V72,V64), P_s-{T}(V72,V60), P_s-{T}(V72,V89)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1432: mergings( V0 == V14, V8 == V22, V14 == V28, V28 == V95, V95 == V97, V97 == V99, V99 == V101, V101 == V103, V103 == V105, V105 == V107, V107 == V109, V109 == V111, V111 == V113, V113 == V115, V115 == V117, V117 == V119, V119 == V121, V121 == V123, V123 == V125, V125 == V127, V127 == V129, V129 == V131, V131 == V133, V133 == V135, V135 == V137, V137 == V139, V139 == V141, V141 == V143, V143 == V145, V145 == V147, V147 == V149, V149 == V151, V151 == V153, V153 == V155, V155 == V157, V157 == V159, V159 == V161, V161 == V163, V163 == V165, V165 == V167; #1391 ), references = 1, size of lhs = 200:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V0,V3), V3 == V0, P_s-{F}(V4,V3), b-{F}(V3,V5), b-{F}(V5,V3), b-{F}(V0,V6), P_s-{F}(V7,V6), b-{F}(V0,V8), b-{F}(V8,V0), b-{F}(V0,V9), b-{F}(V9,V0), b-{F}(V0,V10), b-{F}(V10,V0), b-{F}(V0,V11), V11 == V0, P_s-{F}(V12,V11), b-{F}(V11,V13), b-{F}(V13,V11), b-{F}(V0,V14), P_s-{F}(V15,V14), P_s-{F}(V0,V16), V16 == V0, P_s-{F}(V17,V16), P_s-{F}(V18,V16), P_s-{F}(V19,V16), P_s-{F}(V20,V16), P_s-{F}(V21,V16), P_s-{F}(V22,V16), P_s-{F}(V23,V16), P_s-{F}(V24,V16), b-{F}(V0,V25), b-{F}(V25,V0), P_s-{F}(V26,V6), P_s-{F}(V27,V16), P_s-{F}(V28,V14), P_s-{F}(V29,V16), b-{F}(V30,V0), P_s-{F}(V31,V30), r-{F}(V30,V32), b-{F}(V32,V0), P_s-{F}(V33,V30), P_s-{F}(V34,V32), P_s-{F}(V35,V32), P_s-{F}(V36,V35), P_s-{F}(V37,V38), V30 == V38, V38 == V3, V32 == V38, V0 == V38, V38 == V11, V16 == V38, P_s-{F}(V39,V38), P_s-{F}(V40,V38), P_s-{F}(V41,V38), P_s-{F}(V42,V41), P_s-{F}(V43,V38), P_s-{F}(V44,V43), P_s-{F}(V45,V38), P_s-{F}(V46,V45), P_s-{F}(V47,V38), P_s-{F}(V48,V47), P_s-{F}(V49,V38), P_s-{F}(V50,V49), P_s-{F}(V51,V38), P_s-{F}(V52,V51), P_s-{F}(V53,V38), P_s-{F}(V54,V53), P_s-{F}(V55,V38), P_s-{F}(V56,V55), P_s-{F}(V57,V38), P_s-{F}(V58,V57), P_s-{F}(V59,V58), P_s-{F}(V60,V38), P_s-{F}(V61,V60), P_s-{F}(V62,V61), P_s-{F}(V63,V38), P_s-{F}(V64,V63), P_s-{F}(V65,V64), P_s-{F}(V66,V38), P_s-{F}(V67,V66), P_s-{F}(V68,V67), P_s-{F}(V69,V38), P_s-{F}(V70,V69), P_s-{F}(V71,V70), P_s-{F}(V72,V38), P_s-{F}(V73,V72), P_s-{F}(V74,V73), P_s-{F}(V75,V38), P_s-{F}(V76,V75), P_s-{F}(V77,V76), P_s-{F}(V78,V38), P_s-{F}(V79,V78), P_s-{F}(V80,V79), P_s-{F}(V81,V38), P_s-{F}(V82,V81), P_s-{F}(V83,V82), P_s-{F}(V84,V38), P_s-{F}(V85,V84), P_s-{F}(V86,V85), P_s-{F}(V87,V38), P_s-{F}(V88,V87), P_s-{F}(V89,V88), P_s-{F}(V90,V38), P_s-{F}(V91,V90), P_s-{F}(V92,V91), P_s-{F}(V93,V94), V0 == V94, V94 == V3, V94 == V38, P_s-{F}(V95,V96), P_s-{F}(V96,V97), V97 == V0, V97 == V38, V97 == V16, P_s-{F}(V98,V97), P_s-{F}(V99,V98), P_s-{F}(V100,V101), P_s-{F}(V101,V102), V102 == V38, V102 == V0, V102 == V16, P_s-{F}(V103,V102), P_s-{F}(V104,V103), P_s-{F}(V105,V106), V0 == V106, V106 == V11, V106 == V38, P_s-{F}(V107,V108), P_s-{F}(V108,V109), V109 == V0, V109 == V38, V109 == V16, P_s-{F}(V110,V109), P_s-{F}(V111,V110), P_s-{F}(V112,V113), P_s-{F}(V113,V114), V114 == V38, V114 == V0, V114 == V16, P_s-{F}(V115,V114), P_s-{F}(V116,V115), P_s-{F}(V117,V118), V33 == V118, V26 == V118, V40 == V118, V27 == V118, V42 == V118, V44 == V118, V99 == V118, V117 == V118, V46 == V118, V48 == V118, V104 == V118, V59 == V118, V71 == V118, V65 == V118, V62 == V118, V74 == V118, V68 == V118, V34 == V118, V28 == V118, V29 == V118, V36 == V118, V50 == V118, V52 == V118, V111 == V118, V54 == V118, V56 == V118, V116 == V118, V77 == V118, V89 == V118, V83 == V118, V80 == V118, V92 == V118, V86 == V118, P_s-{F}(V119,V118), P_s-{F}(V120,V119), V120 == V118, P_s-{F}(V121,V118), P_s-{F}(V122,V121), V122 == V118, P_s-{F}(V123,V118), P_s-{F}(V124,V123), V124 == V118, P_s-{F}(V125,V118), P_s-{F}(V126,V125), V126 == V118, #-{F} V127, V4 == V127, V37 == V127, V93 == V127, #-{F} V128, V12 == V128, V39 == V128, V105 == V128 | P_s-{T}(V118,V0), P_s-{T}(V118,V31), P_s-{T}(V118,V7), P_s-{T}(V118,V17), P_s-{T}(V118,V18), P_s-{T}(V118,V19), P_s-{T}(V118,V20), P_s-{T}(V118,V95), P_s-{T}(V118,V100), P_s-{T}(V118,V15), P_s-{T}(V118,V21), P_s-{T}(V118,V22), P_s-{T}(V118,V23), P_s-{T}(V118,V24), P_s-{T}(V118,V107), P_s-{T}(V118,V112)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1496: mergings( V28 == V29, V29 == V30, V30 == V32, V32 == V33, V33 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V53, V53 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V0, V0 == V71, V8 == V70, V71 == V14, V70 == V22, V14 == V7, V22 == V6, V7 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V135, V6 == V136, V135 == V140, V136 == V141, V137 == V142, V140 == V21, V141 == V20, V21 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V147, V20 == V148, V142 == V149; #1433 ), references = 1, size of lhs = 176:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V0,V3), V3 == V0, P_s-{F}(V4,V3), b-{F}(V3,V5), b-{F}(V5,V3), b-{F}(V0,V6), b-{F}(V6,V0), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V0,V8), b-{F}(V8,V0), b-{F}(V0,V9), V9 == V0, P_s-{F}(V10,V9), b-{F}(V9,V11), b-{F}(V11,V9), b-{F}(V0,V12), V12 == V0, b-{F}(V12,V0), P_s-{F}(V0,V12), P_s-{F}(V13,V12), P_s-{F}(V14,V12), r-{F}(V12,V15), b-{F}(V15,V0), b-{F}(V0,V16), b-{F}(V16,V0), P_s-{F}(V17,V12), P_s-{F}(V18,V12), P_s-{F}(V19,V12), P_s-{F}(V20,V15), P_s-{F}(V12,V21), V21 == V0, V21 == V12, P_s-{F}(V22,V15), P_s-{F}(V23,V22), P_s-{F}(V24,V21), P_s-{F}(V25,V24), P_s-{F}(V26,V21), P_s-{F}(V27,V26), P_s-{F}(V28,V21), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V31 == V3, V15 == V31, V0 == V31, V31 == V9, V12 == V31, V21 == V31, P_s-{F}(V32,V31), P_s-{F}(V33,V31), P_s-{F}(V34,V31), P_s-{F}(V35,V34), P_s-{F}(V36,V31), P_s-{F}(V37,V36), P_s-{F}(V38,V31), P_s-{F}(V39,V38), P_s-{F}(V40,V31), P_s-{F}(V41,V40), P_s-{F}(V42,V31), P_s-{F}(V43,V42), P_s-{F}(V44,V31), P_s-{F}(V45,V44), P_s-{F}(V46,V31), P_s-{F}(V47,V46), P_s-{F}(V48,V31), P_s-{F}(V49,V48), P_s-{F}(V50,V31), P_s-{F}(V51,V50), P_s-{F}(V52,V51), P_s-{F}(V53,V31), P_s-{F}(V54,V53), P_s-{F}(V55,V54), P_s-{F}(V56,V31), P_s-{F}(V57,V56), P_s-{F}(V58,V57), P_s-{F}(V59,V31), P_s-{F}(V60,V59), P_s-{F}(V61,V60), P_s-{F}(V62,V31), P_s-{F}(V63,V62), P_s-{F}(V64,V63), P_s-{F}(V65,V31), P_s-{F}(V66,V65), P_s-{F}(V67,V66), P_s-{F}(V68,V31), P_s-{F}(V69,V68), P_s-{F}(V70,V69), P_s-{F}(V71,V31), P_s-{F}(V72,V71), P_s-{F}(V73,V72), P_s-{F}(V74,V31), P_s-{F}(V75,V74), P_s-{F}(V76,V75), P_s-{F}(V77,V31), P_s-{F}(V78,V77), P_s-{F}(V79,V78), P_s-{F}(V80,V31), P_s-{F}(V81,V80), P_s-{F}(V82,V81), P_s-{F}(V83,V31), P_s-{F}(V84,V83), P_s-{F}(V85,V84), P_s-{F}(V86,V87), V0 == V87, V87 == V3, V87 == V31, P_s-{F}(V88,V89), V0 == V89, V89 == V9, V89 == V31, P_s-{F}(V90,V91), P_s-{F}(V91,V92), V92 == V31, V92 == V0, V92 == V12, P_s-{F}(V93,V92), P_s-{F}(V94,V93), P_s-{F}(V95,V96), V19 == V96, V13 == V96, V33 == V96, V14 == V96, V35 == V96, V37 == V96, V25 == V96, V95 == V96, V39 == V96, V41 == V96, V27 == V96, V52 == V96, V64 == V96, V58 == V96, V55 == V96, V67 == V96, V61 == V96, V20 == V96, V17 == V96, V18 == V96, V23 == V96, V43 == V96, V45 == V96, V29 == V96, V47 == V96, V49 == V96, V94 == V96, V70 == V96, V82 == V96, V76 == V96, V73 == V96, V85 == V96, V79 == V96, P_s-{F}(V97,V96), P_s-{F}(V98,V97), V98 == V96, P_s-{F}(V99,V96), P_s-{F}(V100,V99), V100 == V96, P_s-{F}(V101,V96), P_s-{F}(V102,V101), V102 == V96, P_s-{F}(V103,V96), P_s-{F}(V104,V103), V104 == V96, #-{F} V105, V4 == V105, V30 == V105, V86 == V105, #-{F} V106, V10 == V106, V32 == V106, V88 == V106 | P_s-{T}(V96,V90)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1565: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V52, V48 == V53, V52 == V2, V53 == V60, V2 == V66, V60 == V47, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V47 == V72, V71 == V74, V72 == V75, V73 == V76, V74 == V77, V75 == V59, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V59 == V83, V76 == V84, V82 == V85, V83 == V86, V84 == V87; #1498 ), references = 1, size of lhs = 171:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V0,V3), V3 == V0, P_s-{F}(V4,V3), b-{F}(V3,V5), b-{F}(V5,V3), b-{F}(V0,V6), b-{F}(V6,V0), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V0,V8), b-{F}(V8,V0), b-{F}(V0,V9), V9 == V0, P_s-{F}(V10,V9), b-{F}(V9,V11), b-{F}(V11,V9), b-{F}(V0,V12), V12 == V0, b-{F}(V12,V0), P_s-{F}(V0,V12), P_s-{F}(V13,V12), P_s-{F}(V14,V12), r-{F}(V12,V15), V15 == V0, b-{F}(V0,V16), b-{F}(V16,V0), P_s-{F}(V17,V12), P_s-{F}(V18,V12), P_s-{F}(V19,V12), P_s-{F}(V20,V15), P_s-{F}(V12,V21), V21 == V0, V21 == V12, P_s-{F}(V22,V15), P_s-{F}(V23,V22), P_s-{F}(V24,V21), P_s-{F}(V25,V24), P_s-{F}(V26,V21), P_s-{F}(V27,V26), P_s-{F}(V28,V21), P_s-{F}(V29,V28), P_s-{F}(V30,V21), P_s-{F}(V31,V30), P_s-{F}(V32,V33), V33 == V3, V15 == V33, V0 == V33, V33 == V9, V12 == V33, V21 == V33, P_s-{F}(V34,V33), P_s-{F}(V35,V33), P_s-{F}(V36,V33), P_s-{F}(V37,V36), P_s-{F}(V38,V33), P_s-{F}(V39,V38), P_s-{F}(V40,V33), P_s-{F}(V41,V40), P_s-{F}(V42,V33), P_s-{F}(V43,V42), P_s-{F}(V44,V33), P_s-{F}(V45,V44), P_s-{F}(V46,V33), P_s-{F}(V47,V46), P_s-{F}(V48,V33), P_s-{F}(V49,V48), P_s-{F}(V50,V33), P_s-{F}(V51,V50), P_s-{F}(V52,V33), P_s-{F}(V53,V52), P_s-{F}(V54,V53), P_s-{F}(V55,V33), P_s-{F}(V56,V55), P_s-{F}(V57,V56), P_s-{F}(V58,V33), P_s-{F}(V59,V58), P_s-{F}(V60,V59), P_s-{F}(V61,V33), P_s-{F}(V62,V61), P_s-{F}(V63,V62), P_s-{F}(V64,V33), P_s-{F}(V65,V64), P_s-{F}(V66,V65), P_s-{F}(V67,V33), P_s-{F}(V68,V67), P_s-{F}(V69,V68), P_s-{F}(V70,V33), P_s-{F}(V71,V70), P_s-{F}(V72,V71), P_s-{F}(V73,V33), P_s-{F}(V74,V73), P_s-{F}(V75,V74), P_s-{F}(V76,V33), P_s-{F}(V77,V76), P_s-{F}(V78,V77), P_s-{F}(V79,V33), P_s-{F}(V80,V79), P_s-{F}(V81,V80), P_s-{F}(V82,V33), P_s-{F}(V83,V82), P_s-{F}(V84,V83), P_s-{F}(V85,V33), P_s-{F}(V86,V85), P_s-{F}(V87,V86), P_s-{F}(V88,V89), V0 == V89, V89 == V3, V89 == V33, P_s-{F}(V90,V91), V0 == V91, V91 == V9, V91 == V33, P_s-{F}(V92,V93), V19 == V93, V13 == V93, V35 == V93, V14 == V93, V37 == V93, V39 == V93, V25 == V93, V92 == V93, V41 == V93, V43 == V93, V27 == V93, V54 == V93, V66 == V93, V60 == V93, V57 == V93, V69 == V93, V63 == V93, V20 == V93, V17 == V93, V18 == V93, V23 == V93, V45 == V93, V47 == V93, V29 == V93, V49 == V93, V51 == V93, V31 == V93, V72 == V93, V84 == V93, V78 == V93, V75 == V93, V87 == V93, V81 == V93, P_s-{F}(V94,V93), P_s-{F}(V95,V94), V95 == V93, P_s-{F}(V96,V93), P_s-{F}(V97,V96), V97 == V93, P_s-{F}(V98,V93), P_s-{F}(V99,V98), V99 == V93, P_s-{F}(V100,V93), P_s-{F}(V101,V100), V101 == V93, #-{F} V102, V4 == V102, V32 == V102, V88 == V102, #-{F} V103, V10 == V103, V34 == V103, V90 == V103 | r-{T}(V15,V0)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1579: mergings( V2 == V7, V7 == V21, V21 == V25, V25 == V30, V30 == V31, V31 == V32; #1572 ), references = 1, size of lhs = 100:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V0,V3), V3 == V0, P_s-{F}(V4,V3), b-{F}(V3,V5), b-{F}(V5,V3), b-{F}(V0,V6), P_s-{F}(V7,V6), P_s-{F}(V0,V8), V8 == V0, P_s-{F}(V9,V8), P_s-{F}(V10,V8), P_s-{F}(V11,V8), P_s-{F}(V12,V8), b-{F}(V0,V13), b-{F}(V13,V0), r-{F}(V0,V14), V0 == V14, r-{F}(V14,V0), r-{F}(V15,V14), r-{F}(V16,V14), P_s-{F}(V17,V14), r-{F}(V18,V14), r-{F}(V19,V14), P_s-{F}(V20,V14), r-{F}(V0,V21), r-{F}(V21,V0), P_s-{F}(V22,V21), r-{F}(V23,V0), r-{F}(V24,V0), b-{F}(V0,V25), r-{F}(V25,V14), b-{F}(V25,V26), b-{F}(V26,V25), b-{F}(V27,V0), P_s-{F}(V28,V27), r-{F}(V27,V29), V14 == V29, V0 == V29, P_s-{F}(V30,V29), r-{F}(V31,V0), P_s-{F}(V32,V31), P_s-{F}(V33,V34), P_s-{F}(V35,V34), P_s-{F}(V36,V34), P_s-{F}(V37,V34), P_s-{F}(V38,V34), P_s-{F}(V39,V34), P_s-{F}(V40,V41), V41 == V0, V41 == V14, P_s-{F}(V42,V43), V0 == V43, V41 == V43, V43 == V15, V43 == V14, V43 == V16, P_s-{F}(V44,V45), V0 == V45, V45 == V3, P_s-{F}(V46,V47), V47 == V0, V47 == V8, P_s-{F}(V48,V47), P_s-{F}(V49,V48), P_s-{F}(V50,V51), V27 == V51, V51 == V6, V51 == V0, V8 == V51, P_s-{F}(V52,V51), P_s-{F}(V53,V52), P_s-{F}(V54,V51), P_s-{F}(V55,V54), P_s-{F}(V56,V57), V57 == V0, V57 == V8, P_s-{F}(V58,V57), P_s-{F}(V59,V58), P_s-{F}(V60,V61), V61 == V0, V61 == V29, V61 == V14, P_s-{F}(V62,V63), V63 == V21, V63 == V0, P_s-{F}(V64,V65), V65 == V21, V63 == V65, V65 == V23, V65 == V0, V65 == V24, #-{F} V66, V4 == V66, V34 == V66, V44 == V66 | P_s-{T}(V34,V0), P_s-{T}(V34,V3), P_s-{T}(V34,V8), P_s-{T}(V34,V21), P_s-{T}(V34,V25), P_s-{T}(V34,V14), P_s-{T}(V34,V27), P_s-{T}(V34,V29), P_s-{T}(V34,V41), P_s-{T}(V34,V43), P_s-{T}(V34,V45), P_s-{T}(V34,V47), P_s-{T}(V34,V51), P_s-{T}(V34,V57), P_s-{T}(V34,V28), P_s-{T}(V34,V34), P_s-{T}(V34,V7), P_s-{T}(V34,V46), P_s-{T}(V34,V9), P_s-{T}(V34,V50), P_s-{T}(V34,V10), P_s-{T}(V34,V11), P_s-{T}(V34,V56), P_s-{T}(V34,V12), P_s-{T}(V34,V33), P_s-{T}(V34,V49), P_s-{T}(V34,V38), P_s-{T}(V34,V36), P_s-{T}(V34,V53), P_s-{T}(V34,V55), P_s-{T}(V34,V35), P_s-{T}(V34,V39), P_s-{T}(V34,V37), P_s-{T}(V34,V59), P_s-{T}(V34,V61), P_s-{T}(V34,V18), P_s-{T}(V34,V19), P_s-{T}(V34,V63), P_s-{T}(V34,V65), P_s-{T}(V34,V17), P_s-{T}(V34,V40), P_s-{T}(V34,V42), P_s-{T}(V34,V30), P_s-{T}(V34,V20), P_s-{T}(V34,V60), P_s-{T}(V34,V32), P_s-{T}(V34,V22), P_s-{T}(V34,V62), P_s-{T}(V34,V64)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1644: mergings( V28 == V29, V29 == V30, V30 == V0, V0 == V19, V19 == V5, V5 == V73, V73 == V75, V75 == V23, V23 == V77, V77 == V79, V79 == V81, V81 == V83, V83 == V85, V85 == V87, V87 == V89, V89 == V91, V91 == V93, V93 == V95, V95 == V97, V97 == V34, V13 == V33, V34 == V99, V99 == V12, V33 == V11, V12 == V101, V101 == V14, V14 == V103, V103 == V15, V15 == V16, V16 == V105, V105 == V17, V17 == V107, V107 == V55, V11 == V54, V55 == V109, V109 == V111, V111 == V59, V54 == V58, V53 == V57, V59 == V61, V58 == V60, V61 == V113, V113 == V115, V115 == V117, V117 == V65, V60 == V64, V57 == V63, V65 == V119, V119 == V121, V121 == V123, V123 == V125, V125 == V127, V127 == V129, V129 == V46, V64 == V47, V46 == V131, V131 == V133, V133 == V135, V135 == V66, V47 == V67, V66 == V137, V137 == V139, V139 == V141; #1580 ), references = 1, size of lhs = 146:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), b-{F}(V0,V4), b-{F}(V4,V0), b-{F}(V0,V5), b-{F}(V5,V0), b-{F}(V0,V6), V6 == V0, P_s-{F}(V7,V6), b-{F}(V6,V8), b-{F}(V8,V6), b-{F}(V0,V9), V9 == V0, V9 == V1, b-{F}(V9,V0), P_s-{F}(V0,V9), b-{F}(V0,V10), b-{F}(V10,V0), P_s-{F}(V11,V6), P_s-{F}(V12,V9), r-{F}(V0,V13), r-{F}(V13,V0), r-{F}(V14,V0), r-{F}(V15,V0), b-{F}(V0,V16), r-{F}(V16,V1), b-{F}(V16,V17), b-{F}(V17,V16), P_s-{F}(V18,V13), P_s-{F}(V19,V16), P_s-{F}(V20,V1), r-{F}(V9,V21), V1 == V21, V0 == V21, V9 == V21, P_s-{F}(V22,V9), P_s-{F}(V23,V21), P_s-{F}(V9,V24), V24 == V0, V24 == V9, P_s-{F}(V25,V24), P_s-{F}(V26,V24), P_s-{F}(V27,V24), P_s-{F}(V28,V9), P_s-{F}(V29,V9), P_s-{F}(V30,V1), P_s-{F}(V31,V30), r-{F}(V32,V1), P_s-{F}(V33,V32), r-{F}(V34,V1), P_s-{F}(V35,V34), P_s-{F}(V36,V1), P_s-{F}(V37,V36), P_s-{F}(V38,V13), P_s-{F}(V39,V38), P_s-{F}(V40,V21), P_s-{F}(V41,V40), r-{F}(V42,V0), P_s-{F}(V43,V42), P_s-{F}(V44,V43), P_s-{F}(V45,V24), P_s-{F}(V46,V45), P_s-{F}(V47,V24), P_s-{F}(V48,V47), P_s-{F}(V49,V24), P_s-{F}(V50,V49), P_s-{F}(V51,V52), V0 == V52, V52 == V6, P_s-{F}(V53,V52), P_s-{F}(V54,V55), V55 == V13, V55 == V14, V55 == V0, V55 == V15, P_s-{F}(V56,V55), P_s-{F}(V57,V58), V0 == V58, V9 == V58, V58 == V2, V58 == V1, V58 == V3, P_s-{F}(V59,V58), P_s-{F}(V60,V59), P_s-{F}(V61,V62), V11 == V62, V12 == V62, V18 == V62, V19 == V62, V20 == V62, V22 == V62, V23 == V62, V28 == V62, V57 == V62, V53 == V62, V25 == V62, V26 == V62, V27 == V62, V61 == V62, V46 == V62, V48 == V62, V50 == V62, V29 == V62, V33 == V62, V35 == V62, V56 == V62, V31 == V62, V60 == V62, V41 == V62, V37 == V62, V44 == V62, V39 == V62, P_s-{F}(V63,V62), P_s-{F}(V64,V63), V64 == V62, P_s-{F}(V65,V62), P_s-{F}(V66,V65), V66 == V62, P_s-{F}(V67,V62), P_s-{F}(V68,V67), V68 == V62, P_s-{F}(V69,V62), P_s-{F}(V70,V69), V70 == V62, P_s-{F}(V71,V62), P_s-{F}(V72,V71), V72 == V62, P_s-{F}(V73,V62), P_s-{F}(V74,V73), V74 == V62, P_s-{F}(V75,V76), V76 == V13, V76 == V0, V76 == V55, V75 == V62, P_s-{F}(V77,V76), P_s-{F}(V78,V77), V78 == V62, #-{F} V79, V7 == V79, V62 == V79, V51 == V79 | P_s-{T}(V62,V54)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #1827: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V44, V44 == V47, V45 == V48, V47 == V50, V48 == V51, V50 == V53, V51 == V54, V53 == V57, V54 == V65, V57 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V65 == V117, V110 == V121, V117 == V122, V121 == V125, V122 == V116, V125 == V126, V126 == V127, V127 == V128, V128 == V129, V129 == V130, V116 == V131, V130 == V133, V131 == V134, V132 == V135, V133 == V136, V134 == V137, V136 == V139, V137 == V140, V139 == V142, V142 == V143, V143 == V144, V144 == V145, V140 == V146, V135 == V147, V145 == V148, V146 == V149, V147 == V150, V148 == V151, V151 == V152, V152 == V153, V153 == V154, V149 == V161, V154 == V163, V163 == V165, V165 == V167, V167 == V178, V178 == V179, V179 == V181, V181 == V182, V182 == V183, V183 == V184, V184 == V185, V185 == V186, V186 == V187, V187 == V188, V188 == V189, V189 == V190, V161 == V191, V190 == V194, V194 == V195, V191 == V160, V195 == V196, V196 == V197, V197 == V198, V198 == V199, V199 == V200, V200 == V201, V201 == V202, V202 == V203, V203 == V204, V160 == V205, V150 == V206, V204 == V208, V208 == V209, V209 == V210, V205 == V211, V206 == V212, V210 == V214, V211 == V215, V214 == V216, V216 == V217, V217 == V218, V218 == V219, V215 == V220, V212 == V221, V219 == V223, V223 == V224, V224 == V225, V225 == V226, V226 == V227, V227 == V228, V228 == V229, V220 == V230, V229 == V232, V232 == V233, V233 == V234, V234 == V235, V230 == V236, V235 == V238, V238 == V239, V239 == V240, V240 == V241, V236 == V242; #1650 ), references = 1, size of lhs = 239:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V0,V3), V3 == V0, P_s-{F}(V4,V3), b-{F}(V3,V5), b-{F}(V5,V3), b-{F}(V0,V6), P_s-{F}(V7,V6), b-{F}(V0,V8), b-{F}(V8,V0), b-{F}(V0,V9), b-{F}(V9,V0), b-{F}(V0,V10), b-{F}(V10,V0), b-{F}(V0,V11), V11 == V0, P_s-{F}(V12,V11), b-{F}(V11,V13), b-{F}(V13,V11), b-{F}(V0,V14), P_s-{F}(V15,V14), b-{F}(V0,V16), b-{F}(V16,V0), b-{F}(V0,V17), b-{F}(V17,V0), b-{F}(V0,V18), b-{F}(V18,V0), b-{F}(V0,V19), V19 == V0, P_s-{F}(V20,V19), b-{F}(V19,V21), b-{F}(V21,V19), b-{F}(V0,V22), b-{F}(V22,V0), b-{F}(V0,V23), b-{F}(V23,V0), b-{F}(V0,V24), b-{F}(V24,V0), b-{F}(V0,V25), V25 == V0, P_s-{F}(V26,V25), b-{F}(V25,V27), b-{F}(V27,V25), b-{F}(V0,V28), b-{F}(V28,V0), P_s-{F}(V29,V25), b-{F}(V0,V30), V30 == V0, b-{F}(V30,V0), P_s-{F}(V0,V30), P_s-{F}(V31,V30), P_s-{F}(V32,V30), P_s-{F}(V33,V30), P_s-{F}(V34,V30), P_s-{F}(V35,V30), P_s-{F}(V36,V30), P_s-{F}(V37,V30), P_s-{F}(V38,V30), P_s-{F}(V39,V30), P_s-{F}(V40,V30), P_s-{F}(V41,V30), P_s-{F}(V42,V30), P_s-{F}(V43,V30), P_s-{F}(V44,V30), P_s-{F}(V45,V30), b-{F}(V0,V46), b-{F}(V46,V0), b-{F}(V0,V47), b-{F}(V47,V0), b-{F}(V0,V48), V48 == V0, P_s-{F}(V49,V48), b-{F}(V48,V50), b-{F}(V50,V48), b-{F}(V0,V51), b-{F}(V51,V0), b-{F}(V0,V52), V52 == V0, P_s-{F}(V53,V52), b-{F}(V52,V54), b-{F}(V54,V52), b-{F}(V30,V55), b-{F}(V55,V30), P_s-{F}(V56,V30), P_s-{F}(V57,V30), P_s-{F}(V58,V30), P_s-{F}(V30,V59), V59 == V0, V59 == V30, P_s-{F}(V60,V59), P_s-{F}(V61,V59), P_s-{F}(V62,V59), P_s-{F}(V63,V30), P_s-{F}(V64,V30), P_s-{F}(V65,V30), P_s-{F}(V66,V30), P_s-{F}(V67,V30), P_s-{F}(V68,V59), P_s-{F}(V69,V68), P_s-{F}(V70,V59), P_s-{F}(V71,V70), P_s-{F}(V72,V59), P_s-{F}(V73,V72), P_s-{F}(V74,V59), P_s-{F}(V75,V74), P_s-{F}(V76,V59), P_s-{F}(V77,V76), P_s-{F}(V78,V59), P_s-{F}(V79,V78), P_s-{F}(V80,V59), P_s-{F}(V81,V80), P_s-{F}(V82,V83), V83 == V3, V0 == V83, V83 == V52, V30 == V83, P_s-{F}(V84,V83), P_s-{F}(V85,V83), P_s-{F}(V86,V83), P_s-{F}(V87,V83), P_s-{F}(V88,V83), P_s-{F}(V89,V83), P_s-{F}(V90,V83), P_s-{F}(V91,V83), P_s-{F}(V92,V83), P_s-{F}(V93,V92), P_s-{F}(V94,V83), P_s-{F}(V95,V94), P_s-{F}(V96,V83), P_s-{F}(V97,V96), P_s-{F}(V98,V83), P_s-{F}(V99,V98), P_s-{F}(V100,V83), P_s-{F}(V101,V100), P_s-{F}(V102,V83), P_s-{F}(V103,V102), P_s-{F}(V104,V83), P_s-{F}(V105,V104), P_s-{F}(V106,V83), P_s-{F}(V107,V106), P_s-{F}(V108,V83), P_s-{F}(V109,V108), P_s-{F}(V110,V83), P_s-{F}(V111,V110), P_s-{F}(V112,V83), P_s-{F}(V113,V112), P_s-{F}(V114,V115), P_s-{F}(V116,V115), P_s-{F}(V117,V115), P_s-{F}(V118,V115), P_s-{F}(V119,V115), P_s-{F}(V120,V115), P_s-{F}(V121,V115), P_s-{F}(V122,V115), P_s-{F}(V123,V115), P_s-{F}(V124,V115), P_s-{F}(V125,V115), P_s-{F}(V126,V115), P_s-{F}(V127,V115), P_s-{F}(V128,V115), P_s-{F}(V129,V115), P_s-{F}(V130,V115), P_s-{F}(V131,V115), P_s-{F}(V132,V115), P_s-{F}(V133,V115), P_s-{F}(V134,V115), P_s-{F}(V135,V115), P_s-{F}(V136,V115), P_s-{F}(V137,V115), P_s-{F}(V138,V115), P_s-{F}(V139,V115), P_s-{F}(V140,V115), P_s-{F}(V141,V115), P_s-{F}(V142,V115), P_s-{F}(V143,V115), P_s-{F}(V144,V115), P_s-{F}(V145,V115), P_s-{F}(V146,V115), P_s-{F}(V147,V146), P_s-{F}(V148,V115), P_s-{F}(V149,V148), P_s-{F}(V150,V115), P_s-{F}(V151,V150), P_s-{F}(V152,V115), P_s-{F}(V153,V152), P_s-{F}(V154,V115), P_s-{F}(V155,V154), P_s-{F}(V156,V115), P_s-{F}(V157,V156), P_s-{F}(V158,V115), P_s-{F}(V159,V158), P_s-{F}(V160,V115), P_s-{F}(V161,V160), P_s-{F}(V162,V115), P_s-{F}(V163,V162), P_s-{F}(V164,V115), P_s-{F}(V165,V164), P_s-{F}(V166,V115), P_s-{F}(V167,V166), P_s-{F}(V168,V115), P_s-{F}(V169,V168), P_s-{F}(V170,V171), V0 == V171, V171 == V11, P_s-{F}(V172,V173), V173 == V0, V173 == V30, P_s-{F}(V174,V173), P_s-{F}(V175,V174), P_s-{F}(V176,V177), V177 == V14, V177 == V0, V30 == V177, P_s-{F}(V178,V177), P_s-{F}(V179,V178), P_s-{F}(V180,V177), P_s-{F}(V181,V180), P_s-{F}(V182,V183), V183 == V0, V183 == V30, P_s-{F}(V184,V183), P_s-{F}(V185,V184), P_s-{F}(V186,V187), V0 == V187, V187 == V19, P_s-{F}(V188,V189), V0 == V189, V189 == V48, P_s-{F}(V190,V191), V0 == V191, V191 == V25, P_s-{F}(V192,V191), #-{F} V193, V26 == V193, V190 == V193 | P_s-{T}(V115,V0), P_s-{T}(V115,V3), P_s-{T}(V115,V83), P_s-{T}(V115,V30), P_s-{T}(V115,V6), P_s-{T}(V115,V41), P_s-{T}(V115,V84), P_s-{T}(V115,V85), P_s-{T}(V115,V7), P_s-{T}(V115,V115), P_s-{T}(V115,V31), P_s-{T}(V115,V86), P_s-{T}(V115,V32), P_s-{T}(V115,V87), P_s-{T}(V115,V33), P_s-{T}(V115,V34), P_s-{T}(V115,V93), P_s-{T}(V115,V114), P_s-{T}(V115,V101), P_s-{T}(V115,V97), P_s-{T}(V115,V116), P_s-{T}(V115,V117), P_s-{T}(V115,V95), P_s-{T}(V115,V103), P_s-{T}(V115,V99), P_s-{T}(V115,V118), P_s-{T}(V115,V11), P_s-{T}(V115,V171), P_s-{T}(V115,V173), P_s-{T}(V115,V177), P_s-{T}(V115,V183), P_s-{T}(V115,V57), P_s-{T}(V115,V15), P_s-{T}(V115,V172), P_s-{T}(V115,V35), P_s-{T}(V115,V176), P_s-{T}(V115,V36), P_s-{T}(V115,V37), P_s-{T}(V115,V182), P_s-{T}(V115,V38), P_s-{T}(V115,V119), P_s-{T}(V115,V175), P_s-{T}(V115,V123), P_s-{T}(V115,V121), P_s-{T}(V115,V179), P_s-{T}(V115,V181), P_s-{T}(V115,V120), P_s-{T}(V115,V124), P_s-{T}(V115,V122), P_s-{T}(V115,V185), P_s-{T}(V115,V19), P_s-{T}(V115,V48), P_s-{T}(V115,V59), P_s-{T}(V115,V187), P_s-{T}(V115,V189), P_s-{T}(V115,V42), P_s-{T}(V115,V39), P_s-{T}(V115,V40), P_s-{T}(V115,V126), P_s-{T}(V115,V127), P_s-{T}(V115,V69), P_s-{T}(V115,V128), P_s-{T}(V115,V129), P_s-{T}(V115,V71), P_s-{T}(V115,V147), P_s-{T}(V115,V155), P_s-{T}(V115,V151), P_s-{T}(V115,V149), P_s-{T}(V115,V157), P_s-{T}(V115,V153), P_s-{T}(V115,V88), P_s-{T}(V115,V43), P_s-{T}(V115,V44), P_s-{T}(V115,V105), P_s-{T}(V115,V130), P_s-{T}(V115,V131), P_s-{T}(V115,V73), P_s-{T}(V115,V132), P_s-{T}(V115,V133), P_s-{T}(V115,V75), P_s-{T}(V115,V159), P_s-{T}(V115,V167), P_s-{T}(V115,V163), P_s-{T}(V115,V161), P_s-{T}(V115,V169), P_s-{T}(V115,V165), P_s-{T}(V115,V134), P_s-{T}(V115,V135), P_s-{T}(V115,V136), P_s-{T}(V115,V137), P_s-{T}(V115,V52), P_s-{T}(V115,V29), P_s-{T}(V115,V45), P_s-{T}(V115,V90), P_s-{T}(V115,V56), P_s-{T}(V115,V91), P_s-{T}(V115,V58), P_s-{T}(V115,V63), P_s-{T}(V115,V192), P_s-{T}(V115,V60), P_s-{T}(V115,V61), P_s-{T}(V115,V62), P_s-{T}(V115,V77), P_s-{T}(V115,V79), P_s-{T}(V115,V81), P_s-{T}(V115,V64), P_s-{T}(V115,V66), P_s-{T}(V115,V67), P_s-{T}(V115,V65), P_s-{T}(V115,V107), P_s-{T}(V115,V138), P_s-{T}(V115,V125), P_s-{T}(V115,V109), P_s-{T}(V115,V113), P_s-{T}(V115,V111), P_s-{T}(V115,V139), P_s-{T}(V115,V140), P_s-{T}(V115,V141), P_s-{T}(V115,V142), P_s-{T}(V115,V143), P_s-{T}(V115,V144), P_s-{T}(V115,V145), P_s-{T}(V115,V4), P_s-{T}(V115,V82), P_s-{T}(V115,V12), P_s-{T}(V115,V170), P_s-{T}(V115,V20), P_s-{T}(V115,V186), P_s-{T}(V115,V49), P_s-{T}(V115,V188), P_s-{T}(V115,V53), P_s-{T}(V115,V89), P_s-{T}(V115,V193)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2086: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V42, V42 == V45, V43 == V46, V45 == V48, V46 == V49, V48 == V51, V49 == V52, V51 == V55, V52 == V63, V55 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V63 == V115, V108 == V119, V115 == V120, V119 == V123, V120 == V114, V123 == V124, V124 == V125, V125 == V126, V126 == V127, V127 == V128, V114 == V129, V128 == V131, V129 == V132, V130 == V133, V131 == V134, V132 == V135, V134 == V137, V135 == V138, V137 == V140, V140 == V141, V141 == V142, V142 == V143, V138 == V144, V133 == V145, V143 == V146, V144 == V147, V145 == V148, V146 == V149, V149 == V150, V150 == V151, V151 == V152, V147 == V159, V152 == V161, V161 == V163, V163 == V165, V165 == V176, V176 == V177, V177 == V179, V179 == V180, V180 == V181, V181 == V182, V182 == V183, V183 == V184, V184 == V185, V185 == V186, V186 == V187, V187 == V188, V159 == V189, V188 == V192, V192 == V193, V189 == V158, V193 == V194, V194 == V195, V195 == V196, V196 == V197, V197 == V198, V198 == V199, V199 == V200, V200 == V201, V201 == V202, V158 == V203, V148 == V204, V202 == V206, V206 == V207, V207 == V208, V203 == V209, V204 == V210, V208 == V212, V209 == V213, V212 == V214, V214 == V215, V215 == V216, V216 == V217, V213 == V218, V210 == V219, V217 == V221, V221 == V222, V222 == V223, V223 == V224, V224 == V225, V225 == V226, V226 == V227, V218 == V228, V227 == V230, V230 == V231, V231 == V232, V232 == V233, V228 == V234, V233 == V236, V236 == V237, V237 == V238, V238 == V239, V234 == V240, V239 == V370, V370 == V372, V372 == V374, V374 == V376, V376 == V378, V378 == V380, V380 == V382, V382 == V384, V384 == V386, V386 == V388, V388 == V390, V390 == V392, V392 == V394, V394 == V396, V396 == V398, V398 == V400, V400 == V402, V402 == V404, V404 == V406, V406 == V408, V408 == V410, V410 == V412, V412 == V414, V414 == V416, V416 == V418, V418 == V420, V420 == V422, V422 == V424, V424 == V426, V426 == V428, V428 == V430, V430 == V432, V432 == V434, V434 == V436, V436 == V438, V438 == V440, V440 == V442, V442 == V444, V444 == V446, V446 == V448, V448 == V450, V450 == V452, V452 == V454, V454 == V456, V456 == V458, V458 == V460, V460 == V462, V462 == V464, V464 == V466, V466 == V468, V468 == V470, V470 == V472, V472 == V474, V474 == V476, V476 == V478, V478 == V480, V480 == V482, V482 == V484, V484 == V486, V486 == V488, V488 == V490, V490 == V492, V492 == V494, V494 == V496, V496 == V498, V498 == V500, V500 == V502, V502 == V504, V504 == V506, V506 == V508, V508 == V510, V510 == V512, V512 == V514, V514 == V516, V516 == V518, V518 == V520, V520 == V522, V522 == V524, V524 == V526, V526 == V528, V528 == V530; #1828 ), references = 1, size of lhs = 400:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V0,V3), V3 == V0, P_s-{F}(V4,V3), b-{F}(V3,V5), b-{F}(V5,V3), b-{F}(V0,V6), P_s-{F}(V7,V6), b-{F}(V0,V8), b-{F}(V8,V0), b-{F}(V0,V9), b-{F}(V9,V0), b-{F}(V0,V10), b-{F}(V10,V0), b-{F}(V0,V11), V11 == V0, P_s-{F}(V12,V11), b-{F}(V11,V13), b-{F}(V13,V11), b-{F}(V0,V14), P_s-{F}(V15,V14), b-{F}(V0,V16), b-{F}(V16,V0), b-{F}(V0,V17), b-{F}(V17,V0), b-{F}(V0,V18), b-{F}(V18,V0), b-{F}(V0,V19), V19 == V0, P_s-{F}(V20,V19), b-{F}(V19,V21), b-{F}(V21,V19), b-{F}(V0,V22), b-{F}(V22,V0), b-{F}(V0,V23), b-{F}(V23,V0), b-{F}(V0,V24), b-{F}(V24,V0), b-{F}(V0,V25), V25 == V0, P_s-{F}(V26,V25), b-{F}(V25,V27), b-{F}(V27,V25), b-{F}(V0,V28), b-{F}(V28,V0), P_s-{F}(V29,V25), b-{F}(V0,V30), V30 == V0, b-{F}(V30,V0), P_s-{F}(V0,V30), P_s-{F}(V31,V30), P_s-{F}(V32,V30), P_s-{F}(V33,V30), P_s-{F}(V34,V30), P_s-{F}(V35,V30), P_s-{F}(V36,V30), P_s-{F}(V37,V30), P_s-{F}(V38,V30), P_s-{F}(V39,V30), P_s-{F}(V40,V30), P_s-{F}(V41,V30), P_s-{F}(V42,V30), P_s-{F}(V43,V30), P_s-{F}(V44,V30), P_s-{F}(V45,V30), b-{F}(V0,V46), b-{F}(V46,V0), b-{F}(V0,V47), b-{F}(V47,V0), b-{F}(V0,V48), V48 == V0, P_s-{F}(V49,V48), b-{F}(V48,V50), b-{F}(V50,V48), b-{F}(V0,V51), b-{F}(V51,V0), b-{F}(V0,V52), V52 == V0, P_s-{F}(V53,V52), b-{F}(V52,V54), b-{F}(V54,V52), b-{F}(V30,V55), b-{F}(V55,V30), P_s-{F}(V56,V30), P_s-{F}(V57,V30), P_s-{F}(V58,V30), P_s-{F}(V30,V59), V59 == V0, V59 == V30, P_s-{F}(V60,V30), P_s-{F}(V61,V30), P_s-{F}(V62,V30), P_s-{F}(V63,V30), P_s-{F}(V64,V30), P_s-{F}(V65,V3), P_s-{F}(V66,V30), P_s-{F}(V67,V30), P_s-{F}(V68,V6), P_s-{F}(V69,V30), P_s-{F}(V70,V30), P_s-{F}(V71,V30), P_s-{F}(V72,V30), P_s-{F}(V73,V11), P_s-{F}(V74,V30), P_s-{F}(V75,V30), P_s-{F}(V76,V19), P_s-{F}(V77,V30), P_s-{F}(V78,V48), P_s-{F}(V79,V30), P_s-{F}(V80,V59), P_s-{F}(V81,V59), P_s-{F}(V82,V59), P_s-{F}(V83,V59), P_s-{F}(V84,V52), P_s-{F}(V85,V30), P_s-{F}(V86,V30), P_s-{F}(V87,V59), P_s-{F}(V88,V87), P_s-{F}(V89,V59), P_s-{F}(V90,V89), P_s-{F}(V91,V59), P_s-{F}(V92,V91), P_s-{F}(V93,V59), P_s-{F}(V94,V93), P_s-{F}(V95,V59), P_s-{F}(V96,V95), P_s-{F}(V97,V59), P_s-{F}(V98,V97), P_s-{F}(V99,V59), P_s-{F}(V100,V99), P_s-{F}(V101,V59), P_s-{F}(V102,V101), P_s-{F}(V103,V59), P_s-{F}(V104,V103), P_s-{F}(V105,V59), P_s-{F}(V106,V105), P_s-{F}(V107,V108), P_s-{F}(V108,V109), V109 == V3, V0 == V109, V109 == V52, V30 == V109, P_s-{F}(V110,V109), P_s-{F}(V111,V109), P_s-{F}(V112,V111), P_s-{F}(V113,V109), P_s-{F}(V114,V113), P_s-{F}(V115,V109), P_s-{F}(V116,V115), P_s-{F}(V117,V109), P_s-{F}(V118,V117), P_s-{F}(V119,V109), P_s-{F}(V120,V119), P_s-{F}(V121,V109), P_s-{F}(V122,V121), P_s-{F}(V123,V109), P_s-{F}(V124,V123), P_s-{F}(V125,V109), P_s-{F}(V126,V125), P_s-{F}(V127,V109), P_s-{F}(V128,V127), P_s-{F}(V129,V109), P_s-{F}(V130,V129), P_s-{F}(V131,V109), P_s-{F}(V132,V131), P_s-{F}(V133,V109), P_s-{F}(V134,V133), P_s-{F}(V135,V109), P_s-{F}(V136,V135), P_s-{F}(V137,V109), P_s-{F}(V138,V137), P_s-{F}(V139,V109), P_s-{F}(V140,V139), P_s-{F}(V141,V109), P_s-{F}(V142,V141), P_s-{F}(V143,V109), P_s-{F}(V144,V143), P_s-{F}(V145,V109), P_s-{F}(V146,V145), P_s-{F}(V147,V109), P_s-{F}(V148,V147), P_s-{F}(V149,V150), P_s-{F}(V150,V151), V65 == V151, V110 == V151, V66 == V151, V67 == V151, V68 == V151, V69 == V151, V70 == V151, V71 == V151, V114 == V151, V116 == V151, V118 == V151, V120 == V151, V72 == V151, V73 == V151, V74 == V151, V75 == V151, V76 == V151, V77 == V151, V78 == V151, V79 == V151, V80 == V151, V81 == V151, V82 == V151, V83 == V151, V122 == V151, V84 == V151, V85 == V151, V126 == V151, V128 == V151, V88 == V151, V90 == V151, V92 == V151, V86 == V151, V112 == V151, V124 == V151, P_s-{F}(V152,V151), V152 == V151, P_s-{F}(V153,V151), P_s-{F}(V154,V153), V154 == V151, P_s-{F}(V155,V151), P_s-{F}(V156,V155), V156 == V151, P_s-{F}(V157,V151), P_s-{F}(V158,V157), V158 == V151, P_s-{F}(V159,V151), P_s-{F}(V160,V159), V160 == V151, P_s-{F}(V161,V151), P_s-{F}(V162,V161), V162 == V151, P_s-{F}(V163,V151), P_s-{F}(V164,V163), V164 == V151, P_s-{F}(V165,V151), P_s-{F}(V166,V165), V166 == V151, P_s-{F}(V167,V151), P_s-{F}(V168,V167), V168 == V151, P_s-{F}(V169,V151), P_s-{F}(V170,V169), V170 == V151, P_s-{F}(V171,V151), P_s-{F}(V172,V171), V172 == V151, P_s-{F}(V173,V151), P_s-{F}(V174,V173), V174 == V151, P_s-{F}(V175,V151), P_s-{F}(V176,V175), V176 == V151, P_s-{F}(V177,V151), P_s-{F}(V178,V177), V178 == V151, P_s-{F}(V179,V151), P_s-{F}(V180,V179), V180 == V151, P_s-{F}(V181,V151), P_s-{F}(V182,V181), V182 == V151, P_s-{F}(V183,V151), P_s-{F}(V184,V183), V184 == V151, P_s-{F}(V185,V151), P_s-{F}(V186,V185), V186 == V151, P_s-{F}(V187,V151), P_s-{F}(V188,V187), V188 == V151, P_s-{F}(V189,V151), P_s-{F}(V190,V189), V190 == V151, P_s-{F}(V191,V151), P_s-{F}(V192,V191), V192 == V151, P_s-{F}(V193,V151), P_s-{F}(V194,V193), V194 == V151, P_s-{F}(V195,V151), P_s-{F}(V196,V195), V196 == V151, P_s-{F}(V197,V151), P_s-{F}(V198,V197), V198 == V151, P_s-{F}(V199,V151), P_s-{F}(V200,V199), V200 == V151, P_s-{F}(V201,V151), P_s-{F}(V202,V201), V202 == V151, P_s-{F}(V203,V151), P_s-{F}(V204,V203), V204 == V151, P_s-{F}(V205,V151), P_s-{F}(V206,V205), V206 == V151, P_s-{F}(V207,V151), P_s-{F}(V208,V207), V208 == V151, P_s-{F}(V209,V151), P_s-{F}(V210,V209), V210 == V151, P_s-{F}(V211,V151), P_s-{F}(V212,V211), V212 == V151, P_s-{F}(V213,V151), P_s-{F}(V214,V213), V214 == V151, P_s-{F}(V215,V151), P_s-{F}(V216,V215), P_s-{F}(V217,V151), P_s-{F}(V218,V217), P_s-{F}(V219,V151), P_s-{F}(V220,V219), P_s-{F}(V221,V151), P_s-{F}(V222,V221), P_s-{F}(V223,V151), P_s-{F}(V224,V223), P_s-{F}(V225,V151), P_s-{F}(V226,V225), P_s-{F}(V227,V151), P_s-{F}(V228,V227), P_s-{F}(V229,V151), P_s-{F}(V230,V229), P_s-{F}(V231,V151), P_s-{F}(V232,V231), P_s-{F}(V233,V151), P_s-{F}(V234,V233), P_s-{F}(V235,V151), P_s-{F}(V236,V235), P_s-{F}(V237,V238), P_s-{F}(V238,V239), V239 == V0, V239 == V30, P_s-{F}(V240,V239), V240 == V151, P_s-{F}(V241,V239), P_s-{F}(V242,V241), V242 == V151, P_s-{F}(V243,V244), P_s-{F}(V244,V245), V245 == V14, V245 == V0, V30 == V245, P_s-{F}(V246,V245), V246 == V151, P_s-{F}(V247,V245), P_s-{F}(V248,V247), V248 == V151, P_s-{F}(V249,V245), P_s-{F}(V250,V249), P_s-{F}(V251,V252), P_s-{F}(V252,V253), V253 == V0, V253 == V30, P_s-{F}(V254,V253), V254 == V151, P_s-{F}(V255,V253), P_s-{F}(V256,V255), V256 == V151, P_s-{F}(V257,V258), V0 == V258, V258 == V25, P_s-{F}(V259,V258), P_s-{F}(V260,V259), V260 == V151, P_s-{F}(V261,V262), V0 == V262, V262 == V11, V261 == V151, P_s-{F}(V263,V262), P_s-{F}(V264,V263), V264 == V151, P_s-{F}(V265,V266), V0 == V266, V266 == V19, V265 == V151, P_s-{F}(V267,V266), P_s-{F}(V268,V267), V268 == V151, P_s-{F}(V269,V270), V0 == V270, V270 == V48, V269 == V151, P_s-{F}(V271,V270), P_s-{F}(V272,V271), V272 == V151, P_s-{F}(V273,V274), V26 == V274, V257 == V274, V273 == V151 | P_s-{T}(V151,V0), P_s-{T}(V151,V41), P_s-{T}(V151,V7), P_s-{T}(V151,V31), P_s-{T}(V151,V32), P_s-{T}(V151,V33), P_s-{T}(V151,V34), P_s-{T}(V151,V107), P_s-{T}(V151,V136), P_s-{T}(V151,V132), P_s-{T}(V151,V130), P_s-{T}(V151,V138), P_s-{T}(V151,V134), P_s-{T}(V151,V57), P_s-{T}(V151,V15), P_s-{T}(V151,V35), P_s-{T}(V151,V36), P_s-{T}(V151,V37), P_s-{T}(V151,V38), P_s-{T}(V151,V237), P_s-{T}(V151,V243), P_s-{T}(V151,V250), P_s-{T}(V151,V251), P_s-{T}(V151,V42), P_s-{T}(V151,V39), P_s-{T}(V151,V40), P_s-{T}(V151,V94), P_s-{T}(V151,V96), P_s-{T}(V151,V149), P_s-{T}(V151,V222), P_s-{T}(V151,V218), P_s-{T}(V151,V216), P_s-{T}(V151,V224), P_s-{T}(V151,V220), P_s-{T}(V151,V43), P_s-{T}(V151,V44), P_s-{T}(V151,V140), P_s-{T}(V151,V98), P_s-{T}(V151,V100), P_s-{T}(V151,V226), P_s-{T}(V151,V234), P_s-{T}(V151,V230), P_s-{T}(V151,V228), P_s-{T}(V151,V236), P_s-{T}(V151,V232), P_s-{T}(V151,V29), P_s-{T}(V151,V45), P_s-{T}(V151,V56), P_s-{T}(V151,V58), P_s-{T}(V151,V60), P_s-{T}(V151,V102), P_s-{T}(V151,V104), P_s-{T}(V151,V106), P_s-{T}(V151,V61), P_s-{T}(V151,V63), P_s-{T}(V151,V64), P_s-{T}(V151,V62), P_s-{T}(V151,V142), P_s-{T}(V151,V144), P_s-{T}(V151,V148), P_s-{T}(V151,V146), P_s-{T}(V151,V4), P_s-{T}(V151,V12), P_s-{T}(V151,V20), P_s-{T}(V151,V49), P_s-{T}(V151,V53)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2455: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V42, V42 == V45, V43 == V46, V45 == V48, V46 == V49, V48 == V51, V49 == V52, V51 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V119, V52 == V120, V119 == V34, V34 == V108, V120 == V115, V108 == V123, V115 == V114, V123 == V124, V124 == V125, V125 == V126, V126 == V127, V127 == V128, V114 == V129, V128 == V131, V129 == V132, V130 == V133, V131 == V134, V132 == V135, V134 == V137, V135 == V138, V137 == V140, V140 == V141, V141 == V142, V142 == V143, V138 == V144, V133 == V145, V143 == V146, V144 == V147, V145 == V148, V146 == V149, V149 == V150, V150 == V151, V151 == V152, V147 == V159, V152 == V161, V161 == V163, V163 == V176, V176 == V177, V177 == V179, V179 == V180, V180 == V181, V181 == V182, V182 == V183, V183 == V184, V184 == V185, V185 == V186, V186 == V187, V187 == V188, V159 == V189, V188 == V55, V189 == V63, V55 == V192, V192 == V193, V63 == V158, V193 == V194, V194 == V195, V195 == V196, V196 == V197, V197 == V198, V198 == V199, V199 == V200, V200 == V201, V201 == V202, V158 == V203, V148 == V204, V202 == V205, V205 == V206, V206 == V207, V203 == V208, V204 == V209, V207 == V210, V208 == V211, V210 == V212, V212 == V213, V213 == V214, V214 == V215, V211 == V216, V209 == V217, V215 == V218, V218 == V219, V219 == V220, V220 == V221, V221 == V222, V222 == V223, V223 == V224, V216 == V225, V224 == V227, V227 == V228, V228 == V229, V229 == V230, V225 == V231, V230 == V233, V233 == V234, V234 == V235, V235 == V236, V231 == V237, V236 == V241, V241 == V243, V243 == V244, V244 == V246, V246 == V248, V248 == V250, V250 == V252, V252 == V254, V254 == V256, V256 == V257, V257 == V258, V258 == V259, V259 == V260, V260 == V261, V261 == V262, V262 == V263, V263 == V264, V264 == V265, V265 == V267, V267 == V269, V269 == V271, V271 == V273, V273 == V274, V274 == V275, V275 == V276, V276 == V277, V277 == V278, V278 == V279, V279 == V280, V280 == V281, V281 == V282, V282 == V283, V283 == V284, V284 == V285, V285 == V286, V286 == V288, V288 == V290, V290 == V292, V292 == V294, V294 == V296, V296 == V298, V298 == V300, V300 == V302, V302 == V303, V303 == V304, V304 == V305, V305 == V306, V306 == V307, V307 == V308, V308 == V309, V309 == V310, V310 == V311, V311 == V312, V312 == V313, V313 == V314, V314 == V315, V315 == V316, V316 == V317, V317 == V319, V319 == V321, V321 == V322, V322 == V323, V323 == V324, V324 == V325, V325 == V326, V326 == V327, V327 == V328, V328 == V329, V329 == V330, V330 == V331, V331 == V332, V332 == V333, V333 == V334, V334 == V335, V335 == V337, V337 == V338, V338 == V339, V339 == V340, V340 == V341, V341 == V342, V342 == V343, V343 == V121, V121 == V41, V237 == V40, V41 == V44, V44 == V47, V47 == V50, V50 == V53, V53 == V364, V40 == V365, V217 == V366, V364 == V393, V365 == V392, V393 == V389, V392 == V388, V389 == V387, V388 == V386, V387 == V395, V386 == V394, V395 == V391, V394 == V390, V391 == V165, V165 == V190, V190 == V62, V390 == V61, V62 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V494, V61 == V495, V366 == V496, V494 == V500, V495 == V501, V496 == V502, V500 == V507, V501 == V506, V507 == V508, V506 == V509, V502 == V510, V508 == V122, V122 == V117, V117 == V118, V118 == V351, V509 == V350, V351 == V353, V350 == V352, V353 == V406, V352 == V407, V510 == V408, V406 == V479, V407 == V478, V479 == V475, V478 == V474, V475 == V473, V474 == V472, V473 == V481, V472 == V480, V481 == V477, V480 == V476, V477 == V136, V136 == V139, V139 == V397, V476 == V396, V397 == V355, V396 == V354, V355 == V357, V354 == V356, V357 == V483, V356 == V482, V483 == V491, V482 == V490, V491 == V487, V490 == V486, V487 == V485, V486 == V484, V485 == V493, V484 == V492, V493 == V489, V492 == V488, V489 == V162, V488 == V155, V162 == V164, V164 == V178, V178 == V191, V191 == V226, V226 == V359, V155 == V358, V359 == V361, V358 == V360, V361 == V363, V360 == V362, V363 == V232, V232 == V239, V239 == V240, V240 == V238, V238 == V399, V362 == V398, V399 == V401, V398 == V400, V401 == V405, V400 == V404, V405 == V403, V404 == V402, V403 == V38, V402 == V37, V38 == V59, V37 == V58, V59 == V112, V58 == V111, V112 == V169, V111 == V168; #2087 ), references = 1, size of lhs = 280:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V0,V3), b-{F}(V3,V0), b-{F}(V0,V4), b-{F}(V4,V0), b-{F}(V0,V5), b-{F}(V5,V0), b-{F}(V0,V6), b-{F}(V6,V0), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V0,V8), b-{F}(V8,V0), b-{F}(V0,V9), b-{F}(V9,V0), b-{F}(V0,V10), b-{F}(V10,V0), b-{F}(V0,V11), b-{F}(V11,V0), b-{F}(V0,V12), b-{F}(V12,V0), b-{F}(V0,V13), b-{F}(V13,V0), b-{F}(V0,V14), b-{F}(V14,V0), b-{F}(V0,V15), V15 == V0, b-{F}(V15,V0), P_s-{F}(V0,V15), b-{F}(V15,V16), b-{F}(V16,V15), b-{F}(V15,V17), b-{F}(V17,V15), P_s-{F}(V18,V15), b-{F}(V15,V19), b-{F}(V19,V15), b-{F}(V15,V20), b-{F}(V20,V15), b-{F}(V15,V21), b-{F}(V21,V15), P_s-{F}(V22,V15), P_s-{F}(V23,V15), P_s-{F}(V24,V15), P_s-{F}(V25,V15), P_s-{F}(V26,V15), P_s-{F}(V27,V15), P_s-{F}(V28,V15), P_s-{F}(V29,V15), P_s-{F}(V30,V15), P_s-{F}(V31,V15), P_s-{F}(V32,V15), P_s-{F}(V33,V15), P_s-{F}(V34,V15), P_s-{F}(V35,V15), P_s-{F}(V36,V15), P_s-{F}(V37,V15), b-{F}(V15,V38), b-{F}(V38,V15), b-{F}(V0,V39), b-{F}(V39,V0), b-{F}(V0,V40), V40 == V0, P_s-{F}(V41,V40), b-{F}(V40,V42), b-{F}(V42,V40), P_s-{F}(V43,V15), P_s-{F}(V44,V40), P_s-{F}(V15,V45), V45 == V40, V45 == V0, V45 == V15, V22 == V45, V23 == V45, V24 == V45, V25 == V45, V26 == V45, V27 == V45, V28 == V45, V29 == V45, V30 == V45, V31 == V45, V32 == V45, V33 == V45, V34 == V45, V43 == V45, V35 == V45, V44 == V45, V36 == V45, V37 == V45, P_s-{F}(V46,V45), V46 == V45, P_s-{F}(V47,V45), V47 == V45, P_s-{F}(V48,V45), V48 == V45, P_s-{F}(V49,V45), V49 == V45, P_s-{F}(V50,V45), V50 == V45, P_s-{F}(V51,V45), V51 == V45, P_s-{F}(V52,V45), V52 == V45, P_s-{F}(V53,V45), V53 == V45, P_s-{F}(V54,V45), V54 == V45, P_s-{F}(V55,V45), P_s-{F}(V56,V55), V56 == V45, P_s-{F}(V57,V45), P_s-{F}(V58,V57), V58 == V45, P_s-{F}(V59,V45), P_s-{F}(V60,V59), V60 == V45, P_s-{F}(V61,V45), P_s-{F}(V62,V61), V62 == V45, P_s-{F}(V63,V45), P_s-{F}(V64,V63), V64 == V45, P_s-{F}(V65,V45), P_s-{F}(V66,V65), V66 == V45, P_s-{F}(V67,V45), P_s-{F}(V68,V67), V68 == V45, P_s-{F}(V69,V45), P_s-{F}(V70,V69), V70 == V45, P_s-{F}(V71,V45), P_s-{F}(V72,V71), V72 == V45, P_s-{F}(V73,V45), P_s-{F}(V74,V73), V74 == V45, P_s-{F}(V75,V45), P_s-{F}(V76,V75), V76 == V45, P_s-{F}(V77,V45), P_s-{F}(V78,V77), V78 == V45, P_s-{F}(V79,V45), P_s-{F}(V80,V79), V80 == V45, P_s-{F}(V81,V45), P_s-{F}(V82,V81), V82 == V45, P_s-{F}(V83,V45), P_s-{F}(V84,V83), V84 == V45, P_s-{F}(V85,V45), P_s-{F}(V86,V85), V86 == V45, P_s-{F}(V87,V45), P_s-{F}(V88,V87), V88 == V45, P_s-{F}(V89,V45), P_s-{F}(V90,V89), V90 == V45, P_s-{F}(V91,V45), P_s-{F}(V92,V91), V92 == V45, P_s-{F}(V93,V45), P_s-{F}(V94,V93), V94 == V45, P_s-{F}(V95,V45), P_s-{F}(V96,V95), V96 == V45, P_s-{F}(V97,V45), P_s-{F}(V98,V97), V98 == V45, P_s-{F}(V99,V45), P_s-{F}(V100,V99), V100 == V45, P_s-{F}(V101,V45), P_s-{F}(V102,V101), V102 == V45, P_s-{F}(V103,V45), P_s-{F}(V104,V103), V104 == V45, P_s-{F}(V105,V45), P_s-{F}(V106,V105), V106 == V45, P_s-{F}(V107,V45), P_s-{F}(V108,V107), V108 == V45, P_s-{F}(V109,V45), P_s-{F}(V110,V109), V110 == V45, P_s-{F}(V111,V45), P_s-{F}(V112,V111), V112 == V45, P_s-{F}(V113,V45), P_s-{F}(V114,V113), V114 == V45, P_s-{F}(V115,V45), P_s-{F}(V116,V115), V116 == V45, P_s-{F}(V117,V45), P_s-{F}(V118,V117), V118 == V45, P_s-{F}(V119,V45), P_s-{F}(V120,V119), V120 == V45, P_s-{F}(V121,V45), P_s-{F}(V122,V121), V122 == V45, P_s-{F}(V123,V45), P_s-{F}(V124,V123), V124 == V45, P_s-{F}(V125,V45), P_s-{F}(V126,V125), V126 == V45, P_s-{F}(V127,V45), P_s-{F}(V128,V127), V128 == V45, P_s-{F}(V129,V45), P_s-{F}(V130,V129), V130 == V45, P_s-{F}(V131,V45), P_s-{F}(V132,V131), V132 == V45, P_s-{F}(V133,V45), P_s-{F}(V134,V133), V134 == V45, P_s-{F}(V135,V45), P_s-{F}(V136,V135), V136 == V45, P_s-{F}(V137,V45), P_s-{F}(V138,V137), V138 == V45, P_s-{F}(V139,V45), P_s-{F}(V140,V139), V140 == V45, P_s-{F}(V141,V45), P_s-{F}(V142,V141), V142 == V45, P_s-{F}(V143,V45), P_s-{F}(V144,V143), V144 == V45, P_s-{F}(V145,V45), P_s-{F}(V146,V145), V146 == V45, P_s-{F}(V147,V148), V0 == V148, V148 == V15, P_s-{F}(V149,V148), P_s-{F}(V150,V149), V150 == V45, P_s-{F}(V151,V152), V0 == V152, V152 == V15, V151 == V45, P_s-{F}(V153,V152), P_s-{F}(V154,V153), V154 == V45, P_s-{F}(V155,V156), V0 == V156, V156 == V15, V155 == V45, P_s-{F}(V157,V156), P_s-{F}(V158,V157), V158 == V45, P_s-{F}(V159,V160), V0 == V160, V160 == V15, V159 == V45, P_s-{F}(V161,V160), P_s-{F}(V162,V161), V162 == V45, P_s-{F}(V163,V164), V18 == V164, V147 == V164, V163 == V45 | P_s-{T}(V45,V41)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2813: mergings( V85 == V99, V99 == V113, V113 == V129, V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V39, V38 == V40, V39 == V41, V40 == V42, V41 == V43, V42 == V44, V43 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V44 == V2, V84 == V86, V86 == V87, V2 == V129, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V129 == V92, V91 == V94, V92 == V95, V93 == V96, V94 == V97, V97 == V98, V98 == V100, V100 == V101, V101 == V102, V102 == V103, V95 == V104, V96 == V105, V103 == V106, V104 == V107, V105 == V108, V106 == V109, V109 == V110, V110 == V111, V111 == V114, V114 == V115, V115 == V116, V116 == V117, V117 == V118, V118 == V119, V119 == V120, V120 == V121, V121 == V122, V122 == V123, V123 == V124, V124 == V125, V125 == V126, V126 == V127, V107 == V128, V127 == V1, V1 == V130, V130 == V131, V131 == V132, V132 == V133, V133 == V134, V134 == V135, V135 == V136, V136 == V137, V137 == V138, V138 == V139, V139 == V140, V128 == V141, V108 == V142, V140 == V143, V143 == V144, V144 == V145, V141 == V146, V142 == V147, V145 == V148, V146 == V149, V148 == V150, V150 == V151, V151 == V152, V152 == V153, V149 == V154, V147 == V155, V153 == V156, V156 == V157, V157 == V158, V158 == V159, V159 == V160, V160 == V161, V161 == V162, V154 == V163, V162 == V164, V164 == V165, V165 == V166, V166 == V167, V163 == V168, V167 == V169, V169 == V170, V170 == V171, V171 == V172, V168 == V173, V172 == V174, V174 == V176, V176 == V177, V177 == V179, V179 == V181, V181 == V183, V183 == V185, V185 == V187, V187 == V189, V189 == V190, V190 == V191, V191 == V192, V192 == V193, V193 == V194, V194 == V195, V195 == V196, V196 == V197, V197 == V198, V198 == V200, V200 == V202, V202 == V204, V204 == V206, V206 == V207, V207 == V208, V208 == V209, V209 == V210, V210 == V211, V211 == V212, V212 == V213, V213 == V214, V214 == V215, V215 == V216, V216 == V217, V217 == V218, V218 == V219, V219 == V221, V221 == V223, V223 == V224, V224 == V226, V226 == V228, V228 == V230, V230 == V232, V232 == V234, V234 == V235, V235 == V236, V236 == V237, V237 == V238, V238 == V239, V239 == V240, V240 == V241, V241 == V242, V242 == V243, V243 == V244, V244 == V245, V245 == V246, V246 == V247, V247 == V248, V248 == V249, V249 == V250, V250 == V252, V252 == V253, V253 == V254, V254 == V255, V255 == V256, V256 == V257, V257 == V258, V258 == V259, V259 == V260, V260 == V261, V261 == V262, V262 == V263, V263 == V264, V264 == V265, V265 == V266, V266 == V268, V268 == V269, V269 == V270, V270 == V271, V271 == V272, V272 == V273, V273 == V274, V274 == V275, V275 == V276, V276 == V277, V277 == V278, V278 == V279, V279 == V280, V280 == V281, V173 == V282, V155 == V283, V281 == V285, V282 == V286, V285 == V287, V286 == V288, V287 == V289, V288 == V290, V289 == V291, V290 == V292, V291 == V293, V292 == V294, V293 == V297, V297 == V298, V298 == V299, V299 == V300, V300 == V301, V301 == V302, V302 == V303, V294 == V304, V283 == V305, V303 == V307, V304 == V308, V305 == V309, V307 == V311, V308 == V312, V311 == V313, V312 == V314, V309 == V315, V313 == V317, V317 == V318, V318 == V319, V319 == V320, V314 == V321, V320 == V322, V321 == V323, V322 == V324, V323 == V325, V315 == V326, V324 == V328, V325 == V329, V328 == V330, V329 == V331, V330 == V332, V331 == V333, V332 == V334, V333 == V335, V334 == V336, V335 == V337, V336 == V338, V338 == V339, V339 == V340, V337 == V341, V340 == V342, V341 == V343, V342 == V344, V343 == V345, V344 == V346, V345 == V347, V346 == V348, V347 == V349, V348 == V350, V349 == V351, V350 == V352, V351 == V353, V352 == V354, V353 == V355, V354 == V356, V355 == V357, V356 == V358, V358 == V359, V359 == V360, V360 == V361, V361 == V362, V362 == V363, V357 == V364, V363 == V365, V364 == V366, V365 == V367, V366 == V368, V367 == V369, V369 == V370, V370 == V371, V371 == V372, V372 == V373, V368 == V374, V373 == V375, V374 == V376, V375 == V377, V376 == V378, V377 == V379, V378 == V380, V379 == V381, V381 == V382, V382 == V383, V383 == V384, V384 == V385; #2457 ), references = 2, size of lhs = 231:
% 98.43/98.62 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), P_s-{F}(V8,V1), P_s-{F}(V9,V1), P_s-{F}(V10,V1), P_s-{F}(V11,V1), P_s-{F}(V12,V1), P_s-{F}(V13,V1), P_s-{F}(V14,V1), P_s-{F}(V15,V1), P_s-{F}(V16,V1), P_s-{F}(V17,V1), P_s-{F}(V18,V1), P_s-{F}(V19,V1), P_s-{F}(V20,V1), P_s-{F}(V1,V21), V21 == V0, V21 == V1, V3 == V21, V4 == V21, V5 == V21, V6 == V21, V7 == V21, V8 == V21, V9 == V21, V10 == V21, V11 == V21, V12 == V21, V13 == V21, V14 == V21, V15 == V21, V19 == V21, V16 == V21, V20 == V21, V17 == V21, V18 == V21, P_s-{F}(V22,V21), V22 == V21, P_s-{F}(V23,V21), V23 == V21, P_s-{F}(V24,V21), V24 == V21, P_s-{F}(V25,V21), V25 == V21, P_s-{F}(V26,V21), V26 == V21, P_s-{F}(V27,V21), V27 == V21, P_s-{F}(V28,V21), V28 == V21, P_s-{F}(V29,V21), V29 == V21, P_s-{F}(V30,V21), V30 == V21, P_s-{F}(V31,V21), P_s-{F}(V32,V31), V32 == V21, P_s-{F}(V33,V21), P_s-{F}(V34,V33), V34 == V21, P_s-{F}(V35,V21), P_s-{F}(V36,V35), V36 == V21, P_s-{F}(V37,V21), P_s-{F}(V38,V37), V38 == V21, P_s-{F}(V39,V21), P_s-{F}(V40,V39), V40 == V21, P_s-{F}(V41,V21), P_s-{F}(V42,V41), V42 == V21, P_s-{F}(V43,V21), P_s-{F}(V44,V43), V44 == V21, P_s-{F}(V45,V21), P_s-{F}(V46,V45), V46 == V21, P_s-{F}(V47,V21), P_s-{F}(V48,V47), V48 == V21, P_s-{F}(V49,V21), P_s-{F}(V50,V49), V50 == V21, P_s-{F}(V51,V21), P_s-{F}(V52,V51), V52 == V21, P_s-{F}(V53,V21), P_s-{F}(V54,V53), V54 == V21, P_s-{F}(V55,V21), P_s-{F}(V56,V55), V56 == V21, P_s-{F}(V57,V21), P_s-{F}(V58,V57), V58 == V21, P_s-{F}(V59,V21), P_s-{F}(V60,V59), V60 == V21, P_s-{F}(V61,V21), P_s-{F}(V62,V61), V62 == V21, P_s-{F}(V63,V21), P_s-{F}(V64,V63), V64 == V21, P_s-{F}(V65,V21), P_s-{F}(V66,V65), V66 == V21, P_s-{F}(V67,V21), P_s-{F}(V68,V67), V68 == V21, P_s-{F}(V69,V21), P_s-{F}(V70,V69), V70 == V21, P_s-{F}(V71,V21), P_s-{F}(V72,V71), V72 == V21, P_s-{F}(V73,V21), P_s-{F}(V74,V73), V74 == V21, P_s-{F}(V75,V21), P_s-{F}(V76,V75), V76 == V21, P_s-{F}(V77,V21), P_s-{F}(V78,V77), V78 == V21, P_s-{F}(V79,V21), P_s-{F}(V80,V79), V80 == V21, P_s-{F}(V81,V21), P_s-{F}(V82,V81), V82 == V21, P_s-{F}(V83,V21), P_s-{F}(V84,V83), V84 == V21, P_s-{F}(V85,V21), P_s-{F}(V86,V85), V86 == V21, P_s-{F}(V87,V21), P_s-{F}(V88,V87), V88 == V21, P_s-{F}(V89,V21), P_s-{F}(V90,V89), V90 == V21, P_s-{F}(V91,V21), P_s-{F}(V92,V91), V92 == V21, P_s-{F}(V93,V21), P_s-{F}(V94,V93), V94 == V21, P_s-{F}(V95,V21), P_s-{F}(V96,V95), V96 == V21, P_s-{F}(V97,V21), P_s-{F}(V98,V97), V98 == V21, P_s-{F}(V99,V21), P_s-{F}(V100,V99), V100 == V21, P_s-{F}(V101,V21), P_s-{F}(V102,V101), V102 == V21, P_s-{F}(V103,V21), P_s-{F}(V104,V103), V104 == V21, P_s-{F}(V105,V21), P_s-{F}(V106,V105), V106 == V21, P_s-{F}(V107,V21), P_s-{F}(V108,V107), V108 == V21, P_s-{F}(V109,V21), P_s-{F}(V110,V109), V110 == V21, P_s-{F}(V111,V21), P_s-{F}(V112,V111), V112 == V21, P_s-{F}(V113,V21), P_s-{F}(V114,V113), V114 == V21, P_s-{F}(V115,V21), P_s-{F}(V116,V115), V116 == V21, P_s-{F}(V117,V21), P_s-{F}(V118,V117), V118 == V21, P_s-{F}(V119,V21), P_s-{F}(V120,V119), V120 == V21, P_s-{F}(V121,V21), P_s-{F}(V122,V121), V122 == V21, P_s-{F}(V123,V124), V0 == V124, V124 == V1, P_s-{F}(V125,V124), P_s-{F}(V126,V125), V126 == V21, P_s-{F}(V127,V128), V0 == V128, V128 == V1, V127 == V21, P_s-{F}(V129,V128), P_s-{F}(V130,V129), V130 == V21, P_s-{F}(V131,V132), V0 == V132, V132 == V1, V131 == V21, P_s-{F}(V133,V132), P_s-{F}(V134,V133), V134 == V21, P_s-{F}(V135,V136), V0 == V136, V136 == V1, V135 == V21, P_s-{F}(V137,V136), P_s-{F}(V138,V137), V138 == V21, P_s-{F}(V139,V140), V2 == V140, V123 == V140, V139 == V21 | r-{T}(V0,V1)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2819: mergings( V0 == V2; #2817 ), references = 2, size of lhs = 54:
% 98.43/98.62 P_z-{F}(V0), b-{F}(V0,V1), V0 == V1, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), r-{F}(V0,V5), P_s-{F}(V6,V1), P_s-{F}(V7,V5), P_s-{F}(V8,V9), V9 == V1, V9 == V0, V5 == V9, P_s-{F}(V10,V9), P_s-{F}(V11,V12), V0 == V12, V12 == V9, V12 == V1, P_s-{F}(V13,V14), V1 == V14, V14 == V0, V14 == V9, P_s-{F}(V15,V14), P_s-{F}(V16,V17), V0 == V17, V17 == V14, V17 == V1, P_s-{F}(V18,V19), V0 == V19, V19 == V1, P_s-{F}(V20,V19), P_s-{F}(V21,V22), V9 == V22, V22 == V5, V22 == V0, #-{F} V23, V8 == V23, V2 == V23, V11 == V23, #-{F} V24, V13 == V24, V3 == V24, V16 == V24, #-{F} V25, V6 == V25, V10 == V25, V15 == V25, V20 == V25, V7 == V25, V21 == V25, #-{F} V26, V25 == V26, V4 == V26, V18 == V26 | b-{T}(V1,V0)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2828: mergings( V0 == V3, V3 == V1, V1 == V12, V12 == V13; #2823 ), references = 1, size of lhs = 141:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), P_s-{F}(V2,V1), P_s-{F}(V0,V3), V3 == V0, P_s-{F}(V4,V3), P_s-{F}(V5,V3), P_s-{F}(V6,V3), P_s-{F}(V7,V3), r-{F}(V0,V8), b-{F}(V8,V0), r-{F}(V8,V9), V9 == V0, P_s-{F}(V10,V9), P_s-{F}(V11,V9), P_s-{F}(V12,V9), P_s-{F}(V13,V9), P_s-{F}(V14,V9), P_s-{F}(V15,V9), P_s-{F}(V16,V8), P_s-{F}(V17,V18), V18 == V9, V18 == V0, V1 == V18, P_s-{F}(V19,V18), P_s-{F}(V20,V21), V0 == V21, V21 == V18, V21 == V9, P_s-{F}(V22,V23), V9 == V23, V23 == V0, V23 == V18, P_s-{F}(V24,V23), P_s-{F}(V25,V26), V0 == V26, V26 == V23, V26 == V9, P_s-{F}(V27,V28), V0 == V28, V28 == V9, P_s-{F}(V29,V28), P_s-{F}(V30,V31), V18 == V31, V31 == V1, V31 == V0, P_s-{F}(V32,V33), V8 == V33, V3 == V33, V0 == V33, V33 == V9, P_s-{F}(V34,V33), P_s-{F}(V35,V33), P_s-{F}(V36,V33), P_s-{F}(V37,V33), P_s-{F}(V38,V33), P_s-{F}(V39,V38), P_s-{F}(V40,V33), P_s-{F}(V41,V40), P_s-{F}(V42,V33), P_s-{F}(V43,V42), P_s-{F}(V44,V33), P_s-{F}(V45,V44), P_s-{F}(V46,V33), P_s-{F}(V47,V46), P_s-{F}(V48,V33), P_s-{F}(V49,V48), P_s-{F}(V50,V51), V0 == V51, V51 == V9, V51 == V33, P_s-{F}(V52,V53), V53 == V0, V53 == V33, V53 == V3, P_s-{F}(V54,V53), P_s-{F}(V55,V54), P_s-{F}(V56,V57), V8 == V57, V57 == V9, V33 == V57, V57 == V0, V3 == V57, P_s-{F}(V58,V57), P_s-{F}(V59,V58), P_s-{F}(V60,V57), P_s-{F}(V61,V60), P_s-{F}(V62,V63), V63 == V33, V63 == V0, V63 == V3, P_s-{F}(V64,V63), P_s-{F}(V65,V64), P_s-{F}(V66,V67), V16 == V67, V34 == V67, V35 == V67, V10 == V67, V52 == V67, V4 == V67, V56 == V67, V36 == V67, V5 == V67, V37 == V67, V6 == V67, V62 == V67, V7 == V67, V66 == V67, V39 == V67, V55 == V67, V47 == V67, V43 == V67, V59 == V67, V61 == V67, V41 == V67, V49 == V67, V45 == V67, V65 == V67, #-{F} V68, V17 == V68, V11 == V68, V20 == V68, #-{F} V69, V22 == V69, V12 == V69, V25 == V69, #-{F} V70, V14 == V70, V19 == V70, V24 == V70, V29 == V70, V2 == V70, V30 == V70, #-{F} V71, V70 == V71, V13 == V71, V27 == V71, #-{F} V72, V15 == V72, V32 == V72, V50 == V72 | r-{T}(V0,V9)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2836: mergings( V2 == V3, V3 == V4, V4 == V12, V12 == V13, V13 == V23; #2830 ), references = 1, size of lhs = 70:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), P_s-{F}(V2,V1), P_s-{F}(V0,V3), V3 == V0, P_s-{F}(V4,V3), P_s-{F}(V5,V3), P_s-{F}(V6,V3), P_s-{F}(V7,V3), r-{F}(V0,V8), b-{F}(V8,V0), r-{F}(V8,V9), V9 == V0, P_s-{F}(V10,V9), P_s-{F}(V11,V9), P_s-{F}(V12,V9), P_s-{F}(V13,V9), P_s-{F}(V14,V9), P_s-{F}(V15,V9), P_s-{F}(V16,V8), r-{F}(V0,V17), r-{F}(V17,V9), P_s-{F}(V18,V19), V0 == V19, V19 == V9, P_s-{F}(V20,V21), V9 == V21, V21 == V0, P_s-{F}(V22,V21), P_s-{F}(V23,V24), V24 == V1, V24 == V0, P_s-{F}(V25,V26), V8 == V26, V3 == V26, V0 == V26, V26 == V9, P_s-{F}(V27,V26), P_s-{F}(V28,V26), P_s-{F}(V29,V26), P_s-{F}(V30,V26), P_s-{F}(V31,V26), P_s-{F}(V32,V31), P_s-{F}(V33,V26), P_s-{F}(V34,V33), P_s-{F}(V35,V26), P_s-{F}(V36,V35), P_s-{F}(V37,V26), P_s-{F}(V38,V37), P_s-{F}(V39,V26), P_s-{F}(V40,V39), P_s-{F}(V41,V26), P_s-{F}(V42,V41), P_s-{F}(V43,V44), V44 == V0, V44 == V26, V44 == V3, P_s-{F}(V45,V44), P_s-{F}(V46,V45), P_s-{F}(V47,V48), P_s-{F}(V49,V48), P_s-{F}(V50,V51), V51 == V26, V51 == V0, V51 == V3, P_s-{F}(V52,V51), P_s-{F}(V53,V52), #-{F} V54, V13 == V54, V48 == V54 | P_s-{T}(V48,V9), P_s-{T}(V48,V0), P_s-{T}(V48,V1), P_s-{T}(V48,V19), P_s-{T}(V48,V21), P_s-{T}(V48,V24), P_s-{T}(V48,V26), P_s-{T}(V48,V8), P_s-{T}(V48,V3), P_s-{T}(V48,V16), P_s-{T}(V48,V27), P_s-{T}(V48,V28), P_s-{T}(V48,V10), P_s-{T}(V48,V43), P_s-{T}(V48,V4), P_s-{T}(V48,V48), P_s-{T}(V48,V29), P_s-{T}(V48,V5), P_s-{T}(V48,V30), P_s-{T}(V48,V6), P_s-{T}(V48,V50), P_s-{T}(V48,V7), P_s-{T}(V48,V32), P_s-{T}(V48,V46), P_s-{T}(V48,V40), P_s-{T}(V48,V36), P_s-{T}(V48,V47), P_s-{T}(V48,V49), P_s-{T}(V48,V34), P_s-{T}(V48,V42), P_s-{T}(V48,V38), P_s-{T}(V48,V53), P_s-{T}(V48,V11), P_s-{T}(V48,V18), P_s-{T}(V48,V20), P_s-{T}(V48,V12), P_s-{T}(V48,V14), P_s-{T}(V48,V22), P_s-{T}(V48,V2), P_s-{T}(V48,V23), P_s-{T}(V48,V54), P_s-{T}(V48,V15), P_s-{T}(V48,V25)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2889: mergings( V0 == V1, V1 == V10, V10 == V11, V11 == V21, V21 == V60, V60 == V2, V2 == V62, V62 == V64, V64 == V66, V66 == V68, V68 == V70, V70 == V72, V72 == V74, V74 == V20, V5 == V12, V20 == V76, V76 == V78, V78 == V80, V80 == V82, V82 == V6, V6 == V84, V84 == V86, V86 == V7, V7 == V88, V88 == V8, V8 == V90, V90 == V9, V9 == V92, V92 == V51, V12 == V50, V51 == V94, V94 == V96, V96 == V98, V98 == V100, V100 == V102, V102 == V104, V104 == V106, V106 == V58, V50 == V57, V49 == V56, V58 == V108, V108 == V110, V110 == V112, V112 == V114, V114 == V116, V116 == V118, V118 == V4, V57 == V3, V4 == V120, V120 == V122, V122 == V124; #2837 ), references = 1, size of lhs = 121:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), P_s-{F}(V0,V1), r-{F}(V1,V2), V2 == V0, P_s-{F}(V3,V2), r-{F}(V0,V4), r-{F}(V4,V2), P_s-{F}(V5,V2), P_s-{F}(V6,V1), P_s-{F}(V7,V1), P_s-{F}(V8,V1), P_s-{F}(V1,V9), V9 == V0, V9 == V1, P_s-{F}(V10,V2), P_s-{F}(V11,V10), P_s-{F}(V12,V2), P_s-{F}(V13,V12), P_s-{F}(V14,V2), P_s-{F}(V15,V14), P_s-{F}(V16,V2), P_s-{F}(V17,V16), P_s-{F}(V18,V2), P_s-{F}(V19,V18), P_s-{F}(V20,V9), P_s-{F}(V21,V20), P_s-{F}(V22,V9), P_s-{F}(V23,V22), P_s-{F}(V24,V25), V1 == V25, V0 == V25, V25 == V2, V9 == V25, P_s-{F}(V26,V25), P_s-{F}(V27,V25), P_s-{F}(V28,V27), P_s-{F}(V29,V25), P_s-{F}(V30,V29), P_s-{F}(V31,V25), P_s-{F}(V32,V31), P_s-{F}(V33,V25), P_s-{F}(V34,V33), P_s-{F}(V35,V25), P_s-{F}(V36,V35), P_s-{F}(V37,V36), P_s-{F}(V38,V25), P_s-{F}(V39,V38), P_s-{F}(V40,V39), P_s-{F}(V41,V25), P_s-{F}(V42,V41), P_s-{F}(V43,V42), P_s-{F}(V44,V25), P_s-{F}(V45,V44), P_s-{F}(V46,V45), P_s-{F}(V47,V25), P_s-{F}(V48,V47), P_s-{F}(V49,V48), P_s-{F}(V50,V25), P_s-{F}(V51,V50), P_s-{F}(V52,V51), P_s-{F}(V53,V54), V0 == V54, V54 == V2, P_s-{F}(V55,V54), P_s-{F}(V56,V55), P_s-{F}(V57,V58), V2 == V58, V58 == V0, P_s-{F}(V59,V58), P_s-{F}(V60,V59), P_s-{F}(V61,V58), P_s-{F}(V62,V61), P_s-{F}(V63,V64), V64 == V1, V64 == V0, P_s-{F}(V65,V64), P_s-{F}(V66,V65), P_s-{F}(V67,V68), V5 == V68, V6 == V68, V53 == V68, V57 == V68, V63 == V68, V26 == V68, V7 == V68, V8 == V68, V28 == V68, V30 == V68, V11 == V68, V21 == V68, V67 == V68, V32 == V68, V34 == V68, V23 == V68, V37 == V68, V49 == V68, V43 == V68, V40 == V68, V52 == V68, V46 == V68, V13 == V68, V56 == V68, V60 == V68, V15 == V68, V17 == V68, V62 == V68, V66 == V68, V19 == V68, P_s-{F}(V69,V68), P_s-{F}(V70,V69), V70 == V68, P_s-{F}(V71,V68), P_s-{F}(V72,V71), V72 == V68, P_s-{F}(V73,V74), V3 == V74, V68 == V74, V73 == V68 | P_s-{T}(V68,V24)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2945: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V14, V14 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V22, V22 == V24, V11 == V1, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V1 == V39, V38 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V39 == V49, V40 == V50, V48 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V49 == V10, V57 == V58, V58 == V59, V59 == V60, V60 == V61; #2891 ), references = 1, size of lhs = 121:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), P_s-{F}(V0,V1), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V1,V5), V5 == V0, V5 == V1, P_s-{F}(V6,V5), P_s-{F}(V7,V6), P_s-{F}(V8,V5), P_s-{F}(V9,V8), P_s-{F}(V10,V11), V1 == V11, V11 == V0, P_s-{F}(V12,V11), P_s-{F}(V13,V11), P_s-{F}(V14,V13), P_s-{F}(V15,V11), P_s-{F}(V16,V15), P_s-{F}(V17,V11), P_s-{F}(V18,V17), P_s-{F}(V19,V11), P_s-{F}(V20,V19), P_s-{F}(V21,V11), P_s-{F}(V22,V21), P_s-{F}(V23,V24), V1 == V24, V0 == V24, V24 == V11, V5 == V24, P_s-{F}(V25,V24), P_s-{F}(V26,V25), P_s-{F}(V27,V24), P_s-{F}(V28,V27), P_s-{F}(V29,V24), P_s-{F}(V30,V29), P_s-{F}(V31,V24), P_s-{F}(V32,V31), P_s-{F}(V33,V24), P_s-{F}(V34,V33), P_s-{F}(V35,V24), P_s-{F}(V36,V35), P_s-{F}(V37,V36), P_s-{F}(V38,V24), P_s-{F}(V39,V38), P_s-{F}(V40,V39), P_s-{F}(V41,V24), P_s-{F}(V42,V41), P_s-{F}(V43,V42), P_s-{F}(V44,V24), P_s-{F}(V45,V44), P_s-{F}(V46,V45), P_s-{F}(V47,V24), P_s-{F}(V48,V47), P_s-{F}(V49,V48), P_s-{F}(V50,V24), P_s-{F}(V51,V50), P_s-{F}(V52,V51), P_s-{F}(V53,V54), V0 == V54, V54 == V11, P_s-{F}(V55,V54), P_s-{F}(V56,V55), P_s-{F}(V57,V58), V11 == V58, V58 == V0, P_s-{F}(V59,V58), P_s-{F}(V60,V59), P_s-{F}(V61,V58), P_s-{F}(V62,V61), P_s-{F}(V63,V64), V64 == V1, V64 == V0, P_s-{F}(V65,V64), P_s-{F}(V66,V65), P_s-{F}(V67,V68), V12 == V68, V2 == V68, V53 == V68, V57 == V68, V63 == V68, V23 == V68, V3 == V68, V4 == V68, V28 == V68, V30 == V68, V14 == V68, V7 == V68, V67 == V68, V32 == V68, V34 == V68, V9 == V68, V37 == V68, V49 == V68, V43 == V68, V40 == V68, V52 == V68, V46 == V68, V16 == V68, V56 == V68, V60 == V68, V18 == V68, V20 == V68, V62 == V68, V66 == V68, V22 == V68, V26 == V68, P_s-{F}(V69,V68), P_s-{F}(V70,V69), V70 == V68, P_s-{F}(V71,V68), P_s-{F}(V72,V71), V72 == V68, P_s-{F}(V73,V74), V10 == V74, V68 == V74, V73 == V68 | b-{T}(V1,V11)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2950: mergings( V0 == V1, V1 == V9; #2947 ), references = 1, size of lhs = 55:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), P_s-{F}(V2,V1), b-{F}(V3,V0), b-{F}(V3,V4), V0 == V4, P_s-{F}(V5,V4), P_s-{F}(V6,V4), P_s-{F}(V7,V4), P_s-{F}(V8,V4), P_s-{F}(V9,V10), V10 == V4, V10 == V0, V1 == V10, P_s-{F}(V11,V10), P_s-{F}(V12,V13), V0 == V13, V13 == V10, V13 == V4, P_s-{F}(V14,V15), V4 == V15, V15 == V0, V15 == V10, P_s-{F}(V16,V15), P_s-{F}(V17,V18), V0 == V18, V18 == V15, V18 == V4, P_s-{F}(V19,V20), V0 == V20, V20 == V4, P_s-{F}(V21,V20), P_s-{F}(V22,V23), V10 == V23, V23 == V1, V23 == V0, #-{F} V24, V9 == V24, V5 == V24, V12 == V24, #-{F} V25, V14 == V25, V6 == V25, V17 == V25, #-{F} V26, V8 == V26, V11 == V26, V16 == V26, V21 == V26, V2 == V26, V22 == V26, #-{F} V27, V26 == V27, V7 == V27, V19 == V27 | r-{T}(V0,V4)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2954: mergings( V2 == V3; #2952 ), references = 1, size of lhs = 15:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, b-{F}(V3,V4), V3 == V4, r-{F}(V4,V3), r-{F}(V4,V2), r-{F}(V5,V3), r-{F}(V5,V2), #-{F} V6, #-{F} V7, V3 == V7, V7 == V2, V7 == V4 | P_s-{T}(V6,V3), P_s-{T}(V6,V2), P_s-{T}(V6,V4), P_s-{T}(V6,V7)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #2960: mergings( V0 == V1, V1 == V9, V9 == V11, V11 == V13; #2955 ), references = 1, size of lhs = 20:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, b-{F}(V3,V4), V3 == V4, r-{F}(V4,V3), r-{F}(V4,V2), r-{F}(V5,V3), r-{F}(V5,V2), P_s-{F}(V6,V3), P_s-{F}(V7,V2), P_s-{F}(V8,V9), V3 == V9, V9 == V2, V9 == V4, #-{F} V10, V6 == V10, V7 == V10, V8 == V10 | P_s-{T}(V10,V4)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #3026: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V13, V13 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V21, V21 == V23, V11 == V12, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V12 == V38, V37 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V38 == V48, V39 == V49, V47 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V48 == V10, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68; #2964 ), references = 1, size of lhs = 83:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, P_s-{F}(V0,V1), b-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V1,V5), V5 == V0, V5 == V1, r-{F}(V0,V6), P_s-{F}(V7,V6), r-{F}(V0,V8), V8 == V0, b-{F}(V8,V0), P_s-{F}(V9,V8), P_s-{F}(V10,V5), P_s-{F}(V11,V10), P_s-{F}(V12,V5), P_s-{F}(V13,V12), P_s-{F}(V14,V15), V1 == V15, V0 == V15, V15 == V8, P_s-{F}(V16,V15), P_s-{F}(V17,V15), P_s-{F}(V18,V15), P_s-{F}(V19,V15), P_s-{F}(V20,V15), P_s-{F}(V21,V15), P_s-{F}(V22,V15), P_s-{F}(V23,V22), P_s-{F}(V24,V15), P_s-{F}(V25,V24), P_s-{F}(V26,V15), P_s-{F}(V27,V26), P_s-{F}(V28,V15), P_s-{F}(V29,V28), P_s-{F}(V30,V15), P_s-{F}(V31,V30), P_s-{F}(V32,V33), P_s-{F}(V34,V33), P_s-{F}(V35,V33), P_s-{F}(V36,V33), P_s-{F}(V37,V33), P_s-{F}(V38,V33), P_s-{F}(V39,V33), P_s-{F}(V40,V33), P_s-{F}(V41,V33), P_s-{F}(V42,V33), P_s-{F}(V43,V33), P_s-{F}(V44,V43), P_s-{F}(V45,V33), P_s-{F}(V46,V45), P_s-{F}(V47,V33), P_s-{F}(V48,V47), P_s-{F}(V49,V33), P_s-{F}(V50,V49), P_s-{F}(V51,V33), P_s-{F}(V52,V51), P_s-{F}(V53,V33), P_s-{F}(V54,V53), P_s-{F}(V55,V56), V56 == V1, V56 == V0, P_s-{F}(V57,V56), P_s-{F}(V58,V57), P_s-{F}(V59,V60), V14 == V60, P_s-{F}(V61,V62), V0 == V62, V62 == V15, P_s-{F}(V63,V64), V15 == V64, V64 == V0, P_s-{F}(V65,V64), P_s-{F}(V66,V67), V67 == V6, V67 == V0, #-{F} V68, V19 == V68, V33 == V68 | P_s-{T}(V33,V1), P_s-{T}(V33,V0), P_s-{T}(V33,V15), P_s-{T}(V33,V5), P_s-{T}(V33,V16), P_s-{T}(V33,V2), P_s-{T}(V33,V33), P_s-{T}(V33,V55), P_s-{T}(V33,V3), P_s-{T}(V33,V4), P_s-{T}(V33,V34), P_s-{T}(V33,V35), P_s-{T}(V33,V23), P_s-{T}(V33,V11), P_s-{T}(V33,V36), P_s-{T}(V33,V37), P_s-{T}(V33,V13), P_s-{T}(V33,V44), P_s-{T}(V33,V52), P_s-{T}(V33,V48), P_s-{T}(V33,V46), P_s-{T}(V33,V54), P_s-{T}(V33,V50), P_s-{T}(V33,V25), P_s-{T}(V33,V38), P_s-{T}(V33,V39), P_s-{T}(V33,V27), P_s-{T}(V33,V29), P_s-{T}(V33,V40), P_s-{T}(V33,V58), P_s-{T}(V33,V31), P_s-{T}(V33,V32), P_s-{T}(V33,V41), P_s-{T}(V33,V42), P_s-{T}(V33,V60), P_s-{T}(V33,V59), P_s-{T}(V33,V6), P_s-{T}(V33,V62), P_s-{T}(V33,V64), P_s-{T}(V33,V67), P_s-{T}(V33,V8), P_s-{T}(V33,V17), P_s-{T}(V33,V61), P_s-{T}(V33,V63), P_s-{T}(V33,V18), P_s-{T}(V33,V20), P_s-{T}(V33,V65), P_s-{T}(V33,V7), P_s-{T}(V33,V66), P_s-{T}(V33,V68), P_s-{T}(V33,V9), P_s-{T}(V33,V21)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #3162: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V11, V11 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V19, V19 == V21, V21 == V7, V10 == V9, V7 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V9 == V36, V35 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V36 == V46, V37 == V47, V45 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V46 == V8, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V130, V130 == V132, V132 == V134, V134 == V136, V136 == V138, V138 == V140, V140 == V12, V12 == V142, V142 == V144, V144 == V18, V18 == V20, V20 == V146, V146 == V148, V148 == V84, V8 == V83, V47 == V76, V84 == V72, V83 == V71, V72 == V150, V150 == V152, V152 == V74, V71 == V73, V74 == V105, V73 == V104, V76 == V94, V105 == V113, V104 == V112, V113 == V109, V112 == V108, V109 == V107, V108 == V106, V107 == V115, V106 == V114, V115 == V111, V114 == V110, V111 == V86, V110 == V85, V86 == V154, V154 == V156, V156 == V88, V85 == V87, V88 == V90, V87 == V89, V90 == V158, V158 == V119, V89 == V118, V94 == V117, V119 == V92, V118 == V91, V92 == V160, V160 == V162, V162 == V164, V164 == V166, V166 == V168, V168 == V170, V170 == V172, V172 == V174, V174 == V176, V176 == V178, V178 == V180, V180 == V122, V91 == V123, V122 == V124, V123 == V125, V124 == V182, V182 == V184, V184 == V126, V126 == V68, V125 == V67, V68 == V186, V186 == V129, V129 == V70, V67 == V69; #3027 ), references = 2, size of lhs = 90:
% 98.43/98.62 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), P_s-{F}(V0,V1), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V1,V4), V2 == V4, V3 == V4, V4 == V1, V4 == V0, P_s-{F}(V5,V4), V5 == V4, P_s-{F}(V6,V4), V6 == V4, P_s-{F}(V7,V4), P_s-{F}(V8,V4), V8 == V0, P_s-{F}(V9,V4), P_s-{F}(V10,V4), V10 == V4, P_s-{F}(V11,V4), V11 == V4, P_s-{F}(V12,V1), V12 == V4, P_s-{F}(V13,V1), V13 == V4, P_s-{F}(V14,V1), V14 == V4, P_s-{F}(V15,V1), V15 == V4, P_s-{F}(V16,V4), P_s-{F}(V17,V16), V17 == V4, P_s-{F}(V18,V4), P_s-{F}(V19,V18), V19 == V4, P_s-{F}(V20,V4), P_s-{F}(V21,V20), V21 == V4, P_s-{F}(V22,V4), P_s-{F}(V23,V22), V23 == V4, P_s-{F}(V24,V4), P_s-{F}(V25,V24), V25 == V4, P_s-{F}(V26,V4), P_s-{F}(V27,V26), V27 == V4, P_s-{F}(V28,V4), P_s-{F}(V29,V28), V29 == V4, P_s-{F}(V30,V4), P_s-{F}(V31,V30), V31 == V4, P_s-{F}(V32,V4), P_s-{F}(V33,V32), V33 == V4, P_s-{F}(V34,V4), P_s-{F}(V35,V34), V35 == V4, P_s-{F}(V36,V4), P_s-{F}(V37,V36), V37 == V4, P_s-{F}(V38,V4), P_s-{F}(V39,V38), V39 == V4, P_s-{F}(V40,V4), P_s-{F}(V41,V40), V41 == V4, P_s-{F}(V42,V4), P_s-{F}(V43,V42), V43 == V4, P_s-{F}(V44,V4), P_s-{F}(V45,V44), V45 == V4, P_s-{F}(V46,V47), V7 == V47, V46 == V4, P_s-{F}(V48,V47), P_s-{F}(V49,V48), V49 == V4, P_s-{F}(V50,V51), V51 == V1, V51 == V0, V50 == V4, P_s-{F}(V52,V51), P_s-{F}(V53,V52), V53 == V4 | P_s-{T}(V4,V9)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #3174: mergings( V2 == V33; #3172 ), references = 1, size of lhs = 115:
% 98.43/98.62 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), P_s-{F}(V8,V1), P_s-{F}(V9,V1), P_s-{F}(V10,V1), P_s-{F}(V11,V1), P_s-{F}(V12,V1), P_s-{F}(V13,V1), P_s-{F}(V14,V1), P_s-{F}(V15,V1), P_s-{F}(V16,V1), P_s-{F}(V17,V1), P_s-{F}(V18,V1), P_s-{F}(V19,V1), P_s-{F}(V20,V1), P_s-{F}(V21,V1), P_s-{F}(V22,V1), P_s-{F}(V23,V1), P_s-{F}(V24,V1), P_s-{F}(V25,V1), P_s-{F}(V26,V1), P_s-{F}(V27,V1), P_s-{F}(V28,V1), P_s-{F}(V29,V1), P_s-{F}(V30,V1), P_s-{F}(V31,V1), P_s-{F}(V32,V1), P_s-{F}(V33,V1), P_s-{F}(V34,V1), P_s-{F}(V35,V1), P_s-{F}(V36,V1), P_s-{F}(V37,V1), P_s-{F}(V38,V1), P_s-{F}(V39,V1), P_s-{F}(V40,V1), P_s-{F}(V41,V1), P_s-{F}(V42,V1), P_s-{F}(V43,V1), P_s-{F}(V44,V1), P_s-{F}(V45,V1), P_s-{F}(V46,V1), P_s-{F}(V47,V1), P_s-{F}(V48,V1), P_s-{F}(V49,V1), P_s-{F}(V50,V1), P_s-{F}(V51,V1), P_s-{F}(V52,V1), P_s-{F}(V53,V1), P_s-{F}(V54,V1), P_s-{F}(V55,V1), P_s-{F}(V56,V1), P_s-{F}(V57,V1), P_s-{F}(V58,V1), P_s-{F}(V59,V1), P_s-{F}(V60,V1), P_s-{F}(V61,V1), P_s-{F}(V62,V1), P_s-{F}(V63,V1), P_s-{F}(V64,V1), P_s-{F}(V65,V1), P_s-{F}(V66,V1), P_s-{F}(V67,V1), P_s-{F}(V68,V1), P_s-{F}(V69,V1), P_s-{F}(V70,V1), P_s-{F}(V71,V1), P_s-{F}(V72,V1), P_s-{F}(V73,V1), P_s-{F}(V74,V1), P_s-{F}(V75,V1), P_s-{F}(V76,V1), P_s-{F}(V77,V1), P_s-{F}(V78,V1), P_s-{F}(V79,V1), P_s-{F}(V80,V1), P_s-{F}(V81,V1), P_s-{F}(V82,V1), P_s-{F}(V83,V1), P_s-{F}(V84,V1), P_s-{F}(V85,V1), P_s-{F}(V86,V1), P_s-{F}(V87,V1), P_s-{F}(V88,V1), P_s-{F}(V89,V1), P_s-{F}(V90,V1), P_s-{F}(V91,V1), P_s-{F}(V92,V1), P_s-{F}(V93,V1), P_s-{F}(V94,V1), P_s-{F}(V95,V1), P_s-{F}(V96,V1), P_s-{F}(V97,V1), P_s-{F}(V98,V1), P_s-{F}(V99,V1), P_s-{F}(V100,V1), P_s-{F}(V101,V1), P_s-{F}(V102,V1), P_s-{F}(V103,V1), P_s-{F}(V104,V1), P_s-{F}(V105,V1), P_s-{F}(V106,V1), P_s-{F}(V107,V1), P_s-{F}(V108,V1), P_s-{F}(V109,V1), P_s-{F}(V110,V1), P_s-{F}(V111,V1), P_s-{F}(V112,V1), P_s-{F}(V113,V1) | P_s-{T}(V1,V0), P_s-{T}(V1,V1), P_s-{T}(V1,V8), P_s-{T}(V1,V9), P_s-{T}(V1,V10), P_s-{T}(V1,V11), P_s-{T}(V1,V12), P_s-{T}(V1,V13), P_s-{T}(V1,V14), P_s-{T}(V1,V15), P_s-{T}(V1,V16), P_s-{T}(V1,V17), P_s-{T}(V1,V18), P_s-{T}(V1,V19), P_s-{T}(V1,V20), P_s-{T}(V1,V24), P_s-{T}(V1,V21), P_s-{T}(V1,V25), P_s-{T}(V1,V22), P_s-{T}(V1,V23), P_s-{T}(V1,V26), P_s-{T}(V1,V27), P_s-{T}(V1,V28), P_s-{T}(V1,V29), P_s-{T}(V1,V30), P_s-{T}(V1,V31), P_s-{T}(V1,V35), P_s-{T}(V1,V36), P_s-{T}(V1,V37), P_s-{T}(V1,V38), P_s-{T}(V1,V39), P_s-{T}(V1,V40), P_s-{T}(V1,V41), P_s-{T}(V1,V42), P_s-{T}(V1,V43), P_s-{T}(V1,V44), P_s-{T}(V1,V45), P_s-{T}(V1,V46), P_s-{T}(V1,V47), P_s-{T}(V1,V48), P_s-{T}(V1,V49), P_s-{T}(V1,V50), P_s-{T}(V1,V51), P_s-{T}(V1,V52), P_s-{T}(V1,V53), P_s-{T}(V1,V54), P_s-{T}(V1,V55), P_s-{T}(V1,V56), P_s-{T}(V1,V57), P_s-{T}(V1,V58), P_s-{T}(V1,V59), P_s-{T}(V1,V60), P_s-{T}(V1,V61), P_s-{T}(V1,V62), P_s-{T}(V1,V63), P_s-{T}(V1,V64), P_s-{T}(V1,V65), P_s-{T}(V1,V66), P_s-{T}(V1,V67), P_s-{T}(V1,V68), P_s-{T}(V1,V69), P_s-{T}(V1,V70), P_s-{T}(V1,V71), P_s-{T}(V1,V72), P_s-{T}(V1,V73), P_s-{T}(V1,V74), P_s-{T}(V1,V75), P_s-{T}(V1,V76), P_s-{T}(V1,V77), P_s-{T}(V1,V78), P_s-{T}(V1,V79), P_s-{T}(V1,V80), P_s-{T}(V1,V81), P_s-{T}(V1,V82), P_s-{T}(V1,V83), P_s-{T}(V1,V84), P_s-{T}(V1,V85), P_s-{T}(V1,V86), P_s-{T}(V1,V87), P_s-{T}(V1,V88), P_s-{T}(V1,V89), P_s-{T}(V1,V90), P_s-{T}(V1,V91), P_s-{T}(V1,V92), P_s-{T}(V1,V93), P_s-{T}(V1,V94), P_s-{T}(V1,V95), P_s-{T}(V1,V96), P_s-{T}(V1,V4), P_s-{T}(V1,V32), P_s-{T}(V1,V33), P_s-{T}(V1,V34), P_s-{T}(V1,V5), P_s-{T}(V1,V6), P_s-{T}(V1,V97), P_s-{T}(V1,V98), P_s-{T}(V1,V99), P_s-{T}(V1,V100), P_s-{T}(V1,V101), P_s-{T}(V1,V102), P_s-{T}(V1,V103), P_s-{T}(V1,V104), P_s-{T}(V1,V105), P_s-{T}(V1,V106), P_s-{T}(V1,V107), P_s-{T}(V1,V2), P_s-{T}(V1,V3), P_s-{T}(V1,V108), P_s-{T}(V1,V109), P_s-{T}(V1,V110), P_s-{T}(V1,V111), P_s-{T}(V1,V7), P_s-{T}(V1,V112), P_s-{T}(V1,V113)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #3289: mergings( V32 == V0, V0 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V24, V24 == V21, V21 == V25, V25 == V22, V22 == V23, V23 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V4, V4 == V33, V33 == V34, V34 == V35, V35 == V5, V5 == V6, V6 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V2, V2 == V3, V3 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V7, V7 == V113, V113 == V114; #3175 ), references = 1, size of lhs = 3:
% 98.43/98.62 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0 | P_s-{T}(V1,V1)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #3294: mergings( V2 == V0, V0 == V3; #3291 ), references = 1, size of lhs = 1:
% 98.43/98.62 P_z-{F}(V0) | P_s-{T}(V0,V0)
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 #3297: exists( #8, #3295 ), references = 1, size of lhs = 0:
% 98.43/98.62 FALSE | FALSE
% 98.43/98.62 (used 0 times, uses = {})
% 98.43/98.62
% 98.43/98.62 number of learnt formulas = 68
% 98.43/98.62
% 98.43/98.62
% 98.43/98.62 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.43/98.62
% 98.43/98.62 randbase = 1
%------------------------------------------------------------------------------