%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : GRA171-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n003.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:34 PM UTC 2026
% Result : Unsatisfiable 57.87s 58.05s
% Output : Refutation 57.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRA171-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.18/0.34 % Computer : n003.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34 % CPULimit : 300
% 0.18/0.34 % WCLimit : 300
% 0.18/0.34 % DateTime : Tue May 5 00:57:56 EDT 2026
% 0.18/0.35 % CPUTime :
% 57.87/58.05 GeoParameters:
% 57.87/58.05
% 57.87/58.05 tptp_input = 1
% 57.87/58.05 tptp_output = 0
% 57.87/58.05 nonempty = 1
% 57.87/58.05 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 57.87/58.05 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 57.87/58.05
% 57.87/58.05
% 57.87/58.05 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 57.87/58.05 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 57.87/58.05
% 57.87/58.05 RuleSystem INPUT:
% 57.87/58.05
% 57.87/58.05 Initial Rules:
% 57.87/58.05 #0: input, references = 10, size of lhs = 2:
% 57.87/58.05 P_z-{F}(V0), P_s-{F}(V1,V0) | FALSE
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1: input, references = 8, size of lhs = 4:
% 57.87/58.05 P_z-{F}(V0), P_s-{F}(V1,V4), P_s-{F}(V2,V4), V1 == V2 | FALSE
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #2: input, references = 3, size of lhs = 2:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V1) | FALSE
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #3: input, references = 3, size of lhs = 2:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V1) | FALSE
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #4: input, references = 32, size of lhs = 4:
% 57.87/58.05 P_z-{F}(V0), #-{F} V1, #-{F} V2, V1 == V2 | r-{T}(V1,V2), b-{T}(V1,V2)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #5: input, references = 26, size of lhs = 4:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V3,V1), r-{F}(V3,V2) | FALSE
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #6: input, references = 6, size of lhs = 7:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V3,V1), b-{F}(V3,V2), b-{F}(V1,V4), b-{F}(V2,V5), b-{F}(V5,V4) | FALSE
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #7: input, references = 14, size of lhs = 1:
% 57.87/58.05 #-{F} V0 | EXISTS V1: P_s-{T}(V0,V1)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #8: input, references = 4, size of lhs = 0:
% 57.87/58.05 FALSE | EXISTS V0: P_z-{T}(V0)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 number of initial rules = 9
% 57.87/58.05
% 57.87/58.05 Simplifiers:
% 57.87/58.05 #9: unsound, references = 3, size of lhs = 3:
% 57.87/58.05 P_s-{F}(V0,V1), P_s-{F}(V0,V3), V1 == V3 | FALSE
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #10: unsound, references = 3, size of lhs = 3:
% 57.87/58.05 P_z-{F}(V0), P_z-{F}(V1), V0 == V1 | FALSE
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 number of simplifiers = 2
% 57.87/58.05
% 57.87/58.05 Learnt:
% 57.87/58.05 #13: mergings( V0 == V3; #11 ), references = 13, size of lhs = 6:
% 57.87/58.05 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)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #16: mergings( V0 == V3; #14 ), references = 9, size of lhs = 7:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V1,V3), b-{F}(V2,V4), b-{F}(V5,V4), V3 == V5 | r-{T}(V3,V5)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #24: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #19 ), references = 8, size of lhs = 12:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V2), b-{F}(V1,V4), b-{F}(V4,V5), V1 == V5, V5 == V2, b-{F}(V4,V6), b-{F}(V7,V6), V5 == V7, r-{F}(V7,V2) | r-{T}(V1,V5)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #29: mergings( V0 == V3, V3 == V4; #26 ), references = 4, size of lhs = 8:
% 57.87/58.05 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)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #36: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #31 ), references = 6, size of lhs = 10:
% 57.87/58.05 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)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #41: mergings( V0 == V3, V3 == V4; #38 ), references = 6, size of lhs = 8:
% 57.87/58.05 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)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #44: mergings( V0 == V3; #42 ), references = 3, size of lhs = 4:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V3,V2), V3 == V1 | b-{T}(V3,V1)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #58: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9; #50 ), references = 3, size of lhs = 31:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V2), r-{F}(V4,V2), b-{F}(V4,V5), b-{F}(V6,V5), V1 == V6, b-{F}(V6,V7), V1 == V7, V7 == V2, V7 == V4, b-{F}(V1,V8), b-{F}(V8,V9), b-{F}(V9,V8), b-{F}(V6,V10), V1 == V10, V10 == V8, V10 == V7, b-{F}(V6,V11), b-{F}(V12,V11), V10 == V12, r-{F}(V12,V8), b-{F}(V13,V10), b-{F}(V13,V7), b-{F}(V14,V7), b-{F}(V14,V10), b-{F}(V15,V7), V7 == V15, r-{F}(V16,V15), V7 == V16 | r-{T}(V1,V6)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #67: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #62 ), references = 3, size of lhs = 30:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V2), r-{F}(V4,V2), b-{F}(V4,V5), V5 == V1, b-{F}(V4,V6), V6 == V5, V6 == V1, b-{F}(V4,V7), V1 == V7, V7 == V2, V7 == V4, V7 == V5, V7 == V6, r-{F}(V1,V8), V7 == V8, V5 == V8, V6 == V8, r-{F}(V8,V2), b-{F}(V8,V7), b-{F}(V9,V6), b-{F}(V9,V5), b-{F}(V10,V5), b-{F}(V10,V6), b-{F}(V11,V5), V5 == V11, r-{F}(V12,V11), V5 == V12 | r-{T}(V1,V7)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #86: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13; #74 ), references = 1, size of lhs = 29:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V3,V2), r-{F}(V3,V4), V2 == V4, b-{F}(V4,V2), r-{F}(V5,V3), r-{F}(V6,V3), #-{F} V7, V7 == V4, V7 == V2, V7 == V1, V7 == V3, #-{F} V8, V8 == V4, V2 == V8, V8 == V1, V7 == V8, V8 == V3, V8 == V6, #-{F} V9, V9 == V4, V1 == V9, V9 == V2, V9 == V8, V7 == V9, V9 == V3, V9 == V5 | r-{T}(V2,V4)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #102: 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; #88 ), references = 2, size of lhs = 26:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V2,V4), V3 == V4, r-{F}(V4,V2), r-{F}(V5,V2), r-{F}(V6,V3), r-{F}(V6,V4), #-{F} V7, V7 == V3, V7 == V4, V7 == V2, #-{F} V8, V3 == V8, V8 == V4, V7 == V8, V8 == V2, V8 == V5, #-{F} V9, V4 == V9, V9 == V3, V9 == V8, V7 == V9, V9 == V2, V9 == V1 | r-{T}(V4,V3)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #119: 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; #104 ), references = 1, size of lhs = 23:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V2,V4), V3 == V4, r-{F}(V4,V2), r-{F}(V5,V2), r-{F}(V6,V3), r-{F}(V6,V4), r-{F}(V7,V4), r-{F}(V7,V3), #-{F} V8, #-{F} V9, V3 == V9, V9 == V4, V9 == V2, V9 == V5, #-{F} V10, V4 == V10, V10 == V3, V10 == V9, V10 == V2, V10 == V1 | P_s-{T}(V8,V3), P_s-{T}(V8,V4), P_s-{T}(V8,V2), P_s-{T}(V8,V9), P_s-{T}(V8,V10)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #139: 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 == V25, V25 == V18, V18 == V27, V27 == V29; #120 ), references = 1, size of lhs = 28:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V1,V3), V3 == V0, r-{F}(V4,V1), r-{F}(V5,V3), r-{F}(V5,V0), r-{F}(V6,V0), r-{F}(V6,V3), P_s-{F}(V7,V3), P_s-{F}(V8,V1), P_s-{F}(V9,V10), V3 == V10, V10 == V0, V10 == V1, V10 == V4, #-{F} V11, V7 == V11, V8 == V11, V9 == V11, #-{F} V12, V0 == V12, V12 == V3, V12 == V10, V12 == V1, V12 == V2 | P_s-{T}(V11,V12)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #162: 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 == V23, V23 == V25, V25 == V26; #141 ), references = 4, size of lhs = 25:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V6), V1 == V6, V6 == V0, P_s-{F}(V7,V8), V6 == V8, V8 == V0, V8 == V1, V8 == V3, P_s-{F}(V9,V10), V0 == V10, V10 == V6, V10 == V8, V10 == V1, V10 == V2, #-{F} V11, V5 == V11, V4 == V11, V7 == V11, V9 == V11 | b-{T}(V1,V6)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #166: mergings( V2 == V3; #164 ), references = 1, size of lhs = 23:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V2,V4), V3 == V4, r-{F}(V4,V2), r-{F}(V5,V2), r-{F}(V6,V3), r-{F}(V6,V4), r-{F}(V4,V7), r-{F}(V7,V3), #-{F} V8, #-{F} V9, V3 == V9, V9 == V4, V9 == V2, V9 == V5, #-{F} V10, V4 == V10, V10 == V3, V10 == V9, V10 == V2, V10 == V1 | P_s-{T}(V8,V3), P_s-{T}(V8,V4), P_s-{T}(V8,V2), P_s-{T}(V8,V9), P_s-{T}(V8,V10)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #173: mergings( V0 == V1, V1 == V12, V12 == V14, V14 == V16, V16 == V18; #167 ), references = 1, size of lhs = 29:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V2,V4), V3 == V4, r-{F}(V4,V2), r-{F}(V5,V2), r-{F}(V6,V3), r-{F}(V6,V4), r-{F}(V4,V7), r-{F}(V7,V3), P_s-{F}(V8,V3), P_s-{F}(V9,V4), P_s-{F}(V10,V11), V3 == V11, V11 == V4, V11 == V2, V11 == V5, P_s-{F}(V12,V13), V4 == V13, V13 == V3, V13 == V11, V13 == V2, V13 == V1, #-{F} V14, V8 == V14, V9 == V14, V10 == V14, V12 == V14 | P_s-{T}(V14,V2)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #183: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V1; #175 ), references = 5, size of lhs = 25:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V2,V0), r-{F}(V0,V3), r-{F}(V3,V0), P_s-{F}(V4,V3), P_s-{F}(V5,V6), V0 == V6, V6 == V3, P_s-{F}(V7,V8), V6 == V8, V8 == V3, V8 == V0, V8 == V2, P_s-{F}(V9,V10), V3 == V10, V10 == V6, V10 == V8, V10 == V0, V10 == V1, #-{F} V11, V5 == V11, V4 == V11, V7 == V11, V9 == V11 | b-{T}(V0,V6)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #194: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7; #188 ), references = 2, size of lhs = 46:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V1,V3), b-{F}(V3,V2), b-{F}(V3,V4), V4 == V3, V4 == V1, b-{F}(V3,V5), V5 == V3, V4 == V5, b-{F}(V3,V6), b-{F}(V7,V6), V5 == V7, r-{F}(V7,V3), b-{F}(V8,V5), b-{F}(V8,V4), b-{F}(V9,V5), V5 == V9, r-{F}(V10,V3), b-{F}(V10,V11), b-{F}(V9,V11), b-{F}(V3,V12), V12 == V3, V12 == V4, V12 == V5, V12 == V9, r-{F}(V13,V3), b-{F}(V13,V14), b-{F}(V9,V14), b-{F}(V9,V15), V12 == V15, V15 == V3, V15 == V10, b-{F}(V9,V16), V12 == V16, V16 == V3, V16 == V15, V16 == V13, b-{F}(V17,V16), b-{F}(V17,V15), b-{F}(V18,V15), b-{F}(V18,V16), b-{F}(V19,V15), V15 == V19, r-{F}(V20,V19), V15 == V20 | r-{T}(V12,V3)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #246: 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 == V23, V23 == V25, V25 == V26, V26 == V27, V27 == V31, V31 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64; #205 ), references = 1, size of lhs = 80:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), P_s-{F}(V4,V1), r-{F}(V5,V1), r-{F}(V6,V1), P_s-{F}(V7,V1), r-{F}(V8,V1), r-{F}(V9,V1), P_s-{F}(V10,V1), r-{F}(V11,V0), r-{F}(V12,V0), r-{F}(V0,V13), r-{F}(V13,V0), P_s-{F}(V14,V13), r-{F}(V15,V0), r-{F}(V16,V0), r-{F}(V0,V17), r-{F}(V17,V0), P_s-{F}(V18,V17), r-{F}(V19,V0), r-{F}(V20,V0), r-{F}(V0,V21), r-{F}(V21,V0), P_s-{F}(V22,V21), r-{F}(V23,V0), r-{F}(V24,V1), P_s-{F}(V25,V26), V26 == V13, V26 == V0, V26 == V1, V26 == V24, P_s-{F}(V27,V26), P_s-{F}(V28,V29), V26 == V29, V29 == V0, V29 == V1, V29 == V3, P_s-{F}(V30,V31), V31 == V17, V31 == V0, V31 == V1, V31 == V26, P_s-{F}(V32,V31), P_s-{F}(V33,V34), V31 == V34, V34 == V0, V34 == V1, V34 == V6, P_s-{F}(V35,V36), V36 == V0, V36 == V1, V36 == V9, P_s-{F}(V37,V38), V0 == V38, V38 == V36, V38 == V1, V38 == V8, P_s-{F}(V39,V40), V26 == V40, V40 == V13, V40 == V0, V40 == V12, P_s-{F}(V41,V42), V31 == V42, V42 == V17, V42 == V0, V42 == V16, P_s-{F}(V43,V44), V44 == V21, V44 == V0, V44 == V20, P_s-{F}(V45,V46), V21 == V46, V46 == V44, V46 == V0, V46 == V19, #-{F} V47 | P_s-{T}(V47,V0), P_s-{T}(V47,V26), P_s-{T}(V47,V29), P_s-{T}(V47,V1), P_s-{T}(V47,V2), P_s-{T}(V47,V31), P_s-{T}(V47,V34), P_s-{T}(V47,V5), P_s-{T}(V47,V21), P_s-{T}(V47,V23), P_s-{T}(V47,V36), P_s-{T}(V47,V38), P_s-{T}(V47,V13), P_s-{T}(V47,V40), P_s-{T}(V47,V11), P_s-{T}(V47,V17), P_s-{T}(V47,V42), P_s-{T}(V47,V15), P_s-{T}(V47,V44), P_s-{T}(V47,V46), P_s-{T}(V47,V25), P_s-{T}(V47,V4), P_s-{T}(V47,V28), P_s-{T}(V47,V47), P_s-{T}(V47,V30), P_s-{T}(V47,V7), P_s-{T}(V47,V33), P_s-{T}(V47,V10), P_s-{T}(V47,V35), P_s-{T}(V47,V37), P_s-{T}(V47,V27), P_s-{T}(V47,V14), P_s-{T}(V47,V39), P_s-{T}(V47,V32), P_s-{T}(V47,V18), P_s-{T}(V47,V41), P_s-{T}(V47,V22), P_s-{T}(V47,V43), P_s-{T}(V47,V45)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #318: 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 == V21, V21 == V23, V23 == V24, V24 == V25, V25 == V29, V29 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V88, V88 == V90, V90 == V92, V92 == V94, V94 == V96, V96 == V98, V98 == V100, V100 == V102, V102 == V104, V104 == V106, V106 == V108, V108 == V110, V110 == V112, V112 == V114, V114 == V116, V116 == V118, V118 == V120, V120 == V122, V122 == V124, V124 == V126, V126 == V128, V128 == V130, V130 == V132, V132 == V134, V134 == V136, V136 == V138, V138 == V140, V140 == V142, V142 == V144, V144 == V146; #247 ), references = 1, size of lhs = 139:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), P_s-{F}(V4,V1), r-{F}(V5,V1), r-{F}(V6,V1), P_s-{F}(V7,V1), r-{F}(V8,V1), r-{F}(V9,V1), P_s-{F}(V10,V1), r-{F}(V11,V0), r-{F}(V0,V12), r-{F}(V12,V0), P_s-{F}(V13,V12), r-{F}(V14,V0), r-{F}(V0,V15), r-{F}(V15,V0), P_s-{F}(V16,V15), r-{F}(V17,V0), r-{F}(V18,V0), r-{F}(V0,V19), r-{F}(V19,V0), P_s-{F}(V20,V19), r-{F}(V21,V1), P_s-{F}(V22,V1), P_s-{F}(V23,V19), P_s-{F}(V24,V12), P_s-{F}(V25,V15), r-{F}(V26,V0), P_s-{F}(V27,V26), r-{F}(V28,V0), P_s-{F}(V29,V28), r-{F}(V30,V0), P_s-{F}(V31,V30), P_s-{F}(V32,V33), V33 == V12, V33 == V0, V33 == V1, V33 == V21, P_s-{F}(V34,V33), P_s-{F}(V35,V34), P_s-{F}(V36,V33), P_s-{F}(V37,V36), P_s-{F}(V38,V39), V33 == V39, V39 == V0, V39 == V1, V39 == V3, P_s-{F}(V40,V39), P_s-{F}(V41,V40), P_s-{F}(V42,V43), V43 == V15, V43 == V0, V43 == V1, V43 == V33, P_s-{F}(V44,V43), P_s-{F}(V45,V44), P_s-{F}(V46,V43), P_s-{F}(V47,V46), P_s-{F}(V48,V49), V43 == V49, V49 == V0, V49 == V1, V49 == V6, P_s-{F}(V50,V49), P_s-{F}(V51,V50), P_s-{F}(V52,V53), V53 == V0, V53 == V1, V53 == V9, P_s-{F}(V54,V53), P_s-{F}(V55,V54), P_s-{F}(V56,V57), V0 == V57, V57 == V53, V57 == V1, V57 == V8, P_s-{F}(V58,V57), P_s-{F}(V59,V58), P_s-{F}(V60,V61), V33 == V61, V61 == V12, V61 == V0, V61 == V11, P_s-{F}(V62,V61), P_s-{F}(V63,V62), P_s-{F}(V64,V65), V43 == V65, V65 == V15, V65 == V0, V65 == V14, P_s-{F}(V66,V65), P_s-{F}(V67,V66), P_s-{F}(V68,V69), V69 == V19, V69 == V0, V69 == V18, P_s-{F}(V70,V69), P_s-{F}(V71,V70), P_s-{F}(V72,V73), V19 == V73, V73 == V69, V73 == V0, V73 == V17, P_s-{F}(V74,V73), P_s-{F}(V75,V74), P_s-{F}(V76,V77), V32 == V77, V38 == V77, V22 == V77, V42 == V77, V48 == V77, V23 == V77, V31 == V77, V52 == V77, V56 == V77, V24 == V77, V60 == V77, V27 == V77, V25 == V77, V64 == V77, V29 == V77, V68 == V77, V72 == V77, V35 == V77, V41 == V77, V76 == V77, V45 == V77, V51 == V77, V55 == V77, V59 == V77, V37 == V77, V63 == V77, V47 == V77, V67 == V77, V71 == V77, V75 == V77 | P_s-{T}(V77,V0), P_s-{T}(V77,V2), P_s-{T}(V77,V5), P_s-{T}(V77,V4), P_s-{T}(V77,V7), P_s-{T}(V77,V10), P_s-{T}(V77,V13), P_s-{T}(V77,V16), P_s-{T}(V77,V20)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #399: 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 == V21, V21 == V23, V23 == V24, V24 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V62, V62 == V63, V63 == V64, V64 == V66, V66 == V67, V67 == V68, V68 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V75, V75 == V76, V76 == V77, V77 == 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 == V17, V17 == V25, V25 == V29, V29 == V40, V40 == V19, V19 == V26, V26 == V22, V22 == V28, V28 == V32, V32 == V43, V18 == V42, V43 == V46, V42 == V45; #319 ), references = 1, size of lhs = 127:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V2,V0), r-{F}(V3,V0), r-{F}(V4,V0), r-{F}(V0,V5), r-{F}(V5,V0), P_s-{F}(V6,V5), P_s-{F}(V7,V5), r-{F}(V0,V8), r-{F}(V8,V0), P_s-{F}(V0,V8), r-{F}(V9,V8), r-{F}(V10,V8), r-{F}(V11,V8), r-{F}(V12,V8), r-{F}(V13,V8), P_s-{F}(V14,V8), P_s-{F}(V15,V8), P_s-{F}(V16,V8), r-{F}(V17,V0), P_s-{F}(V18,V17), r-{F}(V19,V0), P_s-{F}(V20,V19), r-{F}(V21,V0), P_s-{F}(V22,V21), P_s-{F}(V23,V24), V24 == V0, V24 == V8, V24 == V13, P_s-{F}(V25,V24), P_s-{F}(V26,V25), P_s-{F}(V27,V24), P_s-{F}(V28,V27), P_s-{F}(V29,V30), V24 == V30, V30 == V0, V30 == V8, V30 == V9, P_s-{F}(V31,V30), P_s-{F}(V32,V31), P_s-{F}(V33,V34), V34 == V0, V34 == V8, V34 == V24, P_s-{F}(V35,V34), P_s-{F}(V36,V35), P_s-{F}(V37,V34), P_s-{F}(V38,V37), P_s-{F}(V39,V40), V34 == V40, V40 == V0, V40 == V8, V40 == V10, P_s-{F}(V41,V40), P_s-{F}(V42,V41), P_s-{F}(V43,V44), V44 == V0, V44 == V8, V44 == V12, P_s-{F}(V45,V44), P_s-{F}(V46,V45), P_s-{F}(V47,V48), V0 == V48, V48 == V44, V48 == V8, V48 == V11, P_s-{F}(V49,V48), P_s-{F}(V50,V49), P_s-{F}(V51,V52), V24 == V52, V52 == V8, V52 == V0, V52 == V1, P_s-{F}(V53,V52), P_s-{F}(V54,V53), P_s-{F}(V55,V56), V34 == V56, V56 == V8, V56 == V0, V56 == V2, P_s-{F}(V57,V56), P_s-{F}(V58,V57), P_s-{F}(V59,V60), V60 == V5, V60 == V0, V60 == V4, P_s-{F}(V61,V60), P_s-{F}(V62,V61), P_s-{F}(V63,V64), V5 == V64, V64 == V60, V64 == V0, V64 == V3, P_s-{F}(V65,V64), P_s-{F}(V66,V65), P_s-{F}(V67,V68), V23 == V68, V29 == V68, V14 == V68, V33 == V68, V39 == V68, V7 == V68, V22 == V68, V43 == V68, V47 == V68, V15 == V68, V51 == V68, V18 == V68, V16 == V68, V55 == V68, V20 == V68, V59 == V68, V63 == V68, V26 == V68, V32 == V68, V67 == V68, V36 == V68, V42 == V68, V46 == V68, V50 == V68, V28 == V68, V54 == V68, V38 == V68, V58 == V68, V62 == V68, V66 == V68 | P_s-{T}(V68,V6)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #476: 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 == V1, V1 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83; #401 ), references = 1, size of lhs = 114:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V2,V0), r-{F}(V3,V0), r-{F}(V4,V0), P_s-{F}(V0,V5), V0 == V5, r-{F}(V5,V0), P_s-{F}(V6,V5), P_s-{F}(V7,V5), P_s-{F}(V8,V5), P_s-{F}(V9,V5), r-{F}(V10,V0), P_s-{F}(V11,V10), r-{F}(V12,V0), P_s-{F}(V13,V12), r-{F}(V14,V0), P_s-{F}(V15,V14), P_s-{F}(V16,V17), V17 == V5, V17 == V0, P_s-{F}(V18,V17), P_s-{F}(V19,V18), P_s-{F}(V20,V17), P_s-{F}(V21,V20), P_s-{F}(V22,V23), V17 == V23, V23 == V5, V23 == V0, P_s-{F}(V24,V23), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V27 == V0, V27 == V5, V27 == V17, P_s-{F}(V28,V27), P_s-{F}(V29,V28), P_s-{F}(V30,V27), P_s-{F}(V31,V30), P_s-{F}(V32,V33), V27 == V33, V33 == V5, V33 == V0, P_s-{F}(V34,V33), P_s-{F}(V35,V34), P_s-{F}(V36,V37), V37 == V5, V37 == V0, P_s-{F}(V38,V37), P_s-{F}(V39,V38), P_s-{F}(V40,V41), V41 == V37, V41 == V5, V41 == V0, P_s-{F}(V42,V41), P_s-{F}(V43,V42), P_s-{F}(V44,V45), V17 == V45, V45 == V5, V45 == V0, V45 == V1, P_s-{F}(V46,V45), P_s-{F}(V47,V46), P_s-{F}(V48,V49), V27 == V49, V49 == V5, V49 == V0, V49 == V2, P_s-{F}(V50,V49), P_s-{F}(V51,V50), P_s-{F}(V52,V53), V53 == V5, V53 == V0, V53 == V4, P_s-{F}(V54,V53), P_s-{F}(V55,V54), P_s-{F}(V56,V57), V5 == V57, V57 == V53, V57 == V0, V57 == V3, P_s-{F}(V58,V57), P_s-{F}(V59,V58), P_s-{F}(V60,V61), V16 == V61, V22 == V61, V6 == V61, V26 == V61, V32 == V61, V7 == V61, V15 == V61, V36 == V61, V40 == V61, V8 == V61, V44 == V61, V11 == V61, V9 == V61, V48 == V61, V13 == V61, V52 == V61, V56 == V61, V19 == V61, V25 == V61, V60 == V61, V29 == V61, V35 == V61, V39 == V61, V43 == V61, V21 == V61, V47 == V61, V31 == V61, V51 == V61, V55 == V61, V59 == V61 | b-{T}(V0,V5)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #479: mergings( V0 == V3; #477 ), references = 15, size of lhs = 4:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3 | b-{T}(V2,V3)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #489: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6; #484 ), references = 1, size of lhs = 16:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V2), b-{F}(V1,V4), r-{F}(V4,V5), b-{F}(V5,V6), b-{F}(V6,V5), r-{F}(V4,V7), b-{F}(V7,V5), b-{F}(V4,V8), b-{F}(V9,V8), r-{F}(V9,V2), r-{F}(V1,V10), b-{F}(V4,V10), #-{F} V11 | P_s-{T}(V11,V4), P_s-{T}(V11,V5), P_s-{T}(V11,V7), P_s-{T}(V11,V1), P_s-{T}(V11,V2), P_s-{T}(V11,V9), P_s-{T}(V11,V10)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #501: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V16, V16 == V9, V9 == V18, V18 == V5, V5 == V20, V20 == V22; #490 ), references = 1, size of lhs = 24:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), b-{F}(V2,V3), b-{F}(V3,V2), b-{F}(V0,V4), r-{F}(V4,V0), r-{F}(V4,V5), b-{F}(V5,V0), b-{F}(V4,V6), r-{F}(V0,V7), b-{F}(V4,V7), P_s-{F}(V8,V4), P_s-{F}(V9,V5), P_s-{F}(V10,V2), b-{F}(V11,V6), r-{F}(V11,V2), P_s-{F}(V12,V11), #-{F} V13, V8 == V13, V9 == V13, V10 == V13, V12 == V13 | P_s-{T}(V13,V7)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #524: 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 == V20, V20 == V21; #507 ), references = 6, size of lhs = 19:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V5), V1 == V5, V5 == V0, P_s-{F}(V6,V5), P_s-{F}(V7,V8), V0 == V8, V8 == V5, V8 == V1, #-{F} V9, V2 == V9, V4 == V9, V6 == V9, V3 == V9, V7 == V9 | b-{T}(V1,V5)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #531: mergings( V0 == V3, V3 == V4, V4 == V5; #527 ), references = 6, size of lhs = 10:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V1,V3), b-{F}(V3,V4), b-{F}(V4,V2), b-{F}(V4,V5), V5 == V1, V5 == V3, b-{F}(V3,V6), b-{F}(V6,V5) | r-{T}(V3,V5)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #646: 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 == 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 == V95, V95 == V96, V96 == V97, V97 == V99, V99 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V113; #546 ), references = 1, size of lhs = 64:
% 57.87/58.05 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), r-{F}(V8,V0), r-{F}(V9,V0), r-{F}(V10,V0), r-{F}(V11,V0), P_s-{F}(V12,V1), P_s-{F}(V13,V1), r-{F}(V14,V0), P_s-{F}(V15,V14), r-{F}(V16,V0), P_s-{F}(V17,V16), r-{F}(V18,V0), P_s-{F}(V19,V18), P_s-{F}(V20,V21), V21 == V1, V21 == V0, P_s-{F}(V22,V21), P_s-{F}(V23,V22), P_s-{F}(V24,V21), P_s-{F}(V25,V24), P_s-{F}(V26,V27), P_s-{F}(V28,V27), P_s-{F}(V29,V27), P_s-{F}(V30,V27), P_s-{F}(V31,V27), P_s-{F}(V32,V27), P_s-{F}(V33,V34), V34 == V1, V34 == V0, P_s-{F}(V35,V34), P_s-{F}(V36,V35), P_s-{F}(V37,V38), V38 == V1, V38 == V0, P_s-{F}(V39,V38), P_s-{F}(V40,V39), P_s-{F}(V41,V42), V42 == V1, V42 == V0, V42 == V9, P_s-{F}(V43,V42), P_s-{F}(V44,V43), P_s-{F}(V45,V46), V46 == V1, V46 == V0, V46 == V11, P_s-{F}(V47,V46), P_s-{F}(V48,V47), P_s-{F}(V49,V50), V50 == V1, V50 == V0, P_s-{F}(V51,V50), P_s-{F}(V52,V53), V0 == V53, V53 == V1 | P_s-{T}(V27,V21), P_s-{T}(V27,V1), P_s-{T}(V27,V0), P_s-{T}(V27,V34), P_s-{T}(V27,V38), P_s-{T}(V27,V8), P_s-{T}(V27,V42), P_s-{T}(V27,V46), P_s-{T}(V27,V10), P_s-{T}(V27,V20), P_s-{T}(V27,V27), P_s-{T}(V27,V2), P_s-{T}(V27,V33), P_s-{T}(V27,V3), P_s-{T}(V27,V19), P_s-{T}(V27,V37), P_s-{T}(V27,V4), P_s-{T}(V27,V15), P_s-{T}(V27,V5), P_s-{T}(V27,V41), P_s-{T}(V27,V17), P_s-{T}(V27,V45), P_s-{T}(V27,V23), P_s-{T}(V27,V26), P_s-{T}(V27,V28), P_s-{T}(V27,V36), P_s-{T}(V27,V40), P_s-{T}(V27,V30), P_s-{T}(V27,V25), P_s-{T}(V27,V31), P_s-{T}(V27,V29), P_s-{T}(V27,V44), P_s-{T}(V27,V48), P_s-{T}(V27,V32), P_s-{T}(V27,V50), P_s-{T}(V27,V53), P_s-{T}(V27,V6), P_s-{T}(V27,V49), P_s-{T}(V27,V51), P_s-{T}(V27,V7), P_s-{T}(V27,V12), P_s-{T}(V27,V13), P_s-{T}(V27,V52)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #745: 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 == 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 == V95, V95 == V96, V96 == V97, V97 == V99, V99 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V113; #547 ), references = 1, size of lhs = 64:
% 57.87/58.05 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), r-{F}(V8,V0), r-{F}(V9,V0), r-{F}(V10,V0), r-{F}(V11,V0), P_s-{F}(V12,V1), P_s-{F}(V13,V1), r-{F}(V14,V0), P_s-{F}(V15,V14), r-{F}(V16,V0), P_s-{F}(V17,V16), r-{F}(V18,V0), P_s-{F}(V19,V18), P_s-{F}(V20,V21), V21 == V1, V21 == V0, P_s-{F}(V22,V21), P_s-{F}(V23,V22), P_s-{F}(V24,V21), P_s-{F}(V25,V24), P_s-{F}(V26,V27), P_s-{F}(V28,V27), P_s-{F}(V29,V27), P_s-{F}(V30,V27), P_s-{F}(V31,V27), P_s-{F}(V32,V27), P_s-{F}(V33,V34), V34 == V1, V34 == V0, P_s-{F}(V35,V34), P_s-{F}(V36,V35), P_s-{F}(V37,V38), V38 == V1, V38 == V0, P_s-{F}(V39,V38), P_s-{F}(V40,V39), P_s-{F}(V41,V42), V42 == V1, V42 == V0, V42 == V9, P_s-{F}(V43,V42), P_s-{F}(V44,V43), P_s-{F}(V45,V46), V46 == V1, V46 == V0, V46 == V11, P_s-{F}(V47,V46), P_s-{F}(V48,V47), P_s-{F}(V49,V50), V50 == V1, V50 == V0, P_s-{F}(V51,V50), P_s-{F}(V52,V53), V0 == V53, V53 == V1 | P_s-{T}(V27,V21), P_s-{T}(V27,V1), P_s-{T}(V27,V0), P_s-{T}(V27,V34), P_s-{T}(V27,V38), P_s-{T}(V27,V8), P_s-{T}(V27,V42), P_s-{T}(V27,V46), P_s-{T}(V27,V10), P_s-{T}(V27,V20), P_s-{T}(V27,V27), P_s-{T}(V27,V2), P_s-{T}(V27,V33), P_s-{T}(V27,V3), P_s-{T}(V27,V19), P_s-{T}(V27,V37), P_s-{T}(V27,V4), P_s-{T}(V27,V15), P_s-{T}(V27,V5), P_s-{T}(V27,V41), P_s-{T}(V27,V17), P_s-{T}(V27,V45), P_s-{T}(V27,V23), P_s-{T}(V27,V26), P_s-{T}(V27,V28), P_s-{T}(V27,V36), P_s-{T}(V27,V40), P_s-{T}(V27,V30), P_s-{T}(V27,V25), P_s-{T}(V27,V31), P_s-{T}(V27,V29), P_s-{T}(V27,V44), P_s-{T}(V27,V48), P_s-{T}(V27,V32), P_s-{T}(V27,V50), P_s-{T}(V27,V53), P_s-{T}(V27,V6), P_s-{T}(V27,V49), P_s-{T}(V27,V51), P_s-{T}(V27,V7), P_s-{T}(V27,V12), P_s-{T}(V27,V13), P_s-{T}(V27,V52)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #870: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == 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 == 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 == V93, V93 == V94, V94 == V95, V95 == V97, V97 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == V152, V152 == V154, V154 == V156, V156 == V158, V158 == V160, V160 == V162, V162 == V164, V164 == V166, V166 == V168, V168 == V170, V170 == V172, V172 == V174, V174 == V176, V176 == V178, V178 == V180, V180 == V182, V182 == V184, V184 == V186, V186 == V188, V188 == V190, V190 == V192, V192 == V194, V194 == V196, V196 == V198, V198 == V200; #746 ), references = 1, size of lhs = 114:
% 57.87/58.05 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), r-{F}(V8,V0), r-{F}(V9,V0), P_s-{F}(V10,V1), P_s-{F}(V11,V1), P_s-{F}(V12,V1), r-{F}(V13,V0), P_s-{F}(V14,V13), r-{F}(V15,V0), P_s-{F}(V16,V15), r-{F}(V17,V0), P_s-{F}(V18,V17), r-{F}(V19,V0), P_s-{F}(V20,V19), r-{F}(V21,V0), P_s-{F}(V22,V21), P_s-{F}(V23,V24), P_s-{F}(V24,V25), V25 == V1, V25 == V0, P_s-{F}(V26,V25), P_s-{F}(V27,V25), P_s-{F}(V28,V27), P_s-{F}(V29,V25), P_s-{F}(V30,V29), P_s-{F}(V31,V32), P_s-{F}(V32,V33), V33 == V1, V33 == V0, P_s-{F}(V34,V33), P_s-{F}(V35,V33), P_s-{F}(V36,V35), P_s-{F}(V37,V38), P_s-{F}(V38,V39), V39 == V1, V39 == V0, P_s-{F}(V40,V39), P_s-{F}(V41,V39), P_s-{F}(V42,V41), P_s-{F}(V43,V44), P_s-{F}(V44,V45), V45 == V1, V45 == V0, V45 == V8, P_s-{F}(V46,V45), P_s-{F}(V47,V45), P_s-{F}(V48,V47), P_s-{F}(V49,V50), P_s-{F}(V50,V51), V51 == V1, V51 == V0, V51 == V9, P_s-{F}(V52,V51), P_s-{F}(V53,V51), P_s-{F}(V54,V53), P_s-{F}(V55,V56), V26 == V56, V12 == V56, V34 == V56, V40 == V56, V14 == V56, V46 == V56, V52 == V56, V16 == V56, V28 == V56, V55 == V56, V36 == V56, V42 == V56, V48 == V56, V54 == V56, P_s-{F}(V57,V56), P_s-{F}(V58,V57), V58 == V56, P_s-{F}(V59,V56), P_s-{F}(V60,V59), V60 == V56, P_s-{F}(V61,V56), P_s-{F}(V62,V61), V62 == V56, P_s-{F}(V63,V56), P_s-{F}(V64,V63), V64 == V56, P_s-{F}(V65,V56), P_s-{F}(V66,V65), V66 == V56, P_s-{F}(V67,V56), P_s-{F}(V68,V67), V68 == V56, P_s-{F}(V69,V70), V70 == V1, V70 == V0, V69 == V56, P_s-{F}(V71,V70), P_s-{F}(V72,V71), V72 == V56, P_s-{F}(V73,V70), P_s-{F}(V74,V73), V74 == V56, P_s-{F}(V75,V76), V0 == V76, V76 == V1, V75 == V56, P_s-{F}(V77,V76), P_s-{F}(V78,V77), V78 == V56 | P_s-{T}(V56,V0), P_s-{T}(V56,V2), P_s-{T}(V56,V3), P_s-{T}(V56,V22), P_s-{T}(V56,V4), P_s-{T}(V56,V18), P_s-{T}(V56,V5), P_s-{T}(V56,V20), P_s-{T}(V56,V23), P_s-{T}(V56,V31), P_s-{T}(V56,V37), P_s-{T}(V56,V30), P_s-{T}(V56,V43), P_s-{T}(V56,V49), P_s-{T}(V56,V6), P_s-{T}(V56,V7), P_s-{T}(V56,V10), P_s-{T}(V56,V11)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1024: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == 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 == 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 == V93, V93 == V94, V94 == V95, V95 == V97, V97 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == 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 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V133, V133 == V134, V134 == V135, V135 == V70, V70 == V71, V71 == V145, V69 == V144, V145 == V72, V72 == V141, V144 == V140, V141 == V73, V73 == V143, V140 == V142, V143 == V146, V142 == V147, V146 == V154, V147 == V155, V148 == V156, V154 == V160, V155 == V161, V156 == V162, V160 == V153, V161 == V152, V153 == V166, V152 == V167, V162 == V168, V166 == V172, V167 == V173, V168 == V174, V172 == V92, V92 == V96, V96 == V100; #871 ), references = 1, size of lhs = 82:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V2,V0), P_s-{F}(V0,V3), V0 == V3, r-{F}(V3,V0), P_s-{F}(V4,V3), P_s-{F}(V5,V3), P_s-{F}(V3,V6), V6 == V1, V6 == V3, V6 == V0, V6 == V2, P_s-{F}(V7,V6), P_s-{F}(V8,V6), P_s-{F}(V9,V6), P_s-{F}(V10,V6), P_s-{F}(V11,V6), r-{F}(V12,V0), P_s-{F}(V13,V12), r-{F}(V14,V0), P_s-{F}(V15,V14), P_s-{F}(V16,V6), P_s-{F}(V17,V16), P_s-{F}(V18,V6), P_s-{F}(V19,V18), P_s-{F}(V20,V6), P_s-{F}(V21,V20), P_s-{F}(V22,V6), P_s-{F}(V23,V22), P_s-{F}(V24,V6), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V7 == V27, V5 == V27, V8 == V27, V9 == V27, V13 == V27, V10 == V27, V11 == V27, V15 == V27, V17 == V27, V26 == V27, V19 == V27, V21 == V27, V23 == V27, V25 == V27, P_s-{F}(V28,V27), P_s-{F}(V29,V28), V29 == V27, P_s-{F}(V30,V27), P_s-{F}(V31,V30), V31 == V27, P_s-{F}(V32,V27), P_s-{F}(V33,V32), V33 == V27, P_s-{F}(V34,V27), P_s-{F}(V35,V34), V35 == V27, P_s-{F}(V36,V27), P_s-{F}(V37,V36), V37 == V27, P_s-{F}(V38,V27), P_s-{F}(V39,V38), V39 == V27, P_s-{F}(V40,V41), V41 == V3, V41 == V0, V40 == V27, P_s-{F}(V42,V41), P_s-{F}(V43,V42), V43 == V27, P_s-{F}(V44,V41), P_s-{F}(V45,V44), V45 == V27, P_s-{F}(V46,V47), V0 == V47, V47 == V3, V46 == V27, P_s-{F}(V48,V47), P_s-{F}(V49,V48), V49 == V27 | P_s-{T}(V27,V4)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1178: 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 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V2, V2 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == 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 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V133, V133 == V134, V1 == V135, V134 == V138, V135 == V139, V136 == V140, V138 == V142, V139 == V143, V140 == V144, V142 == V146, V143 == V147, V146 == V148, V147 == V149, V144 == V150, V148 == V152, V149 == V153, V150 == V154, V152 == V156, V156 == V157, V157 == V158, V158 == V159; #1026 ), references = 2, size of lhs = 74:
% 57.87/58.05 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, P_s-{F}(V2,V1), P_s-{F}(V1,V3), V3 == V0, V3 == V1, P_s-{F}(V4,V3), P_s-{F}(V5,V3), P_s-{F}(V6,V3), P_s-{F}(V7,V3), P_s-{F}(V8,V3), P_s-{F}(V9,V1), P_s-{F}(V10,V1), P_s-{F}(V11,V3), P_s-{F}(V12,V11), P_s-{F}(V13,V3), P_s-{F}(V14,V13), P_s-{F}(V15,V3), P_s-{F}(V16,V15), P_s-{F}(V17,V3), P_s-{F}(V18,V17), P_s-{F}(V19,V3), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V4 == V22, V2 == V22, V5 == V22, V6 == V22, V9 == V22, V7 == V22, V8 == V22, V10 == V22, V12 == V22, V21 == V22, V14 == V22, V16 == V22, V18 == V22, V20 == V22, P_s-{F}(V23,V22), P_s-{F}(V24,V23), V24 == V22, P_s-{F}(V25,V22), P_s-{F}(V26,V25), V26 == V22, P_s-{F}(V27,V22), P_s-{F}(V28,V27), V28 == V22, P_s-{F}(V29,V22), P_s-{F}(V30,V29), V30 == V22, P_s-{F}(V31,V22), P_s-{F}(V32,V31), V32 == V22, P_s-{F}(V33,V22), P_s-{F}(V34,V33), V34 == V22, P_s-{F}(V35,V36), V36 == V1, V36 == V0, V35 == V22, P_s-{F}(V37,V36), P_s-{F}(V38,V37), V38 == V22, P_s-{F}(V39,V36), P_s-{F}(V40,V39), V40 == V22, P_s-{F}(V41,V42), V0 == V42, V42 == V1, V41 == V22, P_s-{F}(V43,V42), P_s-{F}(V44,V43), V44 == V22 | b-{T}(V1,V0)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1181: mergings( V0 == V3; #1179 ), references = 1, size of lhs = 7:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V3,V2), V3 == V1, b-{F}(V1,V4), b-{F}(V2,V5), b-{F}(V5,V4) | r-{T}(V3,V1)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1188: mergings( V0 == V3, V3 == V4, V4 == V5; #1184 ), references = 2, size of lhs = 11:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V2,V1), b-{F}(V1,V3), r-{F}(V2,V3), b-{F}(V3,V4), b-{F}(V4,V3), #-{F} V5, V5 == V1, V5 == V2, V5 == V3 | r-{T}(V1,V5)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1206: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12; #1195 ), references = 1, size of lhs = 25:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V2,V1), b-{F}(V1,V3), r-{F}(V2,V3), r-{F}(V1,V4), b-{F}(V4,V5), V3 == V5, r-{F}(V5,V4), b-{F}(V5,V3), r-{F}(V5,V6), b-{F}(V6,V5), r-{F}(V6,V3), #-{F} V7, V7 == V1, V7 == V2, V7 == V3, V7 == V4, V7 == V5, #-{F} V8, V8 == V5, V8 == V6, V8 == V3, V7 == V8, V8 == V4 | r-{T}(V3,V5)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1230: 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 == V1, V1 == V22, V22 == V23; #1213 ), references = 1, size of lhs = 59:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V0), r-{F}(V1,V2), V2 == V0, P_s-{F}(V3,V2), P_s-{F}(V4,V2), P_s-{F}(V5,V2), P_s-{F}(V6,V2), r-{F}(V0,V7), V2 == V7, V7 == V0, r-{F}(V0,V8), b-{F}(V8,V9), b-{F}(V7,V9), P_s-{F}(V10,V7), P_s-{F}(V11,V7), r-{F}(V0,V12), b-{F}(V12,V0), r-{F}(V0,V13), b-{F}(V13,V0), r-{F}(V13,V2), P_s-{F}(V14,V15), V15 == V2, V15 == V0, V7 == V15, V15 == V8, P_s-{F}(V16,V15), P_s-{F}(V17,V18), V0 == V18, V18 == V15, V18 == V2, P_s-{F}(V19,V20), V0 == V20, V20 == V7, V20 == V2, #-{F} V21, V21 == V13, V21 == V2, V21 == V12, V21 == V0, #-{F} V22, V22 == V0, V22 == V1, V22 == V2, V21 == V22, V22 == V12, #-{F} V23, V3 == V23, V14 == V23, V16 == V23, V4 == V23, V17 == V23, #-{F} V24, V5 == V24, V10 == V24, V11 == V24, V6 == V24, V19 == V24 | r-{T}(V0,V2)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1250: 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 == V23, V23 == V24, V24 == V32; #1232 ), references = 1, size of lhs = 33:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V0), r-{F}(V1,V2), V2 == V0, P_s-{F}(V3,V2), P_s-{F}(V4,V2), P_s-{F}(V5,V2), P_s-{F}(V6,V2), r-{F}(V0,V7), V2 == V7, V7 == V0, r-{F}(V0,V8), b-{F}(V8,V9), b-{F}(V7,V9), P_s-{F}(V10,V7), P_s-{F}(V11,V7), r-{F}(V0,V12), b-{F}(V12,V0), r-{F}(V0,V13), b-{F}(V13,V0), r-{F}(V13,V2), r-{F}(V0,V14), r-{F}(V14,V2), P_s-{F}(V15,V16), V0 == V16, V16 == V2, #-{F} V17, #-{F} V18, V18 == V0, V18 == V1, V18 == V2, V18 == V12 | P_s-{T}(V17,V2), P_s-{T}(V17,V0), P_s-{T}(V17,V7), P_s-{T}(V17,V8), P_s-{T}(V17,V16), P_s-{T}(V17,V13), P_s-{T}(V17,V12), P_s-{T}(V17,V18), P_s-{T}(V17,V3), P_s-{T}(V17,V17), P_s-{T}(V17,V4), P_s-{T}(V17,V15), P_s-{T}(V17,V5), P_s-{T}(V17,V10), P_s-{T}(V17,V11), P_s-{T}(V17,V6)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1283: 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 == V21, V21 == V22, V22 == V30, V30 == V36, V36 == V14, V14 == V38, V38 == V40, V40 == V42, V42 == V44, V44 == V46, V46 == V48, V48 == V50, V50 == V52, V52 == V54, V54 == V56, V56 == V58, V58 == V26, V26 == V27; #1251 ), references = 2, size of lhs = 54:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V0), r-{F}(V1,V2), V2 == V0, P_s-{F}(V3,V2), r-{F}(V0,V4), V2 == V4, V4 == V0, P_s-{F}(V0,V4), r-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V4,V6), r-{F}(V0,V7), b-{F}(V7,V0), r-{F}(V0,V8), b-{F}(V8,V0), r-{F}(V8,V2), r-{F}(V0,V9), r-{F}(V9,V2), P_s-{F}(V10,V2), P_s-{F}(V11,V4), P_s-{F}(V12,V5), P_s-{F}(V13,V8), P_s-{F}(V14,V7), P_s-{F}(V15,V2), P_s-{F}(V16,V15), P_s-{F}(V17,V2), P_s-{F}(V18,V17), P_s-{F}(V19,V2), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V0 == V22, V22 == V2, P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V26 == V0, V26 == V1, V26 == V2, V26 == V7, P_s-{F}(V27,V28), V10 == V28, V11 == V28, V12 == V28, V21 == V28, V13 == V28, V14 == V28, V25 == V28, V16 == V28, V27 == V28, V18 == V28, V24 == V28, V20 == V28 | P_s-{T}(V28,V3)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1319: 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 == V27, V27 == V29, V29 == V31, V31 == V32, V32 == V34, V34 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44; #1285 ), references = 2, size of lhs = 51:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, P_s-{F}(V0,V1), r-{F}(V0,V2), b-{F}(V2,V3), b-{F}(V1,V3), r-{F}(V0,V4), b-{F}(V4,V0), r-{F}(V0,V5), b-{F}(V5,V0), P_s-{F}(V6,V1), P_s-{F}(V7,V2), P_s-{F}(V8,V5), P_s-{F}(V9,V4), P_s-{F}(V10,V11), V5 == V11, V11 == V0, V11 == V1, P_s-{F}(V12,V11), P_s-{F}(V13,V12), P_s-{F}(V14,V11), P_s-{F}(V15,V14), P_s-{F}(V16,V11), P_s-{F}(V17,V16), P_s-{F}(V18,V11), P_s-{F}(V19,V18), P_s-{F}(V20,V21), V0 == V21, V21 == V11, P_s-{F}(V22,V21), P_s-{F}(V23,V22), P_s-{F}(V24,V25), V25 == V0, V25 == V5, V25 == V11, V25 == V4, P_s-{F}(V26,V27), V10 == V27, V6 == V27, V7 == V27, V20 == V27, V8 == V27, V9 == V27, V24 == V27, V15 == V27, V26 == V27, V17 == V27, V23 == V27, V19 == V27, V13 == V27 | b-{T}(V5,V11)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1329: mergings( V0 == V3, V3 == V4, V4 == V5; #1324 ), references = 2, size of lhs = 9:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V3 == V2, b-{F}(V4,V3), b-{F}(V4,V2), r-{F}(V2,V5), V3 == V5, b-{F}(V5,V3) | r-{T}(V2,V3)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1333: mergings( V0 == V3, V3 == V4, V4 == V15; #1325 ), references = 1, size of lhs = 54:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, P_s-{F}(V0,V1), r-{F}(V0,V2), b-{F}(V2,V3), b-{F}(V1,V3), r-{F}(V0,V4), b-{F}(V4,V0), r-{F}(V0,V5), b-{F}(V5,V0), b-{F}(V5,V6), r-{F}(V6,V5), P_s-{F}(V7,V1), P_s-{F}(V8,V2), P_s-{F}(V9,V5), P_s-{F}(V10,V4), P_s-{F}(V11,V12), V12 == V6, V12 == V5, V12 == V0, V12 == V1, P_s-{F}(V13,V12), P_s-{F}(V14,V13), P_s-{F}(V15,V12), P_s-{F}(V16,V15), P_s-{F}(V17,V12), P_s-{F}(V18,V17), P_s-{F}(V19,V12), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V0 == V22, V22 == V12, P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V26 == V0, V26 == V5, V26 == V12, V26 == V4, P_s-{F}(V27,V28), V11 == V28, V7 == V28, V8 == V28, V21 == V28, V9 == V28, V10 == V28, V25 == V28, V16 == V28, V27 == V28, V18 == V28, V24 == V28, V20 == V28, V14 == V28 | r-{T}(V6,V12)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1384: 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 == V27, V27 == V29, V29 == V31, V31 == V32, V32 == V34, V34 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V22 == V46, V45 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62; #1340 ), references = 1, size of lhs = 56:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V2), r-{F}(V0,V3), b-{F}(V3,V0), r-{F}(V0,V4), b-{F}(V4,V0), P_s-{F}(V5,V1), P_s-{F}(V6,V4), P_s-{F}(V7,V3), r-{F}(V0,V8), V8 == V0, b-{F}(V8,V2), P_s-{F}(V0,V8), P_s-{F}(V9,V8), r-{F}(V0,V10), b-{F}(V10,V11), b-{F}(V8,V11), r-{F}(V0,V12), b-{F}(V12,V0), r-{F}(V0,V13), b-{F}(V13,V0), P_s-{F}(V14,V8), P_s-{F}(V15,V10), P_s-{F}(V16,V13), P_s-{F}(V17,V12), b-{F}(V13,V18), r-{F}(V18,V13), b-{F}(V4,V18), r-{F}(V18,V4), P_s-{F}(V19,V20), V20 == V0, V20 == V8, V20 == V18, V20 == V4, P_s-{F}(V21,V20), P_s-{F}(V22,V21), P_s-{F}(V23,V20), P_s-{F}(V24,V23), P_s-{F}(V25,V20), P_s-{F}(V26,V25), P_s-{F}(V27,V20), P_s-{F}(V28,V27), P_s-{F}(V29,V30), P_s-{F}(V31,V30), P_s-{F}(V32,V30), P_s-{F}(V33,V30), P_s-{F}(V34,V30), P_s-{F}(V35,V36), V0 == V36, P_s-{F}(V37,V36), P_s-{F}(V38,V37), P_s-{F}(V39,V40), V40 == V0, V40 == V13, V40 == V12 | P_s-{T}(V30,V0), P_s-{T}(V30,V20), P_s-{T}(V30,V4), P_s-{T}(V30,V3), P_s-{T}(V30,V19), P_s-{T}(V30,V9), P_s-{T}(V30,V5), P_s-{T}(V30,V30), P_s-{T}(V30,V6), P_s-{T}(V30,V7), P_s-{T}(V30,V24), P_s-{T}(V30,V26), P_s-{T}(V30,V29), P_s-{T}(V30,V28), P_s-{T}(V30,V22), P_s-{T}(V30,V8), P_s-{T}(V30,V18), P_s-{T}(V30,V13), P_s-{T}(V30,V36), P_s-{T}(V30,V40), P_s-{T}(V30,V14), P_s-{T}(V30,V15), P_s-{T}(V30,V35), P_s-{T}(V30,V16), P_s-{T}(V30,V17), P_s-{T}(V30,V39), P_s-{T}(V30,V32), P_s-{T}(V30,V33), P_s-{T}(V30,V38), P_s-{T}(V30,V34), P_s-{T}(V30,V31)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1445: 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 == V25, V25 == V27, V27 == V29, V29 == V30, V30 == V32, V32 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V20 == V44, V43 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V84, V84 == V86, V86 == V88, V88 == V90, V90 == V92, V92 == V94, V94 == V96, V96 == V98, V98 == V100, V100 == V102, V102 == V104, V104 == V106, V106 == V108, V108 == V110, V110 == V112, V112 == V114; #1385 ), references = 1, size of lhs = 88:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V2), r-{F}(V0,V3), b-{F}(V3,V0), r-{F}(V0,V4), b-{F}(V4,V0), P_s-{F}(V5,V1), P_s-{F}(V6,V4), P_s-{F}(V7,V3), r-{F}(V0,V8), V8 == V0, b-{F}(V8,V2), P_s-{F}(V0,V8), P_s-{F}(V9,V8), r-{F}(V0,V10), b-{F}(V10,V11), b-{F}(V8,V11), r-{F}(V0,V12), b-{F}(V12,V0), r-{F}(V0,V13), b-{F}(V13,V0), P_s-{F}(V14,V8), P_s-{F}(V15,V10), P_s-{F}(V16,V13), P_s-{F}(V17,V12), b-{F}(V13,V18), r-{F}(V18,V13), b-{F}(V4,V18), r-{F}(V18,V4), P_s-{F}(V19,V4), P_s-{F}(V20,V3), P_s-{F}(V21,V8), P_s-{F}(V22,V13), P_s-{F}(V23,V24), P_s-{F}(V24,V25), V25 == V0, V25 == V8, V25 == V18, V25 == V4, P_s-{F}(V26,V25), P_s-{F}(V27,V25), P_s-{F}(V28,V27), P_s-{F}(V29,V25), P_s-{F}(V30,V29), P_s-{F}(V31,V25), P_s-{F}(V32,V31), P_s-{F}(V33,V25), P_s-{F}(V34,V33), P_s-{F}(V35,V36), P_s-{F}(V36,V37), V0 == V37, P_s-{F}(V38,V37), P_s-{F}(V39,V37), P_s-{F}(V40,V39), P_s-{F}(V41,V42), V26 == V42, V19 == V42, V20 == V42, V28 == V42, V41 == V42, V21 == V42, V22 == V42, V38 == V42, V40 == V42, P_s-{F}(V43,V42), P_s-{F}(V44,V43), V44 == V42, P_s-{F}(V45,V42), P_s-{F}(V46,V45), V46 == V42, P_s-{F}(V47,V42), P_s-{F}(V48,V47), V48 == V42, P_s-{F}(V49,V42), P_s-{F}(V50,V49), V50 == V42, P_s-{F}(V51,V42), P_s-{F}(V52,V51), V52 == V42, P_s-{F}(V53,V54), V54 == V0, V54 == V13, V54 == V12, V53 == V42, P_s-{F}(V55,V54), P_s-{F}(V56,V55), V56 == V42 | P_s-{T}(V42,V0), P_s-{T}(V42,V9), P_s-{T}(V42,V5), P_s-{T}(V42,V6), P_s-{T}(V42,V7), P_s-{T}(V42,V30), P_s-{T}(V42,V32), P_s-{T}(V42,V34), P_s-{T}(V42,V23), P_s-{T}(V42,V18), P_s-{T}(V42,V14), P_s-{T}(V42,V15), P_s-{T}(V42,V16), P_s-{T}(V42,V17), P_s-{T}(V42,V35)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1529: 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 == V25, V25 == V27, V27 == V29, V29 == V30, V30 == V32, V32 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V62, V62 == V63, V63 == V65, V65 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V72, V72 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V19, V19 == V61, V61 == V43, V20 == V44, V43 == V26, V26 == V28, V44 == V21, V28 == V31, V21 == V24, V31 == V33, V24 == V23, V33 == V89, V23 == V88, V89 == V91, V88 == V90, V91 == V93, V90 == V92, V93 == V82, V92 == V83, V82 == V49, V49 == V50, V83 == V45, V50 == V51, V45 == V48, V51 == V52, V48 == V47; #1446 ), references = 1, size of lhs = 55:
% 57.87/58.05 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), P_s-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V1,V3), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), P_s-{F}(V1,V8), V8 == V0, V8 == V1, P_s-{F}(V9,V8), P_s-{F}(V10,V8), P_s-{F}(V11,V10), P_s-{F}(V12,V13), P_s-{F}(V13,V14), V0 == V14, P_s-{F}(V15,V14), P_s-{F}(V16,V14), P_s-{F}(V17,V16), P_s-{F}(V18,V19), V9 == V19, V4 == V19, V5 == V19, V11 == V19, V18 == V19, V6 == V19, V7 == V19, V15 == V19, V17 == V19, P_s-{F}(V20,V19), P_s-{F}(V21,V20), V21 == V19, P_s-{F}(V22,V19), P_s-{F}(V23,V22), V23 == V19, P_s-{F}(V24,V19), P_s-{F}(V25,V24), V25 == V19, P_s-{F}(V26,V19), P_s-{F}(V27,V26), V27 == V19, P_s-{F}(V28,V19), P_s-{F}(V29,V28), V29 == V19, P_s-{F}(V30,V31), V31 == V0, V31 == V1, V30 == V19, P_s-{F}(V32,V31), P_s-{F}(V33,V32), V33 == V19 | P_s-{T}(V19,V12)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1609: 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 == 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 == V1, V1 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V2 == V71, V70 == V74, V71 == V75, V74 == V76, V75 == V77, V76 == V78, V77 == V79, V78 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V79 == V85, V72 == V86; #1531 ), references = 2, size of lhs = 51:
% 57.87/58.05 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), b-{F}(V1,V2), b-{F}(V1,V3), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), P_s-{F}(V1,V8), V8 == V1, V0 == V8, P_s-{F}(V9,V8), P_s-{F}(V10,V8), P_s-{F}(V11,V8), P_s-{F}(V12,V11), P_s-{F}(V13,V8), P_s-{F}(V14,V13), P_s-{F}(V15,V16), V9 == V16, V4 == V16, V5 == V16, V12 == V16, V15 == V16, V6 == V16, V7 == V16, V10 == V16, V14 == V16, P_s-{F}(V17,V16), P_s-{F}(V18,V17), V18 == V16, P_s-{F}(V19,V16), P_s-{F}(V20,V19), V20 == V16, P_s-{F}(V21,V16), P_s-{F}(V22,V21), V22 == V16, P_s-{F}(V23,V16), P_s-{F}(V24,V23), V24 == V16, P_s-{F}(V25,V16), P_s-{F}(V26,V25), V26 == V16, P_s-{F}(V27,V28), V28 == V0, V28 == V1, V27 == V16, P_s-{F}(V29,V28), P_s-{F}(V30,V29), V30 == V16 | b-{T}(V0,V1)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1614: mergings( V0 == V2, V2 == V5; #1611 ), references = 1, size of lhs = 23:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V3,V1), b-{F}(V4,V1), b-{F}(V4,V5), V1 == V5, V5 == V0, P_s-{F}(V6,V5), P_s-{F}(V7,V5), b-{F}(V5,V8), b-{F}(V8,V5), P_s-{F}(V9,V10), V0 == V10, V10 == V5, V10 == V1, #-{F} V11, V2 == V11, V6 == V11, V7 == V11, V3 == V11, V9 == V11 | b-{T}(V1,V0)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1634: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V15, V15 == V16, V16 == V17; #1624 ), references = 3, size of lhs = 52:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V2,V1), r-{F}(V3,V1), b-{F}(V3,V0), b-{F}(V0,V4), b-{F}(V4,V0), r-{F}(V3,V5), b-{F}(V5,V0), b-{F}(V0,V6), b-{F}(V6,V0), P_s-{F}(V7,V8), V3 == V8, V8 == V1, V8 == V0, V8 == V5, P_s-{F}(V9,V8), P_s-{F}(V10,V11), V3 == V11, V11 == V5, V11 == V8, V11 == V0, P_s-{F}(V12,V11), P_s-{F}(V13,V14), V11 == V14, V14 == V8, V14 == V0, P_s-{F}(V15,V16), V16 == V11, V16 == V14, V16 == V8, V16 == V0, P_s-{F}(V17,V18), V11 == V18, V18 == V0, V18 == V8, P_s-{F}(V19,V20), V20 == V11, V20 == V18, V20 == V0, V20 == V8, #-{F} V21, V10 == V21, V7 == V21, V13 == V21, V15 == V21, #-{F} V22, V12 == V22, V9 == V22, V17 == V22, V19 == V22 | b-{T}(V3,V8)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1654: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V1, V1 == V23, V23 == V24, V24 == V25; #1644 ), references = 3, size of lhs = 137:
% 57.87/58.05 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}(V5,V6), b-{F}(V6,V5), b-{F}(V5,V7), b-{F}(V7,V5), b-{F}(V5,V8), b-{F}(V8,V5), b-{F}(V5,V9), b-{F}(V9,V5), b-{F}(V0,V10), V10 == V0, P_s-{F}(V11,V10), P_s-{F}(V12,V10), b-{F}(V10,V13), b-{F}(V13,V10), b-{F}(V5,V14), b-{F}(V14,V5), P_s-{F}(V15,V16), V16 == V0, V16 == V5, V16 == V10, P_s-{F}(V17,V16), P_s-{F}(V18,V19), V0 == V19, V19 == V10, V19 == V16, P_s-{F}(V20,V21), V0 == V21, V21 == V5, V21 == V16, P_s-{F}(V22,V21), P_s-{F}(V23,V21), P_s-{F}(V24,V25), V16 == V25, V25 == V5, V25 == V21, V25 == V0, P_s-{F}(V26,V25), P_s-{F}(V27,V28), V25 == V28, V28 == V21, V28 == V0, P_s-{F}(V29,V30), V30 == V25, V30 == V28, V30 == V21, V30 == V0, P_s-{F}(V31,V32), V25 == V32, V32 == V0, V32 == V21, P_s-{F}(V33,V34), V34 == V25, V34 == V32, V34 == V0, V34 == V21, P_s-{F}(V35,V36), V0 == V36, V36 == V21, V36 == V5, V36 == V16, P_s-{F}(V37,V36), P_s-{F}(V38,V36), P_s-{F}(V39,V40), V16 == V40, V40 == V5, V40 == V36, V40 == V0, P_s-{F}(V41,V40), P_s-{F}(V42,V43), V40 == V43, V43 == V36, V43 == V0, P_s-{F}(V44,V45), V45 == V40, V45 == V43, V45 == V36, V45 == V0, P_s-{F}(V46,V47), V40 == V47, V47 == V0, V47 == V36, P_s-{F}(V48,V49), V49 == V40, V49 == V47, V49 == V0, V49 == V36, P_s-{F}(V50,V51), V36 == V51, V51 == V0, V51 == V21, P_s-{F}(V52,V53), V53 == V36, V53 == V51, V53 == V0, V53 == V21, #-{F} V54, V15 == V54, V11 == V54, V12 == V54, V17 == V54, V18 == V54, #-{F} V55, V24 == V55, V20 == V55, V27 == V55, V29 == V55, #-{F} V56, V26 == V56, V22 == V56, V31 == V56, V33 == V56, #-{F} V57, V39 == V57, V35 == V57, V42 == V57, V44 == V57, #-{F} V58, V41 == V58, V37 == V58, V46 == V58, V48 == V58, #-{F} V59, V38 == V59, V23 == V59, V50 == V59, V52 == V59 | r-{T}(V0,V16)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1675: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V55, V55 == V56, V56 == V57; #1661 ), references = 1, size of lhs = 252:
% 57.87/58.05 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}(V5,V6), b-{F}(V6,V5), b-{F}(V5,V7), b-{F}(V7,V5), b-{F}(V5,V8), b-{F}(V8,V5), b-{F}(V5,V9), b-{F}(V9,V5), b-{F}(V0,V10), V10 == V0, P_s-{F}(V11,V10), P_s-{F}(V12,V10), b-{F}(V10,V13), b-{F}(V13,V10), b-{F}(V5,V14), b-{F}(V14,V5), b-{F}(V0,V15), b-{F}(V15,V0), b-{F}(V0,V16), b-{F}(V16,V0), b-{F}(V0,V17), b-{F}(V17,V0), b-{F}(V0,V18), b-{F}(V18,V0), b-{F}(V0,V19), b-{F}(V19,V0), b-{F}(V19,V20), b-{F}(V20,V19), b-{F}(V19,V21), b-{F}(V21,V19), b-{F}(V19,V22), b-{F}(V22,V19), b-{F}(V19,V23), b-{F}(V23,V19), b-{F}(V0,V24), V24 == V0, P_s-{F}(V25,V24), P_s-{F}(V26,V24), b-{F}(V24,V27), b-{F}(V27,V24), b-{F}(V19,V28), b-{F}(V28,V19), b-{F}(V0,V29), b-{F}(V29,V0), b-{F}(V0,V30), b-{F}(V30,V0), b-{F}(V0,V31), b-{F}(V31,V0), b-{F}(V0,V32), b-{F}(V32,V0), b-{F}(V0,V33), b-{F}(V33,V0), b-{F}(V33,V34), b-{F}(V34,V33), b-{F}(V33,V35), b-{F}(V35,V33), b-{F}(V33,V36), b-{F}(V36,V33), b-{F}(V33,V37), b-{F}(V37,V33), b-{F}(V0,V38), V38 == V0, P_s-{F}(V39,V38), P_s-{F}(V40,V38), b-{F}(V38,V41), b-{F}(V41,V38), b-{F}(V33,V42), b-{F}(V42,V33), P_s-{F}(V43,V44), V44 == V0, V44 == V5, V44 == V10, P_s-{F}(V45,V44), P_s-{F}(V46,V47), V0 == V47, V47 == V10, V47 == V44, P_s-{F}(V48,V49), V0 == V49, V49 == V5, V49 == V44, P_s-{F}(V50,V49), P_s-{F}(V51,V49), P_s-{F}(V52,V53), V53 == V49, V53 == V0, P_s-{F}(V54,V55), V55 == V53, V55 == V49, V55 == V0, P_s-{F}(V56,V57), V57 == V0, V57 == V49, P_s-{F}(V58,V59), V59 == V57, V59 == V0, V59 == V49, P_s-{F}(V60,V61), V44 == V61, V61 == V5, V61 == V0, P_s-{F}(V62,V61), P_s-{F}(V63,V64), V61 == V64, V64 == V0, P_s-{F}(V65,V66), V66 == V61, V66 == V64, V66 == V0, P_s-{F}(V67,V68), V61 == V68, V68 == V0, P_s-{F}(V69,V70), V70 == V61, V70 == V68, V70 == V0, P_s-{F}(V71,V72), V72 == V0, V72 == V49, P_s-{F}(V73,V74), V74 == V72, V74 == V0, V74 == V49, P_s-{F}(V75,V76), V76 == V0, V76 == V19, V76 == V24, V76 == V44, P_s-{F}(V77,V76), P_s-{F}(V78,V79), V0 == V79, V79 == V24, V79 == V76, P_s-{F}(V80,V81), V0 == V81, V81 == V19, V81 == V76, P_s-{F}(V82,V81), P_s-{F}(V83,V81), P_s-{F}(V84,V85), V85 == V81, V85 == V0, P_s-{F}(V86,V87), V87 == V85, V87 == V81, V87 == V0, P_s-{F}(V88,V89), V89 == V0, V89 == V81, P_s-{F}(V90,V91), V91 == V89, V91 == V0, V91 == V81, P_s-{F}(V92,V93), V76 == V93, V93 == V19, V93 == V0, P_s-{F}(V94,V93), P_s-{F}(V95,V96), V93 == V96, V96 == V0, P_s-{F}(V97,V98), V98 == V93, V98 == V96, V98 == V0, P_s-{F}(V99,V100), V93 == V100, V100 == V0, P_s-{F}(V101,V102), V102 == V93, V102 == V100, V102 == V0, P_s-{F}(V103,V104), V104 == V0, V104 == V81, P_s-{F}(V105,V106), V106 == V104, V106 == V0, V106 == V81, P_s-{F}(V107,V108), V0 == V108, V108 == V38, P_s-{F}(V109,V110), V0 == V110, V110 == V33, P_s-{F}(V111,V110), P_s-{F}(V112,V110), P_s-{F}(V113,V114), V114 == V33, V114 == V110, V114 == V0, P_s-{F}(V115,V114), P_s-{F}(V116,V117), V117 == V114, V117 == V110, V117 == V0, P_s-{F}(V118,V119), V119 == V114, V119 == V0, V119 == V110, P_s-{F}(V120,V121), V0 == V121, V121 == V110, V121 == V33, P_s-{F}(V122,V121), P_s-{F}(V123,V121), P_s-{F}(V124,V125), V125 == V33, V125 == V121, V125 == V0, P_s-{F}(V126,V125), P_s-{F}(V127,V128), V128 == V125, V128 == V121, V128 == V0, P_s-{F}(V129,V130), V130 == V125, V130 == V0, V130 == V121, P_s-{F}(V131,V132), V132 == V121, V132 == V0, V132 == V110, #-{F} V133, #-{F} V134, V43 == V134, V11 == V134, V12 == V134, V45 == V134, V46 == V134, #-{F} V135, V75 == V135, V25 == V135, V26 == V135, V77 == V135, V78 == V135, #-{F} V136, V39 == V136, V40 == V136, V133 == V136, V107 == V136 | P_s-{T}(V133,V44), P_s-{T}(V133,V5), P_s-{T}(V133,V49), P_s-{T}(V133,V0), P_s-{T}(V133,V53), P_s-{T}(V133,V55), P_s-{T}(V133,V57), P_s-{T}(V133,V59), P_s-{T}(V133,V61), P_s-{T}(V133,V64), P_s-{T}(V133,V66), P_s-{T}(V133,V68), P_s-{T}(V133,V70), P_s-{T}(V133,V72), P_s-{T}(V133,V74), P_s-{T}(V133,V76), P_s-{T}(V133,V19), P_s-{T}(V133,V81), P_s-{T}(V133,V85), P_s-{T}(V133,V87), P_s-{T}(V133,V89), P_s-{T}(V133,V91), P_s-{T}(V133,V93), P_s-{T}(V133,V96), P_s-{T}(V133,V98), P_s-{T}(V133,V100), P_s-{T}(V133,V102), P_s-{T}(V133,V104), P_s-{T}(V133,V106), P_s-{T}(V133,V33), P_s-{T}(V133,V38), P_s-{T}(V133,V108), P_s-{T}(V133,V110), P_s-{T}(V133,V114), P_s-{T}(V133,V117), P_s-{T}(V133,V119), P_s-{T}(V133,V121), P_s-{T}(V133,V125), P_s-{T}(V133,V128), P_s-{T}(V133,V130), P_s-{T}(V133,V132), P_s-{T}(V133,V133), P_s-{T}(V133,V48), P_s-{T}(V133,V52), P_s-{T}(V133,V54), P_s-{T}(V133,V50), P_s-{T}(V133,V56), P_s-{T}(V133,V58), P_s-{T}(V133,V60), P_s-{T}(V133,V63), P_s-{T}(V133,V65), P_s-{T}(V133,V62), P_s-{T}(V133,V67), P_s-{T}(V133,V69), P_s-{T}(V133,V51), P_s-{T}(V133,V71), P_s-{T}(V133,V73), P_s-{T}(V133,V80), P_s-{T}(V133,V84), P_s-{T}(V133,V86), P_s-{T}(V133,V82), P_s-{T}(V133,V88), P_s-{T}(V133,V90), P_s-{T}(V133,V92), P_s-{T}(V133,V95), P_s-{T}(V133,V97), P_s-{T}(V133,V94), P_s-{T}(V133,V99), P_s-{T}(V133,V101), P_s-{T}(V133,V83), P_s-{T}(V133,V103), P_s-{T}(V133,V105), P_s-{T}(V133,V113), P_s-{T}(V133,V109), P_s-{T}(V133,V116), P_s-{T}(V133,V115), P_s-{T}(V133,V111), P_s-{T}(V133,V118), P_s-{T}(V133,V124), P_s-{T}(V133,V120), P_s-{T}(V133,V127), P_s-{T}(V133,V126), P_s-{T}(V133,V122), P_s-{T}(V133,V129), P_s-{T}(V133,V123), P_s-{T}(V133,V112), P_s-{T}(V133,V131)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1761: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V53, V53 == V54, V54 == V55, V55 == V150, V150 == V152, V152 == V154, V154 == V156, V156 == V158, V158 == V160, V160 == V162, V162 == V164, V164 == V166, V166 == V168, V168 == V170, V170 == V172, V172 == V174, V174 == V176, V176 == V178, V178 == V180, V180 == V182, V182 == V184, V184 == V186, V186 == V188, V188 == V190, V190 == V192, V192 == V194, V194 == V196, V196 == V198, V198 == V200, V200 == V202, V202 == V204, V204 == V206, V206 == V208, V208 == V210, V210 == V212, V212 == V214, V214 == V216, V216 == V218, V218 == V220, V220 == V222, V222 == V224, V224 == V226, V226 == V228, V228 == V230, V230 == V232, V232 == V234, V234 == V236, V236 == V238, V238 == V240, V240 == V242, V242 == V244, V244 == V246, V246 == V248, V248 == V250, V250 == V252, V252 == V254, V254 == V256, V256 == V258, V258 == V260, V260 == V262, V262 == V264, V264 == V266, V266 == V268, V268 == V270, V270 == V272, V272 == V274, V274 == V276, V276 == V278, V278 == V280, V280 == V282, V282 == V284, V284 == V286, V286 == V288, V288 == V290; #1676 ), references = 1, size of lhs = 393:
% 57.87/58.05 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}(V5,V6), b-{F}(V6,V5), b-{F}(V5,V7), b-{F}(V7,V5), b-{F}(V5,V8), b-{F}(V8,V5), b-{F}(V5,V9), b-{F}(V9,V5), b-{F}(V0,V10), V10 == V0, P_s-{F}(V11,V10), P_s-{F}(V12,V10), b-{F}(V10,V13), b-{F}(V13,V10), b-{F}(V5,V14), b-{F}(V14,V5), b-{F}(V0,V15), b-{F}(V15,V0), b-{F}(V0,V16), b-{F}(V16,V0), b-{F}(V0,V17), b-{F}(V17,V0), b-{F}(V0,V18), b-{F}(V18,V0), b-{F}(V0,V19), b-{F}(V19,V0), b-{F}(V19,V20), b-{F}(V20,V19), b-{F}(V19,V21), b-{F}(V21,V19), b-{F}(V19,V22), b-{F}(V22,V19), b-{F}(V19,V23), b-{F}(V23,V19), b-{F}(V0,V24), V24 == V0, P_s-{F}(V25,V24), P_s-{F}(V26,V24), b-{F}(V24,V27), b-{F}(V27,V24), b-{F}(V19,V28), b-{F}(V28,V19), b-{F}(V0,V29), b-{F}(V29,V0), b-{F}(V0,V30), b-{F}(V30,V0), b-{F}(V0,V31), b-{F}(V31,V0), b-{F}(V0,V32), b-{F}(V32,V0), b-{F}(V0,V33), b-{F}(V33,V0), b-{F}(V33,V34), b-{F}(V34,V33), b-{F}(V33,V35), b-{F}(V35,V33), b-{F}(V33,V36), b-{F}(V36,V33), b-{F}(V33,V37), b-{F}(V37,V33), b-{F}(V0,V38), V38 == V0, P_s-{F}(V39,V38), P_s-{F}(V40,V38), b-{F}(V38,V41), b-{F}(V41,V38), b-{F}(V33,V42), b-{F}(V42,V33), P_s-{F}(V43,V5), P_s-{F}(V44,V19), P_s-{F}(V45,V33), P_s-{F}(V46,V38), P_s-{F}(V47,V48), V48 == V0, V48 == V5, V48 == V10, P_s-{F}(V49,V48), P_s-{F}(V50,V48), P_s-{F}(V51,V52), V0 == V52, V52 == V10, V52 == V48, P_s-{F}(V53,V54), V54 == V0, P_s-{F}(V55,V54), P_s-{F}(V56,V57), V57 == V0, P_s-{F}(V58,V57), P_s-{F}(V59,V60), V60 == V0, P_s-{F}(V61,V60), P_s-{F}(V62,V63), V63 == V0, P_s-{F}(V64,V63), P_s-{F}(V65,V66), V66 == V0, P_s-{F}(V67,V66), P_s-{F}(V68,V69), V69 == V0, V69 == V19, V69 == V24, V69 == V48, P_s-{F}(V70,V69), P_s-{F}(V71,V69), P_s-{F}(V72,V73), V0 == V73, V73 == V24, V73 == V69, P_s-{F}(V74,V75), V75 == V0, P_s-{F}(V76,V75), P_s-{F}(V77,V78), V78 == V0, P_s-{F}(V79,V78), P_s-{F}(V80,V81), V81 == V0, P_s-{F}(V82,V81), P_s-{F}(V83,V84), V84 == V0, P_s-{F}(V85,V84), P_s-{F}(V86,V87), V87 == V0, P_s-{F}(V88,V87), P_s-{F}(V89,V90), V0 == V90, V90 == V38, P_s-{F}(V91,V90), P_s-{F}(V92,V93), V93 == V0, P_s-{F}(V94,V93), P_s-{F}(V95,V96), V96 == V0, P_s-{F}(V97,V96), P_s-{F}(V98,V99), V99 == V0, P_s-{F}(V100,V99), P_s-{F}(V101,V102), V102 == V0, P_s-{F}(V103,V102), P_s-{F}(V104,V105), V105 == V0, P_s-{F}(V106,V105), P_s-{F}(V107,V108), V0 == V108, V108 == V5, V108 == V48, V54 == V108, V57 == V108, V66 == V108, P_s-{F}(V109,V108), P_s-{F}(V110,V109), P_s-{F}(V111,V108), P_s-{F}(V112,V111), P_s-{F}(V113,V108), P_s-{F}(V114,V113), P_s-{F}(V115,V116), V116 == V108, V116 == V0, V54 == V116, P_s-{F}(V117,V116), P_s-{F}(V118,V117), P_s-{F}(V119,V120), V120 == V0, V120 == V108, V57 == V120, P_s-{F}(V121,V120), P_s-{F}(V122,V121), P_s-{F}(V123,V124), V48 == V124, V124 == V5, V124 == V0, V60 == V124, V63 == V124, P_s-{F}(V125,V124), P_s-{F}(V126,V125), P_s-{F}(V127,V124), P_s-{F}(V128,V127), P_s-{F}(V129,V130), V124 == V130, V130 == V0, V60 == V130, P_s-{F}(V131,V130), P_s-{F}(V132,V131), P_s-{F}(V133,V134), V124 == V134, V134 == V0, V63 == V134, P_s-{F}(V135,V134), P_s-{F}(V136,V135), P_s-{F}(V137,V138), V138 == V0, V138 == V108, V66 == V138, P_s-{F}(V139,V138), P_s-{F}(V140,V139), P_s-{F}(V141,V142), V0 == V142, V142 == V19, V142 == V69, V75 == V142, V78 == V142, V87 == V142, P_s-{F}(V143,V142), P_s-{F}(V144,V143), P_s-{F}(V145,V142), P_s-{F}(V146,V145), P_s-{F}(V147,V142), P_s-{F}(V148,V147), P_s-{F}(V149,V150), V150 == V142, V150 == V0, V75 == V150, P_s-{F}(V151,V150), P_s-{F}(V152,V151), P_s-{F}(V153,V154), V154 == V0, V154 == V142, V78 == V154, P_s-{F}(V155,V154), P_s-{F}(V156,V155), P_s-{F}(V157,V158), V69 == V158, V158 == V19, V158 == V0, V81 == V158, V84 == V158, P_s-{F}(V159,V158), P_s-{F}(V160,V159), P_s-{F}(V161,V158), P_s-{F}(V162,V161), P_s-{F}(V163,V164), V158 == V164, V164 == V0, V81 == V164, P_s-{F}(V165,V164), P_s-{F}(V166,V165), P_s-{F}(V167,V168), V158 == V168, V168 == V0, V84 == V168, P_s-{F}(V169,V168), P_s-{F}(V170,V169), P_s-{F}(V171,V172), V172 == V0, V172 == V142, V87 == V172, P_s-{F}(V173,V172), P_s-{F}(V174,V173), P_s-{F}(V175,V176), V0 == V176, V176 == V33, V93 == V176, V96 == V176, V105 == V176, P_s-{F}(V177,V176), P_s-{F}(V178,V177), P_s-{F}(V179,V176), P_s-{F}(V180,V179), P_s-{F}(V181,V176), P_s-{F}(V182,V181), P_s-{F}(V183,V184), V184 == V33, V184 == V176, V184 == V0, V93 == V184, V96 == V184, P_s-{F}(V185,V184), P_s-{F}(V186,V185), P_s-{F}(V187,V184), P_s-{F}(V188,V187), P_s-{F}(V189,V190), V0 == V190, V190 == V176, V190 == V33, V99 == V190, V102 == V190, V105 == V190, P_s-{F}(V191,V190), P_s-{F}(V192,V191), P_s-{F}(V193,V190), P_s-{F}(V194,V193), P_s-{F}(V195,V190), P_s-{F}(V196,V195), P_s-{F}(V197,V198), V198 == V33, V198 == V190, V198 == V0, V99 == V198, V102 == V198, P_s-{F}(V199,V198), P_s-{F}(V200,V199), P_s-{F}(V201,V198), P_s-{F}(V202,V201), P_s-{F}(V203,V204), V50 == V204, V43 == V204, V107 == V204, V115 == V204, V55 == V204, V119 == V204, V58 == V204, V123 == V204, V129 == V204, V61 == V204, V133 == V204, V64 == V204, V137 == V204, V67 == V204, V71 == V204, V44 == V204, V141 == V204, V149 == V204, V76 == V204, V153 == V204, V79 == V204, V157 == V204, V163 == V204, V82 == V204, V167 == V204, V85 == V204, V171 == V204, V88 == V204, V45 == V204, V46 == V204, V91 == V204, V175 == V204, V183 == V204, V94 == V204, V97 == V204, V189 == V204, V197 == V204, V100 == V204, V103 == V204, V106 == V204, V203 == V204, V110 == V204, V118 == V204, V112 == V204, V122 == V204, V126 == V204, V132 == V204, V128 == V204, V136 == V204, V114 == V204, V140 == V204, V144 == V204, V152 == V204, V146 == V204, V156 == V204, V160 == V204, V166 == V204, V162 == V204, V170 == V204, V148 == V204, V174 == V204, V186 == V204, V178 == V204, V188 == V204, V180 == V204, V200 == V204, V192 == V204, V202 == V204, V194 == V204, V196 == V204, V182 == V204, #-{F} V205, V47 == V205, V11 == V205, V12 == V205, V49 == V205, V51 == V205, #-{F} V206, V68 == V206, V25 == V206, V26 == V206, V70 == V206, V72 == V206, #-{F} V207, V39 == V207, V40 == V207, V204 == V207, V89 == V207 | P_s-{T}(V204,V0), P_s-{T}(V204,V53), P_s-{T}(V204,V56), P_s-{T}(V204,V59), P_s-{T}(V204,V62), P_s-{T}(V204,V65), P_s-{T}(V204,V74), P_s-{T}(V204,V77), P_s-{T}(V204,V80), P_s-{T}(V204,V83), P_s-{T}(V204,V86), P_s-{T}(V204,V92), P_s-{T}(V204,V95), P_s-{T}(V204,V98), P_s-{T}(V204,V101), P_s-{T}(V204,V104)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1874: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == 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 == 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 == V88, V88 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, 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 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V10, V10 == V137, V137 == V140, V138 == V141, V140 == V143, V141 == V144, V143 == V146, V144 == V147, V146 == V149, V147 == V150, V149 == V158, V150 == V159, V158 == V161, V159 == V162, V161 == V164, V162 == V165, V164 == V167, V165 == V168, V167 == V170, V168 == V171, V170 == V176, V171 == V177, V176 == V179, V177 == V180, V179 == V182, V180 == V183, V182 == V185, V183 == V186; #1762 ), references = 1, size of lhs = 357:
% 57.87/58.05 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}(V5,V6), b-{F}(V6,V5), b-{F}(V5,V7), b-{F}(V7,V5), b-{F}(V5,V8), b-{F}(V8,V5), b-{F}(V5,V9), b-{F}(V9,V5), b-{F}(V0,V10), V10 == V0, P_s-{F}(V11,V10), P_s-{F}(V12,V10), b-{F}(V10,V13), b-{F}(V13,V10), b-{F}(V5,V14), b-{F}(V14,V5), b-{F}(V0,V15), b-{F}(V15,V0), b-{F}(V0,V16), b-{F}(V16,V0), b-{F}(V0,V17), b-{F}(V17,V0), b-{F}(V0,V18), b-{F}(V18,V0), b-{F}(V0,V19), b-{F}(V19,V0), b-{F}(V19,V20), b-{F}(V20,V19), b-{F}(V19,V21), b-{F}(V21,V19), b-{F}(V19,V22), b-{F}(V22,V19), b-{F}(V19,V23), b-{F}(V23,V19), b-{F}(V0,V24), V24 == V0, P_s-{F}(V25,V24), P_s-{F}(V26,V24), b-{F}(V24,V27), b-{F}(V27,V24), b-{F}(V19,V28), b-{F}(V28,V19), b-{F}(V0,V29), b-{F}(V29,V0), b-{F}(V0,V30), b-{F}(V30,V0), b-{F}(V0,V31), b-{F}(V31,V0), b-{F}(V0,V32), b-{F}(V32,V0), b-{F}(V0,V33), b-{F}(V33,V0), b-{F}(V33,V34), b-{F}(V34,V33), b-{F}(V33,V35), b-{F}(V35,V33), b-{F}(V33,V36), b-{F}(V36,V33), b-{F}(V33,V37), b-{F}(V37,V33), b-{F}(V0,V38), V38 == V0, P_s-{F}(V39,V38), P_s-{F}(V40,V38), b-{F}(V38,V41), b-{F}(V41,V38), b-{F}(V33,V42), b-{F}(V42,V33), P_s-{F}(V43,V5), P_s-{F}(V44,V19), P_s-{F}(V45,V33), P_s-{F}(V46,V38), P_s-{F}(V0,V47), V47 == V0, P_s-{F}(V48,V47), P_s-{F}(V49,V47), P_s-{F}(V50,V47), P_s-{F}(V51,V47), P_s-{F}(V52,V47), P_s-{F}(V53,V47), P_s-{F}(V54,V47), P_s-{F}(V55,V47), P_s-{F}(V56,V47), P_s-{F}(V57,V47), P_s-{F}(V58,V47), P_s-{F}(V59,V47), P_s-{F}(V60,V47), P_s-{F}(V61,V47), P_s-{F}(V62,V63), V63 == V0, V63 == V5, V63 == V10, P_s-{F}(V64,V63), P_s-{F}(V65,V63), P_s-{F}(V66,V67), V0 == V67, V67 == V10, V67 == V63, P_s-{F}(V68,V69), V69 == V0, V69 == V19, V69 == V24, V69 == V63, P_s-{F}(V70,V69), P_s-{F}(V71,V69), P_s-{F}(V72,V73), V0 == V73, V73 == V24, V73 == V69, P_s-{F}(V74,V75), V0 == V75, V75 == V38, P_s-{F}(V76,V75), P_s-{F}(V77,V78), V78 == V0, P_s-{F}(V79,V78), P_s-{F}(V80,V81), V0 == V81, V81 == V5, V81 == V63, V47 == V81, P_s-{F}(V82,V81), P_s-{F}(V83,V82), P_s-{F}(V84,V81), P_s-{F}(V85,V84), P_s-{F}(V86,V81), P_s-{F}(V87,V86), P_s-{F}(V88,V89), V89 == V81, V89 == V0, V47 == V89, P_s-{F}(V90,V89), P_s-{F}(V91,V90), P_s-{F}(V92,V93), V93 == V0, V93 == V81, V47 == V93, P_s-{F}(V94,V93), P_s-{F}(V95,V94), P_s-{F}(V96,V97), V63 == V97, V97 == V5, V97 == V0, V47 == V97, P_s-{F}(V98,V97), P_s-{F}(V99,V98), P_s-{F}(V100,V97), P_s-{F}(V101,V100), P_s-{F}(V102,V103), V97 == V103, V103 == V0, V47 == V103, P_s-{F}(V104,V103), P_s-{F}(V105,V104), P_s-{F}(V106,V107), V97 == V107, V107 == V0, V47 == V107, P_s-{F}(V108,V107), P_s-{F}(V109,V108), P_s-{F}(V110,V111), V111 == V0, V111 == V81, V47 == V111, P_s-{F}(V112,V111), P_s-{F}(V113,V112), P_s-{F}(V114,V115), V0 == V115, V115 == V19, V115 == V69, V47 == V115, P_s-{F}(V116,V115), P_s-{F}(V117,V116), P_s-{F}(V118,V115), P_s-{F}(V119,V118), P_s-{F}(V120,V115), P_s-{F}(V121,V120), P_s-{F}(V122,V123), V123 == V115, V123 == V0, V47 == V123, P_s-{F}(V124,V123), P_s-{F}(V125,V124), P_s-{F}(V126,V127), V127 == V0, V127 == V115, V47 == V127, P_s-{F}(V128,V127), P_s-{F}(V129,V128), P_s-{F}(V130,V131), V69 == V131, V131 == V19, V131 == V0, V47 == V131, P_s-{F}(V132,V131), P_s-{F}(V133,V132), P_s-{F}(V134,V131), P_s-{F}(V135,V134), P_s-{F}(V136,V137), V131 == V137, V137 == V0, V47 == V137, P_s-{F}(V138,V137), P_s-{F}(V139,V138), P_s-{F}(V140,V141), V131 == V141, V141 == V0, V47 == V141, P_s-{F}(V142,V141), P_s-{F}(V143,V142), P_s-{F}(V144,V145), V145 == V0, V145 == V115, V47 == V145, P_s-{F}(V146,V145), P_s-{F}(V147,V146), P_s-{F}(V148,V149), V0 == V149, V149 == V33, V47 == V149, V78 == V149, P_s-{F}(V150,V149), P_s-{F}(V151,V150), P_s-{F}(V152,V149), P_s-{F}(V153,V152), P_s-{F}(V154,V149), P_s-{F}(V155,V154), P_s-{F}(V156,V157), V157 == V33, V157 == V149, V157 == V0, V47 == V157, P_s-{F}(V158,V157), P_s-{F}(V159,V158), P_s-{F}(V160,V157), P_s-{F}(V161,V160), P_s-{F}(V162,V163), V0 == V163, V163 == V149, V163 == V33, V47 == V163, V78 == V163, P_s-{F}(V164,V163), P_s-{F}(V165,V164), P_s-{F}(V166,V163), P_s-{F}(V167,V166), P_s-{F}(V168,V163), P_s-{F}(V169,V168), P_s-{F}(V170,V171), V171 == V33, V171 == V163, V171 == V0, V47 == V171, P_s-{F}(V172,V171), P_s-{F}(V173,V172), P_s-{F}(V174,V171), P_s-{F}(V175,V174), P_s-{F}(V176,V177), V65 == V177, V43 == V177, V80 == V177, V88 == V177, V48 == V177, V92 == V177, V49 == V177, V96 == V177, V102 == V177, V50 == V177, V106 == V177, V51 == V177, V110 == V177, V52 == V177, V71 == V177, V44 == V177, V114 == V177, V122 == V177, V53 == V177, V126 == V177, V54 == V177, V130 == V177, V136 == V177, V55 == V177, V140 == V177, V56 == V177, V144 == V177, V57 == V177, V45 == V177, V46 == V177, V76 == V177, V148 == V177, V156 == V177, V58 == V177, V59 == V177, V162 == V177, V170 == V177, V60 == V177, V61 == V177, V79 == V177, V176 == V177, V83 == V177, V91 == V177, V85 == V177, V95 == V177, V99 == V177, V105 == V177, V101 == V177, V109 == V177, V87 == V177, V113 == V177, V117 == V177, V125 == V177, V119 == V177, V129 == V177, V133 == V177, V139 == V177, V135 == V177, V143 == V177, V121 == V177, V147 == V177, V159 == V177, V151 == V177, V161 == V177, V153 == V177, V173 == V177, V165 == V177, V175 == V177, V167 == V177, V169 == V177, V155 == V177, #-{F} V178, V62 == V178, V11 == V178, V12 == V178, V64 == V178, V66 == V178, #-{F} V179, V68 == V179, V25 == V179, V26 == V179, V70 == V179, V72 == V179, #-{F} V180, V39 == V180, V40 == V180, V177 == V180, V74 == V180 | P_s-{T}(V177,V77)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #1990: 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 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V133, V133 == V136, V134 == V137, V136 == V139, V137 == V140, V139 == V142, V140 == V143, V142 == V145, V143 == V146, V145 == V148, V146 == V149, V148 == V151, V149 == V152, V151 == V154, V152 == V155, V154 == V157, V155 == V158, V157 == V160, V158 == V161, V160 == V163, V161 == V164, V163 == V166, V164 == V167, V166 == V169, V167 == V170, V169 == V172, V170 == V173, V172 == V175, V173 == V176; #1876 ), references = 1, size of lhs = 193:
% 57.87/58.05 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}(V5,V6), b-{F}(V6,V5), b-{F}(V5,V7), b-{F}(V7,V5), b-{F}(V5,V8), b-{F}(V8,V5), b-{F}(V5,V9), b-{F}(V9,V5), b-{F}(V0,V10), V10 == V0, P_s-{F}(V11,V10), P_s-{F}(V12,V10), b-{F}(V10,V13), b-{F}(V13,V10), b-{F}(V5,V14), b-{F}(V14,V5), b-{F}(V0,V15), b-{F}(V15,V0), b-{F}(V0,V16), b-{F}(V16,V0), b-{F}(V0,V17), b-{F}(V17,V0), b-{F}(V0,V18), b-{F}(V18,V0), b-{F}(V0,V19), b-{F}(V19,V0), b-{F}(V19,V20), b-{F}(V20,V19), b-{F}(V19,V21), b-{F}(V21,V19), b-{F}(V19,V22), b-{F}(V22,V19), b-{F}(V19,V23), b-{F}(V23,V19), b-{F}(V0,V24), V24 == V0, P_s-{F}(V25,V24), P_s-{F}(V26,V24), b-{F}(V24,V27), b-{F}(V27,V24), b-{F}(V19,V28), b-{F}(V28,V19), b-{F}(V0,V29), b-{F}(V29,V0), b-{F}(V0,V30), b-{F}(V30,V0), b-{F}(V0,V31), b-{F}(V31,V0), b-{F}(V0,V32), b-{F}(V32,V0), b-{F}(V0,V33), b-{F}(V33,V0), b-{F}(V33,V34), b-{F}(V34,V33), b-{F}(V33,V35), b-{F}(V35,V33), b-{F}(V33,V36), b-{F}(V36,V33), b-{F}(V33,V37), b-{F}(V37,V33), b-{F}(V0,V38), V38 == V0, P_s-{F}(V39,V38), P_s-{F}(V40,V38), b-{F}(V38,V41), b-{F}(V41,V38), b-{F}(V33,V42), b-{F}(V42,V33), P_s-{F}(V43,V5), P_s-{F}(V44,V19), P_s-{F}(V45,V33), P_s-{F}(V46,V38), P_s-{F}(V0,V47), V47 == V0, P_s-{F}(V48,V47), P_s-{F}(V49,V47), P_s-{F}(V50,V47), P_s-{F}(V51,V47), P_s-{F}(V52,V47), P_s-{F}(V53,V47), P_s-{F}(V54,V47), P_s-{F}(V55,V47), P_s-{F}(V56,V47), P_s-{F}(V57,V47), P_s-{F}(V58,V47), P_s-{F}(V59,V47), P_s-{F}(V60,V47), P_s-{F}(V61,V47), P_s-{F}(V62,V47), P_s-{F}(V63,V64), V64 == V0, V64 == V5, V64 == V10, P_s-{F}(V65,V64), P_s-{F}(V66,V64), P_s-{F}(V67,V68), V0 == V68, V68 == V24, P_s-{F}(V69,V70), V0 == V70, V70 == V38, P_s-{F}(V71,V70), P_s-{F}(V72,V73), P_s-{F}(V74,V73), P_s-{F}(V75,V73), P_s-{F}(V76,V73), P_s-{F}(V77,V73), P_s-{F}(V78,V73), P_s-{F}(V79,V73), P_s-{F}(V80,V73), P_s-{F}(V81,V73), P_s-{F}(V82,V73), P_s-{F}(V83,V73), P_s-{F}(V84,V73), P_s-{F}(V85,V73), P_s-{F}(V86,V73), P_s-{F}(V87,V73), P_s-{F}(V88,V89), V89 == V0, V47 == V89, P_s-{F}(V90,V89), P_s-{F}(V91,V90), P_s-{F}(V92,V93), V93 == V0, V47 == V93, P_s-{F}(V94,V93), P_s-{F}(V95,V94), P_s-{F}(V96,V97), V97 == V0, V47 == V97, P_s-{F}(V98,V97), P_s-{F}(V99,V98), P_s-{F}(V100,V101), V101 == V0, V47 == V101, P_s-{F}(V102,V101), P_s-{F}(V103,V102), P_s-{F}(V104,V105), V105 == V0, V47 == V105, P_s-{F}(V106,V105), P_s-{F}(V107,V106), P_s-{F}(V108,V109), V0 == V109, V109 == V19, V47 == V109, P_s-{F}(V110,V109), P_s-{F}(V111,V110), P_s-{F}(V112,V109), P_s-{F}(V113,V112), P_s-{F}(V114,V109), P_s-{F}(V115,V114), P_s-{F}(V116,V117), V117 == V19, V117 == V0, V47 == V117, P_s-{F}(V118,V117), P_s-{F}(V119,V118), P_s-{F}(V120,V117), P_s-{F}(V121,V120), P_s-{F}(V122,V123), V0 == V123, V123 == V33, V47 == V123, P_s-{F}(V124,V123), P_s-{F}(V125,V124), P_s-{F}(V126,V123), P_s-{F}(V127,V126), P_s-{F}(V128,V123), P_s-{F}(V129,V128), P_s-{F}(V130,V131), V131 == V33, V131 == V0, V47 == V131, P_s-{F}(V132,V131), P_s-{F}(V133,V132), P_s-{F}(V134,V131), P_s-{F}(V135,V134), #-{F} V136, V39 == V136, V40 == V136, V69 == V136 | P_s-{T}(V73,V0), P_s-{T}(V73,V10), P_s-{T}(V73,V64), P_s-{T}(V73,V19), P_s-{T}(V73,V24), P_s-{T}(V73,V68), P_s-{T}(V73,V5), P_s-{T}(V73,V47), P_s-{T}(V73,V89), P_s-{T}(V73,V93), P_s-{T}(V73,V97), P_s-{T}(V73,V101), P_s-{T}(V73,V105), P_s-{T}(V73,V109), P_s-{T}(V73,V117), P_s-{T}(V73,V33), P_s-{T}(V73,V123), P_s-{T}(V73,V131), P_s-{T}(V73,V66), P_s-{T}(V73,V43), P_s-{T}(V73,V73), P_s-{T}(V73,V88), P_s-{T}(V73,V48), P_s-{T}(V73,V92), P_s-{T}(V73,V49), P_s-{T}(V73,V96), P_s-{T}(V73,V50), P_s-{T}(V73,V100), P_s-{T}(V73,V51), P_s-{T}(V73,V104), P_s-{T}(V73,V52), P_s-{T}(V73,V44), P_s-{T}(V73,V108), P_s-{T}(V73,V53), P_s-{T}(V73,V54), P_s-{T}(V73,V116), P_s-{T}(V73,V55), P_s-{T}(V73,V56), P_s-{T}(V73,V57), P_s-{T}(V73,V45), P_s-{T}(V73,V46), P_s-{T}(V73,V71), P_s-{T}(V73,V122), P_s-{T}(V73,V58), P_s-{T}(V73,V59), P_s-{T}(V73,V130), P_s-{T}(V73,V60), P_s-{T}(V73,V61), P_s-{T}(V73,V62), P_s-{T}(V73,V72), P_s-{T}(V73,V91), P_s-{T}(V73,V74), P_s-{T}(V73,V95), P_s-{T}(V73,V76), P_s-{T}(V73,V99), P_s-{T}(V73,V77), P_s-{T}(V73,V103), P_s-{T}(V73,V75), P_s-{T}(V73,V107), P_s-{T}(V73,V111), P_s-{T}(V73,V78), P_s-{T}(V73,V113), P_s-{T}(V73,V79), P_s-{T}(V73,V119), P_s-{T}(V73,V80), P_s-{T}(V73,V121), P_s-{T}(V73,V81), P_s-{T}(V73,V115), P_s-{T}(V73,V82), P_s-{T}(V73,V83), P_s-{T}(V73,V125), P_s-{T}(V73,V84), P_s-{T}(V73,V127), P_s-{T}(V73,V133), P_s-{T}(V73,V85), P_s-{T}(V73,V135), P_s-{T}(V73,V86), P_s-{T}(V73,V87), P_s-{T}(V73,V129), P_s-{T}(V73,V63), P_s-{T}(V73,V11), P_s-{T}(V73,V12), P_s-{T}(V73,V65), P_s-{T}(V73,V25), P_s-{T}(V73,V26), P_s-{T}(V73,V67), P_s-{T}(V73,V136)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #2167: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == 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 == V82, V82 == V83, V83 == V84, V84 == V131, V131 == V134, V132 == V135, V134 == V137, V135 == V138, V137 == V140, V138 == V141, V140 == V143, V141 == V144, V143 == V146, V144 == V147, V146 == V149, V147 == V150, V149 == V152, V150 == V153, V152 == V155, V153 == V156, V155 == V158, V156 == V159, V158 == V161, V159 == V162, V161 == V164, V162 == V165, V164 == V167, V165 == V168, V167 == V170, V168 == V171, V170 == V173, V171 == V174, V173 == V250, V250 == V252, V252 == V254, V254 == V256, V256 == V258, V258 == V260, V260 == V262, V262 == V264, V264 == V266, V266 == V268, V268 == V270, V270 == V272, V272 == V274, V274 == V276, V276 == V278, V278 == V280, V280 == V282, V282 == V284, V284 == V286, V286 == V288, V288 == V290, V290 == V292, V292 == V294, V294 == V296, V296 == V298, V298 == V300, V300 == V302, V302 == V304, V304 == V306, V306 == V308, V308 == V310, V310 == V312, V312 == V314, V314 == V316, V316 == V318, V318 == V320, V320 == V322, V322 == V324, V324 == V326, V326 == V328, V328 == V330, V330 == V332, V332 == V334, V334 == V336, V336 == V338, V338 == V340, V340 == V342, V342 == V344, V344 == V346, V346 == V348, V348 == V350, V350 == V352, V352 == V354, V354 == V356, V356 == V358, V358 == V360, V360 == V362, V362 == V364, V364 == V366, V366 == V368, V368 == V370, V370 == V372; #1991 ), references = 1, size of lhs = 316:
% 57.87/58.05 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}(V5,V6), b-{F}(V6,V5), b-{F}(V5,V7), b-{F}(V7,V5), b-{F}(V5,V8), b-{F}(V8,V5), b-{F}(V5,V9), b-{F}(V9,V5), b-{F}(V0,V10), V10 == V0, P_s-{F}(V11,V10), P_s-{F}(V12,V10), b-{F}(V10,V13), b-{F}(V13,V10), b-{F}(V5,V14), b-{F}(V14,V5), b-{F}(V0,V15), b-{F}(V15,V0), b-{F}(V0,V16), b-{F}(V16,V0), b-{F}(V0,V17), b-{F}(V17,V0), b-{F}(V0,V18), b-{F}(V18,V0), b-{F}(V0,V19), b-{F}(V19,V0), b-{F}(V19,V20), b-{F}(V20,V19), b-{F}(V19,V21), b-{F}(V21,V19), b-{F}(V19,V22), b-{F}(V22,V19), b-{F}(V19,V23), b-{F}(V23,V19), b-{F}(V0,V24), V24 == V0, P_s-{F}(V25,V24), P_s-{F}(V26,V24), b-{F}(V24,V27), b-{F}(V27,V24), b-{F}(V19,V28), b-{F}(V28,V19), b-{F}(V0,V29), b-{F}(V29,V0), b-{F}(V0,V30), b-{F}(V30,V0), b-{F}(V0,V31), b-{F}(V31,V0), b-{F}(V0,V32), b-{F}(V32,V0), b-{F}(V0,V33), b-{F}(V33,V0), b-{F}(V33,V34), b-{F}(V34,V33), b-{F}(V33,V35), b-{F}(V35,V33), b-{F}(V33,V36), b-{F}(V36,V33), b-{F}(V33,V37), b-{F}(V37,V33), b-{F}(V0,V38), V38 == V0, P_s-{F}(V39,V38), P_s-{F}(V40,V38), b-{F}(V38,V41), b-{F}(V41,V38), b-{F}(V33,V42), b-{F}(V42,V33), P_s-{F}(V43,V5), P_s-{F}(V44,V19), P_s-{F}(V45,V33), P_s-{F}(V46,V38), P_s-{F}(V0,V47), V47 == V0, P_s-{F}(V48,V47), P_s-{F}(V49,V47), P_s-{F}(V50,V47), P_s-{F}(V51,V47), P_s-{F}(V52,V47), P_s-{F}(V53,V47), P_s-{F}(V54,V47), P_s-{F}(V55,V47), P_s-{F}(V56,V47), P_s-{F}(V57,V47), P_s-{F}(V58,V47), P_s-{F}(V59,V47), P_s-{F}(V60,V47), P_s-{F}(V61,V47), P_s-{F}(V62,V47), P_s-{F}(V63,V10), P_s-{F}(V64,V19), P_s-{F}(V65,V24), P_s-{F}(V66,V5), P_s-{F}(V67,V47), P_s-{F}(V68,V47), P_s-{F}(V69,V47), P_s-{F}(V70,V47), P_s-{F}(V71,V47), P_s-{F}(V72,V47), P_s-{F}(V73,V47), P_s-{F}(V74,V47), P_s-{F}(V75,V47), P_s-{F}(V76,V47), P_s-{F}(V77,V33), P_s-{F}(V78,V47), P_s-{F}(V79,V47), P_s-{F}(V80,V47), P_s-{F}(V81,V47), P_s-{F}(V82,V47), P_s-{F}(V83,V84), V0 == V84, V84 == V38, P_s-{F}(V85,V84), P_s-{F}(V86,V85), P_s-{F}(V87,V88), P_s-{F}(V88,V89), V89 == V0, V47 == V89, P_s-{F}(V90,V89), P_s-{F}(V91,V89), P_s-{F}(V92,V91), P_s-{F}(V93,V94), P_s-{F}(V94,V95), V95 == V0, V47 == V95, P_s-{F}(V96,V95), P_s-{F}(V97,V95), P_s-{F}(V98,V97), P_s-{F}(V99,V100), P_s-{F}(V100,V101), V101 == V0, V47 == V101, P_s-{F}(V102,V101), P_s-{F}(V103,V101), P_s-{F}(V104,V103), P_s-{F}(V105,V106), P_s-{F}(V106,V107), V107 == V0, V47 == V107, P_s-{F}(V108,V107), P_s-{F}(V109,V107), P_s-{F}(V110,V109), P_s-{F}(V111,V112), P_s-{F}(V112,V113), V113 == V0, V47 == V113, P_s-{F}(V114,V113), P_s-{F}(V115,V113), P_s-{F}(V116,V115), P_s-{F}(V117,V118), P_s-{F}(V118,V119), V0 == V119, V119 == V19, V47 == V119, P_s-{F}(V120,V119), P_s-{F}(V121,V119), P_s-{F}(V122,V121), P_s-{F}(V123,V119), P_s-{F}(V124,V123), P_s-{F}(V125,V119), P_s-{F}(V126,V125), P_s-{F}(V127,V128), P_s-{F}(V128,V129), V129 == V19, V129 == V0, V47 == V129, P_s-{F}(V130,V129), P_s-{F}(V131,V129), P_s-{F}(V132,V131), P_s-{F}(V133,V129), P_s-{F}(V134,V133), P_s-{F}(V135,V136), P_s-{F}(V136,V137), V0 == V137, V137 == V33, V47 == V137, P_s-{F}(V138,V137), P_s-{F}(V139,V137), P_s-{F}(V140,V139), P_s-{F}(V141,V137), P_s-{F}(V142,V141), P_s-{F}(V143,V137), P_s-{F}(V144,V143), P_s-{F}(V145,V146), P_s-{F}(V146,V147), V147 == V33, V147 == V0, V47 == V147, P_s-{F}(V148,V147), P_s-{F}(V149,V147), P_s-{F}(V150,V149), P_s-{F}(V151,V147), P_s-{F}(V152,V151), P_s-{F}(V153,V154), V154 == V0, V154 == V5, V154 == V10, P_s-{F}(V155,V154), P_s-{F}(V156,V155), P_s-{F}(V157,V154), P_s-{F}(V158,V157), P_s-{F}(V159,V154), P_s-{F}(V160,V159), P_s-{F}(V161,V162), V0 == V162, V162 == V24, P_s-{F}(V163,V162), P_s-{F}(V164,V163), P_s-{F}(V165,V166), V63 == V166, V153 == V166, V64 == V166, V65 == V166, V161 == V166, V66 == V166, V67 == V166, V68 == V166, V69 == V166, V90 == V166, V96 == V166, V70 == V166, V71 == V166, V102 == V166, V108 == V166, V114 == V166, V120 == V166, V72 == V166, V73 == V166, V130 == V166, V74 == V166, V75 == V166, V76 == V166, V77 == V166, V138 == V166, V78 == V166, V79 == V166, V80 == V166, V81 == V166, V82 == V166, V148 == V166, V160 == V166, V165 == V166, V92 == V166, V98 == V166, V104 == V166, V110 == V166, V116 == V166, V122 == V166, V132 == V166, V86 == V166, V140 == V166, V150 == V166, V156 == V166, V158 == V166, V164 == V166, P_s-{F}(V167,V166), P_s-{F}(V168,V167), V168 == V166, P_s-{F}(V169,V166), P_s-{F}(V170,V169), V170 == V166, P_s-{F}(V171,V166), P_s-{F}(V172,V171), V172 == V166, P_s-{F}(V173,V166), P_s-{F}(V174,V173), V174 == V166, P_s-{F}(V175,V166), P_s-{F}(V176,V175), V176 == V166, P_s-{F}(V177,V166), P_s-{F}(V178,V177), V178 == V166, P_s-{F}(V179,V166), P_s-{F}(V180,V179), V180 == V166, P_s-{F}(V181,V166), P_s-{F}(V182,V181), V182 == V166, P_s-{F}(V183,V166), P_s-{F}(V184,V183), V184 == V166, P_s-{F}(V185,V166), P_s-{F}(V186,V185), V186 == V166, P_s-{F}(V187,V166), P_s-{F}(V188,V187), V188 == V166, P_s-{F}(V189,V166), P_s-{F}(V190,V189), V190 == V166, P_s-{F}(V191,V166), P_s-{F}(V192,V191), V192 == V166, P_s-{F}(V193,V166), P_s-{F}(V194,V193), V194 == V166, P_s-{F}(V195,V166), P_s-{F}(V196,V195), V196 == V166, P_s-{F}(V197,V198), V39 == V198, V40 == V198, V83 == V198, V197 == V166 | P_s-{T}(V166,V0), P_s-{T}(V166,V43), P_s-{T}(V166,V48), P_s-{T}(V166,V49), P_s-{T}(V166,V50), P_s-{T}(V166,V51), P_s-{T}(V166,V52), P_s-{T}(V166,V44), P_s-{T}(V166,V53), P_s-{T}(V166,V54), P_s-{T}(V166,V55), P_s-{T}(V166,V56), P_s-{T}(V166,V57), P_s-{T}(V166,V45), P_s-{T}(V166,V46), P_s-{T}(V166,V58), P_s-{T}(V166,V59), P_s-{T}(V166,V60), P_s-{T}(V166,V61), P_s-{T}(V166,V62), P_s-{T}(V166,V87), P_s-{T}(V166,V93), P_s-{T}(V166,V99), P_s-{T}(V166,V105), P_s-{T}(V166,V111), P_s-{T}(V166,V117), P_s-{T}(V166,V124), P_s-{T}(V166,V127), P_s-{T}(V166,V134), P_s-{T}(V166,V126), P_s-{T}(V166,V135), P_s-{T}(V166,V142), P_s-{T}(V166,V145), P_s-{T}(V166,V152), P_s-{T}(V166,V144), P_s-{T}(V166,V11), P_s-{T}(V166,V12), P_s-{T}(V166,V25), P_s-{T}(V166,V26)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #2410: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == 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 == V82, V82 == V83, V83 == V131, V131 == V134, V132 == V135, V134 == V137, V135 == V138, V137 == V140, V138 == V141, V140 == V143, V141 == V144, V143 == V146, V144 == V147, V146 == V149, V147 == V150, V149 == V152, V150 == V153, V152 == V155, V153 == V156, V155 == V158, V156 == V159, V158 == V161, V159 == V162, V161 == V164, V162 == V165, V164 == V167, V165 == V168, V167 == V170, V168 == V171, V170 == V173, V171 == V174, V173 == V176, V176 == V178, V178 == V179, V179 == V181, V181 == V183, V183 == V184, V184 == V186, V186 == V188, V188 == V190, V190 == V192, V192 == V193, V193 == V194, V194 == V196, V196 == V198, V198 == V199, V199 == V200, V200 == V201, V201 == V202, V202 == V204, V204 == V206, V206 == V207, V207 == V209, V209 == V211, V211 == V213, V213 == V215, V215 == V216, V216 == V218, V218 == V220, V220 == V222, V222 == V224, V224 == V226, V226 == V227, V227 == V228, V228 == V229, V229 == V230, V230 == V231, V231 == V232, V232 == V233, V233 == V234, V234 == V235, V235 == V236, V236 == V237, V237 == V238, V238 == V239, V239 == V240, V240 == V241, V241 == V242, V242 == V243, V243 == V244, V244 == V245, V245 == V246, V246 == V247, V247 == V248, V248 == V249, V249 == V250, V250 == V251, V251 == V252, V252 == V253, V253 == V254, V254 == V255, V255 == V256, V256 == V257, V257 == V84, V84 == V127, V174 == V89, V127 == V133, V133 == V136, V136 == V139, V139 == V142, V142 == V145, V145 == V128, V89 == V103, V128 == V148, V148 == V151, V151 == V154, V154 == V157, V157 == V160, V160 == V129, V103 == V117, V129 == V130, V117 == V122, V130 == V163, V163 == V166, V166 == V169, V169 == V172, V172 == V175, V175 == V262, V122 == V263, V262 == V268, V263 == V269, V264 == V270, V268 == V274, V269 == V275, V270 == V276, V274 == V280, V275 == V281, V276 == V282, V280 == V286, V281 == V287, V282 == V288, V286 == V292, V287 == V293, V288 == V294, V292 == V299, V293 == V298, V299 == V302, V298 == V303, V294 == V304, V302 == V309, V303 == V308, V309 == V301, V308 == V300, V301 == V310, V300 == V311, V304 == V312, V310 == V317, V311 == V316, V317 == V320, V316 == V321, V312 == V322, V320 == V327, V321 == V326, V327 == V319, V326 == V318, V319 == V95, V318 == V94, V95 == V96, V96 == V109, V94 == V108; #2168 ), references = 2, size of lhs = 234:
% 57.87/58.05 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V0,V3), b-{F}(V3,V0), b-{F}(V0,V4), b-{F}(V4,V0), b-{F}(V0,V5), b-{F}(V5,V0), b-{F}(V0,V6), b-{F}(V6,V0), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V0,V8), b-{F}(V8,V0), b-{F}(V0,V9), b-{F}(V9,V0), b-{F}(V0,V10), b-{F}(V10,V0), b-{F}(V0,V11), b-{F}(V11,V0), b-{F}(V0,V12), b-{F}(V12,V0), b-{F}(V0,V13), V13 == V0, b-{F}(V13,V0), P_s-{F}(V0,V13), P_s-{F}(V14,V13), P_s-{F}(V15,V13), P_s-{F}(V16,V13), P_s-{F}(V17,V13), P_s-{F}(V18,V13), P_s-{F}(V19,V13), P_s-{F}(V20,V13), P_s-{F}(V21,V13), P_s-{F}(V22,V13), P_s-{F}(V23,V13), P_s-{F}(V24,V13), P_s-{F}(V25,V13), P_s-{F}(V26,V13), P_s-{F}(V27,V13), P_s-{F}(V28,V13), b-{F}(V13,V29), b-{F}(V29,V13), b-{F}(V13,V30), b-{F}(V30,V13), b-{F}(V13,V31), b-{F}(V31,V13), b-{F}(V13,V32), b-{F}(V32,V13), b-{F}(V13,V33), b-{F}(V33,V13), b-{F}(V13,V34), b-{F}(V34,V13), b-{F}(V13,V35), b-{F}(V35,V13), b-{F}(V13,V36), b-{F}(V36,V13), b-{F}(V13,V37), b-{F}(V37,V13), b-{F}(V13,V38), b-{F}(V38,V13), P_s-{F}(V39,V13), b-{F}(V13,V40), b-{F}(V40,V13), b-{F}(V13,V41), b-{F}(V41,V13), b-{F}(V13,V42), b-{F}(V42,V13), b-{F}(V13,V43), b-{F}(V43,V13), b-{F}(V13,V44), b-{F}(V44,V13), b-{F}(V13,V45), b-{F}(V45,V13), P_s-{F}(V46,V13), P_s-{F}(V47,V13), b-{F}(V13,V48), b-{F}(V48,V13), b-{F}(V13,V49), b-{F}(V49,V13), P_s-{F}(V50,V13), P_s-{F}(V51,V13), P_s-{F}(V52,V13), P_s-{F}(V53,V13), P_s-{F}(V54,V13), P_s-{F}(V13,V55), V55 == V0, V13 == V55, P_s-{F}(V56,V55), P_s-{F}(V57,V55), P_s-{F}(V58,V55), P_s-{F}(V59,V55), P_s-{F}(V60,V55), P_s-{F}(V61,V55), P_s-{F}(V62,V55), P_s-{F}(V63,V55), P_s-{F}(V64,V55), P_s-{F}(V65,V55), P_s-{F}(V66,V65), P_s-{F}(V67,V55), P_s-{F}(V68,V67), P_s-{F}(V69,V55), P_s-{F}(V70,V69), P_s-{F}(V71,V55), P_s-{F}(V72,V71), P_s-{F}(V73,V55), P_s-{F}(V74,V73), P_s-{F}(V75,V55), P_s-{F}(V76,V75), P_s-{F}(V77,V55), P_s-{F}(V78,V77), P_s-{F}(V79,V55), P_s-{F}(V80,V79), P_s-{F}(V81,V55), P_s-{F}(V82,V81), P_s-{F}(V83,V84), V0 == V84, V84 == V13, P_s-{F}(V85,V84), P_s-{F}(V86,V85), P_s-{F}(V87,V88), V88 == V0, V88 == V13, P_s-{F}(V89,V88), P_s-{F}(V90,V89), P_s-{F}(V91,V88), P_s-{F}(V92,V91), P_s-{F}(V93,V88), P_s-{F}(V94,V93), P_s-{F}(V95,V96), V0 == V96, V96 == V13, P_s-{F}(V97,V96), P_s-{F}(V98,V97), P_s-{F}(V99,V100), V50 == V100, V87 == V100, V51 == V100, V52 == V100, V95 == V100, V53 == V100, V14 == V100, V15 == V100, V16 == V100, V56 == V100, V57 == V100, V17 == V100, V18 == V100, V58 == V100, V59 == V100, V60 == V100, V61 == V100, V19 == V100, V20 == V100, V62 == V100, V21 == V100, V22 == V100, V23 == V100, V54 == V100, V63 == V100, V24 == V100, V25 == V100, V26 == V100, V27 == V100, V28 == V100, V64 == V100, V94 == V100, V99 == V100, V66 == V100, V68 == V100, V70 == V100, V72 == V100, V74 == V100, V76 == V100, V78 == V100, V86 == V100, V80 == V100, V82 == V100, V90 == V100, V92 == V100, V98 == V100, P_s-{F}(V101,V100), P_s-{F}(V102,V101), V102 == V100, P_s-{F}(V103,V100), P_s-{F}(V104,V103), V104 == V100, P_s-{F}(V105,V100), P_s-{F}(V106,V105), V106 == V100, P_s-{F}(V107,V100), P_s-{F}(V108,V107), V108 == V100, P_s-{F}(V109,V100), P_s-{F}(V110,V109), V110 == V100, P_s-{F}(V111,V100), P_s-{F}(V112,V111), V112 == V100, P_s-{F}(V113,V100), P_s-{F}(V114,V113), V114 == V100, P_s-{F}(V115,V100), P_s-{F}(V116,V115), V116 == V100, P_s-{F}(V117,V100), P_s-{F}(V118,V117), V118 == V100, P_s-{F}(V119,V100), P_s-{F}(V120,V119), V120 == V100, P_s-{F}(V121,V100), P_s-{F}(V122,V121), V122 == V100, P_s-{F}(V123,V100), P_s-{F}(V124,V123), V124 == V100, P_s-{F}(V125,V100), P_s-{F}(V126,V125), V126 == V100, P_s-{F}(V127,V100), P_s-{F}(V128,V127), V128 == V100, P_s-{F}(V129,V100), P_s-{F}(V130,V129), V130 == V100, P_s-{F}(V131,V132), V46 == V132, V47 == V132, V83 == V132, V131 == V100 | P_s-{T}(V100,V39)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #2419: mergings( V2 == V32; #2417 ), references = 1, size of lhs = 83:
% 57.87/58.05 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), P_s-{F}(V8,V1), P_s-{F}(V9,V1), P_s-{F}(V10,V1), P_s-{F}(V11,V1), P_s-{F}(V12,V1), P_s-{F}(V13,V1), P_s-{F}(V14,V1), P_s-{F}(V15,V1), P_s-{F}(V16,V1), P_s-{F}(V17,V1), P_s-{F}(V18,V1), P_s-{F}(V19,V1), P_s-{F}(V20,V1), P_s-{F}(V21,V1), P_s-{F}(V22,V1), P_s-{F}(V23,V1), P_s-{F}(V24,V1), P_s-{F}(V25,V1), P_s-{F}(V26,V1), P_s-{F}(V27,V1), P_s-{F}(V28,V1), P_s-{F}(V29,V1), P_s-{F}(V30,V1), P_s-{F}(V31,V1), P_s-{F}(V32,V1), P_s-{F}(V33,V1), P_s-{F}(V34,V1), P_s-{F}(V35,V1), P_s-{F}(V36,V1), P_s-{F}(V37,V1), P_s-{F}(V38,V1), P_s-{F}(V39,V1), P_s-{F}(V40,V1), P_s-{F}(V41,V1), P_s-{F}(V42,V1), P_s-{F}(V43,V1), P_s-{F}(V44,V1), P_s-{F}(V45,V1), P_s-{F}(V46,V1), P_s-{F}(V47,V1), P_s-{F}(V48,V1), P_s-{F}(V49,V1), P_s-{F}(V50,V1), P_s-{F}(V51,V1), P_s-{F}(V52,V1), P_s-{F}(V53,V1), P_s-{F}(V54,V1), P_s-{F}(V55,V1), P_s-{F}(V56,V1), P_s-{F}(V57,V1), P_s-{F}(V58,V1), P_s-{F}(V59,V1), P_s-{F}(V60,V1), P_s-{F}(V61,V1), P_s-{F}(V62,V1), P_s-{F}(V63,V1), P_s-{F}(V64,V1), P_s-{F}(V65,V1), P_s-{F}(V66,V1), P_s-{F}(V67,V1), P_s-{F}(V68,V1), P_s-{F}(V69,V1), P_s-{F}(V70,V1), P_s-{F}(V71,V1), P_s-{F}(V72,V1), P_s-{F}(V73,V1), P_s-{F}(V74,V1), P_s-{F}(V75,V1), P_s-{F}(V76,V1), P_s-{F}(V77,V1), P_s-{F}(V78,V1), P_s-{F}(V79,V1), P_s-{F}(V80,V1), P_s-{F}(V81,V1) | P_s-{T}(V1,V0), P_s-{T}(V1,V1), P_s-{T}(V1,V2), P_s-{T}(V1,V3), P_s-{T}(V1,V4), P_s-{T}(V1,V31), P_s-{T}(V1,V32), P_s-{T}(V1,V33), P_s-{T}(V1,V34), P_s-{T}(V1,V35), 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,V5), P_s-{T}(V1,V6), P_s-{T}(V1,V36), P_s-{T}(V1,V7), P_s-{T}(V1,V8), P_s-{T}(V1,V37), P_s-{T}(V1,V56), P_s-{T}(V1,V57), P_s-{T}(V1,V58), P_s-{T}(V1,V59), P_s-{T}(V1,V60), P_s-{T}(V1,V61), P_s-{T}(V1,V26), P_s-{T}(V1,V27), P_s-{T}(V1,V28), P_s-{T}(V1,V29), P_s-{T}(V1,V9), P_s-{T}(V1,V10), P_s-{T}(V1,V11), P_s-{T}(V1,V12), P_s-{T}(V1,V13), P_s-{T}(V1,V14), P_s-{T}(V1,V15), P_s-{T}(V1,V16), P_s-{T}(V1,V17), P_s-{T}(V1,V18), P_s-{T}(V1,V30), P_s-{T}(V1,V19), P_s-{T}(V1,V20), P_s-{T}(V1,V21), P_s-{T}(V1,V22), P_s-{T}(V1,V23), P_s-{T}(V1,V65), 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,V62), P_s-{T}(V1,V45), P_s-{T}(V1,V46), P_s-{T}(V1,V63), P_s-{T}(V1,V64), P_s-{T}(V1,V66), P_s-{T}(V1,V67), P_s-{T}(V1,V68), P_s-{T}(V1,V69), P_s-{T}(V1,V70), P_s-{T}(V1,V71), P_s-{T}(V1,V72), P_s-{T}(V1,V73), P_s-{T}(V1,V74), P_s-{T}(V1,V75), P_s-{T}(V1,V76), P_s-{T}(V1,V77), P_s-{T}(V1,V78), P_s-{T}(V1,V79), P_s-{T}(V1,V80), P_s-{T}(V1,V81), P_s-{T}(V1,V24), P_s-{T}(V1,V25)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #2502: mergings( V31 == V0, V0 == V2, V2 == V3, V3 == V4, V4 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V5, V5 == V6, V6 == V37, V37 == V7, V7 == V8, V8 == V38, V38 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V30, V30 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V66, V66 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V63, V63 == V46, V46 == V47, V47 == V64, V64 == V65, V65 == 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 == V24, V24 == V25; #2420 ), references = 1, size of lhs = 3:
% 57.87/58.05 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0 | P_s-{T}(V1,V1)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #2506: mergings( V0 == V2; #2504 ), references = 1, size of lhs = 1:
% 57.87/58.05 P_z-{F}(V0) | P_s-{T}(V0,V0)
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 #2509: exists( #8, #2507 ), references = 1, size of lhs = 0:
% 57.87/58.05 FALSE | FALSE
% 57.87/58.05 (used 0 times, uses = {})
% 57.87/58.05
% 57.87/58.05 number of learnt formulas = 58
% 57.87/58.05
% 57.87/58.05
% 57.87/58.05 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 57.87/58.05
% 57.87/58.05 randbase = 1
%------------------------------------------------------------------------------