%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : GRA136-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n013.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:31 PM UTC 2026
% Result : Unsatisfiable 40.14s 40.40s
% Output : Refutation 40.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRA136-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.16/0.33 % Computer : n013.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.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 23:03:10 EDT 2026
% 0.16/0.34 % CPUTime :
% 40.14/40.40 GeoParameters:
% 40.14/40.40
% 40.14/40.40 tptp_input = 1
% 40.14/40.40 tptp_output = 0
% 40.14/40.40 nonempty = 1
% 40.14/40.40 inputfile = /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.14/40.40 includepath = /export/starexec/sandbox2/solver/bin/../../benchmark/
% 40.14/40.40
% 40.14/40.40
% 40.14/40.40 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.14/40.40 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.14/40.40
% 40.14/40.40 RuleSystem INPUT:
% 40.14/40.40
% 40.14/40.40 Initial Rules:
% 40.14/40.40 #0: input, references = 15, size of lhs = 2:
% 40.14/40.40 P_z-{F}(V0), P_s-{F}(V1,V0) | FALSE
% 40.14/40.40 (used 0 times, uses = {})
% 40.14/40.40
% 40.14/40.40 #1: input, references = 8, size of lhs = 4:
% 40.14/40.40 P_z-{F}(V0), P_s-{F}(V1,V4), P_s-{F}(V2,V4), V1 == V2 | FALSE
% 40.14/40.40 (used 0 times, uses = {})
% 40.14/40.40
% 40.14/40.40 #2: input, references = 3, size of lhs = 2:
% 40.14/40.40 P_z-{F}(V0), r-{F}(V1,V1) | FALSE
% 40.14/40.40 (used 0 times, uses = {})
% 40.14/40.40
% 40.14/40.40 #3: input, references = 3, size of lhs = 2:
% 40.14/40.40 P_z-{F}(V0), b-{F}(V1,V1) | FALSE
% 40.14/40.40 (used 0 times, uses = {})
% 40.14/40.40
% 40.14/40.40 #4: input, references = 34, size of lhs = 4:
% 40.14/40.40 P_z-{F}(V0), #-{F} V1, #-{F} V2, V1 == V2 | r-{T}(V1,V2), b-{T}(V1,V2)
% 40.14/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #5: input, references = 24, size of lhs = 5:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V4,V1), r-{F}(V4,V3) | FALSE
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #6: input, references = 11, size of lhs = 8:
% 40.24/40.40 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
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #7: input, references = 18, size of lhs = 1:
% 40.24/40.40 #-{F} V0 | EXISTS V1: P_s-{T}(V0,V1)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #8: input, references = 4, size of lhs = 0:
% 40.24/40.40 FALSE | EXISTS V0: P_z-{T}(V0)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 number of initial rules = 9
% 40.24/40.40
% 40.24/40.40 Simplifiers:
% 40.24/40.40 #9: unsound, references = 3, size of lhs = 3:
% 40.24/40.40 P_s-{F}(V0,V1), P_s-{F}(V0,V3), V1 == V3 | FALSE
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #10: unsound, references = 3, size of lhs = 3:
% 40.24/40.40 P_z-{F}(V0), P_z-{F}(V1), V0 == V1 | FALSE
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 number of simplifiers = 2
% 40.24/40.40
% 40.24/40.40 Learnt:
% 40.24/40.40 #13: mergings( V0 == V3; #11 ), references = 19, size of lhs = 6:
% 40.24/40.40 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)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #16: mergings( V0 == V3; #14 ), references = 4, size of lhs = 8:
% 40.24/40.40 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)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #24: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #19 ), references = 6, size of lhs = 12:
% 40.24/40.40 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-{F}(V4,V7) | r-{T}(V1,V5)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #29: mergings( V0 == V3, V3 == V4; #26 ), references = 3, size of lhs = 8:
% 40.24/40.40 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)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #36: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #31 ), references = 6, size of lhs = 10:
% 40.24/40.40 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)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #41: mergings( V0 == V3, V3 == V4; #38 ), references = 5, size of lhs = 8:
% 40.24/40.40 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)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #44: mergings( V0 == V3; #42 ), references = 17, size of lhs = 5:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V4,V3), V4 == V1 | b-{T}(V4,V1)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #58: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9; #50 ), references = 3, size of lhs = 32:
% 40.24/40.40 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, r-{F}(V4,V7), b-{F}(V1,V8), b-{F}(V8,V9), b-{F}(V9,V8), r-{F}(V10,V8), b-{F}(V10,V11), V1 == V11, V11 == V8, V11 == V10, V11 == V5, b-{F}(V6,V11), r-{F}(V10,V12), b-{F}(V13,V11), b-{F}(V13,V5), b-{F}(V14,V5), b-{F}(V14,V11), b-{F}(V15,V5), V5 == V15, r-{F}(V16,V15), V5 == V16, r-{F}(V16,V17) | r-{T}(V1,V6)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #75: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10; #66 ), references = 1, size of lhs = 24:
% 40.24/40.40 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, r-{F}(V4,V9), r-{F}(V5,V10), b-{F}(V11,V8), b-{F}(V11,V12), V12 == V8, V12 == V6, b-{F}(V13,V12), b-{F}(V13,V6) | r-{T}(V1,V6)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #82: mergings( V0 == V3, V3 == V4, V4 == V5; #78 ), references = 2, size of lhs = 40:
% 40.24/40.40 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, r-{F}(V6,V8), b-{F}(V2,V9), b-{F}(V9,V2), r-{F}(V10,V2), b-{F}(V10,V11), V11 == V2, V11 == V10, V11 == V7, r-{F}(V10,V12), b-{F}(V13,V11), b-{F}(V13,V7), b-{F}(V14,V7), b-{F}(V14,V11), r-{F}(V4,V15), r-{F}(V4,V16), b-{F}(V16,V7), b-{F}(V16,V11), b-{F}(V17,V7), V7 == V17, r-{F}(V18,V17), V7 == V18, r-{F}(V18,V19), #-{F} V20, V20 == V2, V20 == V4, V20 == V7, V20 == V11, V20 == V16 | r-{T}(V20,V2)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 = 41:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V1,V4), r-{F}(V2,V5), r-{F}(V2,V6), V6 == V2, r-{F}(V2,V7), r-{F}(V2,V8), V6 == V8, b-{F}(V8,V6), r-{F}(V9,V8), r-{F}(V9,V6), r-{F}(V2,V10), r-{F}(V2,V11), r-{F}(V12,V8), r-{F}(V12,V6), r-{F}(V2,V13), r-{F}(V2,V14), r-{F}(V15,V2), r-{F}(V15,V16), r-{F}(V17,V2), r-{F}(V17,V18), #-{F} V19, V19 == V1, V19 == V8, V19 == V6, V19 == V2, #-{F} V20, V20 == V6, V20 == V8, V20 == V2, V19 == V20, #-{F} V21, V6 == V21, V21 == V8, V20 == V21, V19 == V21, V21 == V15, V21 == V2, V21 == V17 | r-{T}(V6,V8)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 = 42:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V1,V4), r-{F}(V2,V5), r-{F}(V2,V6), V6 == V2, r-{F}(V2,V7), r-{F}(V2,V8), V6 == V8, r-{F}(V9,V8), r-{F}(V9,V6), r-{F}(V2,V10), r-{F}(V2,V11), r-{F}(V12,V8), r-{F}(V12,V6), r-{F}(V2,V13), r-{F}(V2,V14), r-{F}(V15,V2), r-{F}(V15,V16), r-{F}(V17,V2), r-{F}(V17,V18), r-{F}(V19,V6), r-{F}(V19,V8), #-{F} V20, V20 == V1, V20 == V8, V20 == V6, V20 == V2, #-{F} V21, V21 == V6, V21 == V8, V21 == V2, V20 == V21, #-{F} V22, V6 == V22, V22 == V8, V21 == V22, V20 == V22, V22 == V15, V22 == V2, V22 == V17 | r-{T}(V8,V6)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 = 38:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V1,V4), r-{F}(V2,V5), r-{F}(V2,V6), V6 == V2, r-{F}(V2,V7), r-{F}(V2,V8), V6 == V8, r-{F}(V9,V8), r-{F}(V9,V6), r-{F}(V2,V10), r-{F}(V2,V11), r-{F}(V12,V8), r-{F}(V12,V6), r-{F}(V2,V13), r-{F}(V2,V14), r-{F}(V15,V2), r-{F}(V15,V16), r-{F}(V17,V2), r-{F}(V17,V18), r-{F}(V19,V6), r-{F}(V19,V8), r-{F}(V20,V8), r-{F}(V20,V6), #-{F} V21, #-{F} V22, V22 == V6, V22 == V8, V22 == V2, #-{F} V23, V6 == V23, V23 == V8, V22 == V23, V23 == V15, V23 == V2, V23 == V17 | P_s-{T}(V21,V1), P_s-{T}(V21,V8), P_s-{T}(V21,V6), P_s-{T}(V21,V2), P_s-{T}(V21,V22), P_s-{T}(V21,V23)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 == V50, V50 == V52, V52 == V54, V54 == V56; #173 ), references = 1, size of lhs = 44:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V1,V4), r-{F}(V2,V5), r-{F}(V2,V6), V6 == V2, r-{F}(V2,V7), r-{F}(V2,V8), V6 == V8, r-{F}(V9,V8), r-{F}(V9,V6), r-{F}(V2,V10), r-{F}(V2,V11), r-{F}(V12,V8), r-{F}(V12,V6), r-{F}(V2,V13), r-{F}(V2,V14), r-{F}(V15,V2), r-{F}(V15,V16), r-{F}(V17,V2), r-{F}(V17,V18), r-{F}(V19,V6), r-{F}(V19,V8), r-{F}(V20,V8), r-{F}(V20,V6), P_s-{F}(V21,V8), P_s-{F}(V22,V2), P_s-{F}(V23,V24), V24 == V6, V24 == V8, V24 == V2, P_s-{F}(V25,V26), V6 == V26, V26 == V8, V24 == V26, V26 == V15, V26 == V2, V26 == V17, #-{F} V27, V21 == V27, V22 == V27, V23 == V27, V25 == V27 | P_s-{T}(V27,V1), P_s-{T}(V27,V6)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 = 44:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V2), r-{F}(V0,V3), r-{F}(V1,V4), r-{F}(V1,V5), V5 == V1, r-{F}(V1,V6), r-{F}(V1,V7), V5 == V7, r-{F}(V8,V7), r-{F}(V8,V5), r-{F}(V1,V9), r-{F}(V1,V10), r-{F}(V11,V7), r-{F}(V11,V5), r-{F}(V1,V12), r-{F}(V1,V13), r-{F}(V14,V1), r-{F}(V14,V15), r-{F}(V16,V1), r-{F}(V16,V17), r-{F}(V18,V5), r-{F}(V18,V7), r-{F}(V19,V7), r-{F}(V19,V5), P_s-{F}(V20,V7), P_s-{F}(V21,V1), P_s-{F}(V22,V23), V23 == V5, V23 == V7, V23 == V1, P_s-{F}(V24,V25), V5 == V25, V25 == V7, V23 == V25, V25 == V14, V25 == V1, V25 == V16, #-{F} V26, V20 == V26, V21 == V26, V22 == V26, V24 == V26 | P_s-{T}(V26,V5)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 == V38; #239 ), references = 4, size of lhs = 36:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V0,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), r-{F}(V1,V7), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V10,V1), r-{F}(V10,V11), r-{F}(V12,V1), r-{F}(V12,V13), P_s-{F}(V14,V1), P_s-{F}(V15,V16), V1 == V16, V0 == V16, P_s-{F}(V17,V18), V18 == V0, V18 == V16, V18 == V1, P_s-{F}(V19,V20), V0 == V20, V20 == V16, V18 == V20, V20 == V10, V20 == V1, V20 == V12, #-{F} V21, V15 == V21, V14 == V21, V17 == V21, V19 == V21 | b-{T}(V1,V16)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #292: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8; #284 ), references = 8, size of lhs = 15:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), b-{F}(V1,V4), V4 == V3, V4 == V1, b-{F}(V5,V4), b-{F}(V5,V6), V6 == V4, b-{F}(V7,V4), b-{F}(V7,V8), V8 == V4, V6 == V8, b-{F}(V9,V8), b-{F}(V9,V6) | b-{T}(V4,V3)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #299: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8; #285 ), references = 1, size of lhs = 15:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), b-{F}(V1,V4), V4 == V3, V4 == V1, b-{F}(V5,V4), b-{F}(V5,V6), V6 == V4, b-{F}(V7,V4), b-{F}(V7,V8), V8 == V4, V6 == V8, b-{F}(V9,V8), b-{F}(V9,V6) | b-{T}(V4,V3)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #303: mergings( V2 == V3; #301 ), references = 1, size of lhs = 39:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V1,V4), r-{F}(V2,V5), r-{F}(V2,V6), V6 == V2, r-{F}(V2,V7), r-{F}(V2,V8), V6 == V8, r-{F}(V9,V8), r-{F}(V9,V6), r-{F}(V2,V10), r-{F}(V2,V11), r-{F}(V12,V8), r-{F}(V12,V6), r-{F}(V2,V13), r-{F}(V2,V14), r-{F}(V15,V2), r-{F}(V15,V16), r-{F}(V17,V2), r-{F}(V17,V18), r-{F}(V19,V6), r-{F}(V19,V8), r-{F}(V8,V20), r-{F}(V20,V6), r-{F}(V20,V21), #-{F} V22, #-{F} V23, V23 == V6, V23 == V8, V23 == V2, #-{F} V24, V6 == V24, V24 == V8, V23 == V24, V24 == V15, V24 == V2, V24 == V17 | P_s-{T}(V22,V1), P_s-{T}(V22,V8), P_s-{T}(V22,V6), P_s-{T}(V22,V2), P_s-{T}(V22,V23), P_s-{T}(V22,V24)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #311: mergings( V0 == V1, V1 == V26, V26 == V28, V28 == V30, V30 == V32, V32 == V34; #304 ), references = 1, size of lhs = 47:
% 40.24/40.40 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), r-{F}(V6,V7), P_s-{F}(V8,V2), P_s-{F}(V9,V3), r-{F}(V10,V3), V3 == V10, r-{F}(V10,V2), r-{F}(V10,V11), r-{F}(V10,V12), r-{F}(V10,V13), r-{F}(V10,V14), r-{F}(V10,V15), r-{F}(V10,V16), r-{F}(V10,V17), r-{F}(V18,V10), r-{F}(V18,V19), r-{F}(V20,V10), r-{F}(V20,V21), r-{F}(V22,V10), r-{F}(V22,V23), P_s-{F}(V24,V22), P_s-{F}(V25,V26), V26 == V3, V26 == V2, V26 == V10, P_s-{F}(V27,V28), V3 == V28, V28 == V2, V26 == V28, V28 == V18, V28 == V10, V28 == V20, #-{F} V29, V24 == V29, V8 == V29, V9 == V29, V25 == V29, V27 == V29 | P_s-{T}(V29,V10)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #322: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V1; #313 ), references = 3, size of lhs = 31:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), r-{F}(V3,V0), r-{F}(V3,V4), r-{F}(V5,V0), r-{F}(V5,V6), r-{F}(V7,V0), r-{F}(V7,V8), P_s-{F}(V9,V7), P_s-{F}(V10,V11), V11 == V0, V11 == V1, P_s-{F}(V12,V13), V13 == V11, V13 == V1, V13 == V0, P_s-{F}(V14,V15), V11 == V15, V15 == V1, V13 == V15, V15 == V3, V15 == V0, V15 == V5, #-{F} V16, V9 == V16, V2 == V16, V10 == V16, V12 == V16, V14 == V16 | b-{T}(V0,V11)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 == V39, V39 == V50, V50 == V64, V64 == 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 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109; #345 ), references = 1, size of lhs = 88:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V0,V2), r-{F}(V0,V3), r-{F}(V0,V4), V0 == V4, r-{F}(V4,V0), r-{F}(V4,V5), r-{F}(V4,V6), r-{F}(V4,V7), r-{F}(V4,V8), r-{F}(V4,V9), r-{F}(V4,V10), r-{F}(V4,V11), r-{F}(V12,V4), r-{F}(V12,V13), r-{F}(V14,V4), r-{F}(V14,V15), P_s-{F}(V16,V4), r-{F}(V4,V17), r-{F}(V4,V18), r-{F}(V4,V19), r-{F}(V4,V20), r-{F}(V4,V21), r-{F}(V4,V22), r-{F}(V4,V23), r-{F}(V24,V4), r-{F}(V24,V25), r-{F}(V26,V4), r-{F}(V26,V27), P_s-{F}(V28,V4), r-{F}(V4,V29), r-{F}(V4,V30), r-{F}(V4,V31), r-{F}(V4,V32), r-{F}(V4,V33), r-{F}(V4,V34), r-{F}(V4,V35), r-{F}(V36,V4), r-{F}(V36,V37), r-{F}(V38,V4), r-{F}(V38,V39), P_s-{F}(V40,V4), r-{F}(V4,V41), r-{F}(V4,V42), r-{F}(V4,V43), r-{F}(V0,V44), r-{F}(V44,V0), P_s-{F}(V45,V44), r-{F}(V46,V0), r-{F}(V46,V47), r-{F}(V48,V0), r-{F}(V48,V49), r-{F}(V0,V50), r-{F}(V51,V0), r-{F}(V51,V52), P_s-{F}(V53,V51), P_s-{F}(V54,V55), V55 == V0, V55 == V44, V55 == V4, P_s-{F}(V56,V55), P_s-{F}(V57,V58), V58 == V0, V58 == V55, V58 == V4, P_s-{F}(V59,V60), V60 == V0, V60 == V4, V60 == V55, P_s-{F}(V61,V62), V62 == V0, V62 == V60, V62 == V4, P_s-{F}(V63,V64), V64 == V0, V64 == V4, P_s-{F}(V65,V66), V0 == V66, V64 == V66, V66 == V36, V66 == V4, V66 == V38, P_s-{F}(V67,V68), V68 == V55, V68 == V44, V68 == V0, #-{F} V69 | P_s-{T}(V69,V0), P_s-{T}(V69,V55), P_s-{T}(V69,V58), P_s-{T}(V69,V12), P_s-{T}(V69,V4), P_s-{T}(V69,V14), P_s-{T}(V69,V60), P_s-{T}(V69,V62), P_s-{T}(V69,V24), P_s-{T}(V69,V26), P_s-{T}(V69,V64), P_s-{T}(V69,V66), P_s-{T}(V69,V44), P_s-{T}(V69,V68), P_s-{T}(V69,V46), P_s-{T}(V69,V48), P_s-{T}(V69,V54), P_s-{T}(V69,V16), P_s-{T}(V69,V57), P_s-{T}(V69,V69), P_s-{T}(V69,V59), P_s-{T}(V69,V28), P_s-{T}(V69,V61), P_s-{T}(V69,V40), P_s-{T}(V69,V63), P_s-{T}(V69,V65), P_s-{T}(V69,V53), P_s-{T}(V69,V45), P_s-{T}(V69,V56), P_s-{T}(V69,V67)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 == V37, V37 == V48, V48 == V62, V62 == 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 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V128, V128 == V130, V130 == V132, V132 == V134, V134 == V136, V136 == V138, V138 == V140, V140 == V142, V142 == V144, V144 == V146, V146 == V148, V148 == V150, V150 == V152, V152 == V154, V154 == V156, V156 == V158, V158 == V160, V160 == V162, V162 == V164, V164 == V166; #406 ), references = 1, size of lhs = 127:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V0,V2), r-{F}(V0,V3), r-{F}(V0,V4), V0 == V4, r-{F}(V4,V0), r-{F}(V4,V5), r-{F}(V4,V6), r-{F}(V4,V7), r-{F}(V4,V8), r-{F}(V4,V9), r-{F}(V4,V10), r-{F}(V4,V11), r-{F}(V12,V4), r-{F}(V12,V13), r-{F}(V14,V4), r-{F}(V14,V15), P_s-{F}(V16,V4), r-{F}(V4,V17), r-{F}(V4,V18), r-{F}(V4,V19), r-{F}(V4,V20), r-{F}(V4,V21), r-{F}(V4,V22), r-{F}(V4,V23), r-{F}(V24,V4), r-{F}(V24,V25), r-{F}(V26,V4), r-{F}(V26,V27), P_s-{F}(V28,V4), r-{F}(V4,V29), r-{F}(V4,V30), r-{F}(V4,V31), r-{F}(V4,V32), r-{F}(V4,V33), r-{F}(V4,V34), r-{F}(V4,V35), r-{F}(V36,V4), r-{F}(V36,V37), r-{F}(V38,V4), r-{F}(V38,V39), P_s-{F}(V40,V4), r-{F}(V4,V41), r-{F}(V4,V42), r-{F}(V4,V43), r-{F}(V0,V44), r-{F}(V44,V0), P_s-{F}(V45,V44), r-{F}(V0,V46), P_s-{F}(V47,V4), P_s-{F}(V48,V44), r-{F}(V49,V0), r-{F}(V49,V50), P_s-{F}(V51,V49), r-{F}(V52,V0), r-{F}(V52,V53), P_s-{F}(V54,V52), r-{F}(V55,V0), r-{F}(V55,V56), P_s-{F}(V57,V55), P_s-{F}(V58,V59), V59 == V0, V59 == V44, V59 == V4, P_s-{F}(V60,V59), P_s-{F}(V61,V60), P_s-{F}(V62,V59), P_s-{F}(V63,V62), P_s-{F}(V64,V65), V65 == V0, V65 == V59, V65 == V4, P_s-{F}(V66,V65), P_s-{F}(V67,V66), P_s-{F}(V68,V69), V69 == V0, V69 == V4, V69 == V59, P_s-{F}(V70,V69), P_s-{F}(V71,V70), P_s-{F}(V72,V73), V73 == V0, V73 == V69, V73 == V4, P_s-{F}(V74,V73), P_s-{F}(V75,V74), P_s-{F}(V76,V77), V77 == V0, V77 == V4, P_s-{F}(V78,V77), P_s-{F}(V79,V78), P_s-{F}(V80,V81), V0 == V81, V77 == V81, V81 == V36, V81 == V4, V81 == V38, P_s-{F}(V82,V81), P_s-{F}(V83,V82), P_s-{F}(V84,V85), V85 == V59, V85 == V44, V85 == V0, P_s-{F}(V86,V85), P_s-{F}(V87,V86), P_s-{F}(V88,V89), V58 == V89, V64 == V89, V47 == V89, V68 == V89, V72 == V89, V76 == V89, V80 == V89, V48 == V89, V84 == V89, V51 == V89, V54 == V89, V61 == V89, V67 == V89, V88 == V89, V71 == V89, V75 == V89, V79 == V89, V83 == V89, V63 == V89, V87 == V89 | P_s-{T}(V89,V0), P_s-{T}(V89,V12), P_s-{T}(V89,V14), P_s-{T}(V89,V24), P_s-{T}(V89,V26), P_s-{T}(V89,V16), P_s-{T}(V89,V28), P_s-{T}(V89,V40), P_s-{T}(V89,V57), P_s-{T}(V89,V45)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 == V37, V37 == V48, V48 == V62, V62 == 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 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V105, V105 == V106, V106 == V107, V107 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V113, V113 == V115, V115 == V116, V116 == V117, V117 == V118, V118 == V119, V119 == V120, V120 == V121, V121 == V122, V122 == V123, V123 == V124, V124 == V125, V125 == V126, V126 == V43, V43 == V45, V45 == V57, V57 == V59, V59 == V47, V47 == V61, V61 == V75, V75 == V135, V33 == V133; #486 ), references = 1, size of lhs = 119:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V0,V2), r-{F}(V0,V3), r-{F}(V0,V4), r-{F}(V4,V0), P_s-{F}(V5,V4), r-{F}(V0,V6), P_s-{F}(V7,V4), r-{F}(V0,V8), r-{F}(V0,V9), r-{F}(V0,V10), r-{F}(V0,V11), V0 == V11, P_s-{F}(V0,V11), r-{F}(V11,V0), r-{F}(V11,V12), r-{F}(V11,V13), r-{F}(V11,V14), r-{F}(V11,V15), r-{F}(V11,V16), r-{F}(V11,V17), r-{F}(V11,V18), r-{F}(V11,V19), r-{F}(V11,V20), r-{F}(V11,V21), r-{F}(V11,V22), r-{F}(V11,V23), r-{F}(V11,V24), r-{F}(V11,V25), r-{F}(V11,V26), r-{F}(V11,V27), r-{F}(V11,V28), r-{F}(V11,V29), r-{F}(V11,V30), r-{F}(V11,V31), r-{F}(V11,V32), r-{F}(V33,V11), r-{F}(V33,V34), r-{F}(V35,V11), r-{F}(V35,V36), r-{F}(V11,V37), r-{F}(V11,V38), r-{F}(V11,V39), P_s-{F}(V40,V11), r-{F}(V0,V41), r-{F}(V11,V42), r-{F}(V43,V0), r-{F}(V43,V44), P_s-{F}(V45,V43), r-{F}(V46,V0), r-{F}(V46,V47), P_s-{F}(V48,V46), P_s-{F}(V49,V50), V50 == V0, V50 == V4, V50 == V11, 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 == V0, V56 == V50, V56 == V11, P_s-{F}(V57,V56), P_s-{F}(V58,V57), P_s-{F}(V59,V60), V60 == V0, V60 == V11, V60 == V50, P_s-{F}(V61,V60), P_s-{F}(V62,V61), P_s-{F}(V63,V64), V64 == V0, V64 == V60, V64 == V11, P_s-{F}(V65,V64), P_s-{F}(V66,V65), P_s-{F}(V67,V68), V68 == V0, V68 == V11, P_s-{F}(V69,V68), P_s-{F}(V70,V69), P_s-{F}(V71,V72), V0 == V72, V68 == V72, V72 == V33, V72 == V11, V72 == V35, P_s-{F}(V73,V72), P_s-{F}(V74,V73), P_s-{F}(V75,V76), V76 == V50, V76 == V4, V76 == V0, P_s-{F}(V77,V76), P_s-{F}(V78,V77), P_s-{F}(V79,V80), V49 == V80, V55 == V80, V40 == V80, V59 == V80, V63 == V80, V67 == V80, V71 == V80, V7 == V80, V75 == V80, V45 == V80, V48 == V80, V52 == V80, V58 == V80, V79 == V80, V62 == V80, V66 == V80, V70 == V80, V74 == V80, V54 == V80, V78 == V80 | P_s-{T}(V80,V5)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 == V37, V37 == 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 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V1, V1 == V104, V104 == V105, V105 == V106, V106 == V107, V2 == V108, V107 == V110; #576 ), references = 1, size of lhs = 100:
% 40.24/40.40 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), r-{F}(V1,V7), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V1,V10), r-{F}(V1,V11), r-{F}(V1,V12), r-{F}(V1,V13), r-{F}(V1,V14), r-{F}(V1,V15), r-{F}(V1,V16), r-{F}(V1,V17), r-{F}(V1,V18), r-{F}(V1,V19), r-{F}(V1,V20), r-{F}(V1,V21), r-{F}(V1,V22), r-{F}(V1,V23), r-{F}(V1,V24), r-{F}(V1,V25), P_s-{F}(V26,V1), P_s-{F}(V27,V1), r-{F}(V1,V28), r-{F}(V29,V0), r-{F}(V29,V30), P_s-{F}(V31,V29), r-{F}(V32,V0), r-{F}(V32,V33), P_s-{F}(V34,V32), P_s-{F}(V35,V36), V36 == V0, V36 == V1, P_s-{F}(V37,V36), P_s-{F}(V38,V37), P_s-{F}(V39,V36), P_s-{F}(V40,V39), P_s-{F}(V41,V42), V42 == V0, V42 == V36, V42 == V1, P_s-{F}(V43,V42), P_s-{F}(V44,V43), P_s-{F}(V45,V46), V46 == V0, V46 == V1, V46 == V36, P_s-{F}(V47,V46), P_s-{F}(V48,V47), P_s-{F}(V49,V50), V50 == V0, V50 == V46, V50 == V1, P_s-{F}(V51,V50), P_s-{F}(V52,V51), P_s-{F}(V53,V54), V54 == V0, V54 == V1, P_s-{F}(V55,V54), P_s-{F}(V56,V55), P_s-{F}(V57,V58), V54 == V58, V58 == V1, V58 == V0, P_s-{F}(V59,V58), P_s-{F}(V60,V59), P_s-{F}(V61,V62), V62 == V36, V62 == V1, V62 == V0, P_s-{F}(V63,V62), P_s-{F}(V64,V63), P_s-{F}(V65,V66), V35 == V66, V41 == V66, V26 == V66, V45 == V66, V49 == V66, V53 == V66, V57 == V66, V27 == V66, V61 == V66, V31 == V66, V34 == V66, V38 == V66, V44 == V66, V65 == V66, V48 == V66, V52 == V66, V56 == V66, V60 == V66, V40 == V66, V64 == V66 | b-{T}(V0,V1)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #676: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10; #667 ), references = 1, size of lhs = 23:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V1,V2), V1 == V2, r-{F}(V2,V3), r-{F}(V2,V4), r-{F}(V2,V5), r-{F}(V2,V6), b-{F}(V1,V7), V7 == V4, r-{F}(V2,V7), b-{F}(V4,V7), r-{F}(V2,V8), #-{F} V9, V9 == V4, V1 == V9, V9 == V7, V9 == V2, #-{F} V10, V10 == V4, V1 == V10, V10 == V7, V10 == V2, V9 == V10 | r-{T}(V7,V4)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #689: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12; #678 ), references = 4, size of lhs = 21:
% 40.24/40.40 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}(V4,V5), r-{F}(V4,V6), r-{F}(V4,V7), r-{F}(V4,V8), #-{F} V9, V3 == V9, V9 == V2, V9 == V4, #-{F} V10, V3 == V10, V10 == V2, V10 == V4, V9 == V10 | r-{T}(V3,V2)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 = 19:
% 40.24/40.40 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}(V4,V5), r-{F}(V4,V6), r-{F}(V4,V7), r-{F}(V4,V8), r-{F}(V9,V3), r-{F}(V9,V2), #-{F} V10, #-{F} V11, V3 == V11, V11 == V2, V11 == V4 | P_s-{T}(V10,V3), P_s-{T}(V10,V2), P_s-{T}(V10,V4), P_s-{T}(V10,V11)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 == V23, V23 == V25, V25 == V27; #704 ), references = 3, size of lhs = 24:
% 40.24/40.40 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}(V4,V5), r-{F}(V4,V6), r-{F}(V4,V7), r-{F}(V4,V8), r-{F}(V9,V3), r-{F}(V9,V2), P_s-{F}(V10,V2), P_s-{F}(V11,V4), P_s-{F}(V12,V13), V3 == V13, V13 == V2, V13 == V4, #-{F} V14, V10 == V14, V11 == V14, V12 == V14 | P_s-{T}(V14,V3)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 = 7, size of lhs = 20:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), P_s-{F}(V6,V1), P_s-{F}(V7,V8), V1 == V8, V8 == V0, P_s-{F}(V9,V10), V0 == V10, V10 == V8, V10 == V1, #-{F} V11, V7 == V11, V6 == V11, V9 == V11 | b-{T}(V1,V8)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #741: mergings( V0 == V3; #739 ), references = 2, size of lhs = 5:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V1,V2), V2 == V1, b-{F}(V2,V3), b-{F}(V3,V1) | r-{T}(V2,V1)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #751: mergings( V2 == V9, V9 == V10, V10 == V11, V11 == V12; #746 ), references = 1, size of lhs = 35:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), P_s-{F}(V6,V1), b-{F}(V1,V7), b-{F}(V8,V7), V7 == V8, r-{F}(V8,V9), r-{F}(V8,V10), V7 == V10, b-{F}(V11,V7), b-{F}(V11,V12), V12 == V7, b-{F}(V1,V12), b-{F}(V10,V13), b-{F}(V13,V7), r-{F}(V10,V14), V14 == V7, P_s-{F}(V15,V16), V0 == V16, V16 == V1, #-{F} V17, #-{F} V18, V17 == V18, V6 == V18, V15 == V18, #-{F} V19, V7 == V19, V19 == V14, V19 == V10 | P_s-{T}(V17,V1), P_s-{T}(V17,V0), P_s-{T}(V17,V7), P_s-{T}(V17,V12), P_s-{T}(V17,V16), P_s-{T}(V17,V14), P_s-{T}(V17,V10), P_s-{T}(V17,V19)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #763: mergings( V0 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V24, V24 == V26, V26 == V28, V28 == V30, V30 == V32, V32 == V34; #752 ), references = 1, size of lhs = 46:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), P_s-{F}(V6,V1), b-{F}(V1,V7), b-{F}(V8,V7), V7 == V8, r-{F}(V8,V9), r-{F}(V8,V10), V7 == V10, b-{F}(V11,V7), b-{F}(V11,V12), V12 == V7, b-{F}(V1,V12), b-{F}(V10,V13), b-{F}(V13,V7), r-{F}(V10,V14), V14 == V7, P_s-{F}(V15,V1), P_s-{F}(V16,V7), P_s-{F}(V17,V12), P_s-{F}(V18,V14), P_s-{F}(V19,V20), V0 == V20, V20 == V1, P_s-{F}(V21,V20), P_s-{F}(V22,V23), V7 == V23, V23 == V14, V23 == V10, #-{F} V24, V15 == V24, V16 == V24, V17 == V24, V21 == V24, V18 == V24, V22 == V24, #-{F} V25, V24 == V25, V6 == V25, V19 == V25 | P_s-{T}(V24,V0), P_s-{T}(V24,V10)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #775: mergings( V7 == V8, V8 == V9, V9 == V10, V10 == V19, V19 == V21, V21 == V23, V23 == V25, V25 == V26, V26 == V28, V28 == V0; #764 ), references = 1, size of lhs = 46:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), P_s-{F}(V6,V1), b-{F}(V1,V7), b-{F}(V8,V7), V7 == V8, r-{F}(V8,V9), r-{F}(V8,V10), V7 == V10, b-{F}(V11,V7), b-{F}(V11,V12), V12 == V7, b-{F}(V1,V12), b-{F}(V10,V13), b-{F}(V13,V7), r-{F}(V10,V14), V14 == V7, P_s-{F}(V15,V1), P_s-{F}(V16,V7), P_s-{F}(V17,V12), P_s-{F}(V18,V14), P_s-{F}(V19,V20), V0 == V20, V20 == V1, P_s-{F}(V21,V20), P_s-{F}(V22,V23), V7 == V23, V23 == V14, V23 == V10, #-{F} V24, V15 == V24, V16 == V24, V17 == V24, V21 == V24, V18 == V24, V22 == V24, #-{F} V25, V24 == V25, V6 == V25, V19 == V25 | P_s-{T}(V24,V10)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 = 4, size of lhs = 46:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), P_s-{F}(V6,V1), b-{F}(V1,V7), V7 == V0, b-{F}(V8,V7), V7 == V8, r-{F}(V8,V0), r-{F}(V8,V9), b-{F}(V10,V7), b-{F}(V10,V11), V11 == V7, b-{F}(V1,V11), b-{F}(V0,V12), b-{F}(V12,V7), P_s-{F}(V13,V1), P_s-{F}(V14,V7), P_s-{F}(V15,V11), P_s-{F}(V16,V17), V0 == V17, V17 == V7, P_s-{F}(V18,V19), V0 == V19, V19 == V1, P_s-{F}(V20,V19), P_s-{F}(V21,V22), V7 == V22, V22 == V17, V22 == V0, #-{F} V23, V13 == V23, V14 == V23, V15 == V23, V20 == V23, V16 == V23, V21 == V23, #-{F} V24, V23 == V24, V6 == V24, V18 == V24 | b-{T}(V0,V17)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 == V106, V106 == V107, V107 == V108, V79 == V109, V108 == V110, V110 == V112, V112 == V113, V113 == 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, V127 == V128, V128 == V139, V139 == V140, V140 == V141, V141 == V142, V142 == V143, V143 == V144, V144 == V145, V145 == V146, V146 == V147, V147 == V148, V148 == V149, V149 == V164, V164 == V165; #797 ), references = 1, size of lhs = 114:
% 40.24/40.40 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), r-{F}(V1,V7), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V1,V10), r-{F}(V1,V11), r-{F}(V1,V12), r-{F}(V1,V13), r-{F}(V1,V14), r-{F}(V1,V15), r-{F}(V1,V16), r-{F}(V1,V17), r-{F}(V1,V18), r-{F}(V1,V19), r-{F}(V1,V20), r-{F}(V1,V21), r-{F}(V1,V22), r-{F}(V1,V23), r-{F}(V1,V24), r-{F}(V1,V25), P_s-{F}(V26,V1), P_s-{F}(V27,V1), r-{F}(V1,V28), r-{F}(V1,V29), r-{F}(V1,V30), r-{F}(V1,V31), r-{F}(V1,V32), P_s-{F}(V33,V1), r-{F}(V1,V34), r-{F}(V1,V35), r-{F}(V1,V36), r-{F}(V1,V37), P_s-{F}(V38,V1), r-{F}(V1,V39), r-{F}(V1,V40), r-{F}(V1,V41), r-{F}(V1,V42), P_s-{F}(V43,V1), r-{F}(V1,V44), P_s-{F}(V45,V1), r-{F}(V1,V46), r-{F}(V1,V47), r-{F}(V1,V48), r-{F}(V1,V49), P_s-{F}(V50,V1), r-{F}(V1,V51), P_s-{F}(V52,V1), r-{F}(V1,V53), r-{F}(V54,V0), r-{F}(V54,V55), P_s-{F}(V56,V54), r-{F}(V57,V0), r-{F}(V57,V58), P_s-{F}(V59,V57), P_s-{F}(V60,V61), V61 == V0, V61 == V1, P_s-{F}(V62,V61), P_s-{F}(V63,V62), P_s-{F}(V64,V61), P_s-{F}(V65,V64), P_s-{F}(V66,V67), P_s-{F}(V68,V67), P_s-{F}(V69,V67), P_s-{F}(V70,V67), P_s-{F}(V71,V72), V72 == V0, V72 == V1, P_s-{F}(V73,V72), P_s-{F}(V74,V73), P_s-{F}(V75,V76), V76 == V0, V76 == V1, P_s-{F}(V77,V76), P_s-{F}(V78,V77), P_s-{F}(V79,V80), V80 == V0, V80 == V1, P_s-{F}(V81,V80), P_s-{F}(V82,V80), P_s-{F}(V83,V84), V0 == V84, V84 == V1, P_s-{F}(V85,V86), V0 == V86, V1 == V86, P_s-{F}(V87,V88), V0 == V88, V88 == V1, P_s-{F}(V89,V88), P_s-{F}(V90,V91), V91 == V86, V91 == V0, P_s-{F}(V92,V93), V0 == V93, V93 == V1, P_s-{F}(V94,V93), P_s-{F}(V95,V96), V80 == V96, V96 == V0, #-{F} V97, V43 == V97, V87 == V97, #-{F} V98, V50 == V98, V92 == V98 | P_s-{T}(V67,V0), P_s-{T}(V67,V61), P_s-{T}(V67,V1), P_s-{T}(V67,V72), P_s-{T}(V67,V76), P_s-{T}(V67,V60), P_s-{T}(V67,V67), P_s-{T}(V67,V26), P_s-{T}(V67,V71), P_s-{T}(V67,V75), P_s-{T}(V67,V27), P_s-{T}(V67,V56), P_s-{T}(V67,V59), P_s-{T}(V67,V63), P_s-{T}(V67,V66), P_s-{T}(V67,V68), P_s-{T}(V67,V74), P_s-{T}(V67,V78), P_s-{T}(V67,V69), P_s-{T}(V67,V65), P_s-{T}(V67,V70), P_s-{T}(V67,V80), P_s-{T}(V67,V84), P_s-{T}(V67,V86), P_s-{T}(V67,V91), P_s-{T}(V67,V96), P_s-{T}(V67,V79), P_s-{T}(V67,V33), P_s-{T}(V67,V38), P_s-{T}(V67,V83), P_s-{T}(V67,V45), P_s-{T}(V67,V81), P_s-{T}(V67,V89), P_s-{T}(V67,V85), P_s-{T}(V67,V90), P_s-{T}(V67,V97), P_s-{T}(V67,V52), P_s-{T}(V67,V82), P_s-{T}(V67,V94), P_s-{T}(V67,V95), P_s-{T}(V67,V98)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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 == V104, V104 == V105, V105 == V106, V77 == V107, V106 == V108, V108 == V110, V110 == V111, V111 == V112, V112 == V113, V113 == 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 == V137, V137 == V138, V138 == V139, V139 == V140, V140 == V141, V141 == V142, V142 == V143, V143 == V144, V144 == V145, V145 == V146, V146 == V147, V147 == V162, V162 == V163, V163 == V210, V210 == V212, V212 == V214, V214 == V216, V216 == V218, V218 == V220, V220 == V102, V102 == V222, V222 == V224, V224 == V103, V103 == V167, V107 == V165, V167 == V170, V165 == V168, V170 == V174, V168 == V173, V174 == V226, V226 == V228, V228 == V185, V173 == V184, V172 == V183, V185 == V189, V184 == V188, V183 == V187, V189 == V230, V230 == V176, V188 == V175, V176 == V232, V232 == V234, V234 == V236, V236 == V238, V238 == V240, V240 == V242, V242 == V244, V244 == V131, V131 == V136, V136 == V246, V246 == V154, V154 == V248, V248 == V250, V250 == V252, V252 == V201, V175 == V202, V201 == V254, V254 == V161, V161 == V256, V256 == V258, V258 == V206, V202 == V207; #910 ), references = 1, size of lhs = 136:
% 40.24/40.40 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), r-{F}(V1,V7), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V1,V10), r-{F}(V1,V11), r-{F}(V1,V12), r-{F}(V1,V13), r-{F}(V1,V14), r-{F}(V1,V15), r-{F}(V1,V16), r-{F}(V1,V17), r-{F}(V1,V18), r-{F}(V1,V19), r-{F}(V1,V20), r-{F}(V1,V21), r-{F}(V1,V22), r-{F}(V1,V23), r-{F}(V1,V24), r-{F}(V1,V25), r-{F}(V1,V26), r-{F}(V1,V27), r-{F}(V1,V28), r-{F}(V1,V29), r-{F}(V1,V30), r-{F}(V1,V31), r-{F}(V1,V32), r-{F}(V1,V33), r-{F}(V1,V34), r-{F}(V1,V35), r-{F}(V1,V36), r-{F}(V1,V37), r-{F}(V1,V38), P_s-{F}(V39,V1), r-{F}(V1,V40), r-{F}(V1,V41), r-{F}(V1,V42), r-{F}(V1,V43), r-{F}(V1,V44), P_s-{F}(V45,V1), r-{F}(V1,V46), r-{F}(V1,V47), P_s-{F}(V48,V1), r-{F}(V1,V49), r-{F}(V1,V50), P_s-{F}(V1,V51), V51 == V0, V51 == V1, P_s-{F}(V52,V51), P_s-{F}(V53,V51), P_s-{F}(V54,V51), P_s-{F}(V55,V1), P_s-{F}(V56,V1), P_s-{F}(V57,V51), P_s-{F}(V58,V57), P_s-{F}(V59,V51), P_s-{F}(V60,V59), P_s-{F}(V61,V51), P_s-{F}(V62,V61), P_s-{F}(V63,V64), V0 == V64, V64 == V1, P_s-{F}(V65,V64), P_s-{F}(V66,V65), P_s-{F}(V67,V68), V0 == V68, V68 == V1, P_s-{F}(V69,V68), P_s-{F}(V70,V69), P_s-{F}(V71,V72), V52 == V72, V48 == V72, V53 == V72, V54 == V72, V58 == V72, V71 == V72, V60 == V72, V62 == V72, V55 == V72, V56 == V72, V66 == V72, V70 == V72, P_s-{F}(V73,V72), P_s-{F}(V74,V73), V74 == V72, P_s-{F}(V75,V72), P_s-{F}(V76,V75), V76 == V72, P_s-{F}(V77,V72), P_s-{F}(V78,V77), V78 == V72, P_s-{F}(V79,V72), P_s-{F}(V80,V79), V80 == V72, P_s-{F}(V81,V82), V82 == V0, V82 == V1, V81 == V72, P_s-{F}(V83,V82), P_s-{F}(V84,V83), V84 == V72, P_s-{F}(V85,V82), P_s-{F}(V86,V85), V86 == V72, P_s-{F}(V87,V82), P_s-{F}(V88,V87), V88 == V72, P_s-{F}(V89,V90), V0 == V90, V90 == V1, V89 == V72, P_s-{F}(V91,V90), P_s-{F}(V92,V91), V92 == V72, P_s-{F}(V93,V94), V0 == V94, V1 == V94, V93 == V72, P_s-{F}(V95,V94), P_s-{F}(V96,V95), V96 == V72, P_s-{F}(V97,V98), V39 == V98, V63 == V98, V97 == V72, #-{F} V99, V45 == V99, V67 == V99 | P_s-{T}(V72,V99)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #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:
% 40.24/40.40 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)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1240: mergings( V0 == V1, V1 == V8; #1236 ), references = 1, size of lhs = 22:
% 40.24/40.40 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, r-{F}(V4,V5), r-{F}(V4,V6), r-{F}(V4,V7), r-{F}(V4,V8), P_s-{F}(V9,V4), P_s-{F}(V10,V11), V0 == V11, V11 == V1, V11 == V4, #-{F} V12, V2 == V12, V9 == V12, V10 == V12 | r-{T}(V0,V4)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1244: mergings( V0 == V3, V3 == V4, V4 == V1; #1237 ), references = 1, size of lhs = 22:
% 40.24/40.40 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, r-{F}(V4,V5), r-{F}(V4,V6), r-{F}(V4,V7), r-{F}(V4,V8), P_s-{F}(V9,V4), P_s-{F}(V10,V11), V0 == V11, V11 == V1, V11 == V4, #-{F} V12, V3 == V12, V9 == V12, V10 == V12 | r-{T}(V0,V4)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1259: mergings( V2 == V17, V17 == V18, V18 == V19, V19 == V32, V32 == V33, V33 == V34; #1252 ), references = 1, size of lhs = 78:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V0,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), r-{F}(V1,V7), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V10,V1), r-{F}(V10,V11), r-{F}(V12,V1), r-{F}(V12,V13), P_s-{F}(V14,V1), r-{F}(V0,V15), r-{F}(V15,V0), P_s-{F}(V16,V15), r-{F}(V17,V0), r-{F}(V17,V18), r-{F}(V19,V0), r-{F}(V19,V20), r-{F}(V0,V21), r-{F}(V21,V0), P_s-{F}(V22,V21), r-{F}(V23,V0), r-{F}(V23,V24), r-{F}(V25,V0), r-{F}(V25,V26), r-{F}(V1,V27), r-{F}(V1,V28), b-{F}(V28,V29), b-{F}(V29,V28), r-{F}(V1,V30), b-{F}(V0,V31), b-{F}(V0,V32), b-{F}(V32,V28), b-{F}(V32,V1), b-{F}(V32,V33), b-{F}(V33,V32), r-{F}(V34,V0), r-{F}(V34,V35), P_s-{F}(V36,V34), r-{F}(V37,V0), r-{F}(V37,V38), P_s-{F}(V39,V37), P_s-{F}(V40,V41), V41 == V15, V41 == V0, P_s-{F}(V42,V43), V43 == V15, V41 == V43, V43 == V17, V43 == V0, V43 == V19, P_s-{F}(V44,V45), V45 == V21, V45 == V0, V45 == V1, V45 == V28, V31 == V45, V32 == V45, P_s-{F}(V46,V45), P_s-{F}(V47,V48), V0 == V48, V48 == V45, V48 == V10, V48 == V1, V48 == V12, P_s-{F}(V49,V50), V45 == V50, V50 == V21, V50 == V23, V50 == V0, V50 == V25, #-{F} V51 | P_s-{T}(V51,V0), P_s-{T}(V51,V15), P_s-{T}(V51,V31), P_s-{T}(V51,V32), P_s-{T}(V51,V41), P_s-{T}(V51,V43), P_s-{T}(V51,V45), P_s-{T}(V51,V1), P_s-{T}(V51,V48), P_s-{T}(V51,V21), P_s-{T}(V51,V50), P_s-{T}(V51,V36), P_s-{T}(V51,V16), P_s-{T}(V51,V51), P_s-{T}(V51,V40), P_s-{T}(V51,V42), P_s-{T}(V51,V44), P_s-{T}(V51,V14), P_s-{T}(V51,V47), P_s-{T}(V51,V39), P_s-{T}(V51,V22), P_s-{T}(V51,V46), P_s-{T}(V51,V49)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1286: mergings( V0 == V15, V15 == V16, V16 == V17, V17 == V30, V30 == V31, V31 == V32, V32 == V58, V58 == V60, V60 == V62, V62 == V64, V64 == V66, V66 == V68, V68 == V70, V70 == V72, V72 == V74, V74 == V76, V76 == V78, V78 == V80, V80 == V82, V82 == V84, V84 == V86, V86 == V88, V88 == V90, V90 == V92, V92 == V94; #1260 ), references = 1, size of lhs = 115:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V0,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), r-{F}(V1,V7), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V10,V1), r-{F}(V10,V11), r-{F}(V12,V1), r-{F}(V12,V13), r-{F}(V0,V14), r-{F}(V14,V0), r-{F}(V15,V0), r-{F}(V15,V16), r-{F}(V17,V0), r-{F}(V17,V18), r-{F}(V0,V19), r-{F}(V19,V0), r-{F}(V20,V0), r-{F}(V20,V21), r-{F}(V22,V0), r-{F}(V22,V23), r-{F}(V1,V24), r-{F}(V1,V25), b-{F}(V25,V26), b-{F}(V26,V25), r-{F}(V1,V27), b-{F}(V0,V28), b-{F}(V0,V29), b-{F}(V29,V25), b-{F}(V29,V1), b-{F}(V29,V30), b-{F}(V30,V29), P_s-{F}(V31,V14), P_s-{F}(V32,V28), P_s-{F}(V33,V29), P_s-{F}(V34,V1), P_s-{F}(V35,V19), P_s-{F}(V36,V1), P_s-{F}(V37,V36), P_s-{F}(V38,V14), P_s-{F}(V39,V38), P_s-{F}(V40,V19), P_s-{F}(V41,V40), r-{F}(V42,V0), r-{F}(V42,V43), P_s-{F}(V44,V42), P_s-{F}(V45,V44), r-{F}(V46,V0), r-{F}(V46,V47), P_s-{F}(V48,V46), P_s-{F}(V49,V48), P_s-{F}(V50,V51), V51 == V14, V51 == V15, V51 == V0, V51 == V17, P_s-{F}(V52,V51), P_s-{F}(V53,V54), V0 == V54, V54 == V10, V54 == V1, V54 == V12, P_s-{F}(V55,V54), P_s-{F}(V56,V57), V57 == V19, V57 == V20, V57 == V0, V57 == V22, P_s-{F}(V58,V57), P_s-{F}(V59,V60), V60 == V14, V60 == V0, V60 == V51, P_s-{F}(V61,V60), P_s-{F}(V62,V61), P_s-{F}(V63,V64), V64 == V19, V64 == V0, V64 == V1, V64 == V25, V28 == V64, V29 == V64, V54 == V64, V64 == V57, P_s-{F}(V65,V64), P_s-{F}(V66,V65), P_s-{F}(V67,V64), P_s-{F}(V68,V67), P_s-{F}(V69,V70), V31 == V70, V32 == V70, V33 == V70, V59 == V70, V52 == V70, V63 == V70, V34 == V70, V55 == V70, V35 == V70, V58 == V70, V45 == V70, V39 == V70, V69 == V70, V62 == V70, V66 == V70, V37 == V70, V49 == V70, V41 == V70, V68 == V70 | P_s-{T}(V70,V0), P_s-{T}(V70,V50), P_s-{T}(V70,V53), P_s-{T}(V70,V56)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1316: mergings( V14 == V15, V15 == V27, V27 == V28, V28 == V29, V29 == V37, V37 == V39, V39 == V41, V41 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V48, V48 == V49, V49 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V16, V16 == V0, V0 == V75, V75 == V78, V76 == V79; #1287 ), references = 1, size of lhs = 113:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V2,V0), r-{F}(V2,V3), r-{F}(V4,V0), r-{F}(V4,V5), r-{F}(V0,V6), r-{F}(V6,V0), r-{F}(V7,V0), r-{F}(V7,V8), r-{F}(V9,V0), r-{F}(V9,V10), b-{F}(V0,V11), b-{F}(V0,V12), b-{F}(V12,V13), b-{F}(V13,V14), b-{F}(V14,V13), b-{F}(V12,V15), V0 == V15, r-{F}(V15,V13), r-{F}(V15,V0), r-{F}(V0,V15), r-{F}(V15,V16), r-{F}(V0,V17), r-{F}(V15,V18), r-{F}(V15,V19), r-{F}(V15,V20), r-{F}(V15,V21), r-{F}(V15,V22), r-{F}(V15,V23), r-{F}(V24,V15), r-{F}(V24,V25), r-{F}(V26,V15), r-{F}(V26,V27), r-{F}(V15,V28), r-{F}(V15,V29), b-{F}(V12,V30), b-{F}(V30,V12), P_s-{F}(V31,V1), P_s-{F}(V32,V11), P_s-{F}(V33,V12), P_s-{F}(V34,V15), P_s-{F}(V35,V6), P_s-{F}(V0,V36), V36 == V1, V36 == V2, V36 == V4, V0 == V36, V36 == V24, V36 == V15, V36 == V26, P_s-{F}(V37,V36), P_s-{F}(V38,V36), P_s-{F}(V39,V15), P_s-{F}(V40,V39), P_s-{F}(V41,V1), P_s-{F}(V42,V41), P_s-{F}(V43,V6), P_s-{F}(V44,V43), r-{F}(V45,V0), r-{F}(V45,V46), P_s-{F}(V47,V45), P_s-{F}(V48,V47), r-{F}(V49,V0), r-{F}(V49,V50), P_s-{F}(V51,V49), P_s-{F}(V52,V51), P_s-{F}(V53,V54), V54 == V6, V54 == V7, V54 == V0, V54 == V9, P_s-{F}(V55,V54), P_s-{F}(V56,V57), V57 == V1, V57 == V0, V57 == V36, P_s-{F}(V58,V57), P_s-{F}(V59,V58), P_s-{F}(V60,V61), V61 == V6, V61 == V0, V61 == V15, V61 == V13, V11 == V61, V12 == V61, V36 == V61, V61 == V54, P_s-{F}(V62,V61), P_s-{F}(V63,V62), P_s-{F}(V64,V61), P_s-{F}(V65,V64), P_s-{F}(V66,V67), V31 == V67, V32 == V67, V33 == V67, V56 == V67, V37 == V67, V60 == V67, V34 == V67, V38 == V67, V35 == V67, V55 == V67, V48 == V67, V42 == V67, V66 == V67, V59 == V67, V63 == V67, V40 == V67, V52 == V67, V44 == V67, V65 == V67 | P_s-{T}(V67,V53)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1354: 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 == V44, V44 == V47, V45 == V48, V47 == V50, V48 == V51; #1320 ), references = 4, size of lhs = 84:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), V2 == V0, P_s-{F}(V3,V2), b-{F}(V2,V4), b-{F}(V4,V2), b-{F}(V0,V5), b-{F}(V0,V6), b-{F}(V6,V0), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V6,V8), b-{F}(V8,V6), P_s-{F}(V9,V5), P_s-{F}(V10,V6), P_s-{F}(V0,V11), V11 == V0, P_s-{F}(V12,V11), P_s-{F}(V13,V11), P_s-{F}(V14,V11), P_s-{F}(V15,V16), V6 == V16, V0 == V16, V16 == V2, V11 == V16, P_s-{F}(V17,V16), P_s-{F}(V18,V16), P_s-{F}(V19,V16), P_s-{F}(V20,V16), P_s-{F}(V21,V20), P_s-{F}(V22,V16), P_s-{F}(V23,V22), P_s-{F}(V24,V16), P_s-{F}(V25,V24), P_s-{F}(V26,V16), P_s-{F}(V27,V26), P_s-{F}(V28,V16), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V0 == V31, V31 == V2, V31 == V16, P_s-{F}(V32,V33), V33 == V16, V33 == V0, V33 == V11, P_s-{F}(V34,V33), P_s-{F}(V35,V34), P_s-{F}(V36,V37), V37 == V16, V37 == V0, V5 == V37, V6 == V37, V37 == V11, P_s-{F}(V38,V37), P_s-{F}(V39,V38), P_s-{F}(V40,V37), P_s-{F}(V41,V40), P_s-{F}(V42,V43), V17 == V43, V9 == V43, V10 == V43, V32 == V43, V12 == V43, V36 == V43, V18 == V43, V13 == V43, V19 == V43, V14 == V43, V27 == V43, V23 == V43, V42 == V43, V35 == V43, V39 == V43, V21 == V43, V29 == V43, V25 == V43, V41 == V43, #-{F} V44, V3 == V44, V15 == V44, V30 == V44 | r-{T}(V6,V16)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1358: mergings( V2 == V17; #1356 ), references = 1, size of lhs = 50:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), V2 == V0, P_s-{F}(V3,V2), b-{F}(V2,V4), b-{F}(V4,V2), b-{F}(V0,V5), b-{F}(V0,V6), b-{F}(V6,V0), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V6,V8), b-{F}(V8,V6), P_s-{F}(V9,V5), P_s-{F}(V10,V6), P_s-{F}(V0,V11), V11 == V0, P_s-{F}(V12,V11), P_s-{F}(V13,V11), P_s-{F}(V14,V11), r-{F}(V15,V6), r-{F}(V15,V16), V6 == V16, V0 == V16, V16 == V2, V11 == V16, 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,V21), P_s-{F}(V23,V16), P_s-{F}(V24,V23), P_s-{F}(V25,V16), P_s-{F}(V26,V25), P_s-{F}(V27,V16), P_s-{F}(V28,V27), P_s-{F}(V29,V16), P_s-{F}(V30,V29), P_s-{F}(V31,V32), V32 == V16, V32 == V0, V32 == V11, P_s-{F}(V33,V32), P_s-{F}(V34,V33), P_s-{F}(V35,V36), P_s-{F}(V37,V36) | P_s-{T}(V36,V0), P_s-{T}(V36,V2), P_s-{T}(V36,V16), P_s-{T}(V36,V5), P_s-{T}(V36,V6), P_s-{T}(V36,V11), P_s-{T}(V36,V18), P_s-{T}(V36,V9), P_s-{T}(V36,V10), P_s-{T}(V36,V31), P_s-{T}(V36,V12), P_s-{T}(V36,V36), P_s-{T}(V36,V19), P_s-{T}(V36,V13), P_s-{T}(V36,V20), P_s-{T}(V36,V14), P_s-{T}(V36,V28), P_s-{T}(V36,V24), P_s-{T}(V36,V34), P_s-{T}(V36,V35), P_s-{T}(V36,V22), P_s-{T}(V36,V30), P_s-{T}(V36,V26), P_s-{T}(V36,V37), P_s-{T}(V36,V3), P_s-{T}(V36,V17)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1386: mergings( V15 == V0, V0 == V39, V39 == V41, V41 == V43, V43 == V45, V45 == V47, V47 == V49, V49 == V51, V51 == V53, V53 == V55, V55 == V12, V12 == V57, V57 == V59, V59 == V13, V13 == V61, V61 == V14, V14 == V63, V63 == V65, V65 == V35, V11 == V34, V35 == V67, V67 == V69, V69 == V71, V71 == V73, V73 == V75, V75 == V77; #1359 ), references = 1, size of lhs = 86:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), V2 == V0, b-{F}(V2,V3), b-{F}(V3,V2), b-{F}(V0,V4), b-{F}(V0,V5), b-{F}(V5,V0), b-{F}(V0,V6), b-{F}(V6,V0), b-{F}(V5,V7), b-{F}(V7,V5), r-{F}(V8,V5), r-{F}(V8,V9), V5 == V9, V0 == V9, V9 == V2, P_s-{F}(V10,V9), P_s-{F}(V11,V2), P_s-{F}(V12,V9), P_s-{F}(V13,V4), P_s-{F}(V14,V5), P_s-{F}(V0,V15), V15 == V0, V15 == V9, P_s-{F}(V16,V15), P_s-{F}(V15,V17), V17 == V9, V17 == V0, V17 == V15, P_s-{F}(V18,V2), P_s-{F}(V19,V18), P_s-{F}(V20,V4), P_s-{F}(V21,V20), P_s-{F}(V22,V5), P_s-{F}(V23,V22), P_s-{F}(V24,V9), P_s-{F}(V25,V24), P_s-{F}(V26,V9), P_s-{F}(V27,V26), P_s-{F}(V28,V9), P_s-{F}(V29,V28), P_s-{F}(V30,V9), P_s-{F}(V31,V30), P_s-{F}(V32,V31), P_s-{F}(V33,V9), P_s-{F}(V34,V33), P_s-{F}(V35,V34), P_s-{F}(V36,V9), P_s-{F}(V37,V36), P_s-{F}(V38,V37), P_s-{F}(V39,V9), P_s-{F}(V40,V39), P_s-{F}(V41,V40), P_s-{F}(V42,V9), P_s-{F}(V43,V42), P_s-{F}(V44,V43), P_s-{F}(V45,V17), P_s-{F}(V46,V45), P_s-{F}(V47,V48), V11 == V48, V12 == V48, V13 == V48, V14 == V48, V16 == V48, V25 == V48, V21 == V48, V23 == V48, V46 == V48, V47 == V48, V27 == V48, V29 == V48, V41 == V48, V35 == V48, V32 == V48, V44 == V48, V38 == V48, V19 == V48, P_s-{F}(V49,V48), P_s-{F}(V50,V49), V50 == V48, P_s-{F}(V51,V48), P_s-{F}(V52,V51), V52 == V48 | P_s-{T}(V48,V10)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1417: mergings( V0 == V3, V3 == V2, V2 == V8, V8 == V10, V10 == V12, V12 == V14, V14 == V16, V16 == 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, V5 == V31, V30 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39; #1388 ), references = 1, size of lhs = 77:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), V2 == V0, r-{F}(V3,V2), r-{F}(V3,V4), V0 == V4, V4 == V2, P_s-{F}(V5,V2), P_s-{F}(V6,V4), P_s-{F}(V7,V1), P_s-{F}(V8,V2), P_s-{F}(V0,V9), V9 == V0, V9 == V4, P_s-{F}(V10,V9), P_s-{F}(V9,V11), V11 == V4, V11 == V0, V11 == V9, P_s-{F}(V12,V4), P_s-{F}(V13,V12), P_s-{F}(V14,V2), P_s-{F}(V15,V14), P_s-{F}(V16,V1), P_s-{F}(V17,V16), P_s-{F}(V18,V2), P_s-{F}(V19,V18), P_s-{F}(V20,V4), P_s-{F}(V21,V20), P_s-{F}(V22,V4), P_s-{F}(V23,V22), P_s-{F}(V24,V4), P_s-{F}(V25,V24), P_s-{F}(V26,V4), P_s-{F}(V27,V26), P_s-{F}(V28,V27), P_s-{F}(V29,V4), P_s-{F}(V30,V29), P_s-{F}(V31,V30), P_s-{F}(V32,V4), P_s-{F}(V33,V32), P_s-{F}(V34,V33), P_s-{F}(V35,V4), P_s-{F}(V36,V35), P_s-{F}(V37,V36), P_s-{F}(V38,V4), P_s-{F}(V39,V38), P_s-{F}(V40,V39), P_s-{F}(V41,V11), P_s-{F}(V42,V41), P_s-{F}(V43,V44), V5 == V44, V6 == V44, V7 == V44, V8 == V44, V10 == V44, V21 == V44, V17 == V44, V19 == V44, V42 == V44, V43 == V44, V23 == V44, V25 == V44, V37 == V44, V31 == V44, V28 == V44, V40 == V44, V34 == V44, V15 == V44, V13 == V44, P_s-{F}(V45,V44), P_s-{F}(V46,V45), V46 == V44, P_s-{F}(V47,V44), P_s-{F}(V48,V47), V48 == V44 | r-{T}(V2,V0)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1455: 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 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V15 == V25, V24 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V1, V1 == V41; #1423 ), references = 1, size of lhs = 90:
% 40.24/40.40 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V1,V3), V3 == V1, V3 == V0, b-{F}(V0,V4), V4 == V0, P_s-{F}(V5,V4), b-{F}(V4,V6), b-{F}(V6,V4), P_s-{F}(V7,V3), P_s-{F}(V8,V7), P_s-{F}(V9,V10), V0 == V10, V10 == V4, r-{F}(V11,V10), r-{F}(V11,V12), V0 == V12, V12 == V10, V1 == V12, V3 == V12, P_s-{F}(V13,V10), P_s-{F}(V14,V12), P_s-{F}(V15,V10), P_s-{F}(V16,V10), P_s-{F}(V17,V12), P_s-{F}(V18,V17), P_s-{F}(V19,V10), P_s-{F}(V20,V19), P_s-{F}(V21,V10), P_s-{F}(V22,V21), P_s-{F}(V23,V10), P_s-{F}(V24,V23), P_s-{F}(V25,V12), P_s-{F}(V26,V25), P_s-{F}(V27,V12), P_s-{F}(V28,V27), P_s-{F}(V29,V12), P_s-{F}(V30,V29), P_s-{F}(V31,V12), P_s-{F}(V32,V31), P_s-{F}(V33,V32), P_s-{F}(V34,V12), P_s-{F}(V35,V34), P_s-{F}(V36,V35), P_s-{F}(V37,V12), P_s-{F}(V38,V37), P_s-{F}(V39,V38), P_s-{F}(V40,V12), P_s-{F}(V41,V40), P_s-{F}(V42,V41), P_s-{F}(V43,V12), P_s-{F}(V44,V43), P_s-{F}(V45,V44), P_s-{F}(V46,V47), V13 == V47, V14 == V47, V9 == V47, V15 == V47, V2 == V47, V26 == V47, V22 == V47, V24 == V47, V8 == V47, V46 == V47, V28 == V47, V30 == V47, V42 == V47, V36 == V47, V33 == V47, V45 == V47, V39 == V47, V20 == V47, V18 == V47, P_s-{F}(V48,V47), P_s-{F}(V49,V48), V49 == V47, P_s-{F}(V50,V47), P_s-{F}(V51,V50), V51 == V47, P_s-{F}(V52,V53), V0 == V53, V53 == V4, V53 == V10, #-{F} V54, V5 == V54, V16 == V54, V52 == V54 | r-{T}(V0,V10)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1487: 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 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V16 == V26, V25 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V1; #1424 ), references = 1, size of lhs = 90:
% 40.24/40.40 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V1,V3), V3 == V1, V3 == V0, b-{F}(V0,V4), V4 == V0, b-{F}(V4,V5), b-{F}(V5,V4), P_s-{F}(V6,V4), P_s-{F}(V7,V3), P_s-{F}(V8,V7), P_s-{F}(V9,V10), V0 == V10, V10 == V4, r-{F}(V11,V10), r-{F}(V11,V12), V0 == V12, V12 == V10, V1 == V12, V3 == V12, P_s-{F}(V13,V10), P_s-{F}(V14,V12), P_s-{F}(V15,V10), P_s-{F}(V16,V10), P_s-{F}(V17,V12), P_s-{F}(V18,V17), P_s-{F}(V19,V10), P_s-{F}(V20,V19), P_s-{F}(V21,V10), P_s-{F}(V22,V21), P_s-{F}(V23,V10), P_s-{F}(V24,V23), P_s-{F}(V25,V12), P_s-{F}(V26,V25), P_s-{F}(V27,V12), P_s-{F}(V28,V27), P_s-{F}(V29,V12), P_s-{F}(V30,V29), P_s-{F}(V31,V12), P_s-{F}(V32,V31), P_s-{F}(V33,V32), P_s-{F}(V34,V12), P_s-{F}(V35,V34), P_s-{F}(V36,V35), P_s-{F}(V37,V12), P_s-{F}(V38,V37), P_s-{F}(V39,V38), P_s-{F}(V40,V12), P_s-{F}(V41,V40), P_s-{F}(V42,V41), P_s-{F}(V43,V12), P_s-{F}(V44,V43), P_s-{F}(V45,V44), P_s-{F}(V46,V47), V13 == V47, V14 == V47, V9 == V47, V15 == V47, V2 == V47, V26 == V47, V22 == V47, V24 == V47, V8 == V47, V46 == V47, V28 == V47, V30 == V47, V42 == V47, V36 == V47, V33 == V47, V45 == V47, V39 == V47, V20 == V47, V18 == V47, P_s-{F}(V48,V47), P_s-{F}(V49,V48), V49 == V47, P_s-{F}(V50,V47), P_s-{F}(V51,V50), V51 == V47, P_s-{F}(V52,V53), V0 == V53, V53 == V4, V53 == V10, #-{F} V54, V6 == V54, V16 == V54, V52 == V54 | r-{T}(V0,V10)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1493: mergings( V2 == V3; #1490 ), references = 1, size of lhs = 19:
% 40.24/40.40 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}(V4,V5), r-{F}(V4,V6), r-{F}(V4,V7), r-{F}(V4,V8), r-{F}(V9,V3), r-{F}(V9,V2), #-{F} V10, #-{F} V11, V3 == V11, V11 == V2, V11 == V4 | P_s-{T}(V10,V3), P_s-{T}(V10,V2), P_s-{T}(V10,V4), P_s-{T}(V10,V11)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1499: mergings( V0 == V1, V1 == V13, V13 == V15, V15 == V17; #1494 ), references = 1, size of lhs = 25:
% 40.24/40.40 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}(V4,V5), r-{F}(V4,V6), r-{F}(V4,V7), r-{F}(V4,V8), r-{F}(V9,V3), r-{F}(V9,V2), P_s-{F}(V10,V3), P_s-{F}(V11,V2), P_s-{F}(V12,V4), #-{F} V13, V10 == V13, V11 == V13, V12 == V13, #-{F} V14, V3 == V14, V14 == V2, V14 == V4 | P_s-{T}(V13,V14)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1508: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8; #1501 ), references = 5, size of lhs = 23:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V1,V2), V0 == V2, r-{F}(V1,V3), V2 == V3, V3 == V0, r-{F}(V4,V3), r-{F}(V4,V2), P_s-{F}(V5,V3), P_s-{F}(V6,V2), r-{F}(V7,V3), V3 == V7, V0 == V7, r-{F}(V7,V2), r-{F}(V7,V8), r-{F}(V7,V9), r-{F}(V7,V10), r-{F}(V7,V11), P_s-{F}(V12,V7), #-{F} V13, V5 == V13, V6 == V13, V12 == V13 | r-{T}(V3,V7)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1516: mergings( V2 == V17, V17 == V18, V18 == V19; #1512 ), references = 1, size of lhs = 66:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), V2 == V0, P_s-{F}(V3,V2), b-{F}(V2,V4), b-{F}(V4,V2), b-{F}(V0,V5), b-{F}(V0,V6), V0 == V6, b-{F}(V6,V0), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V6,V8), b-{F}(V8,V6), P_s-{F}(V9,V5), P_s-{F}(V10,V6), P_s-{F}(V0,V11), V11 == V0, P_s-{F}(V12,V11), P_s-{F}(V13,V11), P_s-{F}(V14,V11), r-{F}(V6,V15), b-{F}(V16,V15), r-{F}(V16,V6), b-{F}(V15,V17), b-{F}(V17,V15), r-{F}(V6,V18), V0 == V18, P_s-{F}(V19,V18), r-{F}(V6,V20), r-{F}(V6,V21), r-{F}(V6,V22), r-{F}(V6,V23), P_s-{F}(V24,V6), P_s-{F}(V25,V26), P_s-{F}(V27,V26), P_s-{F}(V28,V26), P_s-{F}(V29,V26), P_s-{F}(V30,V26), P_s-{F}(V31,V32), V0 == V32, V32 == V2, P_s-{F}(V33,V34), V34 == V0, V34 == V11, P_s-{F}(V35,V34), P_s-{F}(V36,V35), P_s-{F}(V37,V38), V38 == V0, V5 == V38, V6 == V38, V38 == V11, P_s-{F}(V39,V38), P_s-{F}(V40,V39), P_s-{F}(V41,V38), P_s-{F}(V42,V41), #-{F} V43, V3 == V43, V26 == V43, V31 == V43, #-{F} V44, V26 == V44, V19 == V44, V24 == V44 | P_s-{T}(V26,V0), P_s-{T}(V26,V2), P_s-{T}(V26,V11), P_s-{T}(V26,V16), P_s-{T}(V26,V15), P_s-{T}(V26,V18), P_s-{T}(V26,V6), P_s-{T}(V26,V32), P_s-{T}(V26,V34), P_s-{T}(V26,V38), P_s-{T}(V26,V26), P_s-{T}(V26,V9), P_s-{T}(V26,V10), P_s-{T}(V26,V33), P_s-{T}(V26,V12), P_s-{T}(V26,V37), P_s-{T}(V26,V13), P_s-{T}(V26,V14), P_s-{T}(V26,V29), P_s-{T}(V26,V27), P_s-{T}(V26,V36), P_s-{T}(V26,V40), P_s-{T}(V26,V25), P_s-{T}(V26,V30), P_s-{T}(V26,V28), P_s-{T}(V26,V42)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1538: mergings( V0 == V15, V15 == V16, V16 == V17, V17 == V48, V48 == V50, V50 == V52, V52 == V54, V54 == V56, V56 == V58, V58 == V60, V60 == V62, V62 == V64, V64 == V66, V66 == V68, V68 == V70, V70 == V72, V72 == V74, V74 == V76, V76 == V78, V78 == V80; #1517 ), references = 1, size of lhs = 100:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), V2 == V0, P_s-{F}(V3,V2), b-{F}(V2,V4), b-{F}(V4,V2), b-{F}(V0,V5), b-{F}(V0,V6), V0 == V6, b-{F}(V6,V0), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V6,V8), b-{F}(V8,V6), P_s-{F}(V9,V5), P_s-{F}(V10,V6), P_s-{F}(V0,V11), V11 == V0, P_s-{F}(V12,V11), P_s-{F}(V13,V11), P_s-{F}(V14,V11), r-{F}(V6,V15), b-{F}(V15,V16), b-{F}(V16,V15), r-{F}(V6,V17), V0 == V17, P_s-{F}(V18,V17), r-{F}(V6,V19), r-{F}(V6,V20), r-{F}(V6,V21), r-{F}(V6,V22), P_s-{F}(V23,V6), P_s-{F}(V24,V2), P_s-{F}(V25,V11), P_s-{F}(V26,V15), P_s-{F}(V27,V17), P_s-{F}(V28,V6), b-{F}(V29,V15), r-{F}(V29,V6), P_s-{F}(V30,V29), P_s-{F}(V31,V32), V0 == V32, V32 == V2, P_s-{F}(V33,V32), P_s-{F}(V34,V35), P_s-{F}(V35,V36), V36 == V0, V36 == V11, P_s-{F}(V37,V36), P_s-{F}(V38,V36), P_s-{F}(V39,V38), P_s-{F}(V40,V41), P_s-{F}(V41,V42), V42 == V0, V5 == V42, V6 == V42, V42 == V11, P_s-{F}(V43,V42), P_s-{F}(V44,V42), P_s-{F}(V45,V44), P_s-{F}(V46,V42), P_s-{F}(V47,V46), P_s-{F}(V48,V49), V24 == V49, V25 == V49, V30 == V49, V26 == V49, V27 == V49, V28 == V49, V33 == V49, V37 == V49, V43 == V49, V48 == V49, V39 == V49, V45 == V49, P_s-{F}(V50,V49), P_s-{F}(V51,V50), V51 == V49, P_s-{F}(V52,V49), P_s-{F}(V53,V52), V53 == V49, P_s-{F}(V54,V49), P_s-{F}(V55,V54), V55 == V49, P_s-{F}(V56,V49), P_s-{F}(V57,V56), V57 == V49, P_s-{F}(V58,V49), P_s-{F}(V59,V58), V59 == V49, #-{F} V60, V3 == V60, V49 == V60, V31 == V60, #-{F} V61, V49 == V61, V18 == V61, V23 == V61 | P_s-{T}(V49,V0), P_s-{T}(V49,V9), P_s-{T}(V49,V10), P_s-{T}(V49,V12), P_s-{T}(V49,V13), P_s-{T}(V49,V14), P_s-{T}(V49,V34), P_s-{T}(V49,V40), P_s-{T}(V49,V47)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1572: mergings( V15 == V17, V17 == V27, V27 == V29, V29 == V31, V31 == V32, V32 == V34, V34 == V36, V36 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V0, V0 == V16, V16 == V9, V11 == V5, V9 == V10, V5 == V6, V10 == V12, V12 == V13, V13 == V14, V14 == V54, V6 == V55, V54 == V60, V55 == V61, V56 == V62; #1539 ), references = 1, size of lhs = 86:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), V2 == V0, P_s-{F}(V3,V2), b-{F}(V2,V4), b-{F}(V4,V2), b-{F}(V0,V5), V0 == V5, b-{F}(V5,V0), P_s-{F}(V0,V5), b-{F}(V0,V6), b-{F}(V6,V0), b-{F}(V5,V7), b-{F}(V7,V5), r-{F}(V5,V8), b-{F}(V8,V9), b-{F}(V9,V8), r-{F}(V5,V10), V0 == V10, P_s-{F}(V11,V10), r-{F}(V5,V12), r-{F}(V5,V13), r-{F}(V5,V14), r-{F}(V5,V15), P_s-{F}(V16,V5), P_s-{F}(V17,V2), P_s-{F}(V18,V5), P_s-{F}(V19,V8), P_s-{F}(V20,V10), P_s-{F}(V21,V5), P_s-{F}(V5,V22), V22 == V0, V22 == V5, P_s-{F}(V23,V22), P_s-{F}(V24,V22), b-{F}(V25,V8), r-{F}(V25,V5), P_s-{F}(V26,V25), P_s-{F}(V27,V22), P_s-{F}(V28,V27), P_s-{F}(V29,V22), P_s-{F}(V30,V29), P_s-{F}(V31,V22), P_s-{F}(V32,V31), P_s-{F}(V33,V34), V0 == V34, V34 == V2, P_s-{F}(V35,V34), P_s-{F}(V36,V37), V17 == V37, V18 == V37, V26 == V37, V19 == V37, V20 == V37, V21 == V37, V35 == V37, V23 == V37, V24 == V37, V36 == V37, V28 == V37, V30 == V37, P_s-{F}(V38,V37), P_s-{F}(V39,V38), V39 == V37, P_s-{F}(V40,V37), P_s-{F}(V41,V40), V41 == V37, P_s-{F}(V42,V37), P_s-{F}(V43,V42), V43 == V37, P_s-{F}(V44,V37), P_s-{F}(V45,V44), V45 == V37, P_s-{F}(V46,V37), P_s-{F}(V47,V46), V47 == V37, #-{F} V48, V3 == V48, V37 == V48, V33 == V48, #-{F} V49, V37 == V49, V11 == V49, V16 == V49 | P_s-{T}(V37,V32)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1662: 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 == V41, V41 == V44, V42 == V45, V44 == V47, V45 == V48, V47 == V50, V48 == V60, V50 == 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, V60 == V103, V93 == V108, V108 == V109, V103 == V98, V109 == V110, V98 == V36, V110 == V111, V111 == V112, V112 == V113, V113 == V114, V36 == V115, V114 == V118, V115 == V119, V116 == V120, V118 == V122, V119 == V123; #1580 ), references = 1, size of lhs = 126:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), V2 == V0, P_s-{F}(V3,V2), b-{F}(V2,V4), b-{F}(V4,V2), b-{F}(V0,V5), b-{F}(V0,V6), b-{F}(V6,V0), P_s-{F}(V7,V5), 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), b-{F}(V0,V13), b-{F}(V13,V0), P_s-{F}(V14,V12), b-{F}(V0,V15), b-{F}(V15,V0), b-{F}(V0,V16), V16 == V0, P_s-{F}(V17,V16), b-{F}(V16,V18), b-{F}(V18,V16), b-{F}(V0,V19), V0 == V19, b-{F}(V19,V0), P_s-{F}(V0,V19), b-{F}(V19,V20), b-{F}(V20,V19), P_s-{F}(V21,V19), P_s-{F}(V22,V19), P_s-{F}(V23,V19), P_s-{F}(V24,V19), b-{F}(V19,V25), b-{F}(V25,V19), P_s-{F}(V26,V19), P_s-{F}(V27,V19), P_s-{F}(V28,V19), P_s-{F}(V29,V19), P_s-{F}(V30,V19), P_s-{F}(V31,V19), b-{F}(V0,V32), b-{F}(V32,V0), b-{F}(V19,V33), b-{F}(V33,V19), P_s-{F}(V34,V19), P_s-{F}(V35,V16), P_s-{F}(V36,V19), P_s-{F}(V37,V19), P_s-{F}(V19,V38), V38 == V0, V38 == V19, 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,V46), V46 == V2, V46 == V19, V0 == V46, P_s-{F}(V47,V46), P_s-{F}(V48,V46), P_s-{F}(V49,V46), P_s-{F}(V50,V46), P_s-{F}(V51,V46), P_s-{F}(V52,V46), P_s-{F}(V53,V46), P_s-{F}(V54,V46), P_s-{F}(V55,V46), P_s-{F}(V56,V55), P_s-{F}(V57,V46), P_s-{F}(V58,V57), P_s-{F}(V59,V46), P_s-{F}(V60,V59), P_s-{F}(V61,V46), P_s-{F}(V62,V61), P_s-{F}(V63,V46), P_s-{F}(V64,V63), P_s-{F}(V65,V66), P_s-{F}(V67,V66), P_s-{F}(V68,V66), P_s-{F}(V69,V66), P_s-{F}(V70,V66), P_s-{F}(V71,V66), P_s-{F}(V72,V66), P_s-{F}(V73,V66), P_s-{F}(V74,V66), P_s-{F}(V75,V66), P_s-{F}(V76,V66), P_s-{F}(V77,V66), P_s-{F}(V78,V66), P_s-{F}(V79,V80), V0 == V80, V80 == V9, P_s-{F}(V81,V82), V82 == V0, V82 == V19, P_s-{F}(V83,V82), P_s-{F}(V84,V83), P_s-{F}(V85,V86), V86 == V0, V12 == V86, V86 == V19, P_s-{F}(V87,V86), P_s-{F}(V88,V87), P_s-{F}(V89,V86), P_s-{F}(V90,V89), P_s-{F}(V91,V92), V0 == V92, V92 == V16, P_s-{F}(V93,V92), #-{F} V94, V17 == V94, V91 == V94, #-{F} V95, V52 == V95, V34 == V95 | P_s-{T}(V66,V0), P_s-{T}(V66,V2), P_s-{T}(V66,V46), P_s-{T}(V66,V19), P_s-{T}(V66,V5), P_s-{T}(V66,V47), P_s-{T}(V66,V7), P_s-{T}(V66,V21), P_s-{T}(V66,V66), P_s-{T}(V66,V22), P_s-{T}(V66,V48), P_s-{T}(V66,V23), P_s-{T}(V66,V49), P_s-{T}(V66,V24), P_s-{T}(V66,V62), P_s-{T}(V66,V58), P_s-{T}(V66,V65), P_s-{T}(V66,V67), P_s-{T}(V66,V56), P_s-{T}(V66,V64), P_s-{T}(V66,V60), P_s-{T}(V66,V68), P_s-{T}(V66,V9), P_s-{T}(V66,V80), P_s-{T}(V66,V82), P_s-{T}(V66,V86), P_s-{T}(V66,V14), P_s-{T}(V66,V26), P_s-{T}(V66,V81), P_s-{T}(V66,V27), P_s-{T}(V66,V85), P_s-{T}(V66,V28), P_s-{T}(V66,V29), P_s-{T}(V66,V72), P_s-{T}(V66,V70), P_s-{T}(V66,V84), P_s-{T}(V66,V88), P_s-{T}(V66,V69), P_s-{T}(V66,V73), P_s-{T}(V66,V71), P_s-{T}(V66,V90), P_s-{T}(V66,V35), P_s-{T}(V66,V36), P_s-{T}(V66,V53), P_s-{T}(V66,V54), P_s-{T}(V66,V37), P_s-{T}(V66,V93), P_s-{T}(V66,V39), P_s-{T}(V66,V40), P_s-{T}(V66,V42), P_s-{T}(V66,V44), P_s-{T}(V66,V74), P_s-{T}(V66,V75), P_s-{T}(V66,V76), P_s-{T}(V66,V77), P_s-{T}(V66,V78), P_s-{T}(V66,V3), P_s-{T}(V66,V45), P_s-{T}(V66,V10), P_s-{T}(V66,V79), P_s-{T}(V66,V50), P_s-{T}(V66,V30), P_s-{T}(V66,V51), P_s-{T}(V66,V31), P_s-{T}(V66,V94), P_s-{T}(V66,V95)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1831: 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 == V39, V39 == V42, V40 == V43, V42 == V45, V43 == V46, V45 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == 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, V46 == V101, V91 == V28, V28 == V48, V58 == V101, V48 == V106, V106 == V107, V101 == V96, V107 == V108, V96 == V34, V108 == V109, V109 == V110, V110 == V111, V111 == V112, V34 == V113, V112 == V116, V113 == V117, V114 == V118, V116 == V120, V117 == V121, V120 == V177, V177 == V179, V179 == V181, V181 == V183, V183 == V185, V185 == V187, V187 == V189, V189 == V191, V191 == V37, V121 == V33, V37 == V38, V38 == V193, V193 == V41, V41 == V195, V195 == V44, V44 == V197, V197 == V47, V47 == V143, V33 == V142, V118 == V127, V143 == V139, V142 == V138, V139 == V199, V199 == V201, V201 == V137, V138 == V136, V137 == V145, V136 == V144, V145 == V141, V144 == V140, V141 == V203, V203 == V205, V205 == V207, V207 == V68, V68 == V69, V69 == V209, V209 == V211, V211 == V213, V213 == V56, V140 == V53, V56 == V57, V57 == V215, V215 == V59, V59 == V217, V217 == V60, V60 == V61, V61 == V219, V219 == V221, V221 == V165, V53 == V164, V127 == V163, V165 == V169, V164 == V168, V163 == V167, V169 == V223, V223 == V225, V225 == V227, V227 == V171, V168 == V170, V171 == V103, V170 == V93, V103 == V104, V104 == V229, V229 == V231, V231 == V105, V105 == V233, V233 == V235, V235 == V237, V237 == V123, V93 == V122, V123 == V125, V122 == V124, V125 == V239, V239 == V241, V241 == V243, V243 == V245, V245 == V247, V247 == V31, V124 == V30, V31 == V249, V249 == V51, V30 == V50, V51 == V251, V251 == V253, V253 == V97, V97 == V255, V255 == V98, V98 == V257; #1663 ), references = 1, size of lhs = 154:
% 40.24/40.40 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), V0 == V6, b-{F}(V6,V0), P_s-{F}(V0,V6), b-{F}(V6,V7), b-{F}(V7,V6), b-{F}(V6,V8), b-{F}(V8,V6), b-{F}(V6,V9), b-{F}(V9,V6), b-{F}(V6,V10), b-{F}(V10,V6), P_s-{F}(V11,V6), b-{F}(V6,V12), b-{F}(V12,V6), b-{F}(V0,V13), b-{F}(V13,V0), b-{F}(V6,V14), b-{F}(V14,V6), P_s-{F}(V15,V6), P_s-{F}(V16,V6), P_s-{F}(V17,V6), P_s-{F}(V18,V6), P_s-{F}(V19,V6), P_s-{F}(V20,V6), P_s-{F}(V21,V6), P_s-{F}(V22,V6), P_s-{F}(V23,V6), P_s-{F}(V6,V24), V24 == V0, V24 == V6, P_s-{F}(V25,V24), P_s-{F}(V26,V24), P_s-{F}(V27,V24), P_s-{F}(V28,V24), 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,V24), P_s-{F}(V38,V37), P_s-{F}(V39,V24), P_s-{F}(V40,V39), P_s-{F}(V41,V24), P_s-{F}(V42,V41), P_s-{F}(V43,V24), 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,V24), P_s-{F}(V52,V51), P_s-{F}(V53,V54), V0 == V54, V54 == V6, P_s-{F}(V55,V54), P_s-{F}(V56,V55), P_s-{F}(V57,V58), V16 == V58, V26 == V58, V17 == V58, V18 == V58, V19 == V58, V20 == V58, V21 == V58, V36 == V58, V57 == V58, V38 == V58, V40 == V58, V22 == V58, V23 == V58, V27 == V58, V28 == V58, V50 == V58, V52 == V58, V46 == V58, V48 == V58, V56 == V58, V30 == V58, V32 == V58, V34 == V58, V42 == V58, V44 == V58, P_s-{F}(V59,V58), P_s-{F}(V60,V59), V60 == V58, P_s-{F}(V61,V58), P_s-{F}(V62,V61), V62 == V58, P_s-{F}(V63,V58), P_s-{F}(V64,V63), V64 == V58, P_s-{F}(V65,V58), P_s-{F}(V66,V65), V66 == V58, P_s-{F}(V67,V58), P_s-{F}(V68,V67), V68 == V58, P_s-{F}(V69,V58), P_s-{F}(V70,V69), V70 == V58, P_s-{F}(V71,V58), P_s-{F}(V72,V71), V72 == V58, P_s-{F}(V73,V58), P_s-{F}(V74,V73), V74 == V58, P_s-{F}(V75,V58), P_s-{F}(V76,V75), V76 == V58, P_s-{F}(V77,V58), P_s-{F}(V78,V77), V78 == V58, P_s-{F}(V79,V58), P_s-{F}(V80,V79), V80 == V58, P_s-{F}(V81,V58), P_s-{F}(V82,V81), V82 == V58, P_s-{F}(V83,V58), P_s-{F}(V84,V83), V84 == V58, P_s-{F}(V85,V86), V0 == V86, V86 == V6, V85 == V58, P_s-{F}(V87,V86), P_s-{F}(V88,V87), V88 == V58, P_s-{F}(V89,V90), V11 == V90, V53 == V90, V89 == V58, #-{F} V91, V25 == V91, V15 == V91 | P_s-{T}(V58,V91)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #1995: mergings( V64 == V66, 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 == V33, V32 == V34, V33 == V35, V34 == V36, V35 == 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 == V1, V36 == V66, V1 == V68, V68 == V69, V66 == V2, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V2 == V75, V74 == V77, V75 == V78, V76 == V79, V77 == V80, V78 == V81, V80 == V82, V82 == V84, V84 == V85, V85 == V87, V87 == V89, V89 == V91, V91 == V93, V93 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V81 == V105, V79 == V106, V104 == V109, V105 == V110, V109 == V111, V111 == V112, V112 == V113, V110 == V114, V113 == V115, V114 == V116, V115 == V117, V116 == V118, V117 == V119, V119 == V120, V120 == V122, V122 == V124, V124 == V125, V125 == V126, V126 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V133, V133 == V134, V134 == V135, V135 == V136, V136 == V137, V137 == V138, V118 == V139, V106 == V140, V138 == V142, V139 == V143, V140 == V144, V142 == V146, V146 == V147, V147 == V148, V148 == V149, V143 == V150, V149 == V151, V151 == V152, V152 == V153, V153 == V154, V154 == V155, V155 == V156, V156 == V157, V157 == V158, V158 == V159, V150 == V160, V159 == V161, V160 == V162, V161 == V163, V163 == V164, V164 == V165, V165 == V166, V166 == V167, V167 == V168, V168 == V169, V169 == V170, V170 == V171, V171 == V172, V172 == V173, V173 == V174, V174 == V175, V175 == V176, V176 == V177; #1833 ), references = 2, size of lhs = 130:
% 40.24/40.40 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, 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}(V1,V12), V12 == V0, V12 == V1, P_s-{F}(V13,V12), P_s-{F}(V14,V12), P_s-{F}(V15,V12), P_s-{F}(V16,V12), P_s-{F}(V17,V12), P_s-{F}(V18,V17), P_s-{F}(V19,V12), P_s-{F}(V20,V19), P_s-{F}(V21,V12), P_s-{F}(V22,V21), P_s-{F}(V23,V12), P_s-{F}(V24,V23), P_s-{F}(V25,V12), P_s-{F}(V26,V25), P_s-{F}(V27,V12), P_s-{F}(V28,V27), P_s-{F}(V29,V12), P_s-{F}(V30,V29), P_s-{F}(V31,V12), P_s-{F}(V32,V31), P_s-{F}(V33,V12), P_s-{F}(V34,V33), P_s-{F}(V35,V12), P_s-{F}(V36,V35), P_s-{F}(V37,V12), P_s-{F}(V38,V37), P_s-{F}(V39,V12), P_s-{F}(V40,V39), P_s-{F}(V41,V42), V0 == V42, V42 == V1, P_s-{F}(V43,V42), P_s-{F}(V44,V43), P_s-{F}(V45,V46), V4 == V46, V14 == V46, V5 == V46, V6 == V46, V7 == V46, V8 == V46, V9 == V46, V24 == V46, V45 == V46, V26 == V46, V28 == V46, V10 == V46, V11 == V46, V15 == V46, V16 == V46, V38 == V46, V40 == V46, V34 == V46, V36 == V46, V44 == V46, V18 == V46, V20 == V46, V22 == V46, V30 == V46, V32 == V46, P_s-{F}(V47,V46), P_s-{F}(V48,V47), V48 == V46, P_s-{F}(V49,V46), P_s-{F}(V50,V49), V50 == V46, P_s-{F}(V51,V46), P_s-{F}(V52,V51), V52 == V46, P_s-{F}(V53,V46), P_s-{F}(V54,V53), V54 == V46, P_s-{F}(V55,V46), P_s-{F}(V56,V55), V56 == V46, P_s-{F}(V57,V46), P_s-{F}(V58,V57), V58 == V46, P_s-{F}(V59,V46), P_s-{F}(V60,V59), V60 == V46, P_s-{F}(V61,V46), P_s-{F}(V62,V61), V62 == V46, P_s-{F}(V63,V46), P_s-{F}(V64,V63), V64 == V46, P_s-{F}(V65,V46), P_s-{F}(V66,V65), V66 == V46, P_s-{F}(V67,V46), P_s-{F}(V68,V67), V68 == V46, P_s-{F}(V69,V46), P_s-{F}(V70,V69), V70 == V46, P_s-{F}(V71,V46), P_s-{F}(V72,V71), V72 == V46, P_s-{F}(V73,V74), V0 == V74, V74 == V1, V73 == V46, P_s-{F}(V75,V74), P_s-{F}(V76,V75), V76 == V46, P_s-{F}(V77,V78), V2 == V78, V41 == V78, V77 == V46, P_s-{F}(V79,V80), V13 == V80, V3 == V80, V79 == V46 | r-{T}(V0,V1)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2000: mergings( V0 == V3, V3 == V4; #1997 ), references = 1, size of lhs = 20:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V1,V2), V1 == V2, r-{F}(V2,V1), r-{F}(V2,V3), r-{F}(V2,V4), r-{F}(V2,V5), r-{F}(V2,V6), #-{F} V7, V2 == V7, V7 == V1, #-{F} V8, V1 == V8, V8 == V7, V8 == V2, #-{F} V9, V1 == V9, V9 == V7, V9 == V2, V8 == V9 | b-{T}(V2,V7)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2010: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7; #2004 ), references = 1, size of lhs = 23:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V2,V3), V3 == V2, b-{F}(V3,V2), r-{F}(V2,V4), r-{F}(V2,V5), r-{F}(V2,V6), r-{F}(V2,V7), b-{F}(V1,V8), V8 == V3, V8 == V2, b-{F}(V9,V8), b-{F}(V9,V2), r-{F}(V2,V10), r-{F}(V2,V11), V8 == V11, b-{F}(V11,V8), #-{F} V12, #-{F} V13, V3 == V13, V13 == V8, V13 == V2 | P_s-{T}(V12,V3), P_s-{T}(V12,V8), P_s-{T}(V12,V2), P_s-{T}(V12,V13)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2020: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V19, V19 == V21, V21 == V7; #2011 ), references = 1, size of lhs = 27:
% 40.24/40.40 P_z-{F}(V0), b-{F}(V1,V0), r-{F}(V0,V2), V2 == V0, b-{F}(V2,V0), r-{F}(V0,V3), r-{F}(V0,V4), r-{F}(V0,V5), r-{F}(V0,V6), b-{F}(V1,V7), V7 == V2, V7 == V0, b-{F}(V8,V7), b-{F}(V8,V0), r-{F}(V0,V9), r-{F}(V0,V10), V7 == V10, b-{F}(V10,V7), P_s-{F}(V11,V2), P_s-{F}(V12,V7), #-{F} V13, V11 == V13, V12 == V13, #-{F} V14, V2 == V14, V14 == V7, V14 == V0 | P_s-{T}(V13,V14)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2033: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V20; #2022 ), references = 2, size of lhs = 24:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), r-{F}(V0,V2), r-{F}(V0,V3), r-{F}(V0,V4), r-{F}(V0,V5), r-{F}(V0,V6), r-{F}(V0,V7), b-{F}(V7,V0), P_s-{F}(V8,V1), P_s-{F}(V9,V10), V10 == V1, V10 == V0, V10 == V7, P_s-{F}(V11,V12), V1 == V12, V12 == V10, V12 == V0, #-{F} V13, V8 == V13, V9 == V13, V11 == V13 | r-{T}(V7,V10)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2067: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V20, V20 == V21, V21 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35; #2047 ), references = 1, size of lhs = 38:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), r-{F}(V0,V2), r-{F}(V0,V3), r-{F}(V0,V4), r-{F}(V0,V5), r-{F}(V0,V6), P_s-{F}(V7,V1), r-{F}(V0,V8), V0 == V8, b-{F}(V8,V0), r-{F}(V0,V9), V9 == V0, b-{F}(V9,V0), r-{F}(V0,V10), r-{F}(V0,V11), r-{F}(V0,V12), r-{F}(V0,V13), r-{F}(V0,V14), P_s-{F}(V15,V9), P_s-{F}(V16,V8), P_s-{F}(V17,V8), r-{F}(V18,V8), r-{F}(V18,V19), r-{F}(V18,V20), P_s-{F}(V21,V22), V22 == V1, V22 == V8, V0 == V22, V18 == V22, P_s-{F}(V23,V22), P_s-{F}(V24,V22), P_s-{F}(V25,V26), V9 == V26, V26 == V0, #-{F} V27 | P_s-{T}(V27,V1), P_s-{T}(V27,V22), P_s-{T}(V27,V0), P_s-{T}(V27,V9), P_s-{T}(V27,V8), P_s-{T}(V27,V18), P_s-{T}(V27,V26), P_s-{T}(V27,V7), P_s-{T}(V27,V21), P_s-{T}(V27,V27), P_s-{T}(V27,V15), P_s-{T}(V27,V25), P_s-{T}(V27,V23), P_s-{T}(V27,V16), P_s-{T}(V27,V24), P_s-{T}(V27,V17)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2097: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V18, V18 == V19, V19 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V46, V46 == V48, V48 == V50, V50 == V52, V52 == V54, V54 == V56, V56 == V58, V58 == V60, V60 == V62, V62 == V64; #2068 ), references = 1, size of lhs = 57:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), r-{F}(V0,V2), r-{F}(V0,V3), r-{F}(V0,V4), r-{F}(V0,V5), r-{F}(V0,V6), P_s-{F}(V7,V1), r-{F}(V0,V8), V0 == V8, b-{F}(V8,V0), r-{F}(V0,V9), V9 == V0, b-{F}(V9,V0), r-{F}(V0,V10), r-{F}(V0,V11), r-{F}(V0,V12), r-{F}(V0,V13), r-{F}(V0,V14), P_s-{F}(V15,V9), P_s-{F}(V16,V8), P_s-{F}(V17,V8), r-{F}(V18,V8), r-{F}(V18,V19), r-{F}(V18,V20), P_s-{F}(V21,V1), P_s-{F}(V22,V9), P_s-{F}(V23,V8), P_s-{F}(V24,V25), V25 == V1, V25 == V8, V0 == V25, V18 == V25, P_s-{F}(V26,V25), P_s-{F}(V27,V26), P_s-{F}(V28,V25), P_s-{F}(V29,V28), P_s-{F}(V30,V25), P_s-{F}(V31,V30), P_s-{F}(V32,V33), V9 == V33, V33 == V0, P_s-{F}(V34,V33), P_s-{F}(V35,V34), P_s-{F}(V36,V37), V21 == V37, V24 == V37, V22 == V37, V23 == V37, V32 == V37, V27 == V37, V36 == V37, V35 == V37, V29 == V37, V31 == V37 | P_s-{T}(V37,V0), P_s-{T}(V37,V18), P_s-{T}(V37,V7), P_s-{T}(V37,V15), P_s-{T}(V37,V16), P_s-{T}(V37,V17)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2133: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V18, V18 == V28, V28 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V39, V39 == V41, V41 == V42, V42 == V44, V44 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V9, V9 == V19, V19 == V27, V27 == V29, V29 == V36, V36 == V17, V17 == V26, V10 == V20, V26 == V34, V20 == V16; #2098 ), references = 2, size of lhs = 46:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V0,V2), r-{F}(V0,V3), r-{F}(V0,V4), r-{F}(V0,V5), r-{F}(V0,V6), r-{F}(V0,V7), r-{F}(V0,V8), r-{F}(V0,V9), r-{F}(V0,V10), r-{F}(V0,V11), V0 == V11, b-{F}(V11,V0), P_s-{F}(V0,V11), P_s-{F}(V12,V11), P_s-{F}(V13,V11), P_s-{F}(V14,V11), P_s-{F}(V15,V11), r-{F}(V0,V16), r-{F}(V0,V17), P_s-{F}(V18,V19), V19 == V11, V0 == V19, P_s-{F}(V20,V19), P_s-{F}(V21,V20), P_s-{F}(V22,V19), P_s-{F}(V23,V22), P_s-{F}(V24,V19), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V11 == V27, V27 == V0, P_s-{F}(V28,V27), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V13 == V31, V18 == V31, V14 == V31, V15 == V31, V26 == V31, V21 == V31, V30 == V31, V29 == V31, V23 == V31, V25 == V31 | P_s-{T}(V31,V12)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2146: mergings( V0 == V1, V1 == V27, V27 == V28; #2142 ), references = 1, size of lhs = 98:
% 40.24/40.40 P_z-{F}(V0), r-{F}(V1,V0), V0 == V1, r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), P_s-{F}(V6,V1), r-{F}(V1,V7), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V1,V10), P_s-{F}(V11,V1), r-{F}(V1,V12), r-{F}(V1,V13), r-{F}(V1,V14), r-{F}(V1,V15), P_s-{F}(V16,V1), r-{F}(V1,V17), P_s-{F}(V18,V1), r-{F}(V1,V19), r-{F}(V1,V20), r-{F}(V1,V21), r-{F}(V1,V22), P_s-{F}(V23,V1), r-{F}(V1,V24), P_s-{F}(V25,V1), r-{F}(V1,V26), P_s-{F}(V27,V28), V28 == V0, V28 == V1, P_s-{F}(V29,V28), P_s-{F}(V30,V28), P_s-{F}(V31,V32), V0 == V32, V32 == V28, V32 == V1, P_s-{F}(V33,V34), V34 == V28, V34 == V0, V1 == V34, P_s-{F}(V35,V34), P_s-{F}(V36,V34), P_s-{F}(V37,V34), P_s-{F}(V38,V39), V0 == V39, V39 == V34, V39 == V1, P_s-{F}(V40,V41), V0 == V41, V41 == V34, V1 == V41, P_s-{F}(V42,V43), V0 == V43, V43 == V1, P_s-{F}(V44,V43), P_s-{F}(V45,V46), V34 == V46, V46 == V41, V46 == V0, P_s-{F}(V47,V48), V0 == V48, V48 == V1, P_s-{F}(V49,V48), P_s-{F}(V50,V51), V28 == V51, V51 == V34, V51 == V0, #-{F} V52, V27 == V52, V6 == V52, V31 == V52, #-{F} V53, V33 == V53, V11 == V53, V38 == V53, #-{F} V54, V18 == V54, V35 == V54, V29 == V54, V44 == V54, V40 == V54, V45 == V54, #-{F} V55, V54 == V55, V16 == V55, V42 == V55, #-{F} V56, V25 == V56, V30 == V56, V36 == V56, V49 == V56, V37 == V56, V50 == V56, #-{F} V57, V56 == V57, V23 == V57, V47 == V57 | r-{T}(V0,V1)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2152: mergings( V2 == V21; #2150 ), references = 1, size of lhs = 66:
% 40.24/40.40 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, 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-{T}(V1,V0), P_s-{T}(V1,V1), P_s-{T}(V1,V4), P_s-{T}(V1,V20), P_s-{T}(V1,V21), P_s-{T}(V1,V22), P_s-{T}(V1,V5), P_s-{T}(V1,V6), 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,V2), P_s-{T}(V1,V3), 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,V26), P_s-{T}(V1,V27), P_s-{T}(V1,V28), P_s-{T}(V1,V15), P_s-{T}(V1,V16), P_s-{T}(V1,V33), P_s-{T}(V1,V34), P_s-{T}(V1,V31), P_s-{T}(V1,V32), P_s-{T}(V1,V46), P_s-{T}(V1,V23), P_s-{T}(V1,V24), P_s-{T}(V1,V25), P_s-{T}(V1,V29), P_s-{T}(V1,V30), 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,V7), P_s-{T}(V1,V8), P_s-{T}(V1,V17), P_s-{T}(V1,V18), P_s-{T}(V1,V19), P_s-{T}(V1,V61), P_s-{T}(V1,V64), P_s-{T}(V1,V62), P_s-{T}(V1,V63)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2218: mergings( V20 == V0, V0 == V4, V4 == V21, V21 == V22, V22 == V23, V23 == V5, V5 == V6, V6 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V2, V2 == V3, V3 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V27, V27 == V28, V28 == V29, V29 == V15, V15 == V16, V16 == V34, V34 == V35, V35 == V32, V32 == V33, V33 == V47, V47 == V24, V24 == V25, V25 == V26, V26 == V30, V30 == V31, V31 == 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 == V7, V7 == V8, V8 == V17, V17 == V18, V18 == V19, V19 == V62, V62 == V65, V65 == V63, V63 == V64; #2153 ), references = 1, size of lhs = 3:
% 40.24/40.40 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1 | P_s-{T}(V1,V1)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2222: mergings( V0 == V2; #2220 ), references = 1, size of lhs = 1:
% 40.24/40.40 P_z-{F}(V0) | P_s-{T}(V0,V0)
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 #2225: exists( #8, #2223 ), references = 1, size of lhs = 0:
% 40.24/40.40 FALSE | FALSE
% 40.24/40.40 (used 0 times, uses = {})
% 40.24/40.40
% 40.24/40.40 number of learnt formulas = 70
% 40.24/40.40
% 40.24/40.40
% 40.24/40.40 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.24/40.40
% 40.24/40.40 randbase = 1
%------------------------------------------------------------------------------