%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : GRA169-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n021.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 65.34s 65.57s
% Output : Refutation 65.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GRA169-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.16/0.33 % Computer : n021.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 00:52:25 EDT 2026
% 0.16/0.33 % CPUTime :
% 65.34/65.57 GeoParameters:
% 65.34/65.57
% 65.34/65.57 tptp_input = 1
% 65.34/65.57 tptp_output = 0
% 65.34/65.57 nonempty = 1
% 65.34/65.57 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 65.34/65.57 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 65.34/65.57
% 65.34/65.57
% 65.34/65.57 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 65.34/65.57 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 65.34/65.57
% 65.34/65.57 RuleSystem INPUT:
% 65.34/65.57
% 65.34/65.57 Initial Rules:
% 65.34/65.57 #0: input, references = 15, size of lhs = 2:
% 65.34/65.57 P_z-{F}(V0), P_s-{F}(V1,V0) | FALSE
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1: input, references = 6, size of lhs = 4:
% 65.34/65.57 P_z-{F}(V0), P_s-{F}(V1,V4), P_s-{F}(V2,V4), V1 == V2 | FALSE
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2: input, references = 3, size of lhs = 2:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V1) | FALSE
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #3: input, references = 3, size of lhs = 2:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V1) | FALSE
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #4: input, references = 30, size of lhs = 4:
% 65.34/65.57 P_z-{F}(V0), #-{F} V1, #-{F} V2, V1 == V2 | r-{T}(V1,V2), b-{T}(V1,V2)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #5: input, references = 24, size of lhs = 4:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V3,V1), r-{F}(V3,V2) | FALSE
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #6: input, references = 8, size of lhs = 6:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V3,V1), b-{F}(V4,V3), b-{F}(V5,V4), b-{F}(V5,V3) | FALSE
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #7: input, references = 17, size of lhs = 1:
% 65.34/65.57 #-{F} V0 | EXISTS V1: P_s-{T}(V0,V1)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #8: input, references = 4, size of lhs = 0:
% 65.34/65.57 FALSE | EXISTS V0: P_z-{T}(V0)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 number of initial rules = 9
% 65.34/65.57
% 65.34/65.57 Simplifiers:
% 65.34/65.57 #9: unsound, references = 3, size of lhs = 3:
% 65.34/65.57 P_s-{F}(V0,V1), P_s-{F}(V0,V3), V1 == V3 | FALSE
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #10: unsound, references = 3, size of lhs = 3:
% 65.34/65.57 P_z-{F}(V0), P_z-{F}(V1), V0 == V1 | FALSE
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 number of simplifiers = 2
% 65.34/65.57
% 65.34/65.57 Learnt:
% 65.34/65.57 #13: mergings( V0 == V3; #11 ), references = 10, size of lhs = 6:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, b-{F}(V3,V4), b-{F}(V4,V5) | r-{T}(V2,V3)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #16: mergings( V0 == V3; #14 ), references = 6, size of lhs = 6:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V3,V4), b-{F}(V4,V5), V5 == V1, b-{F}(V3,V5) | r-{T}(V5,V1)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #24: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #19 ), references = 14, size of lhs = 11:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), r-{F}(V5,V2), b-{F}(V5,V6), b-{F}(V1,V7), b-{F}(V7,V8), V1 == V8, V8 == V2, V8 == V5 | r-{T}(V1,V8)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #29: mergings( V0 == V3, V3 == V4; #26 ), references = 4, size of lhs = 8:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), r-{F}(V5,V2), r-{F}(V5,V6), V1 == V6, V6 == V2 | r-{T}(V1,V6)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #36: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #31 ), references = 15, size of lhs = 10:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), r-{F}(V1,V5), b-{F}(V5,V2), #-{F} V6, V1 == V6, V6 == V2, V5 == V6 | b-{T}(V1,V6)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #41: mergings( V0 == V3, V3 == V4; #38 ), references = 4, size of lhs = 8:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, r-{F}(V4,V2), r-{F}(V4,V3), b-{F}(V5,V6), V3 == V5 | r-{T}(V3,V5)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #52: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7; #46 ), references = 8, size of lhs = 30:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), r-{F}(V5,V2), b-{F}(V5,V6), b-{F}(V1,V7), b-{F}(V7,V8), b-{F}(V8,V9), r-{F}(V10,V7), b-{F}(V10,V11), b-{F}(V12,V13), V1 == V12, V1 == V13, V13 == V2, V13 == V5, b-{F}(V12,V14), V1 == V14, V14 == V7, V14 == V10, V14 == V13, b-{F}(V15,V14), b-{F}(V15,V13), b-{F}(V16,V13), b-{F}(V16,V14), r-{F}(V17,V18), V13 == V18, V13 == V17, b-{F}(V18,V19), b-{F}(V17,V20) | r-{T}(V1,V12)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #59: mergings( V0 == V3, V3 == V4, V4 == V5; #55 ), references = 6, size of lhs = 37:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), r-{F}(V1,V5), V5 == V2, b-{F}(V2,V6), b-{F}(V6,V7), r-{F}(V8,V2), b-{F}(V8,V9), b-{F}(V2,V10), b-{F}(V10,V11), r-{F}(V12,V2), b-{F}(V12,V13), r-{F}(V5,V14), b-{F}(V14,V15), V15 == V2, V15 == V8, b-{F}(V14,V16), V16 == V2, V16 == V12, V16 == V15, b-{F}(V17,V16), b-{F}(V17,V15), b-{F}(V18,V15), b-{F}(V18,V16), r-{F}(V19,V20), V15 == V20, V15 == V19, b-{F}(V20,V21), b-{F}(V19,V22), #-{F} V23, V23 == V2, V23 == V5, V23 == V14, V23 == V15, V23 == V16 | r-{T}(V23,V2)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #103: 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; #79 ), references = 1, size of lhs = 46:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, b-{F}(V3,V2), r-{F}(V4,V3), r-{F}(V4,V2), r-{F}(V5,V2), b-{F}(V3,V6), r-{F}(V5,V7), V7 == V2, r-{F}(V7,V8), V8 == V3, V2 == V8, r-{F}(V8,V3), r-{F}(V8,V2), b-{F}(V3,V9), b-{F}(V3,V10), r-{F}(V8,V11), b-{F}(V11,V12), r-{F}(V8,V13), b-{F}(V13,V14), r-{F}(V8,V15), b-{F}(V15,V16), r-{F}(V8,V17), b-{F}(V17,V18), #-{F} V19, V19 == V3, V19 == V8, V19 == V2, V19 == V11, #-{F} V20, V20 == V3, V20 == V2, V20 == V7, V20 == V19, V20 == V17, V20 == V8, #-{F} V21, V21 == V2, V21 == V3, V20 == V21, V19 == V21, V21 == V13, V21 == V15, V21 == V8 | r-{T}(V2,V3)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #127: 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; #80 ), references = 1, size of lhs = 57:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, b-{F}(V3,V2), r-{F}(V4,V2), r-{F}(V4,V3), r-{F}(V5,V2), b-{F}(V3,V6), r-{F}(V5,V7), V7 == V2, r-{F}(V7,V8), V8 == V3, V2 == V8, r-{F}(V8,V3), r-{F}(V8,V2), b-{F}(V3,V9), b-{F}(V3,V10), r-{F}(V11,V2), b-{F}(V3,V12), r-{F}(V11,V13), V13 == V2, r-{F}(V13,V8), b-{F}(V3,V14), b-{F}(V3,V15), r-{F}(V8,V16), b-{F}(V16,V17), r-{F}(V8,V18), b-{F}(V18,V19), r-{F}(V8,V20), b-{F}(V20,V21), r-{F}(V8,V22), b-{F}(V22,V23), r-{F}(V8,V24), b-{F}(V24,V25), #-{F} V26, V2 == V26, V26 == V3, V26 == V8, V26 == V16, #-{F} V27, V27 == V18, V27 == V7, V27 == V26, V27 == V3, V2 == V27, V27 == V22, V27 == V24, V27 == V8, #-{F} V28, V28 == V3, V28 == V2, V28 == V13, V28 == V27, V28 == V26, V28 == V20, V28 == V8 | r-{T}(V2,V3)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #154: 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; #129 ), references = 2, size of lhs = 32:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, r-{F}(V4,V3), r-{F}(V4,V2), r-{F}(V5,V2), r-{F}(V5,V6), V6 == V2, r-{F}(V6,V7), V7 == V3, V2 == V7, r-{F}(V7,V2), r-{F}(V7,V3), r-{F}(V8,V2), r-{F}(V8,V3), #-{F} V9, V9 == V7, V9 == V2, V9 == V3, #-{F} V10, V10 == V2, V10 == V6, V10 == V9, V10 == V3, V10 == V7, #-{F} V11, V11 == V2, V10 == V11, V9 == V11, V11 == V3, V11 == V7 | r-{T}(V3,V2)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #182: 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; #156 ), references = 1, size of lhs = 29:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, r-{F}(V4,V3), r-{F}(V4,V2), r-{F}(V5,V2), r-{F}(V5,V6), V6 == V2, r-{F}(V6,V7), V7 == V3, V2 == V7, r-{F}(V7,V2), r-{F}(V7,V3), r-{F}(V8,V2), r-{F}(V8,V3), r-{F}(V9,V3), r-{F}(V9,V2), #-{F} V10, #-{F} V11, V11 == V2, V11 == V6, V11 == V3, V11 == V7, #-{F} V12, V12 == V2, V11 == V12, V12 == V3, V12 == V7 | P_s-{T}(V10,V7), P_s-{T}(V10,V2), P_s-{T}(V10,V3), P_s-{T}(V10,V11), P_s-{T}(V10,V12)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #213: 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 == V38, V38 == V40, V40 == V42, V42 == V44; #183 ), references = 1, size of lhs = 35:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, r-{F}(V4,V3), r-{F}(V4,V2), r-{F}(V5,V2), r-{F}(V5,V6), V6 == V2, r-{F}(V6,V7), V7 == V3, V2 == V7, r-{F}(V7,V2), r-{F}(V7,V3), r-{F}(V8,V2), r-{F}(V8,V3), r-{F}(V9,V3), r-{F}(V9,V2), P_s-{F}(V10,V7), P_s-{F}(V11,V2), P_s-{F}(V12,V13), V13 == V2, V13 == V6, V13 == V3, V13 == V7, P_s-{F}(V14,V15), V15 == V2, V13 == V15, V15 == V3, V15 == V7, #-{F} V16, V10 == V16, V11 == V16, V12 == V16, V14 == V16 | P_s-{T}(V16,V3)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #247: 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; #215 ), references = 8, size of lhs = 25:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V0), V1 == V0, r-{F}(V1,V2), r-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V5), V5 == V0, V2 == V5, V5 == V1, P_s-{F}(V6,V7), V7 == V5, V7 == V2, V7 == V0, V7 == V1, P_s-{F}(V8,V9), V9 == V5, V7 == V9, V9 == V0, V9 == V1, #-{F} V10, V3 == V10, V4 == V10, V6 == V10, V8 == V10 | b-{T}(V1,V5)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #251: mergings( V2 == V3; #249 ), references = 1, size of lhs = 29:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, r-{F}(V4,V3), r-{F}(V4,V2), r-{F}(V5,V2), r-{F}(V5,V6), V6 == V2, r-{F}(V6,V7), V7 == V3, V2 == V7, r-{F}(V7,V2), r-{F}(V7,V3), r-{F}(V8,V2), r-{F}(V8,V3), r-{F}(V3,V9), r-{F}(V9,V2), #-{F} V10, #-{F} V11, V11 == V2, V11 == V6, V11 == V3, V11 == V7, #-{F} V12, V12 == V2, V11 == V12, V12 == V3, V12 == V7 | P_s-{T}(V10,V7), P_s-{T}(V10,V2), P_s-{T}(V10,V3), P_s-{T}(V10,V11), P_s-{T}(V10,V12)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #258: mergings( V0 == V1, V1 == V14, V14 == V16, V16 == V18, V18 == V20; #252 ), references = 1, size of lhs = 35:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3, r-{F}(V4,V3), r-{F}(V4,V2), r-{F}(V5,V2), r-{F}(V5,V6), V6 == V2, r-{F}(V6,V7), V7 == V3, V2 == V7, r-{F}(V7,V2), r-{F}(V7,V3), r-{F}(V8,V2), r-{F}(V8,V3), r-{F}(V3,V9), r-{F}(V9,V2), P_s-{F}(V10,V2), P_s-{F}(V11,V3), P_s-{F}(V12,V13), V13 == V2, V13 == V6, V13 == V3, V13 == V7, P_s-{F}(V14,V15), V15 == V2, V13 == V15, V15 == V3, V15 == V7, #-{F} V16, V10 == V16, V11 == V16, V12 == V16, V14 == V16 | P_s-{T}(V16,V7)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #268: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V1; #260 ), references = 6, size of lhs = 26:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V0,V2), V0 == V2, r-{F}(V2,V0), P_s-{F}(V3,V2), P_s-{F}(V4,V5), V5 == V0, V5 == V2, V1 == V5, P_s-{F}(V6,V7), V7 == V5, V7 == V1, V7 == V2, V7 == V0, P_s-{F}(V8,V9), V9 == V5, V7 == V9, V9 == V2, V9 == V0, #-{F} V10, V4 == V10, V3 == V10, V6 == V10, V8 == V10 | b-{T}(V0,V5)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #285: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V12, V12 == V13, V13 == V14; #276 ), references = 3, size of lhs = 89:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), V2 == V1, b-{F}(V3,V2), b-{F}(V3,V1), b-{F}(V4,V1), b-{F}(V4,V2), b-{F}(V5,V6), b-{F}(V5,V7), V7 == V1, V7 == V2, V7 == V0, V7 == V6, P_s-{F}(V8,V7), b-{F}(V9,V6), b-{F}(V9,V10), V7 == V10, V6 == V10, b-{F}(V11,V6), V7 == V11, V6 == V11, V1 == V11, V2 == V11, V10 == V11, b-{F}(V11,V10), b-{F}(V11,V7), b-{F}(V11,V12), r-{F}(V13,V11), V6 == V13, b-{F}(V13,V14), r-{F}(V15,V11), V1 == V15, b-{F}(V15,V16), r-{F}(V17,V11), V2 == V17, b-{F}(V17,V18), r-{F}(V19,V11), V10 == V19, b-{F}(V19,V20), r-{F}(V21,V11), b-{F}(V21,V22), r-{F}(V23,V11), b-{F}(V23,V24), r-{F}(V25,V26), V1 == V26, V1 == V25, b-{F}(V26,V27), b-{F}(V25,V28), P_s-{F}(V29,V30), V30 == V0, V6 == V30, V30 == V7, P_s-{F}(V31,V32), V32 == V30, V32 == V6, V32 == V0, V32 == V7, P_s-{F}(V33,V34), V34 == V30, V32 == V34, V34 == V0, V34 == V7, b-{F}(V35,V36), V10 == V35, V7 == V35, b-{F}(V35,V37), V7 == V37, V37 == V11, V37 == V21, b-{F}(V35,V38), V7 == V38, V38 == V11, V38 == V23, V38 == V37, b-{F}(V39,V38), b-{F}(V39,V37), b-{F}(V40,V37), b-{F}(V40,V38), r-{F}(V41,V42), V37 == V42, V37 == V41, b-{F}(V42,V43), b-{F}(V41,V44), #-{F} V45, V8 == V45, V29 == V45, V31 == V45, V33 == V45 | r-{T}(V7,V11)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #337: 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 == V53; #294 ), references = 1, size of lhs = 101:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V0,V2), V0 == V2, r-{F}(V2,V0), P_s-{F}(V3,V2), r-{F}(V0,V4), r-{F}(V4,V0), r-{F}(V0,V5), V0 == V5, r-{F}(V5,V0), P_s-{F}(V6,V5), r-{F}(V0,V7), r-{F}(V7,V0), r-{F}(V0,V8), V0 == V8, r-{F}(V8,V0), P_s-{F}(V9,V8), r-{F}(V0,V10), V10 == V0, r-{F}(V10,V0), r-{F}(V10,V11), r-{F}(V11,V10), P_s-{F}(V12,V10), r-{F}(V10,V13), r-{F}(V13,V10), P_s-{F}(V14,V10), r-{F}(V10,V15), r-{F}(V15,V10), P_s-{F}(V16,V10), P_s-{F}(V17,V18), V11 == V18, V18 == V2, V1 == V18, V18 == V0, V18 == V10, P_s-{F}(V19,V18), P_s-{F}(V20,V21), V21 == V18, V21 == V11, V21 == V0, V21 == V10, P_s-{F}(V22,V23), V13 == V23, V23 == V5, V4 == V23, V23 == V0, V23 == V10, V23 == V18, P_s-{F}(V24,V23), P_s-{F}(V25,V23), P_s-{F}(V26,V23), P_s-{F}(V27,V28), V28 == V23, V28 == V13, V28 == V0, V28 == V10, P_s-{F}(V29,V30), V30 == V15, V30 == V0, V30 == V10, P_s-{F}(V31,V32), V30 == V32, V32 == V0, V32 == V10, P_s-{F}(V33,V34), V34 == V18, V34 == V1, V34 == V2, V34 == V0, P_s-{F}(V35,V36), V36 == V23, V36 == V4, V36 == V5, V36 == V0, P_s-{F}(V37,V38), V38 == V7, V38 == V8, V38 == V0, P_s-{F}(V39,V40), V38 == V40, V40 == V8, V40 == V0, P_s-{F}(V41,V42), V42 == V18, V42 == V0, V42 == V23, P_s-{F}(V43,V44), V42 == V44, V44 == V0, V44 == V23, P_s-{F}(V45,V46), V46 == V18, V46 == V0, V46 == V23, P_s-{F}(V47,V48), V46 == V48, V48 == V0, V48 == V23, #-{F} V49 | P_s-{T}(V49,V18), P_s-{T}(V49,V21), P_s-{T}(V49,V0), P_s-{T}(V49,V10), P_s-{T}(V49,V23), P_s-{T}(V49,V28), P_s-{T}(V49,V15), P_s-{T}(V49,V8), P_s-{T}(V49,V7), P_s-{T}(V49,V30), P_s-{T}(V49,V32), P_s-{T}(V49,V34), P_s-{T}(V49,V2), P_s-{T}(V49,V36), P_s-{T}(V49,V5), P_s-{T}(V49,V38), P_s-{T}(V49,V40), P_s-{T}(V49,V42), P_s-{T}(V49,V44), P_s-{T}(V49,V46), P_s-{T}(V49,V48), P_s-{T}(V49,V12), P_s-{T}(V49,V17), P_s-{T}(V49,V20), P_s-{T}(V49,V49), P_s-{T}(V49,V14), P_s-{T}(V49,V22), P_s-{T}(V49,V27), P_s-{T}(V49,V16), P_s-{T}(V49,V29), P_s-{T}(V49,V31), P_s-{T}(V49,V19), P_s-{T}(V49,V3), P_s-{T}(V49,V33), P_s-{T}(V49,V24), P_s-{T}(V49,V6), P_s-{T}(V49,V35), P_s-{T}(V49,V9), P_s-{T}(V49,V37), P_s-{T}(V49,V39), P_s-{T}(V49,V25), P_s-{T}(V49,V41), P_s-{T}(V49,V43), P_s-{T}(V49,V26), P_s-{T}(V49,V45), P_s-{T}(V49,V47)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #417: 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 == V51, V51 == 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, V146 == V148, V148 == V150, V150 == V152, V152 == V154, V154 == V156, V156 == V158, V158 == V160, V160 == V162; #338 ), references = 1, size of lhs = 172:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V0,V2), V0 == V2, r-{F}(V2,V0), P_s-{F}(V3,V2), r-{F}(V0,V4), r-{F}(V4,V0), r-{F}(V0,V5), V0 == V5, r-{F}(V5,V0), P_s-{F}(V6,V5), r-{F}(V0,V7), r-{F}(V7,V0), r-{F}(V0,V8), V0 == V8, r-{F}(V8,V0), P_s-{F}(V9,V8), r-{F}(V0,V10), V10 == V0, r-{F}(V10,V0), r-{F}(V10,V11), r-{F}(V11,V10), P_s-{F}(V12,V10), r-{F}(V10,V13), r-{F}(V13,V10), P_s-{F}(V14,V10), r-{F}(V10,V15), r-{F}(V15,V10), P_s-{F}(V16,V10), P_s-{F}(V17,V10), P_s-{F}(V18,V8), P_s-{F}(V19,V7), P_s-{F}(V20,V2), P_s-{F}(V21,V5), P_s-{F}(V22,V23), V23 == V0, P_s-{F}(V24,V23), P_s-{F}(V25,V26), V26 == V0, P_s-{F}(V27,V26), P_s-{F}(V28,V29), V11 == V29, V29 == V2, V1 == V29, V29 == V0, V29 == V10, V23 == V29, V26 == V29, P_s-{F}(V30,V29), P_s-{F}(V31,V30), P_s-{F}(V32,V29), P_s-{F}(V33,V32), P_s-{F}(V34,V35), V35 == V29, V35 == V11, V35 == V0, V35 == V10, P_s-{F}(V36,V35), P_s-{F}(V37,V36), P_s-{F}(V38,V39), V13 == V39, V39 == V5, V4 == V39, V39 == V0, V39 == V10, V39 == V29, V23 == V39, V26 == V39, P_s-{F}(V40,V39), P_s-{F}(V41,V40), P_s-{F}(V42,V39), P_s-{F}(V43,V42), P_s-{F}(V44,V39), P_s-{F}(V45,V44), P_s-{F}(V46,V39), P_s-{F}(V47,V46), P_s-{F}(V48,V49), V49 == V39, V49 == V13, V49 == V0, V49 == V10, P_s-{F}(V50,V49), P_s-{F}(V51,V50), P_s-{F}(V52,V53), V53 == V15, V53 == V0, V53 == V10, P_s-{F}(V54,V53), P_s-{F}(V55,V54), P_s-{F}(V56,V57), V53 == V57, V57 == V0, V57 == V10, P_s-{F}(V58,V57), P_s-{F}(V59,V58), P_s-{F}(V60,V61), V61 == V29, V61 == V1, V61 == V2, V61 == V0, P_s-{F}(V62,V61), P_s-{F}(V63,V62), P_s-{F}(V64,V65), V65 == V39, V65 == V4, V65 == V5, V65 == V0, P_s-{F}(V66,V65), P_s-{F}(V67,V66), P_s-{F}(V68,V69), V69 == V7, V69 == V8, V69 == V0, P_s-{F}(V70,V69), P_s-{F}(V71,V70), P_s-{F}(V72,V73), V69 == V73, V73 == V8, V73 == V0, P_s-{F}(V74,V73), P_s-{F}(V75,V74), P_s-{F}(V76,V77), V23 == V77, V77 == V0, V77 == V39, P_s-{F}(V78,V77), P_s-{F}(V79,V78), P_s-{F}(V80,V81), V26 == V81, V81 == V0, V81 == V39, P_s-{F}(V82,V81), P_s-{F}(V83,V82), P_s-{F}(V84,V85), V28 == V85, V34 == V85, V17 == V85, V38 == V85, V48 == V85, V18 == V85, V19 == V85, V52 == V85, V56 == V85, V60 == V85, V20 == V85, V64 == V85, V21 == V85, V68 == V85, V72 == V85, V24 == V85, V76 == V85, V27 == V85, V80 == V85, V31 == V85, V37 == V85, V84 == V85, V41 == V85, V51 == V85, V55 == V85, V59 == V85, V33 == V85, V63 == V85, V43 == V85, V67 == V85, V71 == V85, V75 == V85, V45 == V85, V79 == V85, V47 == V85, V83 == V85 | P_s-{T}(V85,V0), P_s-{T}(V85,V15), P_s-{T}(V85,V12), P_s-{T}(V85,V14), P_s-{T}(V85,V16), P_s-{T}(V85,V3), P_s-{T}(V85,V6), P_s-{T}(V85,V9), P_s-{T}(V85,V22), P_s-{T}(V85,V25)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #509: 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 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V51, V51 == V59, V59 == V60, V60 == V61, V61 == V63, V63 == V64, V64 == V65, V65 == V67, V67 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V74, V74 == V75, V75 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V31, V31 == V32, V32 == V33, V33 == V57, V57 == V41, V41 == V54, V54 == V56, V56 == V58, V58 == V44, V52 == V43, V44 == V47, V43 == V46, V47 == V50, V46 == V49, V50 == V100, V49 == V101; #418 ), references = 1, size of lhs = 149:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V0,V2), r-{F}(V2,V0), r-{F}(V0,V3), r-{F}(V3,V0), r-{F}(V0,V4), V4 == V0, r-{F}(V4,V0), P_s-{F}(V0,V4), r-{F}(V4,V5), r-{F}(V5,V4), r-{F}(V4,V6), r-{F}(V6,V4), P_s-{F}(V7,V4), P_s-{F}(V8,V4), P_s-{F}(V9,V3), P_s-{F}(V10,V4), P_s-{F}(V11,V4), P_s-{F}(V12,V4), P_s-{F}(V13,V14), V14 == V0, P_s-{F}(V15,V14), P_s-{F}(V16,V17), V5 == V17, V1 == V17, V17 == V0, V4 == V17, V14 == V17, 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), V23 == V17, V23 == V5, V23 == V0, V23 == V4, P_s-{F}(V24,V23), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V6 == V27, V2 == V27, V27 == V0, V27 == V17, V4 == V27, V14 == V27, P_s-{F}(V28,V27), P_s-{F}(V29,V28), P_s-{F}(V30,V27), P_s-{F}(V31,V30), P_s-{F}(V32,V27), P_s-{F}(V33,V32), P_s-{F}(V34,V27), P_s-{F}(V35,V34), P_s-{F}(V36,V37), V37 == V27, V37 == V6, V37 == V0, V37 == V4, P_s-{F}(V38,V37), P_s-{F}(V39,V38), P_s-{F}(V40,V41), V41 == V0, V41 == V4, P_s-{F}(V42,V41), P_s-{F}(V43,V42), P_s-{F}(V44,V45), V41 == V45, V45 == V0, V45 == V4, P_s-{F}(V46,V45), P_s-{F}(V47,V46), P_s-{F}(V48,V49), V49 == V17, V49 == V1, V49 == V4, V49 == V0, P_s-{F}(V50,V49), P_s-{F}(V51,V50), P_s-{F}(V52,V53), V53 == V27, V53 == V2, V53 == V4, V53 == V0, P_s-{F}(V54,V53), P_s-{F}(V55,V54), P_s-{F}(V56,V57), V57 == V3, V57 == V4, V57 == V0, P_s-{F}(V58,V57), P_s-{F}(V59,V58), P_s-{F}(V60,V61), V57 == V61, V61 == V4, V61 == V0, P_s-{F}(V62,V61), P_s-{F}(V63,V62), P_s-{F}(V64,V65), V4 == V65, V65 == V0, V65 == V27, P_s-{F}(V66,V65), P_s-{F}(V67,V66), P_s-{F}(V68,V69), V14 == V69, V69 == V0, V69 == V27, P_s-{F}(V70,V69), P_s-{F}(V71,V70), P_s-{F}(V72,V73), V16 == V73, V22 == V73, V7 == V73, V26 == V73, V36 == V73, V8 == V73, V9 == V73, V40 == V73, V44 == V73, V48 == V73, V10 == V73, V52 == V73, V11 == V73, V56 == V73, V60 == V73, V12 == V73, V64 == V73, V15 == V73, V68 == V73, V19 == V73, V25 == V73, V72 == V73, V29 == V73, V39 == V73, V43 == V73, V47 == V73, V21 == V73, V51 == V73, V31 == V73, V55 == V73, V59 == V73, V63 == V73, V33 == V73, V67 == V73, V35 == V73, V71 == V73 | P_s-{T}(V73,V13)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #601: 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 == V1, V1 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V2 == V93, V92 == V95, V93 == V96; #511 ), references = 1, size of lhs = 125:
% 65.34/65.57 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), P_s-{F}(V8,V1), P_s-{F}(V9,V10), V10 == V0, V1 == V10, P_s-{F}(V11,V10), P_s-{F}(V12,V11), P_s-{F}(V13,V10), P_s-{F}(V14,V13), P_s-{F}(V15,V16), V16 == V10, V16 == V0, V16 == V1, P_s-{F}(V17,V16), P_s-{F}(V18,V17), P_s-{F}(V19,V20), V20 == V0, V20 == V10, V1 == V20, 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), V30 == V20, V30 == V0, V30 == V1, P_s-{F}(V31,V30), P_s-{F}(V32,V31), P_s-{F}(V33,V34), V34 == V0, V34 == V1, P_s-{F}(V35,V34), P_s-{F}(V36,V35), P_s-{F}(V37,V38), V34 == V38, V38 == V0, V38 == V1, P_s-{F}(V39,V38), P_s-{F}(V40,V39), P_s-{F}(V41,V42), V42 == V10, V42 == V1, V42 == V0, P_s-{F}(V43,V42), P_s-{F}(V44,V43), P_s-{F}(V45,V46), V46 == V20, V46 == V1, V46 == V0, 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,V51), P_s-{F}(V53,V54), V50 == V54, V54 == V1, V54 == V0, P_s-{F}(V55,V54), P_s-{F}(V56,V55), P_s-{F}(V57,V58), V1 == V58, V58 == V0, V58 == V20, P_s-{F}(V59,V58), P_s-{F}(V60,V59), P_s-{F}(V61,V62), V1 == V62, V62 == V0, V62 == V20, P_s-{F}(V63,V62), P_s-{F}(V64,V63), P_s-{F}(V65,V66), V9 == V66, V15 == V66, V2 == V66, V19 == V66, V29 == V66, V3 == V66, V4 == V66, V33 == V66, V37 == V66, V41 == V66, V5 == V66, V45 == V66, V6 == V66, V49 == V66, V53 == V66, V7 == V66, V57 == V66, V8 == V66, V61 == V66, V12 == V66, V18 == V66, V65 == V66, V22 == V66, V32 == V66, V36 == V66, V40 == V66, V14 == V66, V44 == V66, V24 == V66, V48 == V66, V52 == V66, V56 == V66, V26 == V66, V60 == V66, V28 == V66, V64 == V66 | b-{T}(V0,V1)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #604: mergings( V0 == V3; #602 ), references = 14, size of lhs = 4:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3 | b-{T}(V2,V3)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #612: mergings( V2 == V3, V3 == V4, V4 == V5; #608 ), references = 1, size of lhs = 18:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), r-{F}(V5,V2), b-{F}(V5,V6), b-{F}(V1,V7), r-{F}(V7,V8), b-{F}(V8,V9), b-{F}(V9,V10), r-{F}(V7,V11), b-{F}(V11,V8), r-{F}(V1,V12), b-{F}(V13,V12), b-{F}(V14,V13), b-{F}(V14,V15), b-{F}(V15,V13), #-{F} V16 | P_s-{T}(V16,V7), P_s-{T}(V16,V8), P_s-{T}(V16,V11), P_s-{T}(V16,V1), P_s-{T}(V16,V2), P_s-{T}(V16,V5), P_s-{T}(V16,V12)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #622: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V20, V20 == V22, V22 == V24, V24 == V26, V26 == V28; #613 ), references = 1, size of lhs = 28:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V1,V4), b-{F}(V4,V2), P_s-{F}(V5,V3), r-{F}(V6,V3), b-{F}(V6,V7), b-{F}(V7,V8), b-{F}(V8,V9), b-{F}(V6,V10), r-{F}(V10,V11), b-{F}(V11,V12), b-{F}(V12,V13), r-{F}(V10,V14), b-{F}(V14,V11), P_s-{F}(V15,V10), P_s-{F}(V16,V14), P_s-{F}(V17,V6), r-{F}(V18,V7), b-{F}(V18,V19), P_s-{F}(V20,V18), #-{F} V21, V15 == V21, V16 == V21, V17 == V21, V20 == V21, V5 == V21 | P_s-{T}(V21,V11), P_s-{T}(V21,V7)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #633: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V19; #623 ), references = 2, size of lhs = 28:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), r-{F}(V3,V0), r-{F}(V3,V4), b-{F}(V4,V0), P_s-{F}(V5,V3), P_s-{F}(V6,V4), b-{F}(V7,V3), r-{F}(V7,V8), P_s-{F}(V9,V8), b-{F}(V7,V10), b-{F}(V10,V11), b-{F}(V11,V12), P_s-{F}(V13,V7), r-{F}(V14,V10), b-{F}(V14,V15), P_s-{F}(V16,V14), b-{F}(V17,V8), b-{F}(V18,V17), b-{F}(V18,V19), b-{F}(V19,V17), #-{F} V20, V5 == V20, V6 == V20, V13 == V20, V16 == V20, V9 == V20 | P_s-{T}(V20,V10)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #649: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V16; #636 ), references = 2, size of lhs = 34:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), r-{F}(V5,V0), b-{F}(V5,V6), P_s-{F}(V7,V5), b-{F}(V8,V0), b-{F}(V8,V9), b-{F}(V9,V10), b-{F}(V10,V11), r-{F}(V12,V9), b-{F}(V12,V13), P_s-{F}(V14,V8), b-{F}(V15,V8), b-{F}(V15,V16), V8 == V16, r-{F}(V16,V0), r-{F}(V16,V17), b-{F}(V17,V0), P_s-{F}(V18,V16), P_s-{F}(V19,V17), b-{F}(V16,V20), V8 == V20, V20 == V9, V20 == V12, P_s-{F}(V21,V20), #-{F} V22, V18 == V22, V19 == V22, V14 == V22, V7 == V22, V21 == V22 | r-{T}(V8,V16)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #657: mergings( V2 == V3, V3 == V4, V4 == V5; #653 ), references = 1, size of lhs = 39:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V0), V1 == V0, r-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), r-{F}(V1,V5), b-{F}(V5,V2), b-{F}(V1,V6), V6 == V1, r-{F}(V1,V7), V7 == V1, V7 == V6, b-{F}(V7,V8), V6 == V8, r-{F}(V1,V8), b-{F}(V8,V9), b-{F}(V9,V10), b-{F}(V7,V11), r-{F}(V1,V11), b-{F}(V11,V12), b-{F}(V12,V13), P_s-{F}(V14,V1), b-{F}(V15,V1), b-{F}(V15,V16), V16 == V0, V7 == V16, V16 == V1, P_s-{F}(V17,V16), b-{F}(V16,V18), b-{F}(V18,V19), r-{F}(V1,V20), V6 == V20, b-{F}(V20,V21), P_s-{F}(V22,V23), V23 == V16, V23 == V0, V23 == V1, #-{F} V24 | P_s-{T}(V24,V16), P_s-{T}(V24,V7), P_s-{T}(V24,V0), P_s-{T}(V24,V1), P_s-{T}(V24,V23), P_s-{T}(V24,V2), P_s-{T}(V24,V5), P_s-{T}(V24,V6), P_s-{T}(V24,V11), P_s-{T}(V24,V14), P_s-{T}(V24,V17), P_s-{T}(V24,V24), P_s-{T}(V24,V22)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #673: mergings( V0 == V1, V1 == V3, V3 == V28, V28 == V10, V10 == V2, V2 == V30, V30 == V32, V32 == V5, V5 == V34, V34 == V36, V36 == V38, V38 == V17, V17 == V40, V40 == V42; #658 ), references = 1, size of lhs = 50:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V0,V4), b-{F}(V4,V5), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V8), P_s-{F}(V9,V4), P_s-{F}(V0,V10), V0 == V10, r-{F}(V10,V0), r-{F}(V10,V1), r-{F}(V10,V4), r-{F}(V10,V11), b-{F}(V11,V0), b-{F}(V10,V12), V12 == V10, V0 == V12, V12 == V1, b-{F}(V13,V10), b-{F}(V13,V14), V0 == V14, V14 == V10, b-{F}(V14,V15), b-{F}(V15,V16), r-{F}(V10,V17), V12 == V17, b-{F}(V17,V18), P_s-{F}(V19,V14), P_s-{F}(V20,V10), P_s-{F}(V21,V11), P_s-{F}(V22,V12), P_s-{F}(V23,V14), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V26 == V14, V26 == V0, V26 == V10, P_s-{F}(V27,V26), P_s-{F}(V28,V29), V19 == V29, V20 == V29, V27 == V29, V21 == V29, V22 == V29, V9 == V29, V24 == V29, V28 == V29 | P_s-{T}(V29,V25)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #698: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V21, V21 == V28, V28 == V29, V29 == V30; #678 ), references = 3, size of lhs = 39:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), P_s-{F}(V0,V3), V0 == V3, r-{F}(V3,V0), b-{F}(V0,V3), b-{F}(V0,V4), r-{F}(V3,V5), b-{F}(V5,V6), P_s-{F}(V7,V3), P_s-{F}(V8,V9), V9 == V0, V9 == V3, P_s-{F}(V10,V9), P_s-{F}(V11,V9), P_s-{F}(V12,V9), P_s-{F}(V13,V12), P_s-{F}(V14,V15), V15 == V3, V0 == V15, V15 == V9, V15 == V5, P_s-{F}(V16,V17), V17 == V9, V17 == V0, V17 == V3, P_s-{F}(V18,V17), P_s-{F}(V19,V18), P_s-{F}(V20,V21), V10 == V21, V7 == V21, V16 == V21, V11 == V21, V14 == V21, V8 == V21, V13 == V21, V20 == V21, V19 == V21 | b-{T}(V3,V9)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #708: mergings( V0 == V2, V2 == V4, V4 == V5, V5 == V6; #703 ), references = 1, size of lhs = 47:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), V2 == V0, r-{F}(V0,V2), P_s-{F}(V3,V2), P_s-{F}(V4,V2), b-{F}(V0,V5), b-{F}(V5,V6), V6 == V0, V2 == V6, V6 == V1, P_s-{F}(V7,V6), r-{F}(V1,V8), V6 == V8, b-{F}(V8,V9), P_s-{F}(V10,V11), V0 == V11, V11 == V2, P_s-{F}(V12,V13), V13 == V11, V13 == V0, V13 == V2, P_s-{F}(V14,V15), V15 == V11, V13 == V15, V15 == V0, V15 == V2, P_s-{F}(V16,V17), V17 == V6, V17 == V2, V17 == V0, P_s-{F}(V18,V19), V19 == V6, V17 == V19, V19 == V2, V19 == V0, #-{F} V20, V4 == V20, V10 == V20, V12 == V20, V14 == V20, #-{F} V21, V7 == V21, V3 == V21, V16 == V21, V18 == V21 | b-{T}(V2,V0)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #722: mergings( V2 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V21, V21 == V22, V22 == V23; #713 ), references = 1, size of lhs = 61:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), P_s-{F}(V0,V3), V0 == V3, b-{F}(V0,V3), r-{F}(V3,V0), b-{F}(V0,V4), r-{F}(V3,V5), b-{F}(V5,V6), P_s-{F}(V7,V3), b-{F}(V0,V8), b-{F}(V8,V9), V9 == V0, V9 == V3, r-{F}(V0,V9), b-{F}(V3,V9), P_s-{F}(V10,V9), P_s-{F}(V11,V9), r-{F}(V8,V12), b-{F}(V12,V13), r-{F}(V14,V9), V14 == V3, b-{F}(V14,V3), b-{F}(V3,V15), V9 == V15, V15 == V0, V15 == V3, b-{F}(V3,V16), V14 == V16, V16 == V3, V16 == V9, r-{F}(V3,V17), V15 == V17, b-{F}(V17,V18), r-{F}(V3,V19), b-{F}(V19,V20), P_s-{F}(V21,V22), P_s-{F}(V23,V24), V24 == V3, V0 == V24, V24 == V5, P_s-{F}(V25,V26), V26 == V0, V26 == V3, P_s-{F}(V27,V26), P_s-{F}(V28,V27), P_s-{F}(V29,V30), V30 == V0, V30 == V9, P_s-{F}(V31,V32), V30 == V32, V32 == V0, V32 == V9, P_s-{F}(V33,V34), V34 == V9, V34 == V0, P_s-{F}(V35,V36), V34 == V36, V36 == V9, V36 == V0 | P_s-{T}(V22,V0), P_s-{T}(V22,V8), P_s-{T}(V22,V12), P_s-{T}(V22,V15), P_s-{T}(V22,V14), P_s-{T}(V22,V9), P_s-{T}(V22,V16), P_s-{T}(V22,V19), P_s-{T}(V22,V3), P_s-{T}(V22,V24), P_s-{T}(V22,V26), P_s-{T}(V22,V22), P_s-{T}(V22,V7), P_s-{T}(V22,V25), P_s-{T}(V22,V23), P_s-{T}(V22,V21), P_s-{T}(V22,V28), P_s-{T}(V22,V30), P_s-{T}(V22,V32), P_s-{T}(V22,V34), P_s-{T}(V22,V36), P_s-{T}(V22,V11), P_s-{T}(V22,V29), P_s-{T}(V22,V31), P_s-{T}(V22,V10), P_s-{T}(V22,V33), P_s-{T}(V22,V35)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #751: mergings( V0 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V19, V19 == V20, V20 == V21, V21 == V45, V45 == V47, V47 == V49, V49 == V51, V51 == V53, V53 == V55, V55 == V57, V57 == V59, V59 == V61, V61 == V63, V63 == V65, V65 == V67, V67 == V69, V69 == V71, V71 == V73, V73 == V75, V75 == V77, V77 == V79, V79 == V81; #723 ), references = 1, size of lhs = 99:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), P_s-{F}(V0,V3), V0 == V3, b-{F}(V0,V3), r-{F}(V3,V0), b-{F}(V0,V4), r-{F}(V3,V5), b-{F}(V5,V6), P_s-{F}(V7,V3), b-{F}(V0,V8), b-{F}(V8,V9), V9 == V0, V9 == V3, r-{F}(V0,V9), b-{F}(V3,V9), r-{F}(V8,V10), b-{F}(V10,V11), r-{F}(V12,V9), V12 == V3, b-{F}(V12,V3), b-{F}(V3,V13), V9 == V13, V13 == V0, V13 == V3, b-{F}(V3,V14), V12 == V14, V14 == V3, V14 == V9, r-{F}(V3,V15), V13 == V15, b-{F}(V15,V16), r-{F}(V3,V17), b-{F}(V17,V18), P_s-{F}(V19,V8), P_s-{F}(V20,V13), P_s-{F}(V21,V9), P_s-{F}(V22,V14), P_s-{F}(V23,V3), P_s-{F}(V24,V9), P_s-{F}(V25,V24), P_s-{F}(V26,V9), P_s-{F}(V27,V26), P_s-{F}(V28,V29), P_s-{F}(V29,V30), V30 == V0, V30 == V3, P_s-{F}(V31,V30), P_s-{F}(V32,V30), P_s-{F}(V33,V32), P_s-{F}(V34,V35), V35 == V0, V35 == V9, P_s-{F}(V36,V35), P_s-{F}(V37,V38), V38 == V9, V38 == V0, P_s-{F}(V39,V38), P_s-{F}(V40,V41), V41 == V3, V0 == V41, V41 == V5, P_s-{F}(V42,V41), P_s-{F}(V43,V42), P_s-{F}(V44,V45), V19 == V45, V20 == V45, V21 == V45, V22 == V45, V23 == V45, V40 == V45, V31 == V45, V44 == V45, V33 == V45, V43 == V45, V36 == V45, V39 == V45, V27 == V45, V25 == V45, P_s-{F}(V46,V45), P_s-{F}(V47,V46), V47 == V45, P_s-{F}(V48,V49), V49 == V0, V49 == V9, V49 == V35, V48 == V45, P_s-{F}(V50,V49), P_s-{F}(V51,V50), V51 == V45, P_s-{F}(V52,V53), V53 == V9, V53 == V0, V53 == V38, V52 == V45, P_s-{F}(V54,V53), P_s-{F}(V55,V54), V55 == V45 | P_s-{T}(V45,V0), P_s-{T}(V45,V10), P_s-{T}(V45,V12), P_s-{T}(V45,V17), P_s-{T}(V45,V7), P_s-{T}(V45,V28), P_s-{T}(V45,V34), P_s-{T}(V45,V37)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #788: mergings( V8 == V10, V10 == V11, V11 == V12, V12 == V17, V17 == V18, V18 == V19, V19 == V27, V27 == V29, V29 == V31, V31 == V33, V33 == V35, V35 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V0, V0 == V9, V9 == V15, V15 == V25, V25 == V20, V20 == V7, V7 == V55, V3 == V56, V55 == V61, V56 == V62; #752 ), references = 1, size of lhs = 90:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V0,V3), b-{F}(V0,V4), r-{F}(V4,V0), b-{F}(V4,V5), V5 == V0, r-{F}(V0,V5), b-{F}(V0,V6), b-{F}(V0,V7), P_s-{F}(V8,V4), P_s-{F}(V9,V5), b-{F}(V0,V10), V10 == V0, V10 == V5, b-{F}(V10,V5), r-{F}(V10,V0), P_s-{F}(V0,V10), r-{F}(V10,V11), b-{F}(V11,V12), b-{F}(V10,V13), V5 == V13, V13 == V0, V13 == V10, b-{F}(V10,V14), V14 == V10, V14 == V5, V0 == V14, r-{F}(V10,V15), V13 == V15, b-{F}(V15,V16), P_s-{F}(V17,V13), P_s-{F}(V18,V14), P_s-{F}(V19,V10), P_s-{F}(V10,V20), V20 == V0, V20 == V10, P_s-{F}(V21,V20), P_s-{F}(V22,V10), P_s-{F}(V23,V5), P_s-{F}(V24,V23), P_s-{F}(V25,V5), P_s-{F}(V26,V25), P_s-{F}(V27,V20), P_s-{F}(V28,V27), P_s-{F}(V29,V30), V30 == V5, V30 == V0, P_s-{F}(V31,V30), P_s-{F}(V32,V33), V33 == V10, V0 == V33, V33 == V11, P_s-{F}(V34,V33), P_s-{F}(V35,V34), P_s-{F}(V36,V37), V8 == V37, V17 == V37, V9 == V37, V18 == V37, V19 == V37, V32 == V37, V21 == V37, V36 == V37, V28 == V37, V35 == V37, V22 == V37, V31 == V37, V26 == V37, V24 == V37, P_s-{F}(V38,V37), P_s-{F}(V39,V38), V39 == V37, P_s-{F}(V40,V41), V41 == V0, V41 == V5, V41 == V10, V40 == V37, P_s-{F}(V42,V41), P_s-{F}(V43,V42), V43 == V37, P_s-{F}(V44,V45), V45 == V5, V45 == V0, V45 == V30, V44 == V37, P_s-{F}(V46,V45), P_s-{F}(V47,V46), V47 == V37 | P_s-{T}(V37,V29)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #828: 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 == V1, V1 == V37, V37 == V43, V43 == V50, V50 == V51, V32 == V52, V51 == V55, V52 == V56, V55 == V58, V56 == V59; #790 ), references = 2, size of lhs = 86:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V0,V3), b-{F}(V0,V4), V4 == V0, r-{F}(V4,V0), P_s-{F}(V0,V4), r-{F}(V4,V5), b-{F}(V5,V6), b-{F}(V0,V7), r-{F}(V7,V0), b-{F}(V7,V8), V8 == V0, V4 == V8, b-{F}(V4,V8), b-{F}(V0,V9), b-{F}(V4,V10), V8 == V10, V10 == V0, V10 == V4, b-{F}(V4,V11), V11 == V4, V11 == V8, V0 == V11, r-{F}(V4,V12), V10 == V12, b-{F}(V12,V13), b-{F}(V0,V14), P_s-{F}(V15,V7), P_s-{F}(V16,V10), P_s-{F}(V17,V8), P_s-{F}(V18,V11), P_s-{F}(V19,V4), P_s-{F}(V4,V20), V20 == V0, V20 == V4, P_s-{F}(V21,V20), P_s-{F}(V22,V4), P_s-{F}(V23,V4), P_s-{F}(V24,V8), P_s-{F}(V25,V24), P_s-{F}(V26,V8), P_s-{F}(V27,V26), P_s-{F}(V28,V20), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V31 == V4, V0 == V31, V31 == V5, P_s-{F}(V32,V31), P_s-{F}(V33,V32), P_s-{F}(V34,V35), V15 == V35, V16 == V35, V17 == V35, V18 == V35, V19 == V35, V30 == V35, V21 == V35, V34 == V35, V29 == V35, V33 == V35, V22 == V35, V23 == V35, V27 == V35, V25 == V35, P_s-{F}(V36,V35), P_s-{F}(V37,V36), V37 == V35, P_s-{F}(V38,V39), V39 == V0, V39 == V8, V39 == V4, V38 == V35, P_s-{F}(V40,V39), P_s-{F}(V41,V40), V41 == V35, P_s-{F}(V42,V43), V43 == V8, V43 == V0, V43 == V4, V42 == V35, P_s-{F}(V44,V43), P_s-{F}(V45,V44), V45 == V35 | b-{T}(V0,V8)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #947: 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 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V82 == V94, V93 == V96, V94 == V97, V96 == 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 == V116, V116 == V117, V117 == V118, V118 == V120, V120 == V127, V127 == V128, V128 == V129; #835 ), references = 1, size of lhs = 105:
% 65.34/65.57 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(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}(V1,V13), V13 == V0, V13 == V1, P_s-{F}(V14,V13), P_s-{F}(V15,V1), P_s-{F}(V16,V1), P_s-{F}(V17,V13), P_s-{F}(V18,V17), P_s-{F}(V19,V20), V20 == V0, V1 == V20, P_s-{F}(V21,V20), P_s-{F}(V22,V21), P_s-{F}(V23,V20), P_s-{F}(V24,V23), P_s-{F}(V25,V26), P_s-{F}(V27,V26), P_s-{F}(V28,V26), P_s-{F}(V29,V26), P_s-{F}(V30,V26), P_s-{F}(V31,V26), P_s-{F}(V32,V26), P_s-{F}(V33,V26), P_s-{F}(V34,V26), P_s-{F}(V35,V26), P_s-{F}(V36,V26), P_s-{F}(V37,V26), P_s-{F}(V38,V26), P_s-{F}(V39,V40), V40 == V0, V40 == V1, P_s-{F}(V41,V40), P_s-{F}(V42,V41), P_s-{F}(V43,V44), V44 == V0, V44 == V1, P_s-{F}(V45,V44), P_s-{F}(V46,V45), P_s-{F}(V47,V48), V48 == V1, V48 == V0, P_s-{F}(V49,V48), P_s-{F}(V50,V49), P_s-{F}(V51,V52), V52 == V1, V52 == V0, P_s-{F}(V53,V52), P_s-{F}(V54,V53), P_s-{F}(V55,V56), V1 == V56, V56 == V0, P_s-{F}(V57,V56), P_s-{F}(V58,V57), P_s-{F}(V59,V60), V1 == V60, V60 == V0, P_s-{F}(V61,V60), P_s-{F}(V62,V61), P_s-{F}(V63,V64), V64 == V1, V64 == V0, P_s-{F}(V65,V64), P_s-{F}(V66,V64), P_s-{F}(V67,V64), P_s-{F}(V68,V64), P_s-{F}(V69,V64), P_s-{F}(V70,V69), P_s-{F}(V71,V72), V72 == V1, V72 == V0, P_s-{F}(V73,V74), V74 == V0, V74 == V1, P_s-{F}(V75,V74), P_s-{F}(V76,V75), P_s-{F}(V77,V78), V78 == V1, V78 == V0, P_s-{F}(V79,V78), P_s-{F}(V80,V79), P_s-{F}(V81,V82), V82 == V0, V82 == V1, P_s-{F}(V83,V82), P_s-{F}(V84,V83), P_s-{F}(V85,V86), V86 == V0, V86 == V1, P_s-{F}(V87,V86), P_s-{F}(V88,V87) | P_s-{T}(V26,V20), P_s-{T}(V26,V0), P_s-{T}(V26,V1), P_s-{T}(V26,V40), P_s-{T}(V26,V44), P_s-{T}(V26,V48), P_s-{T}(V26,V52), P_s-{T}(V26,V56), P_s-{T}(V26,V60), P_s-{T}(V26,V19), P_s-{T}(V26,V26), P_s-{T}(V26,V2), P_s-{T}(V26,V39), P_s-{T}(V26,V3), P_s-{T}(V26,V4), P_s-{T}(V26,V43), P_s-{T}(V26,V5), P_s-{T}(V26,V47), P_s-{T}(V26,V6), P_s-{T}(V26,V51), P_s-{T}(V26,V7), P_s-{T}(V26,V55), P_s-{T}(V26,V8), P_s-{T}(V26,V59), P_s-{T}(V26,V22), P_s-{T}(V26,V25), P_s-{T}(V26,V27), P_s-{T}(V26,V42), P_s-{T}(V26,V46), P_s-{T}(V26,V31), P_s-{T}(V26,V24), P_s-{T}(V26,V32), P_s-{T}(V26,V28), P_s-{T}(V26,V50), P_s-{T}(V26,V54), P_s-{T}(V26,V33), P_s-{T}(V26,V29), P_s-{T}(V26,V58), P_s-{T}(V26,V30), P_s-{T}(V26,V62), P_s-{T}(V26,V64), P_s-{T}(V26,V65), P_s-{T}(V26,V9), P_s-{T}(V26,V66), P_s-{T}(V26,V63), P_s-{T}(V26,V70), P_s-{T}(V26,V34), P_s-{T}(V26,V72), P_s-{T}(V26,V74), P_s-{T}(V26,V10), P_s-{T}(V26,V73), P_s-{T}(V26,V71), P_s-{T}(V26,V35), P_s-{T}(V26,V76), P_s-{T}(V26,V11), P_s-{T}(V26,V67), P_s-{T}(V26,V68), P_s-{T}(V26,V12), P_s-{T}(V26,V77), P_s-{T}(V26,V14), P_s-{T}(V26,V18), P_s-{T}(V26,V80), P_s-{T}(V26,V15), P_s-{T}(V26,V16), P_s-{T}(V26,V37), P_s-{T}(V26,V36), P_s-{T}(V26,V38), P_s-{T}(V26,V82), P_s-{T}(V26,V81), P_s-{T}(V26,V84), P_s-{T}(V26,V86), P_s-{T}(V26,V85), P_s-{T}(V26,V88)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1107: 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 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V80 == V92, V91 == V94, V92 == V95, V94 == 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 == V114, V114 == V115, V115 == V116, V116 == V118, V118 == V125, V125 == V126, V126 == V127, V127 == 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, V290 == V292; #948 ), references = 1, size of lhs = 199:
% 65.34/65.57 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(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}(V1,V13), V13 == V0, 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,V13), P_s-{F}(V20,V19), P_s-{F}(V21,V13), P_s-{F}(V22,V21), P_s-{F}(V23,V24), P_s-{F}(V24,V25), V25 == V0, V1 == V25, P_s-{F}(V26,V25), P_s-{F}(V27,V25), P_s-{F}(V28,V27), P_s-{F}(V29,V25), P_s-{F}(V30,V29), P_s-{F}(V31,V32), P_s-{F}(V32,V33), V33 == V0, V33 == V1, 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 == V0, V39 == V1, 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, 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, P_s-{F}(V52,V51), P_s-{F}(V53,V51), P_s-{F}(V54,V53), P_s-{F}(V55,V56), P_s-{F}(V56,V57), V1 == V57, V57 == V0, P_s-{F}(V58,V57), P_s-{F}(V59,V57), P_s-{F}(V60,V59), P_s-{F}(V61,V62), P_s-{F}(V62,V63), V1 == V63, V63 == V0, P_s-{F}(V64,V63), P_s-{F}(V65,V63), P_s-{F}(V66,V65), P_s-{F}(V67,V68), P_s-{F}(V68,V69), V69 == V1, V69 == V0, P_s-{F}(V70,V69), P_s-{F}(V71,V69), P_s-{F}(V72,V71), P_s-{F}(V73,V69), P_s-{F}(V74,V73), P_s-{F}(V75,V69), P_s-{F}(V76,V75), P_s-{F}(V77,V69), P_s-{F}(V78,V77), P_s-{F}(V79,V69), P_s-{F}(V80,V79), P_s-{F}(V81,V82), P_s-{F}(V82,V83), V83 == V0, V83 == V1, P_s-{F}(V84,V83), P_s-{F}(V85,V83), P_s-{F}(V86,V85), P_s-{F}(V87,V88), P_s-{F}(V88,V89), V89 == V1, V89 == V0, P_s-{F}(V90,V89), P_s-{F}(V91,V90), P_s-{F}(V92,V93), P_s-{F}(V93,V94), V94 == V0, V94 == V1, P_s-{F}(V95,V94), P_s-{F}(V96,V94), P_s-{F}(V97,V96), P_s-{F}(V98,V99), P_s-{F}(V99,V100), V100 == V0, V100 == V1, P_s-{F}(V101,V100), P_s-{F}(V102,V100), P_s-{F}(V103,V102), P_s-{F}(V104,V105), V26 == V105, V16 == V105, V17 == V105, V18 == V105, V34 == V105, V40 == V105, V46 == V105, V52 == V105, V58 == V105, V64 == V105, V28 == V105, V104 == V105, V36 == V105, V42 == V105, V48 == V105, V54 == V105, V60 == V105, V66 == V105, V70 == V105, V74 == V105, V76 == V105, V72 == V105, V84 == V105, V86 == V105, V78 == V105, V80 == V105, V91 == V105, V20 == V105, V95 == V105, V97 == V105, V101 == V105, V103 == V105, P_s-{F}(V106,V105), P_s-{F}(V107,V106), V107 == V105, P_s-{F}(V108,V105), P_s-{F}(V109,V108), V109 == V105, P_s-{F}(V110,V105), P_s-{F}(V111,V110), V111 == V105, P_s-{F}(V112,V105), P_s-{F}(V113,V112), V113 == V105, P_s-{F}(V114,V105), P_s-{F}(V115,V114), V115 == V105, P_s-{F}(V116,V105), P_s-{F}(V117,V116), V117 == V105, P_s-{F}(V118,V105), P_s-{F}(V119,V118), V119 == V105, P_s-{F}(V120,V105), P_s-{F}(V121,V120), V121 == V105, P_s-{F}(V122,V105), P_s-{F}(V123,V122), V123 == V105, P_s-{F}(V124,V105), P_s-{F}(V125,V124), V125 == V105, P_s-{F}(V126,V105), P_s-{F}(V127,V126), V127 == V105, P_s-{F}(V128,V105), P_s-{F}(V129,V128), V129 == V105, P_s-{F}(V130,V105), P_s-{F}(V131,V130), V131 == V105, P_s-{F}(V132,V133), V133 == V1, V133 == V0, V132 == V105, P_s-{F}(V134,V133), P_s-{F}(V135,V134), V135 == V105 | P_s-{T}(V105,V0), P_s-{T}(V105,V2), P_s-{T}(V105,V3), P_s-{T}(V105,V4), P_s-{T}(V105,V5), P_s-{T}(V105,V6), P_s-{T}(V105,V7), P_s-{T}(V105,V8), P_s-{T}(V105,V23), P_s-{T}(V105,V31), P_s-{T}(V105,V37), P_s-{T}(V105,V30), P_s-{T}(V105,V43), P_s-{T}(V105,V49), P_s-{T}(V105,V55), P_s-{T}(V105,V61), P_s-{T}(V105,V9), P_s-{T}(V105,V67), P_s-{T}(V105,V10), P_s-{T}(V105,V81), P_s-{T}(V105,V11), P_s-{T}(V105,V12), P_s-{T}(V105,V22), P_s-{T}(V105,V87), P_s-{T}(V105,V14), P_s-{T}(V105,V15), P_s-{T}(V105,V92), P_s-{T}(V105,V98)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1317: 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 == V79, V79 == V76, V76 == V77, V77 == V78, V78 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V80 == V92, V91 == V94, V92 == V95, V94 == 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 == V114, V114 == V115, V115 == V116, V116 == V118, V118 == V124, V124 == V125, V125 == V126, V126 == V127, V127 == V128, V128 == V130, V130 == V132, V132 == V134, V134 == V135, V135 == V136, V136 == V137, V137 == V138, V138 == V139, V139 == V140, V140 == V141, V141 == V142, V142 == V143, V143 == V144, V144 == V145, V145 == V146, V146 == V147, V147 == V148, V148 == V149, V149 == V150, V150 == V151, V151 == V152, V152 == V153, V153 == V154, V154 == V155, V155 == V156, V156 == V157, V157 == V158, V158 == V159, V159 == V160, V160 == V161, V161 == V162, V162 == V163, V163 == V164, V164 == V165, V165 == V166, V166 == V167, V167 == V168, V168 == V169, V169 == V170, V170 == V171, V171 == V172, V172 == V173, V173 == V174, V174 == V175, V175 == V176, V176 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V93, V93 == V96, V96 == V181, V95 == V182, V121 == V183, V181 == V189, V182 == V190, V183 == V191, V189 == V195, V190 == V196, V191 == V197, V195 == V188, V196 == V187, V188 == V201, V187 == V202, V197 == V203, V201 == V207, V202 == V208, V203 == V209, V207 == V213, V208 == V214, V209 == V215, V213 == V219, V214 == V220, V215 == V221, V219 == V113, V113 == V225, V220 == V226, V221 == V227, V225 == V117, V117 == V239, V226 == V240, V227 == V241, V239 == V119, V119 == V120, V120 == V180, V240 == V179, V180 == V245, V179 == V246, V241 == V247, V245 == V122, V122 == V123, V123 == V250, V246 == V251, V247 == V252; #1108 ), references = 1, size of lhs = 138:
% 65.34/65.57 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V1,V5), V5 == V0, V5 == V1, P_s-{F}(V6,V5), P_s-{F}(V7,V5), P_s-{F}(V8,V5), P_s-{F}(V9,V5), P_s-{F}(V10,V5), P_s-{F}(V11,V5), P_s-{F}(V12,V5), P_s-{F}(V13,V5), P_s-{F}(V14,V5), P_s-{F}(V15,V5), P_s-{F}(V16,V5), P_s-{F}(V17,V16), P_s-{F}(V18,V5), P_s-{F}(V19,V18), P_s-{F}(V20,V5), P_s-{F}(V21,V20), P_s-{F}(V22,V5), P_s-{F}(V23,V22), P_s-{F}(V24,V5), P_s-{F}(V25,V24), P_s-{F}(V26,V5), P_s-{F}(V27,V26), P_s-{F}(V28,V5), P_s-{F}(V29,V28), P_s-{F}(V30,V5), P_s-{F}(V31,V30), P_s-{F}(V32,V5), P_s-{F}(V33,V32), P_s-{F}(V34,V5), P_s-{F}(V35,V34), P_s-{F}(V36,V5), P_s-{F}(V37,V36), P_s-{F}(V38,V5), P_s-{F}(V39,V38), P_s-{F}(V40,V5), P_s-{F}(V41,V40), P_s-{F}(V42,V5), P_s-{F}(V43,V42), P_s-{F}(V44,V5), P_s-{F}(V45,V44), P_s-{F}(V46,V5), P_s-{F}(V47,V46), P_s-{F}(V48,V49), P_s-{F}(V49,V50), V50 == V0, V50 == V1, P_s-{F}(V51,V50), P_s-{F}(V52,V50), P_s-{F}(V53,V52), P_s-{F}(V54,V55), V6 == V55, V2 == V55, V3 == V55, V4 == V55, V7 == V55, V8 == V55, V9 == V55, V10 == V55, V11 == V55, V12 == V55, V19 == V55, V54 == V55, V21 == V55, V23 == V55, V25 == V55, V27 == V55, V29 == V55, V31 == V55, V13 == V55, V35 == V55, V37 == V55, V33 == V55, V14 == V55, V43 == V55, V39 == V55, V41 == V55, V45 == V55, V17 == V55, V15 == V55, V47 == V55, V51 == V55, V53 == V55, P_s-{F}(V56,V55), P_s-{F}(V57,V56), V57 == V55, P_s-{F}(V58,V55), P_s-{F}(V59,V58), V59 == V55, P_s-{F}(V60,V55), P_s-{F}(V61,V60), V61 == V55, P_s-{F}(V62,V55), P_s-{F}(V63,V62), V63 == V55, P_s-{F}(V64,V55), P_s-{F}(V65,V64), V65 == V55, P_s-{F}(V66,V55), P_s-{F}(V67,V66), V67 == V55, P_s-{F}(V68,V55), P_s-{F}(V69,V68), V69 == V55, P_s-{F}(V70,V55), P_s-{F}(V71,V70), V71 == V55, P_s-{F}(V72,V55), P_s-{F}(V73,V72), V73 == V55, P_s-{F}(V74,V55), P_s-{F}(V75,V74), V75 == V55, P_s-{F}(V76,V55), P_s-{F}(V77,V76), V77 == V55, P_s-{F}(V78,V55), P_s-{F}(V79,V78), V79 == V55, P_s-{F}(V80,V55), P_s-{F}(V81,V80), V81 == V55, P_s-{F}(V82,V83), V83 == V1, V83 == V0, V82 == V55, P_s-{F}(V84,V83), P_s-{F}(V85,V84), V85 == V55 | P_s-{T}(V55,V48)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1528: 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, V1 == V86, V85 == V87, V86 == V88, V87 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V2, V2 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V114, V114 == V116, V116 == 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 == V136, V136 == V137, V137 == V138, V138 == V139, V139 == V140, V140 == V141, V141 == V142, V142 == V143, V143 == V144, V144 == V145, V145 == V146, V146 == V147, V147 == V148, V148 == V149, V149 == V150, V150 == V151, V151 == V152, V152 == V153, V153 == V154, V154 == V155, V155 == V156, V156 == V157, V157 == V158, V158 == V159, V159 == V160, V160 == V161, V161 == V162, V162 == V163, V163 == V164, V164 == V165, V165 == V166, V166 == V167, V167 == V168, V88 == V169, V107 == V170, V168 == V172, V169 == V173, V170 == V174, V172 == V176, V173 == V177, V174 == V178, V176 == V180, V177 == V181, V180 == V182, V181 == V183, V178 == V184, V182 == V186, V183 == V187, V184 == V188, V186 == V190, V187 == V191, V188 == V192, V190 == V194, V191 == V195, V192 == V196, V194 == V198, V198 == V199, V195 == V200, V196 == V201, V199 == V203, V203 == V204, V200 == V205, V201 == V206, V204 == V208, V208 == V209, V209 == V210, V205 == V211, V210 == V212, V211 == V213, V206 == V214, V212 == V215, V215 == V216, V216 == V217, V213 == V218, V214 == V219, V217 == V221, V218 == V222, V219 == V223; #1319 ), references = 2, size of lhs = 133:
% 65.34/65.57 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V1,V5), V5 == V0, V5 == V1, P_s-{F}(V6,V5), P_s-{F}(V7,V5), P_s-{F}(V8,V5), P_s-{F}(V9,V5), P_s-{F}(V10,V5), P_s-{F}(V11,V5), P_s-{F}(V12,V5), P_s-{F}(V13,V5), P_s-{F}(V14,V5), P_s-{F}(V15,V5), P_s-{F}(V16,V5), P_s-{F}(V17,V5), P_s-{F}(V18,V17), P_s-{F}(V19,V5), P_s-{F}(V20,V19), P_s-{F}(V21,V5), P_s-{F}(V22,V21), P_s-{F}(V23,V5), P_s-{F}(V24,V23), P_s-{F}(V25,V5), P_s-{F}(V26,V25), P_s-{F}(V27,V5), P_s-{F}(V28,V27), P_s-{F}(V29,V5), P_s-{F}(V30,V29), P_s-{F}(V31,V5), P_s-{F}(V32,V31), P_s-{F}(V33,V5), P_s-{F}(V34,V33), P_s-{F}(V35,V5), P_s-{F}(V36,V35), P_s-{F}(V37,V5), P_s-{F}(V38,V37), P_s-{F}(V39,V5), P_s-{F}(V40,V39), P_s-{F}(V41,V5), P_s-{F}(V42,V41), P_s-{F}(V43,V5), P_s-{F}(V44,V43), P_s-{F}(V45,V5), P_s-{F}(V46,V45), P_s-{F}(V47,V5), P_s-{F}(V48,V47), P_s-{F}(V49,V5), P_s-{F}(V50,V49), P_s-{F}(V51,V52), V6 == V52, V2 == V52, V3 == V52, V4 == V52, V7 == V52, V8 == V52, V9 == V52, V10 == V52, V11 == V52, V12 == V52, V20 == V52, V51 == V52, V22 == V52, V24 == V52, V26 == V52, V28 == V52, V30 == V52, V32 == V52, V13 == V52, V36 == V52, V38 == V52, V34 == V52, V14 == V52, V44 == V52, V40 == V52, V42 == V52, V46 == V52, V18 == V52, V15 == V52, V48 == V52, V16 == V52, V50 == V52, P_s-{F}(V53,V52), P_s-{F}(V54,V53), V54 == V52, P_s-{F}(V55,V52), P_s-{F}(V56,V55), V56 == V52, P_s-{F}(V57,V52), P_s-{F}(V58,V57), V58 == V52, P_s-{F}(V59,V52), P_s-{F}(V60,V59), V60 == V52, P_s-{F}(V61,V52), P_s-{F}(V62,V61), V62 == V52, P_s-{F}(V63,V52), P_s-{F}(V64,V63), V64 == V52, P_s-{F}(V65,V52), P_s-{F}(V66,V65), V66 == V52, P_s-{F}(V67,V52), P_s-{F}(V68,V67), V68 == V52, P_s-{F}(V69,V52), P_s-{F}(V70,V69), V70 == V52, P_s-{F}(V71,V52), P_s-{F}(V72,V71), V72 == V52, P_s-{F}(V73,V52), P_s-{F}(V74,V73), V74 == V52, P_s-{F}(V75,V52), P_s-{F}(V76,V75), V76 == V52, P_s-{F}(V77,V52), P_s-{F}(V78,V77), V78 == V52, P_s-{F}(V79,V80), V80 == V1, V80 == V0, V79 == V52, P_s-{F}(V81,V80), P_s-{F}(V82,V81), V82 == V52 | b-{T}(V1,V0)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1544: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V1; #1538 ), references = 1, size of lhs = 30:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), b-{F}(V0,V5), b-{F}(V5,V6), V0 == V6, V6 == V1, r-{F}(V6,V2), r-{F}(V6,V0), P_s-{F}(V7,V6), P_s-{F}(V8,V6), P_s-{F}(V9,V1), b-{F}(V10,V0), b-{F}(V10,V6), P_s-{F}(V11,V10), P_s-{F}(V12,V13), V13 == V2, V1 == V13, V10 == V13, V13 == V0, V13 == V6, #-{F} V14, V8 == V14, V9 == V14, V11 == V14, V7 == V14, V12 == V14 | r-{T}(V0,V6)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1551: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V1, V1 == V10, V10 == V11; #1539 ), references = 1, size of lhs = 32:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), b-{F}(V0,V5), b-{F}(V5,V0), b-{F}(V5,V6), V0 == V6, V6 == V1, V5 == V6, r-{F}(V6,V2), r-{F}(V6,V0), P_s-{F}(V7,V6), P_s-{F}(V8,V5), P_s-{F}(V9,V6), P_s-{F}(V10,V1), b-{F}(V0,V11), b-{F}(V11,V6), P_s-{F}(V12,V13), V13 == V2, V1 == V13, V5 == V13, V13 == V0, V13 == V6, #-{F} V14, V9 == V14, V10 == V14, V8 == V14, V7 == V14, V12 == V14 | r-{T}(V0,V6)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1570: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V13, V13 == V14, V14 == V15, V15 == V16; #1561 ), references = 1, size of lhs = 78:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V0,V2), V0 == V2, r-{F}(V2,V0), P_s-{F}(V3,V2), r-{F}(V0,V4), r-{F}(V4,V0), r-{F}(V0,V5), V0 == V5, r-{F}(V5,V0), P_s-{F}(V6,V5), b-{F}(V7,V0), b-{F}(V7,V8), b-{F}(V8,V9), b-{F}(V9,V10), b-{F}(V7,V11), b-{F}(V11,V12), b-{F}(V12,V13), b-{F}(V7,V14), b-{F}(V14,V15), b-{F}(V15,V16), b-{F}(V7,V17), b-{F}(V17,V18), b-{F}(V18,V19), b-{F}(V7,V20), V20 == V0, V7 == V20, r-{F}(V20,V8), r-{F}(V20,V11), r-{F}(V20,V14), r-{F}(V20,V17), r-{F}(V20,V0), r-{F}(V20,V21), r-{F}(V21,V20), P_s-{F}(V22,V20), r-{F}(V20,V23), r-{F}(V23,V20), P_s-{F}(V24,V20), P_s-{F}(V25,V26), V26 == V21, V26 == V0, V26 == V20, P_s-{F}(V27,V28), V26 == V28, V28 == V0, V28 == V20, P_s-{F}(V29,V30), V30 == V0, V30 == V2, V1 == V30, V7 == V30, V30 == V8, V30 == V20, P_s-{F}(V31,V32), V32 == V30, V32 == V2, V32 == V0, P_s-{F}(V33,V34), V23 == V34, V7 == V34, V34 == V11, V34 == V0, V34 == V20, P_s-{F}(V35,V36), V36 == V34, V36 == V0, V36 == V20, P_s-{F}(V37,V38), V38 == V4, V38 == V5, V38 == V0, P_s-{F}(V39,V40), V38 == V40, V40 == V5, V40 == V0, #-{F} V41 | P_s-{T}(V41,V0), P_s-{T}(V41,V21), P_s-{T}(V41,V17), P_s-{T}(V41,V5), P_s-{T}(V41,V4), P_s-{T}(V41,V7), P_s-{T}(V41,V14), P_s-{T}(V41,V20), P_s-{T}(V41,V26), P_s-{T}(V41,V28), P_s-{T}(V41,V30), P_s-{T}(V41,V1), P_s-{T}(V41,V2), P_s-{T}(V41,V32), P_s-{T}(V41,V34), P_s-{T}(V41,V23), P_s-{T}(V41,V36), P_s-{T}(V41,V38), P_s-{T}(V41,V40), P_s-{T}(V41,V22), P_s-{T}(V41,V41), P_s-{T}(V41,V25), P_s-{T}(V41,V27), P_s-{T}(V41,V29), P_s-{T}(V41,V3), P_s-{T}(V41,V31), P_s-{T}(V41,V24), P_s-{T}(V41,V33), P_s-{T}(V41,V35), P_s-{T}(V41,V6), P_s-{T}(V41,V37), P_s-{T}(V41,V39)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1603: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V50, V50 == V52, V52 == V54, V54 == V56, V56 == V58, V58 == V60, V60 == V62, V62 == V64, V64 == V66, V66 == V68, V68 == V70, V70 == V72, V72 == V74, V74 == V76, V76 == V78, V78 == V80, V80 == V82, V82 == V84, V84 == V86, V86 == V88, V88 == V90, V90 == V92, V92 == V94; #1571 ), references = 1, size of lhs = 123:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V0,V2), V0 == V2, r-{F}(V2,V0), r-{F}(V0,V3), r-{F}(V3,V0), r-{F}(V0,V4), V0 == V4, r-{F}(V4,V0), P_s-{F}(V5,V4), P_s-{F}(V6,V3), P_s-{F}(V7,V1), P_s-{F}(V8,V2), P_s-{F}(V9,V2), P_s-{F}(V10,V9), P_s-{F}(V11,V4), P_s-{F}(V12,V11), b-{F}(V13,V0), b-{F}(V13,V14), b-{F}(V14,V15), b-{F}(V15,V16), b-{F}(V13,V17), b-{F}(V17,V18), b-{F}(V18,V19), b-{F}(V13,V20), b-{F}(V20,V21), b-{F}(V21,V22), b-{F}(V13,V23), b-{F}(V23,V24), b-{F}(V24,V25), b-{F}(V13,V26), V26 == V0, V13 == V26, r-{F}(V26,V14), r-{F}(V26,V17), r-{F}(V26,V20), r-{F}(V26,V23), r-{F}(V26,V0), r-{F}(V26,V27), r-{F}(V27,V26), r-{F}(V26,V28), r-{F}(V28,V26), P_s-{F}(V29,V13), P_s-{F}(V30,V26), P_s-{F}(V31,V26), P_s-{F}(V32,V31), P_s-{F}(V33,V26), P_s-{F}(V34,V33), P_s-{F}(V35,V36), V36 == V0, V36 == V26, P_s-{F}(V37,V36), P_s-{F}(V38,V39), V39 == V2, V39 == V0, P_s-{F}(V40,V39), P_s-{F}(V41,V42), V42 == V0, V42 == V26, P_s-{F}(V43,V42), P_s-{F}(V44,V45), V45 == V4, V45 == V0, P_s-{F}(V46,V45), P_s-{F}(V47,V48), V48 == V27, V48 == V0, V48 == V26, V48 == V36, P_s-{F}(V49,V48), P_s-{F}(V50,V49), P_s-{F}(V51,V52), V52 == V0, V52 == V2, V1 == V52, V13 == V52, V52 == V14, V52 == V26, V39 == V52, P_s-{F}(V53,V52), P_s-{F}(V54,V53), P_s-{F}(V55,V56), V28 == V56, V13 == V56, V56 == V17, V56 == V0, V56 == V26, V42 == V56, P_s-{F}(V57,V56), P_s-{F}(V58,V57), P_s-{F}(V59,V60), V60 == V3, V60 == V4, V60 == V0, V60 == V45, P_s-{F}(V61,V60), P_s-{F}(V62,V61), P_s-{F}(V63,V64), V5 == V64, V6 == V64, V29 == V64, V30 == V64, V47 == V64, V37 == V64, V51 == V64, V7 == V64, V8 == V64, V40 == V64, V55 == V64, V43 == V64, V59 == V64, V46 == V64, V32 == V64, V63 == V64, V50 == V64, V54 == V64, V10 == V64, V34 == V64, V58 == V64, V12 == V64, V62 == V64 | P_s-{T}(V64,V0), P_s-{T}(V64,V27), P_s-{T}(V64,V23), P_s-{T}(V64,V20), P_s-{T}(V64,V28), P_s-{T}(V64,V35), P_s-{T}(V64,V38), P_s-{T}(V64,V41), P_s-{T}(V64,V44)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1645: mergings( V1 == V3, V3 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V15, V15 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V24, V24 == 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 == V0, V0 == V58, V58 == V2, V2 == V51, V51 == V54, V54 == V4, V4 == V59, V59 == V66, V66 == V69, V67 == V70, V69 == V72, V70 == V73; #1604 ), references = 1, size of lhs = 109:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), r-{F}(V0,V5), r-{F}(V5,V0), r-{F}(V0,V6), V0 == V6, r-{F}(V6,V0), r-{F}(V0,V7), r-{F}(V7,V0), r-{F}(V0,V8), V0 == V8, r-{F}(V8,V0), P_s-{F}(V9,V8), P_s-{F}(V10,V7), P_s-{F}(V11,V5), P_s-{F}(V12,V6), r-{F}(V0,V13), V13 == V0, r-{F}(V13,V0), r-{F}(V13,V14), b-{F}(V14,V15), b-{F}(V15,V16), r-{F}(V13,V17), b-{F}(V17,V18), b-{F}(V18,V19), P_s-{F}(V20,V13), P_s-{F}(V0,V21), V21 == V6, V21 == V0, V21 == V13, P_s-{F}(V22,V21), P_s-{F}(V23,V21), P_s-{F}(V24,V21), P_s-{F}(V25,V6), P_s-{F}(V26,V25), P_s-{F}(V27,V8), P_s-{F}(V28,V27), b-{F}(V29,V14), V29 == V13, b-{F}(V29,V17), b-{F}(V29,V0), b-{F}(V29,V13), P_s-{F}(V30,V29), P_s-{F}(V31,V13), P_s-{F}(V32,V31), P_s-{F}(V33,V13), P_s-{F}(V34,V33), P_s-{F}(V35,V36), V36 == V8, V36 == V0, P_s-{F}(V37,V36), P_s-{F}(V38,V39), V39 == V0, V39 == V13, V39 == V21, P_s-{F}(V40,V39), P_s-{F}(V41,V40), P_s-{F}(V42,V43), V43 == V0, V43 == V6, V5 == V43, V29 == V43, V43 == V14, V43 == V13, V21 == V43, P_s-{F}(V44,V43), P_s-{F}(V45,V44), P_s-{F}(V46,V47), V29 == V47, V47 == V17, V47 == V0, V47 == V13, V21 == V47, P_s-{F}(V48,V47), P_s-{F}(V49,V48), P_s-{F}(V50,V51), V51 == V7, V51 == V8, V51 == V0, V51 == V36, P_s-{F}(V52,V51), P_s-{F}(V53,V52), P_s-{F}(V54,V55), V9 == V55, V10 == V55, V30 == V55, V20 == V55, V38 == V55, V22 == V55, V42 == V55, V11 == V55, V12 == V55, V23 == V55, V46 == V55, V24 == V55, V50 == V55, V37 == V55, V32 == V55, V54 == V55, V41 == V55, V45 == V55, V26 == V55, V34 == V55, V49 == V55, V28 == V55, V53 == V55 | P_s-{T}(V55,V35)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1692: 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 == V59, V59 == V62, V60 == V63, V62 == V65, V63 == V66, V65 == V68, V66 == V69; #1649 ), references = 3, size of lhs = 106:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), b-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V0,V8), b-{F}(V8,V9), b-{F}(V0,V10), b-{F}(V10,V0), P_s-{F}(V11,V7), b-{F}(V0,V12), b-{F}(V12,V13), b-{F}(V0,V14), b-{F}(V14,V15), P_s-{F}(V0,V16), V16 == V0, P_s-{F}(V17,V16), P_s-{F}(V18,V16), P_s-{F}(V19,V16), P_s-{F}(V20,V16), P_s-{F}(V21,V10), P_s-{F}(V22,V10), P_s-{F}(V23,V24), V0 == V24, V24 == V7, V16 == V24, V10 == V24, P_s-{F}(V25,V24), P_s-{F}(V26,V24), P_s-{F}(V27,V24), P_s-{F}(V28,V24), P_s-{F}(V29,V24), P_s-{F}(V30,V24), P_s-{F}(V31,V24), P_s-{F}(V32,V31), P_s-{F}(V33,V24), P_s-{F}(V34,V33), P_s-{F}(V35,V24), P_s-{F}(V36,V35), P_s-{F}(V37,V24), P_s-{F}(V38,V37), P_s-{F}(V39,V40), V7 == V40, V10 == V40, V40 == V0, V40 == V24, P_s-{F}(V41,V42), V42 == V0, V42 == V24, V42 == V16, P_s-{F}(V43,V42), P_s-{F}(V44,V43), P_s-{F}(V45,V46), V10 == V46, V46 == V0, V46 == V24, V16 == V46, P_s-{F}(V47,V46), P_s-{F}(V48,V47), P_s-{F}(V49,V50), V10 == V50, V50 == V0, V50 == V24, V16 == V50, P_s-{F}(V51,V50), P_s-{F}(V52,V51), P_s-{F}(V53,V54), V54 == V24, V54 == V0, V54 == V16, P_s-{F}(V55,V54), P_s-{F}(V56,V55), P_s-{F}(V57,V58), V26 == V58, V27 == V58, V22 == V58, V30 == V58, V41 == V58, V17 == V58, V45 == V58, V28 == V58, V29 == V58, V18 == V58, V49 == V58, V19 == V58, V53 == V58, V20 == V58, V36 == V58, V57 == V58, V44 == V58, V48 == V58, V32 == V58, V38 == V58, V52 == V58, V34 == V58, V56 == V58, #-{F} V59, V25 == V59, V11 == V59, V21 == V59, V23 == V59, V39 == V59 | r-{T}(V10,V24)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1698: mergings( V2 == V25, V25 == V26; #1695 ), references = 1, size of lhs = 61:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), b-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V0,V8), b-{F}(V8,V9), b-{F}(V0,V10), b-{F}(V10,V0), P_s-{F}(V11,V7), b-{F}(V0,V12), b-{F}(V12,V13), b-{F}(V0,V14), b-{F}(V14,V15), P_s-{F}(V0,V16), V16 == V0, P_s-{F}(V17,V16), P_s-{F}(V18,V16), P_s-{F}(V19,V16), P_s-{F}(V20,V16), P_s-{F}(V21,V10), P_s-{F}(V22,V10), r-{F}(V10,V23), b-{F}(V23,V24), b-{F}(V24,V25), r-{F}(V10,V26), b-{F}(V26,V23), P_s-{F}(V27,V28), P_s-{F}(V29,V28), P_s-{F}(V30,V28), P_s-{F}(V31,V28), P_s-{F}(V32,V33), V7 == V33, V10 == V33, V33 == V0, P_s-{F}(V34,V35), V35 == V0, V35 == V16, P_s-{F}(V36,V35), P_s-{F}(V37,V36), P_s-{F}(V38,V39), V10 == V39, V39 == V0, V16 == V39, P_s-{F}(V40,V39), P_s-{F}(V41,V40), P_s-{F}(V42,V43), V10 == V43, V43 == V0, V16 == V43, P_s-{F}(V44,V43), P_s-{F}(V45,V44), P_s-{F}(V46,V47), V47 == V0, V47 == V16, P_s-{F}(V48,V47), P_s-{F}(V49,V48) | P_s-{T}(V28,V0), P_s-{T}(V28,V7), P_s-{T}(V28,V16), P_s-{T}(V28,V10), P_s-{T}(V28,V23), P_s-{T}(V28,V26), P_s-{T}(V28,V33), P_s-{T}(V28,V35), P_s-{T}(V28,V39), P_s-{T}(V28,V43), P_s-{T}(V28,V47), P_s-{T}(V28,V28), P_s-{T}(V28,V22), P_s-{T}(V28,V34), P_s-{T}(V28,V17), P_s-{T}(V28,V38), P_s-{T}(V28,V18), P_s-{T}(V28,V42), P_s-{T}(V28,V19), P_s-{T}(V28,V46), P_s-{T}(V28,V20), P_s-{T}(V28,V30), P_s-{T}(V28,V37), P_s-{T}(V28,V41), P_s-{T}(V28,V27), P_s-{T}(V28,V31), P_s-{T}(V28,V45), P_s-{T}(V28,V29), P_s-{T}(V28,V49), P_s-{T}(V28,V11), P_s-{T}(V28,V21), P_s-{T}(V28,V32)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1722: mergings( V0 == V23, V23 == V24, V24 == V52, V52 == V54, V54 == V56, V56 == V58, V58 == V60, V60 == V62, V62 == V64, V64 == V66, V66 == V68, V68 == V70, V70 == V72, V72 == V74, V74 == V76, V76 == V78, V78 == V80, V80 == V82, V82 == V84, V84 == V86, V86 == V88, V88 == V90; #1699 ), references = 1, size of lhs = 101:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), b-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V0,V8), b-{F}(V8,V9), b-{F}(V0,V10), b-{F}(V10,V0), P_s-{F}(V11,V7), b-{F}(V0,V12), b-{F}(V12,V13), b-{F}(V0,V14), b-{F}(V14,V15), P_s-{F}(V0,V16), V16 == V0, P_s-{F}(V17,V16), P_s-{F}(V18,V16), P_s-{F}(V19,V16), P_s-{F}(V20,V16), P_s-{F}(V21,V10), P_s-{F}(V22,V10), r-{F}(V10,V23), b-{F}(V23,V24), b-{F}(V24,V25), r-{F}(V10,V26), b-{F}(V26,V23), P_s-{F}(V27,V7), P_s-{F}(V28,V16), P_s-{F}(V29,V10), P_s-{F}(V30,V23), P_s-{F}(V31,V26), P_s-{F}(V32,V33), P_s-{F}(V33,V34), V34 == V0, V34 == V16, P_s-{F}(V35,V34), P_s-{F}(V36,V34), P_s-{F}(V37,V36), P_s-{F}(V38,V39), P_s-{F}(V39,V40), V10 == V40, V40 == V0, V16 == V40, P_s-{F}(V41,V40), P_s-{F}(V42,V40), P_s-{F}(V43,V42), P_s-{F}(V44,V45), P_s-{F}(V45,V46), V10 == V46, V46 == V0, V16 == V46, P_s-{F}(V47,V46), P_s-{F}(V48,V46), P_s-{F}(V49,V48), P_s-{F}(V50,V51), P_s-{F}(V51,V52), V52 == V0, V52 == V16, P_s-{F}(V53,V52), P_s-{F}(V54,V52), P_s-{F}(V55,V54), P_s-{F}(V56,V57), V7 == V57, V10 == V57, V57 == V0, P_s-{F}(V58,V57), P_s-{F}(V59,V58), P_s-{F}(V60,V61), V27 == V61, V28 == V61, V29 == V61, V30 == V61, V31 == V61, V56 == V61, V35 == V61, V41 == V61, V47 == V61, V53 == V61, V60 == V61, V37 == V61, V43 == V61, V49 == V61, V55 == V61, V59 == V61, P_s-{F}(V62,V61), P_s-{F}(V63,V62), V63 == V61, P_s-{F}(V64,V61), P_s-{F}(V65,V64), V65 == V61, P_s-{F}(V66,V61), P_s-{F}(V67,V66), V67 == V61, P_s-{F}(V68,V61), P_s-{F}(V69,V68), V69 == V61 | P_s-{T}(V61,V0), P_s-{T}(V61,V22), P_s-{T}(V61,V17), P_s-{T}(V61,V18), P_s-{T}(V61,V19), P_s-{T}(V61,V20), P_s-{T}(V61,V32), P_s-{T}(V61,V38), P_s-{T}(V61,V44), P_s-{T}(V61,V50), P_s-{T}(V61,V11), P_s-{T}(V61,V21)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1765: mergings( V23 == V24, V24 == V29, V29 == V31, V31 == V33, V33 == V35, V35 == V37, V37 == 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 == V0, V0 == V22, V16 == V10, V22 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V54, V10 == V55, V54 == V60, V55 == V61, V56 == V62, V60 == V66, V61 == V67, V62 == V68, V66 == V72, V67 == V73, V68 == V74, V72 == V11, V73 == V7; #1723 ), references = 1, size of lhs = 77:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), b-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V8), b-{F}(V0,V9), V9 == V0, b-{F}(V9,V0), P_s-{F}(V0,V9), b-{F}(V0,V10), b-{F}(V10,V11), b-{F}(V0,V12), b-{F}(V12,V13), P_s-{F}(V14,V9), r-{F}(V9,V15), b-{F}(V15,V16), b-{F}(V16,V17), r-{F}(V9,V18), b-{F}(V18,V15), P_s-{F}(V19,V9), P_s-{F}(V20,V9), P_s-{F}(V21,V9), P_s-{F}(V22,V15), P_s-{F}(V23,V18), P_s-{F}(V9,V24), V24 == V0, V24 == V9, P_s-{F}(V25,V24), P_s-{F}(V26,V24), P_s-{F}(V27,V24), P_s-{F}(V28,V24), P_s-{F}(V29,V24), P_s-{F}(V30,V29), P_s-{F}(V31,V24), P_s-{F}(V32,V31), P_s-{F}(V33,V24), P_s-{F}(V34,V33), P_s-{F}(V35,V24), P_s-{F}(V36,V35), P_s-{F}(V37,V38), V9 == V38, V38 == V0, P_s-{F}(V39,V38), P_s-{F}(V40,V39), P_s-{F}(V41,V42), V19 == V42, V20 == V42, V21 == V42, V22 == V42, V23 == V42, V37 == V42, V25 == V42, V26 == V42, V27 == V42, V28 == V42, V41 == V42, V30 == V42, V32 == V42, V34 == V42, V36 == 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-{T}(V42,V14)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #1862: 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 == V53, V53 == V56, V54 == V57, V56 == V59, V57 == V60, V59 == V62, V60 == V63, V62 == V67, V63 == V82, V67 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V113, V82 == V127, V113 == V131, V127 == V47, V131 == V132, V132 == V133, V133 == V134, V134 == V135, V135 == V136, V47 == V137, V136 == V140, V137 == V141, V138 == V142, V140 == V144, V141 == V145, V142 == V146, V144 == V148, V145 == V149, V146 == V150, V148 == V152, V149 == V120, V152 == V153; #1771 ), references = 1, size of lhs = 137:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), b-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V0,V8), b-{F}(V8,V9), P_s-{F}(V10,V7), b-{F}(V0,V11), b-{F}(V11,V12), b-{F}(V0,V13), b-{F}(V13,V14), b-{F}(V0,V15), b-{F}(V15,V16), b-{F}(V0,V17), b-{F}(V17,V18), b-{F}(V0,V19), b-{F}(V19,V20), b-{F}(V0,V21), b-{F}(V21,V0), b-{F}(V0,V22), b-{F}(V22,V23), P_s-{F}(V24,V21), b-{F}(V0,V25), b-{F}(V25,V26), b-{F}(V0,V27), b-{F}(V27,V28), b-{F}(V0,V29), b-{F}(V29,V30), b-{F}(V0,V31), b-{F}(V31,V32), b-{F}(V0,V33), b-{F}(V33,V34), b-{F}(V0,V35), V35 == V0, b-{F}(V35,V0), P_s-{F}(V0,V35), P_s-{F}(V36,V35), P_s-{F}(V37,V35), P_s-{F}(V38,V35), P_s-{F}(V39,V35), P_s-{F}(V40,V35), P_s-{F}(V41,V35), P_s-{F}(V42,V35), P_s-{F}(V43,V35), P_s-{F}(V44,V35), P_s-{F}(V45,V35), P_s-{F}(V46,V35), P_s-{F}(V47,V35), b-{F}(V0,V48), b-{F}(V48,V49), b-{F}(V0,V50), b-{F}(V50,V51), b-{F}(V0,V52), b-{F}(V52,V53), P_s-{F}(V54,V35), P_s-{F}(V55,V35), P_s-{F}(V56,V35), P_s-{F}(V35,V57), V57 == V0, V57 == V35, P_s-{F}(V58,V57), P_s-{F}(V59,V57), P_s-{F}(V60,V57), P_s-{F}(V61,V57), P_s-{F}(V62,V57), P_s-{F}(V63,V62), P_s-{F}(V64,V57), P_s-{F}(V65,V64), P_s-{F}(V66,V57), P_s-{F}(V67,V66), P_s-{F}(V68,V57), P_s-{F}(V69,V68), P_s-{F}(V70,V71), V0 == V71, V71 == V7, V35 == V71, P_s-{F}(V72,V71), P_s-{F}(V73,V71), P_s-{F}(V74,V71), P_s-{F}(V75,V71), P_s-{F}(V76,V71), P_s-{F}(V77,V71), P_s-{F}(V78,V71), P_s-{F}(V79,V71), P_s-{F}(V80,V79), P_s-{F}(V81,V71), P_s-{F}(V82,V81), P_s-{F}(V83,V71), P_s-{F}(V84,V83), P_s-{F}(V85,V71), P_s-{F}(V86,V85), P_s-{F}(V87,V88), P_s-{F}(V89,V88), P_s-{F}(V90,V88), P_s-{F}(V91,V88), P_s-{F}(V92,V88), P_s-{F}(V93,V88), P_s-{F}(V94,V88), P_s-{F}(V95,V88), P_s-{F}(V96,V88), P_s-{F}(V97,V88), P_s-{F}(V98,V88), P_s-{F}(V99,V88), P_s-{F}(V100,V101), V21 == V101, V35 == V101, V101 == V0, P_s-{F}(V102,V103), V103 == V0, V103 == V35, P_s-{F}(V104,V103), P_s-{F}(V105,V104), P_s-{F}(V106,V107), V107 == V0, V35 == V107, P_s-{F}(V108,V107), P_s-{F}(V109,V108), P_s-{F}(V110,V111), V111 == V0, V35 == V111, P_s-{F}(V112,V111), P_s-{F}(V113,V112), P_s-{F}(V114,V115), V115 == V0, V115 == V35, P_s-{F}(V116,V115), P_s-{F}(V117,V116), P_s-{F}(V118,V119), V35 == V119, V119 == V0, P_s-{F}(V120,V119), P_s-{F}(V121,V120) | P_s-{T}(V88,V7), P_s-{T}(V88,V35), P_s-{T}(V88,V0), P_s-{T}(V88,V71), P_s-{T}(V88,V73), P_s-{T}(V88,V74), P_s-{T}(V88,V41), P_s-{T}(V88,V77), P_s-{T}(V88,V88), P_s-{T}(V88,V36), P_s-{T}(V88,V75), P_s-{T}(V88,V76), P_s-{T}(V88,V37), P_s-{T}(V88,V38), P_s-{T}(V88,V39), P_s-{T}(V88,V84), P_s-{T}(V88,V87), P_s-{T}(V88,V89), P_s-{T}(V88,V80), P_s-{T}(V88,V86), P_s-{T}(V88,V90), P_s-{T}(V88,V82), P_s-{T}(V88,V91), P_s-{T}(V88,V21), P_s-{T}(V88,V101), P_s-{T}(V88,V103), P_s-{T}(V88,V107), P_s-{T}(V88,V111), P_s-{T}(V88,V115), P_s-{T}(V88,V47), P_s-{T}(V88,V102), P_s-{T}(V88,V42), P_s-{T}(V88,V106), P_s-{T}(V88,V43), P_s-{T}(V88,V110), P_s-{T}(V88,V44), P_s-{T}(V88,V114), P_s-{T}(V88,V45), P_s-{T}(V88,V94), P_s-{T}(V88,V105), P_s-{T}(V88,V109), P_s-{T}(V88,V92), P_s-{T}(V88,V95), P_s-{T}(V88,V113), P_s-{T}(V88,V93), P_s-{T}(V88,V117), P_s-{T}(V88,V54), P_s-{T}(V88,V55), P_s-{T}(V88,V56), P_s-{T}(V88,V78), P_s-{T}(V88,V118), P_s-{T}(V88,V58), P_s-{T}(V88,V59), P_s-{T}(V88,V60), P_s-{T}(V88,V61), P_s-{T}(V88,V63), P_s-{T}(V88,V65), P_s-{T}(V88,V67), P_s-{T}(V88,V69), P_s-{T}(V88,V121), P_s-{T}(V88,V96), P_s-{T}(V88,V97), P_s-{T}(V88,V98), P_s-{T}(V88,V99), P_s-{T}(V88,V72), P_s-{T}(V88,V10), P_s-{T}(V88,V40), P_s-{T}(V88,V70), P_s-{T}(V88,V24), P_s-{T}(V88,V46), P_s-{T}(V88,V100)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2049: 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 == V51, V51 == V54, V52 == V55, V54 == V57, V55 == V58, V57 == V60, V58 == V61, V60 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V61 == V125, V111 == V35, V35 == V65, V80 == V125, V65 == V129, V125 == V45, V129 == V130, V130 == V131, V131 == V132, V132 == V133, V133 == V134, V45 == V135, V134 == V138, V135 == V139, V136 == V140, V138 == V142, V139 == V143, V140 == V144, V142 == V146, V143 == V147, V144 == V148, V146 == V150, V147 == V118, V150 == V151, V151 == V212, V212 == V214, V214 == V216, V216 == V218, V218 == V220, V220 == V222, V222 == V224, V224 == V226, V226 == V228, V228 == V64, V64 == V230, V230 == V232, V232 == V53, V53 == V234, V234 == V236, V236 == V56, V56 == V59, V59 == V62, V62 == V174, V118 == V173, V148 == V161, V174 == V238, V238 == V240, V240 == V170, V173 == V169, V170 == V176, V169 == V175, V176 == V242, V242 == V172, V175 == V171, V172 == V244, V244 == V246, V246 == V248, V248 == V250, V250 == V252, V252 == V254, V254 == V256, V256 == V258, V258 == V86, V86 == V260, V260 == V81, V81 == V262, V262 == V82, V82 == V264, V264 == V83, V83 == V266, V266 == V84, V84 == V268, V268 == V195, V171 == V194, V161 == V193, V195 == V199, V194 == V198, V193 == V197, V199 == V270, V270 == V272, V272 == V203, V198 == V202, V197 == V201, V203 == V274, V274 == V207, V202 == V206, V201 == V205, V207 == V126, V126 == V127, V127 == V128, V128 == V276, V276 == V278, V278 == V280, V280 == V282, V282 == V284, V284 == V286, V286 == V153, V206 == V152, V153 == V155, V152 == V154, V155 == V157, V154 == V156, V157 == V159, V156 == V158, V159 == V211, V158 == V210, V205 == V209, V211 == V288, V288 == V290, V290 == V292, V292 == V294, V294 == V296, V296 == V46, V210 == V42, V46 == V63, V63 == V298, V298 == V75, V42 == V72, V75 == V85; #1863 ), references = 1, size of lhs = 164:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), b-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V8), b-{F}(V0,V9), b-{F}(V9,V10), b-{F}(V0,V11), b-{F}(V11,V12), b-{F}(V0,V13), b-{F}(V13,V14), b-{F}(V0,V15), b-{F}(V15,V16), b-{F}(V0,V17), b-{F}(V17,V18), b-{F}(V0,V19), b-{F}(V19,V20), b-{F}(V0,V21), b-{F}(V21,V22), b-{F}(V0,V23), b-{F}(V23,V24), b-{F}(V0,V25), b-{F}(V25,V26), b-{F}(V0,V27), b-{F}(V27,V28), b-{F}(V0,V29), b-{F}(V29,V30), b-{F}(V0,V31), V31 == V0, b-{F}(V31,V0), P_s-{F}(V0,V31), b-{F}(V0,V32), b-{F}(V32,V33), b-{F}(V0,V34), b-{F}(V34,V35), b-{F}(V0,V36), b-{F}(V36,V37), P_s-{F}(V38,V31), P_s-{F}(V39,V31), P_s-{F}(V40,V31), P_s-{F}(V41,V31), P_s-{F}(V42,V31), P_s-{F}(V43,V31), P_s-{F}(V44,V31), P_s-{F}(V45,V31), P_s-{F}(V31,V46), V31 == V46, V46 == V0, P_s-{F}(V47,V46), P_s-{F}(V48,V46), P_s-{F}(V49,V46), P_s-{F}(V50,V46), P_s-{F}(V51,V46), P_s-{F}(V52,V46), P_s-{F}(V53,V52), P_s-{F}(V54,V46), P_s-{F}(V55,V54), P_s-{F}(V56,V46), P_s-{F}(V57,V56), P_s-{F}(V58,V46), P_s-{F}(V59,V58), P_s-{F}(V60,V46), P_s-{F}(V61,V60), P_s-{F}(V62,V46), P_s-{F}(V63,V62), P_s-{F}(V64,V46), P_s-{F}(V65,V64), P_s-{F}(V66,V46), P_s-{F}(V67,V66), P_s-{F}(V68,V46), P_s-{F}(V69,V68), P_s-{F}(V70,V46), P_s-{F}(V71,V70), P_s-{F}(V72,V46), P_s-{F}(V73,V72), P_s-{F}(V74,V46), P_s-{F}(V75,V74), P_s-{F}(V76,V46), P_s-{F}(V77,V76), P_s-{F}(V78,V46), P_s-{F}(V79,V78), P_s-{F}(V80,V46), P_s-{F}(V81,V80), P_s-{F}(V82,V46), P_s-{F}(V83,V82), P_s-{F}(V84,V46), P_s-{F}(V85,V84), P_s-{F}(V86,V87), V31 == V87, V87 == V0, P_s-{F}(V88,V87), P_s-{F}(V89,V90), V38 == V90, V39 == V90, V47 == V90, V40 == V90, V41 == V90, V42 == V90, V43 == V90, V65 == V90, V67 == V90, V73 == V90, V89 == V90, V69 == V90, V71 == V90, V44 == V90, V45 == V90, V88 == V90, V48 == V90, V49 == V90, V50 == V90, V51 == V90, V77 == V90, V79 == V90, V81 == V90, V83 == V90, V75 == V90, V85 == V90, V53 == V90, V55 == V90, V57 == V90, V59 == V90, V63 == V90, V61 == V90, P_s-{F}(V91,V90), P_s-{F}(V92,V91), V92 == V90, P_s-{F}(V93,V90), P_s-{F}(V94,V93), V94 == V90, P_s-{F}(V95,V90), P_s-{F}(V96,V95), V96 == V90, P_s-{F}(V97,V90), P_s-{F}(V98,V97), V98 == V90, P_s-{F}(V99,V90), P_s-{F}(V100,V99), V100 == V90, P_s-{F}(V101,V90), P_s-{F}(V102,V101), V102 == V90, P_s-{F}(V103,V90), P_s-{F}(V104,V103), V104 == V90, P_s-{F}(V105,V90), P_s-{F}(V106,V105), V106 == V90, P_s-{F}(V107,V90), P_s-{F}(V108,V107), V108 == V90, P_s-{F}(V109,V90), P_s-{F}(V110,V109), V110 == V90, P_s-{F}(V111,V90), P_s-{F}(V112,V111), V112 == V90, P_s-{F}(V113,V90), P_s-{F}(V114,V113), V114 == V90 | P_s-{T}(V90,V86)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2234: mergings( V82 == V89, 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 == V40, V39 == V41, V40 == V42, V41 == V43, V42 == V44, V43 == V45, V44 == 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, V45 == V89, V1 == V90, V89 == V2, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V2 == V96, V95 == V98, V96 == V99, V97 == V100, V98 == V101, V99 == V102, V100 == V103, V101 == V104, V102 == V105, V103 == V106, V104 == V107, V107 == V108, V108 == V109, V109 == V111, V111 == V113, V113 == V114, V114 == V116, V116 == V118, V118 == V120, V120 == V122, V122 == V123, V123 == V124, V124 == V125, V125 == V126, V126 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V133, V105 == V134, V106 == V135, V133 == V137, V137 == V138, V138 == V139, V134 == V140, V139 == V141, V140 == V142, V141 == V143, V143 == V144, V142 == V145, V144 == V146, V146 == V147, V147 == V149, V149 == V151, V151 == V152, V152 == V153, V153 == V154, V154 == V155, V155 == V156, V156 == V157, V157 == V158, V158 == V159, V159 == V160, V160 == V161, V161 == V162, V162 == V163, V163 == V164, V164 == V165, V165 == V166, V145 == V167, V135 == V168, V166 == V170, V167 == V171, V168 == V172, V170 == V174, V174 == V175, V175 == V176, V171 == V177, V172 == V178, V176 == V180, V180 == V181, V177 == V182, V178 == V183, V181 == V185, V185 == V186, V186 == V187, V187 == V188, V188 == V189, V189 == V190, V190 == V191, V191 == V192, V192 == V193, V193 == V194, V182 == V195, V194 == V196, V195 == V197, V196 == V198, V197 == V199, V198 == V200, V199 == V201, V200 == V202, V201 == V203, V183 == V204, V202 == V205, V205 == V206, V206 == V207, V207 == V208, V208 == V209, V209 == V210, V210 == V211, V211 == V212, V212 == V213, V213 == V214, V214 == V215; #2051 ), references = 2, size of lhs = 147:
% 65.34/65.57 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, b-{F}(V1,V0), b-{F}(V1,V2), b-{F}(V1,V3), b-{F}(V1,V4), b-{F}(V1,V5), b-{F}(V1,V6), b-{F}(V1,V7), b-{F}(V1,V8), b-{F}(V1,V9), b-{F}(V1,V10), b-{F}(V1,V11), b-{F}(V1,V12), b-{F}(V1,V13), b-{F}(V1,V14), b-{F}(V1,V15), b-{F}(V1,V16), b-{F}(V1,V17), b-{F}(V1,V18), b-{F}(V1,V19), 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}(V1,V28), V1 == V28, V28 == V0, P_s-{F}(V29,V28), P_s-{F}(V30,V28), P_s-{F}(V31,V28), P_s-{F}(V32,V28), P_s-{F}(V33,V28), P_s-{F}(V34,V28), P_s-{F}(V35,V34), P_s-{F}(V36,V28), P_s-{F}(V37,V36), P_s-{F}(V38,V28), P_s-{F}(V39,V38), P_s-{F}(V40,V28), P_s-{F}(V41,V40), P_s-{F}(V42,V28), P_s-{F}(V43,V42), P_s-{F}(V44,V28), P_s-{F}(V45,V44), P_s-{F}(V46,V28), P_s-{F}(V47,V46), P_s-{F}(V48,V28), P_s-{F}(V49,V48), P_s-{F}(V50,V28), P_s-{F}(V51,V50), P_s-{F}(V52,V28), P_s-{F}(V53,V52), P_s-{F}(V54,V28), P_s-{F}(V55,V54), P_s-{F}(V56,V28), P_s-{F}(V57,V56), P_s-{F}(V58,V28), P_s-{F}(V59,V58), P_s-{F}(V60,V28), P_s-{F}(V61,V60), P_s-{F}(V62,V28), P_s-{F}(V63,V62), P_s-{F}(V64,V28), P_s-{F}(V65,V64), P_s-{F}(V66,V28), P_s-{F}(V67,V66), P_s-{F}(V68,V69), V1 == V69, V69 == V0, P_s-{F}(V70,V69), P_s-{F}(V71,V70), P_s-{F}(V72,V73), V20 == V73, V21 == V73, V29 == V73, V22 == V73, V23 == V73, V24 == V73, V25 == V73, V47 == V73, V49 == V73, V55 == V73, V72 == V73, V51 == V73, V53 == V73, V26 == V73, V27 == V73, V68 == V73, V30 == V73, V31 == V73, V32 == V73, V33 == V73, V59 == V73, V61 == V73, V63 == V73, V65 == V73, V57 == V73, V67 == V73, V35 == V73, V37 == V73, V39 == V73, V41 == V73, V45 == V73, V43 == V73, V71 == V73, P_s-{F}(V74,V73), P_s-{F}(V75,V74), V75 == V73, P_s-{F}(V76,V73), P_s-{F}(V77,V76), V77 == V73, P_s-{F}(V78,V73), P_s-{F}(V79,V78), V79 == V73, P_s-{F}(V80,V73), P_s-{F}(V81,V80), V81 == V73, P_s-{F}(V82,V73), P_s-{F}(V83,V82), V83 == V73, P_s-{F}(V84,V73), P_s-{F}(V85,V84), V85 == V73, P_s-{F}(V86,V73), P_s-{F}(V87,V86), V87 == V73, P_s-{F}(V88,V73), P_s-{F}(V89,V88), V89 == V73, P_s-{F}(V90,V73), P_s-{F}(V91,V90), V91 == V73, P_s-{F}(V92,V73), P_s-{F}(V93,V92), V93 == V73, P_s-{F}(V94,V73), P_s-{F}(V95,V94), V95 == V73, P_s-{F}(V96,V73), P_s-{F}(V97,V96), V97 == V73 | r-{T}(V0,V1)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2251: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10; #2242 ), references = 1, size of lhs = 21:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V3 == V2, r-{F}(V3,V4), V2 == V4, b-{F}(V4,V2), b-{F}(V4,V3), b-{F}(V4,V5), b-{F}(V4,V6), #-{F} V7, V7 == V4, V1 == V7, V7 == V2, V7 == V3, #-{F} V8, V8 == V4, V1 == V8, V8 == V2, V8 == V3, V8 == V7 | b-{T}(V3,V2)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2271: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13; #2258 ), references = 1, size of lhs = 23:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, r-{F}(V3,V4), V2 == V4, b-{F}(V4,V2), b-{F}(V4,V3), b-{F}(V4,V5), b-{F}(V4,V6), b-{F}(V7,V3), b-{F}(V7,V2), b-{F}(V8,V2), b-{F}(V8,V3), r-{F}(V3,V9), V2 == V9, b-{F}(V9,V10), #-{F} V11, #-{F} V12, V12 == V4, V1 == V12, V12 == V2, V12 == V3 | P_s-{T}(V11,V4), P_s-{T}(V11,V1), P_s-{T}(V11,V2), P_s-{T}(V11,V3), P_s-{T}(V11,V12)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2288: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V24, V24 == V26, V26 == V28, V28 == V30; #2272 ), references = 1, size of lhs = 30:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V2,V3), b-{F}(V3,V2), b-{F}(V3,V4), V4 == V2, V4 == V3, b-{F}(V1,V4), b-{F}(V3,V5), b-{F}(V3,V6), b-{F}(V7,V4), b-{F}(V7,V2), r-{F}(V2,V8), V4 == V8, b-{F}(V8,V9), P_s-{F}(V10,V3), P_s-{F}(V11,V4), b-{F}(V12,V4), b-{F}(V12,V2), P_s-{F}(V13,V12), P_s-{F}(V14,V15), V15 == V3, V12 == V15, V15 == V4, V15 == V2, #-{F} V16, V10 == V16, V13 == V16, V11 == V16, V14 == V16 | P_s-{T}(V16,V2)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2308: 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; #2290 ), references = 4, size of lhs = 22:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V1,V2), b-{F}(V1,V3), r-{F}(V0,V4), b-{F}(V4,V5), P_s-{F}(V6,V1), P_s-{F}(V7,V1), P_s-{F}(V8,V9), V9 == V0, V9 == V1, V9 == V4, P_s-{F}(V10,V11), V1 == V11, V11 == V9, V11 == V0, #-{F} V12, V6 == V12, V7 == V12, V8 == V12, V10 == V12 | r-{T}(V1,V9)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2313: mergings( V0 == V3, V3 == V4; #2310 ), references = 2, size of lhs = 10:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), r-{F}(V1,V5), V5 == V2, r-{F}(V6,V5), r-{F}(V7,V6), V7 == V2, V7 == V5 | r-{T}(V7,V2)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2344: 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 == V27, V27 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39; #2319 ), references = 1, size of lhs = 25:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V2), r-{F}(V0,V3), b-{F}(V3,V0), b-{F}(V3,V4), b-{F}(V3,V5), P_s-{F}(V6,V3), P_s-{F}(V7,V3), b-{F}(V3,V8), b-{F}(V3,V9), r-{F}(V0,V10), b-{F}(V10,V11), P_s-{F}(V12,V3), P_s-{F}(V13,V3), r-{F}(V14,V3), P_s-{F}(V15,V16), V16 == V0, V16 == V3, V16 == V1, V14 == V16, P_s-{F}(V17,V18), V3 == V18, V18 == V0, #-{F} V19 | P_s-{T}(V19,V3), P_s-{T}(V19,V16), P_s-{T}(V19,V0), P_s-{T}(V19,V10), P_s-{T}(V19,V14), P_s-{T}(V19,V18), P_s-{T}(V19,V6), P_s-{T}(V19,V7), P_s-{T}(V19,V15), P_s-{T}(V19,V19), P_s-{T}(V19,V12), P_s-{T}(V19,V13), P_s-{T}(V19,V17)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2377: 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 == V25, V25 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V44, V44 == V46, V46 == V48, V48 == V50, V50 == V52, V52 == V54, V54 == V56; #2345 ), references = 1, size of lhs = 38:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V2), r-{F}(V0,V3), b-{F}(V3,V0), b-{F}(V3,V4), b-{F}(V3,V5), P_s-{F}(V6,V3), P_s-{F}(V7,V3), b-{F}(V3,V8), b-{F}(V3,V9), r-{F}(V0,V10), b-{F}(V10,V11), P_s-{F}(V12,V3), P_s-{F}(V13,V3), r-{F}(V14,V3), P_s-{F}(V15,V3), P_s-{F}(V16,V10), P_s-{F}(V17,V18), V18 == V0, V18 == V3, V18 == V1, V14 == V18, P_s-{F}(V19,V18), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V3 == V22, V22 == V0, P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V15 == V26, V17 == V26, V16 == V26, V21 == V26, V20 == V26, V25 == V26, V24 == V26 | P_s-{T}(V26,V0), P_s-{T}(V26,V14), P_s-{T}(V26,V6), P_s-{T}(V26,V7), P_s-{T}(V26,V12), P_s-{T}(V26,V13)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2414: 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 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V39, V39 == V41, V41 == V42, V42 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V17, V17 == V25, V25 == V38, V38 == V23, V23 == V24, V24 == V30; #2378 ), references = 2, size of lhs = 34:
% 65.34/65.57 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V2), r-{F}(V0,V3), b-{F}(V3,V4), P_s-{F}(V5,V3), r-{F}(V0,V6), b-{F}(V6,V0), P_s-{F}(V0,V6), b-{F}(V6,V7), b-{F}(V6,V8), b-{F}(V6,V9), b-{F}(V6,V10), P_s-{F}(V11,V6), P_s-{F}(V12,V6), P_s-{F}(V13,V14), V14 == V6, V14 == V1, V0 == V14, P_s-{F}(V15,V14), P_s-{F}(V16,V15), P_s-{F}(V17,V18), V6 == V18, V18 == V0, P_s-{F}(V19,V18), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V12 == V22, V13 == V22, V5 == V22, V17 == V22, V16 == V22, V21 == V22, V20 == V22 | P_s-{T}(V22,V11)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2429: mergings( V0 == V1, V1 == V13, V13 == V14, V14 == V15, V15 == V16; #2423 ), references = 1, size of lhs = 38:
% 65.34/65.57 P_z-{F}(V0), b-{F}(V1,V0), V0 == V1, b-{F}(V1,V2), b-{F}(V1,V3), b-{F}(V1,V4), P_s-{F}(V5,V1), P_s-{F}(V6,V1), b-{F}(V1,V7), b-{F}(V1,V8), b-{F}(V1,V9), P_s-{F}(V10,V1), P_s-{F}(V11,V1), P_s-{F}(V12,V13), V13 == V1, V0 == V13, P_s-{F}(V14,V15), V1 == V15, V15 == V13, V15 == V0, P_s-{F}(V16,V17), V17 == V1, V13 == V17, V0 == V17, P_s-{F}(V18,V19), V1 == V19, V19 == V17, V19 == V0, #-{F} V20, V5 == V20, V6 == V20, V12 == V20, V14 == V20, #-{F} V21, V10 == V21, V11 == V21, V16 == V21, V18 == V21 | b-{T}(V0,V1)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2443: mergings( V2 == V16; #2439 ), references = 1, size of lhs = 79:
% 65.34/65.57 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), P_s-{F}(V8,V1), P_s-{F}(V9,V1), P_s-{F}(V10,V1), P_s-{F}(V11,V1), P_s-{F}(V12,V1), P_s-{F}(V13,V1), P_s-{F}(V14,V1), P_s-{F}(V15,V1), P_s-{F}(V16,V1), P_s-{F}(V17,V1), P_s-{F}(V18,V1), P_s-{F}(V19,V1), P_s-{F}(V20,V1), P_s-{F}(V21,V1), P_s-{F}(V22,V1), P_s-{F}(V23,V1), P_s-{F}(V24,V1), P_s-{F}(V25,V1), P_s-{F}(V26,V1), P_s-{F}(V27,V1), P_s-{F}(V28,V1), P_s-{F}(V29,V1), P_s-{F}(V30,V1), P_s-{F}(V31,V1), P_s-{F}(V32,V1), P_s-{F}(V33,V1), P_s-{F}(V34,V1), P_s-{F}(V35,V1), P_s-{F}(V36,V1), P_s-{F}(V37,V1), P_s-{F}(V38,V1), P_s-{F}(V39,V1), P_s-{F}(V40,V1), P_s-{F}(V41,V1), P_s-{F}(V42,V1), P_s-{F}(V43,V1), P_s-{F}(V44,V1), P_s-{F}(V45,V1), P_s-{F}(V46,V1), P_s-{F}(V47,V1), P_s-{F}(V48,V1), P_s-{F}(V49,V1), P_s-{F}(V50,V1), P_s-{F}(V51,V1), P_s-{F}(V52,V1), P_s-{F}(V53,V1), P_s-{F}(V54,V1), P_s-{F}(V55,V1), P_s-{F}(V56,V1), P_s-{F}(V57,V1), P_s-{F}(V58,V1), P_s-{F}(V59,V1), P_s-{F}(V60,V1), P_s-{F}(V61,V1), P_s-{F}(V62,V1), P_s-{F}(V63,V1), P_s-{F}(V64,V1), P_s-{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-{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,V16), P_s-{T}(V1,V17), P_s-{T}(V1,V18), P_s-{T}(V1,V19), P_s-{T}(V1,V20), P_s-{T}(V1,V21), P_s-{T}(V1,V22), P_s-{T}(V1,V24), P_s-{T}(V1,V25), P_s-{T}(V1,V23), P_s-{T}(V1,V28), P_s-{T}(V1,V26), P_s-{T}(V1,V27), P_s-{T}(V1,V29), P_s-{T}(V1,V15), P_s-{T}(V1,V30), P_s-{T}(V1,V31), P_s-{T}(V1,V49), P_s-{T}(V1,V50), P_s-{T}(V1,V51), P_s-{T}(V1,V52), P_s-{T}(V1,V53), P_s-{T}(V1,V54), P_s-{T}(V1,V55), P_s-{T}(V1,V56), P_s-{T}(V1,V57), P_s-{T}(V1,V58), P_s-{T}(V1,V59), P_s-{T}(V1,V60), P_s-{T}(V1,V61), P_s-{T}(V1,V62), P_s-{T}(V1,V5), P_s-{T}(V1,V6), P_s-{T}(V1,V7), P_s-{T}(V1,V8), P_s-{T}(V1,V9), P_s-{T}(V1,V10), P_s-{T}(V1,V38), P_s-{T}(V1,V39), P_s-{T}(V1,V42), P_s-{T}(V1,V40), P_s-{T}(V1,V41), P_s-{T}(V1,V11), P_s-{T}(V1,V12), P_s-{T}(V1,V44), P_s-{T}(V1,V45), P_s-{T}(V1,V46), P_s-{T}(V1,V47), P_s-{T}(V1,V43), P_s-{T}(V1,V48), P_s-{T}(V1,V32), P_s-{T}(V1,V33), P_s-{T}(V1,V34), P_s-{T}(V1,V35), P_s-{T}(V1,V37), P_s-{T}(V1,V36), P_s-{T}(V1,V63), P_s-{T}(V1,V64), P_s-{T}(V1,V65), P_s-{T}(V1,V66), P_s-{T}(V1,V67), P_s-{T}(V1,V68), P_s-{T}(V1,V69), P_s-{T}(V1,V70), P_s-{T}(V1,V71), P_s-{T}(V1,V72), P_s-{T}(V1,V73), P_s-{T}(V1,V74), P_s-{T}(V1,V75), P_s-{T}(V1,V14), P_s-{T}(V1,V13), P_s-{T}(V1,V76), P_s-{T}(V1,V77)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2522: mergings( V15 == V0, V0 == V2, V2 == V3, V3 == V4, V4 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V25, V25 == V26, V26 == V24, V24 == V29, V29 == V27, V27 == V28, V28 == V30, V30 == V16, V16 == V31, V31 == V32, V32 == 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 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V39, V39 == V40, V40 == V43, V43 == V41, V41 == V42, V42 == V11, V11 == V12, V12 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V44, V44 == V49, V49 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V38, V38 == V37, V37 == 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 == V14, V14 == V13, V13 == V77, V77 == V78; #2444 ), references = 1, size of lhs = 3:
% 65.34/65.57 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1 | P_s-{T}(V1,V1)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2526: mergings( V0 == V2; #2524 ), references = 1, size of lhs = 1:
% 65.34/65.57 P_z-{F}(V0) | P_s-{T}(V0,V0)
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 #2529: exists( #8, #2527 ), references = 1, size of lhs = 0:
% 65.34/65.57 FALSE | FALSE
% 65.34/65.57 (used 0 times, uses = {})
% 65.34/65.57
% 65.34/65.57 number of learnt formulas = 64
% 65.34/65.57
% 65.34/65.57
% 65.34/65.57 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 65.34/65.57
% 65.34/65.57 randbase = 1
%------------------------------------------------------------------------------